Mardi 30 mai

Méthodes formelles en sécurité

14:15 - 15:00 - Binary-level Security: Formal Methods to the Rescue

Sébastien Bardin, CEA, Paris-Saclay

Several major classes of security analysis have to be performed on raw executable files, such as vulnerability analysis of mobile code or commercial off-the-shelf, deobfuscation or malware inspection. These analysis are highly challenging, due to the very low-level and intricate nature of binary code, and there is a clear need for more sophisticated and automated tools than currently available syntactic and dynamic approaches. On the other hand, source-level program analysis and formal methods have made tremendous progress in the past decade, and they are now an industrial reality for safety-critical applications.

Our long term goal is precisely to fulfill part of this gap, by developing state-of-the-art binary-level semantic analyses. In this talk, we first present the benefits of binary-level security analysis and the new challenges brought to formal methods, then we describe our early results and achievements, including the open-source BINSEC platform and its underlying key technologies as well as case-studies on deobfuscation and vulnerability analysis.

The BINSEC project is a joint effort involving CEA, INRIA, LORIA, Université de Grenoble-Alpes and Airbus.

15:00 - 15:45 - Language-Based Information Flow Security Enforcements

Tamara Rezk, Inria, Sophia Antipolis

This talk is about the language-based specification and enforcement of strong confidentiality policies based on information flow. Whenever computation using confidential information is possible, a sound information flow enforcement mechanism should prevent the results of the computation from leaking even partial information about confidential inputs. Motivated by the dynamic nature and an extensive list of vulnerabilities found in web applications in recent years, several dynamic and hybrid enforcement mechanisms in the form of information flow monitors have been proposed. In this talk, I will present a taxonomy of such information flow mechanisms and discuss how they can be used to prevent web security common vulnerabilities by compilation.


16:15 - 17:00 : Utilisation de la programmation par contraintes pour la recherche d'attaques différentielles à clés liées contre l'AES.

Marine Minier, LORIA, Nancy

Le chiffrement AES (Advanced Encryption Standard) est comme son nom l'indique le standard actuel de chiffrements par blocs. C'est donc tout naturellement un des algorithmes les plus étudiés. Au cours de ces dernières années, plusieurs cryptanalyses ont été découvertes dans différents modèles d'attaques. Dans cet exposé, nous nous intéresserons aux attaques différentielles à clés liées où l'adversaire peut introduire des différences dans les textes clairs mais également dans la clé. Nous montrons alors comment la programmation par contraintes (CP) peut être utilisée pour modéliser ces attaques et permet de trouver efficacement toutes les chemins différentiels à clés liées optimaux sur AES-128, AES-192 et AES-256. En particulier, nous améliorons la meilleure différentielle contre la version complète d'AES-256 et nous donnons la meilleure différentielle contre 10 tours d'AES-192. Ces résultats nous ont permis d'améliorer, sur AES-256, la complexité du meilleur distingueur à clés liées, de la meilleure attaque de base à clés liées et de la meilleure q-multicollision.

17:00 - 17:45 - Security in Convoluted Systems

Simon Foley,  Institut Mines-Télécom/IMT Atlantique, Rennes

Contemporary systems are convoluted arrangements of frameworks, software stacks, services and third party components. It is in this complexity, that mistakes are often made and that security threats emerge. Despite our best efforts, we continue to have difficulty accurately capturing security objectives, identifying threats and implementing and configuring the security mechanisms that mitigate the threats. The history of the definition of information flow security style properties is a case in point: in the course of 40 years of research, there has been much debate over its meaning and how it might be used in practice. If there can be such variations over what appears to be a conceptually simple security objective---preventing high information from flowing down to low---then what hope have we of defining what is meant by a secure 'convoluted' system?  Security practitioners avoid this by taking a more operational viewpoint. Rather than attempting to provide a declarative meaning for security, security is defined in terms of the security controls that are used to mitigate threats, typically according to some notion of best practice.  However, with large numbers of controls this operational approach in itself becomes convoluted and its not always clear what security objective is achieved.

I consider this question of what is meant by a secure convoluted system and suggest that rather than attempting to explicitly define security declaratively or operationally, one should consider the security of a system by comparing it against others whose security is considered acceptable.


Personnes connectées : 1