Les méthodes de vérification automatique des logiciels connaissent un succès croissant depuis le début des années 2000, suite à plusieurs succès industriels (Microsoft, Airbus, etc.). L'analyse statique vise, à partir d'une description du programme, à inférer automatiquement des propriétés vérifiées par celui-ci. Les techniques standards d'analyse statique travaillent sur le code source du logiciel, écrit par exemple en C ou Java. Cependant, avoir accès au code source n'est pas envisageable pour de nombreuses applications relatives à la sécurité, soit que le code source n'est pas disponible (code mobile, virus informatiques), soit que le développeur ne veut pas le divulguer (composants sur étagère, certification par un tiers).Nous nous intéressons dans cette thèse à la conception et au développement d'une plate-forme d'analyse statique de code binaire à des fins d'analyse de sécurité. Nos principales contributions se font à trois niveaux: sémantique, implémentation et analyse statique.Tout d'abord, la sémantique des programmes binaires analysés est basée sur un formalisme générique appelé DBA qui a été enrichi avec des mécanismes de spécification et d'abstraction. La définition de la sémantique des programmes binaires requiert aussi un modèle mémoire adéquat.Nous proposons un modèle mémoire adapté au binaire, inspiré des travaux récents sur le code C bas-niveau. Ce nouveau modèle permet de profiter de l'abstraction du modèle à régions tout en gardant l'expressivité du modèle plat.Ensuite, notre plate-forme d'analyse de code binaire nommée BinSec offre trois services de base: désassemblage, simulation et analyse statique.Chaque instruction machine est traduite vers un bloc d'instructions DBA avec une sémantique équivalente. Une large partie des instructions x86 est gérée par la plateforme. Une passe de simplification permet d'éliminer les calculs intermédiaires inutiles afin d'optimiser le fonctionnement des analyses ultérieures. Nos simplifications permettent notamment d'éliminer jusqu'à75% des mises à jours de flags.Enfin, nous avons développé un moteur d'analyse statique de programmes binaires basé sur l'interprétation abstraite. Outre des domaines adaptés aux spécificités du code binaire, nous nous sommes concentrés sur le contrôle par l'utilisateur du compromis entre précision/correction et efficacité. De plus, nous proposons une approche originale de reconstruction de conditions dehaut-niveau à partir des conditions bas-niveau afin de gagner plus de précision d'analyse. L'approche est sûre, efficace, indépendante de la plateforme cibleet peut atteindre des taux de reconstruction très élevés. / Automatic software verification methods have seen increasing success since the early 2000s, thanks to several industrial successes (Microsoft, Airbus, etc.).Static program analysis aims to automatically infer verified properties of programs, based on their descriptions. The standard static analysis techniques apply on the software source code, written for instance in C or Java. However, access to source code is not possible for many safety-related applications, whether the source code is not available (mobile code, computer virus), or the developer does not disclose it (shelf components, third party certification).We are interested in this dissertation in design and development of a static binary analysis platform for safety analysis. Our contributions are made at three levels: semantics, implementation and static analysis.First, the semantics of analyzed binary programs is based on a generic, simple and concise formalism called DBA. It is extended with some specification and abstraction mechanisms in this dissertation. A well defined semantics of binary programs requires also an adequate memory model. We propose a new memory model adapted to binary level requirements and inspired from recent work on low-level C. This new model allows to enjoy the abstraction of the region-based memory model while keeping the expressiveness of the flat model.Second, our binary code analysis platform BinSec offers three basic services:disassembly, simulation and static analysis. Each machine instruction is translated into a block of semantically equivalent DBA instructions. The platform handles a large part of x86 instructions. A simplification step eliminates useless intermediate calculations in order to ease further analyses. Our simplifications especially allow to eliminate up to 75% of flag updates.Finally, we developed a static analysis engine for binary programs based on abstract interpretation. Besides abstract domains specifically adapted to binary analysis, we focused on the user control of trade offs between accuracy/correctness and efficiency. In addition, we offer an original approach for high-level conditions recovery from low-level conditions in order to enhance analysis precision. The approach is sound, efficient, platform-independent and it achieves very high ratio of recovery.
| Identifer | oai:union.ndltd.org:theses.fr/2016SACLX093 |
| Date | 02 December 2016 |
| Creators | Djoudi, Adel |
| Contributors | Université Paris-Saclay (ComUE), Goubault, Éric |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.002 seconds