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.

Récemment, la technologie de micro-fabrication par polymérisation à Deux-Photons (TPP), dérivée de l'absorption à deux-photons, a attiré l'attention de chacun en raison de ses possibilités de fabrication de microstructures tridimensionnelles (3D) de formes très diverses et complexes. Selon mon analyse des recherches actuelles, les thématiques ont graduellement évoluées depuis la fabrication de dispositifs aussi petits que possible vers des thèmes relatifs à son opérationnalité tels que la qualité et/ou l'efficacité du procédé de fabrication. Cette thèse propose une démarche d'intégration pour la création et la simulation de fabrication de modèles de micro-produits pour leur micro-fabrication TPP, tant du point de vue de la Conception Assistée par Ordinateur que de la Fabrication Assistée par Ordinateur (CAO/FAO).<br /> Une analyse des caractéristiques principales de la TPP est proposée pour mettre en évidence ses capacités de fabrication. Selon les résultats de cette analyse et l'incorporation des contraintes de forme des microstructures et de leurs contraintes fonctionnelles, on montre que le modèle numérique de tels objets doit pouvoir décrire des objets de type « non-variété ». Par la prise en considération de cette contrainte et en comblant les manques des approches en vigueur, on propose une démarche intégrée de préparation de modèles « non-variétés » pour un produit créé par un bureau d'études. Le modèle CAO importé à partir d'un fichier STEP est facettisé selon les variétés des sous-domaines polyédriques formant le polyèdre de type « non-variété ». De manière similaire, pour un produit existant, son modèle numérique peut être obtenu par une approche de type ingénierie inverse. Cependant, la plupart des approches existantes reconstruisent seulement les formes des objets sans tenir compte de leurs couleurs intrinsèques. Pour cette raison, un processus intégré de numérisation est développé dans cette thèse afin de produire des modèles 3D colorés.<br /> Afin d'éviter la destruction de la microstructure causée par une « sur-polymérisation » et des tailles de voxels incohérentes provoqués par des différences de réflexion de la lumière, un processus de découpage en tranches bidimensionnelles et une planification adaptée des trajectoires sont développés en utilisant les possibilités 3D de l'équipement de fabrication. Ainsi, l'efficacité du procédé de fabrication peut être augmentée par la mise en œuvre des deux processus ci-dessus. De plus, pour améliorer la rigidité de la microstructure, deux méthodes ont été développées à partir des concepts de soudure et de double épaisseur pour renforcer les raccordements entre les domaines élémentaires de la microstructure et augmenter son épaisseur de paroi, respectivement.<br /> En conclusion, pour démontrer l'efficacité de l'approche proposée, plusieurs modèles numériques de microstructures incluant des modèles « non-variétés » ont été fabriqués selon la démarche de préparation de modèles et le schéma d'intégration proposés.