Il devient important d'assurer que tout système critique est fiable. Pour cela différentes techniques existent, telles que le test ou l'utilisation de méthodes formelles. S'assurer que le comportement d'un vérifieur de byte code Java Card n'entraînera pas de faille de sécurité est une tâche complexe. L'automatisation totale de cette vérification n'à popr le moment pas été realisee. Des jeux de tests coûteux ont été produits manuellement, mais ils doivent être refaits à chaque nouvelle spécification. Les travaux présentés dans ce mémoire proposent une nouvelle méthode pour la génération automatique de tests de vulnérabilité. Ceux-ci reposent sur l'utilisation et la transformation automatique de modèles formels. Pour valider cette méthode, un outil à été développé puis utilisé sur différentes implémentations du vérifieur de byte code Java Card. Le langage de modelisation que nous avons utilisé est Event-B. Nos modèles représentent le comportement normal du système que l'on souhaite tester. Chaque instruction est modélisée comme un événement. Leur garde représente l'ensemble des conditions que doit satisfaire une instruction pour être acceptable. À partir de ce modèle initial, une succession de dérivations automatiques génère un ensemble de modèles dérivés. Chacun de ces modèles dérivés représente une faute particulière. On extrait de ces nouveaux modèles les tests de vulnérabilité abstraits. Ceux-ci sont ensuite concrétisés puis envoyés à un système à tester. Ce processus est assuré par notre logiciel qui repose sur les API Rodin, ProB, CapMap et OPAL.

Le contrôle d'accès permet de spécifier une partie de la politique de sécurité d'un SI (système d'informations). Une politique de CA (Contrôle d'accès) permet de définir qui a accès à quoi et sous quelles conditions. Les concepts fondamentaux utilisés en CA sont : les permissions, les interdictions (ou prohibitions), les obligations et la SoD (séparation des devoirs). Les permissions permettent d'autoriser une personne à accéder à des ressources. Au contraire les prohibitions interdisent à une personne d'accéder à certaines ressources. Les obligations lient plusieurs actions. Elles permettent d'exprimer le fait qu'une action doit être réalisée en réponse à une première action. La SoD permet de sécuriser une procédure en confiant la réalisation des actions composant cette procédure à des agents différents. Différentes méthodes de modélisation de politiques de contrôle d'accès existent. L'originalité de la méthode EB3Sec issue de nos travaux repose sur deux points :- permettre d'exprimer tous les types de contraintes utilisées en CA dans un même modèle,- proposer une approche de modélisation basée sur les événements. En effet, aucune des méthodes actuelles ne présente ces deux caractéristiques, au contraire de la méthode EB3Sec. Nous avons défini un ensemble de patrons, chacun des patrons correspond à un type de contraintes de CA. Un modèle réalisé à l'aide de la méthode EB3Sec peut avoir différentes utilisations :- vérification et simulation,- implémentation. La vérification consiste à s'assurer que le modèle satisfait bien certaines propriétés, dont nous avons défini différents types. Principalement, les blocages doivent être détectés. Ils correspondent à des situations où une action n'est plus exécutable ou à des situations où plus aucune action n'est exécutable. Les méthodes actuelles des techniques de preuves par vérification de modèles ne permettent pas de vérifier les règles dynamiques de CA. Elles sont alors combinées à des méthodes de simulation. Une fois qu'un modèle a été vérifié, il peut être utilisé pour implémenter un filtre ou noyau de sécurité. Deux manières différentes ont été proposées pour réaliser cette implémentation : transformer le modèle EB3Sec vers un autre langage, tel XACML, possédant une implémentation ayant déjà atteint la maturité ou réaliser un noyau de sécurité utilisant le langage EB3Sec comme langage d'entrée

La spécification d’un système industriel nécessite la collaboration d’un ingénieur connaissant le système à modéliser et d’un ingénieur connaissant le langage de modélisation. L'utilisation d'un langage de spécification graphique, tel que les ASTD (Algebraic State Transition Diagram), permet de faciliter cette collaboration. Dans cette thèse, nous définissons une méthode de spécification graphique et formelle qui combine les ASTD avec les langages Event-B et B. L’ordonnancement des actions de la spécification est décrit par les ASTD et le modèle de données est décrit dans la spécification Event-B. La spécification B permet de vérifier la cohérence du modèle : les événements Event-B doivent pouvoir être exécutés lorsque les transitions associées doivent l’être. Un raffinement combiné des ASTD et d’Event-B permet la spécification incrémental du système. Afin de valider son apport, la méthode de spécification a été utilisée pour la spécification de cas d’études / Specifying industrial systems requires collaboration between an engineer that knows how the system works and an engineer that know the specification language. Graphical specification languages can help this collaboration. In this PhD Thesis a method is defined that combines ASTD (Algebraic State Transition Diagram), a formal graphical notation, with B and Event-B langagues. The ordering of actions is specified using ASTD and the data model is specified using Event-B. B specification is used to verify the consistency of the model : Event-B events have to be executed when the corresponding transitions have to be executed. A combined refinement allows to incrementaly design the system

Cette thèse propose un nouveau cadre pour la composition de domaines abstraits. L'idée principale en est l'organisation d'une sémantique abstraite suivant la distinction usuelle entre expressions et instructions, en cours dans la plupart des langages impératifs. La définition d'une sémantique abstraite peut alors se diviser entre abstractions de valeurs et abstractions d'états (ou domaine abstrait). Les abstractions de valeurs représentent les valeurs possibles d'une expression en un point donné, et assurent l'interprétation de la sémantique des expressions. Les abstractions d'états représentent les états machines qui peuvent se produire lors de l'exécution d'un programme, et permettent d'interpréter la sémantique des instructions. De ce choix de conception découle naturellement un élégant système de communication entre abstractions. Lors de l'interprétation d'une instruction, les abstractions d'états peuvent échanger des informations au moyen d'abstractions de valeurs, qui expriment des propriétés à propos des expressions. Les valeurs forment donc une interface de communication entre états abstraits, mais sont également des éléments canoniques de l'interprétation abstraite. Ils peuvent donc eux-même être combinés par les moyens existants de composition d'abstractions, permettant encore davantage d'interactions entre les composants des sémantiques abstraites. Cette thèse explore les possibilités offertes par cette nouvelle architecture des sémantiques abstraites. Nous décrivons en particulier des stratégies efficaces pour le calcul d'abstractions de valeurs précises à partir des propriétés inférées par les domaines, et nous illustrons les différentes possibilités d'interactions que ce système offre. L'architecture que nous proposons inclue également une collaboration directe des abstractions pour l'émission des alarmes qui signalent les erreurs possibles du programme analysé. Nous proposons également un mécanisme permettant d'interagir avec les composants d'une combinaison générique de types OCaml. Nous utilisons des GADT pour encoder la structure interne d'une combinaison, et construisons automatiquement les fonctions d'injection et de projection entre le produit et ses composants. Cette fonctionnalité permet d'établir une communication directe entre les différentes abstractions d'un interpréteur abstrait. Enfin, une dernière contribution de cette thèse est l'extension automatique de domaines abstraits à l'aide de prédicats logiques qui évitent les pertes d'information aux points de jonction. De fait, lorsque plusieurs chemins d'exécution se rejoignent, un domaine abstrait doit représenter les comportements possibles de chacun des chemins, ce qui engendre souvent des pertes de précision. Pour remédier à cette limitation, nous proposons de propager un ensemble d'états abstraits, munis chacun d'un prédicat qui indique sous quelle condition l'état est valable. Contrairement à d'autres approches, notre analyse ne maintient pas une stricte partition des états abstraits, car les prédicats utilisés ne sont pas mutuellement exclusifs. Cette particularité rend possible des optimisations cruciales pour le passage à l'échelle de cette technique, confirmée par nos résultats expérimentaux sur un programme industriel généré. L'ensemble du système de composition des abstractions proposé dans cette thèse a été mis en œuvre dans EVA, la nouvelle version de l'interpréteur abstrait de Frama-C. EVA a été spécifiquement conçu pour faciliter l'introduction de nouvelles abstractions et permettre des interactions riches entre ces abstractions. Grâce à son architecture modulaire et extensible, cinq nouveaux domaines abstraits ont pu être introduit dans l'analyseur en moins d'un an, améliorant ainsi tant ses capacités que sa précision. / This thesis proposes a new framework for the combination of multiple domains in the abstract interpretation theory. Its core concept is the structuring of the abstract semantics by following the usual distinction between expressions and statements. This can be achieved by a convenient architecture where abstractions are separated in two layers: value abstractions, in charge of the expression semantics, and state abstractions —or abstract domains—, in charge of the statement semantics. This design leads naturally to an elegant communication system where the abstract domains, when interpreting a statement, interact and exchange information through value abstractions, that express properties about expressions. While the values form the communication interface between domains, they are also standard elements of the abstract interpretation framework. The communication system is thus embedded in the abstract semantics, and the usual tools of abstract interpretation apply naturally to value abstractions. For instance, different kinds of value abstractions can be composed through the existing methods of combination of abstractions, enabling even further interaction between the components of the abstract semantics. This thesis explores the possibilities offered by this framework. We discuss efficient strategies to compute precise value abstractions from the information inferred by abstract domains, and illustrate the means of communication between different state abstractions. Our architecture also features a direct collaboration for the emission of alarms that report the possible errors of a program. We also proposes a mechanism to enable interacting with the components of a modular combination of OCaml types. We use GADT to encode the inner shape of a combination, and automatically build injection and projection functions between a product of datatypes and its components. This allows direct communications between the abstractions of an abstract interpreter. Finally, a last contribution of this thesis is the automatic extension of abstract domains to track sets of disjunctive abstract states, each one being qualified with a predicate for which the state holds. This enhances the precision of an abstract semantics at join points, when several possible paths of a program execution meet. At these points, predicates preserve the information usually lost by the merge of abstract states. Unlike other approaches, the analysis does not maintain a strict partition of the abstract states, as the predicates we use are not mutually exclusive. This design enables some optimizations that are crucial for scalability, as confirmed by our experimental results on an industrial, generated program. The general system of abstractions combination has been implemented within EVA, the new version of the abstract interpreter provided by the Frama-C platform. Thus, Eva enjoys a modular and extensible architecture designed to facilitate the introduction of new abstractions and to enable rich interactions between them. Thanks to this work, five new domains from the literature have been implemented in less than a year, enhancing the scope and the precision of the analyzer.

Dans le domaine médical, la numérisation des documents et l’utilisation des dossiers patient électroniques (DPE, ou en anglais EHR pour Electronic Health Record) offrent de nombreux avantages, tels que la facilité de recherche et de transmission de ces données. Les systèmes informatiques doivent reprendre ainsi progressivement le rôle traditionnellement tenu par les archivistes, rôle qui comprenait notamment la gestion des accès à ces données sensibles. Ces derniers doivent en effet être rigoureusement contrôlés pour tenir compte des souhaits de confidentialité des patients, des règles des établissements et de la législation en vigueur. SGAC, ou Solution de Gestion Automatisée du Consentement, a pour but de fournir une solution dans laquelle l’accès aux données du patient serait non seulement basée sur les règles mises en place par le patient lui-même mais aussi sur le règlement de l’établissement et sur la législation. Cependant, cette liberté octroyée au patient est source de divers problèmes : conflits, masquage des données nécessaires aux soins ou encore tout simplement erreurs de saisie. Pour effectuer ces vérifications, les méthodes formelles fournissent des moyens fiables de vérification de propriétés tels que les preuves ou la vérification de modèles. Cette thèse propose des méthodes de vérification adaptées à SGAC pour le patient : elle introduit le modèle formel de SGAC, des méthodes de vérifications de propriétés. Afin de mener ces vérifications de manière automatisée, SGAC est modélisé en B et Alloy ; ces différentes modélisations donnent accès aux outils Alloy et ProB, et ainsi à la vérification automatisée de propriétés via la vérification de modèles ou model checking. / Abstract : In healthcare, data digitization and the use of the Electronic Health Records (EHR) offer several benefits, such as the reduction of the space occupied by data, or the ease of data search or data exchanges. IT systems must gradually take up the archivist’s role by managing the accesses over sensitive data, which have to be compliant with patient wishes, hospital rules, as well as laws and regulations. SGAC, or Solution de Gestion Automatisée du Consentement (Automated Consent Management Solution), aims to provide a solution in which access to patient data would be based on patient rules, hospital rules and laws. However, the freedom granted to the patient can cause several problems : conflicts, concealment of crucial data needed to treat the patient adequately, and data-capture errors. Therefore, verification and validation of policies are essential : formal methods provide reliable ways, such as proofs or model checking, to conduct verifications of properties. This thesis provides verification methods applied on SGAC for the patient : it introduces the formal model of SGAC, methods to verify properties such as data access resolution, hidden data detection or redundant rule identification. Modeling of SGAC in B and Alloy provides access to the tools Alloy and ProB, and thus, automated property verification through model checking.

Le test à base de modèle, en particulier test basé sur des assistants à la preuve, réduit de façon transparente l'écart entre la théorie, le modèle formel, et l’implémentation d'un système informatique. Actuellement, les techniques de tests offrent une possibilité d'interagir directement avec de "vrais" systèmes : via différentes propriétés formelles, les tests peuvent être dérivés et exécutés sur le système sous test. Convenablement, l'ensemble du processus peut être entièrement automatisé. Le but de cette thèse est de créer un environnement de test de séquence à base de modèle pour les programmes séquentiels et concurrents. Tout d'abord une théorie générique sur les monades est présentée, qui est indépendante de tout programme ou système informatique. Il se trouve que notre théorie basée sur les monades est assez expressive pour couvrir tous les comportements et les concepts de tests. En particulier, nous considérons ici : les exécutions séquentielles, les exécutions concurrentes, les exécutions synchronisées, les exécutions avec interruptions. Sur le plan conceptuel, la théorie apporte des notions comme la notion raffinement de test, les cas de tests abstraits, les cas de test concrets, les oracles de test, les scénarios de test, les données de tests, les pilotes de tests, les relations de conformités et les critères de couverture dans un cadre théorique et pratique. Dans ce cadre, des règles de raffinement de comportements et d'exécution symbolique sont élaborées pour le cas générique, puis affinées et utilisées pour des systèmes complexes spécifique. Comme application pour notre théorie, nous allons instancier notre environnement par un modèle séquentiel d'un microprocesseur appelé VAMP développé au cours du projet Verisoft. Pour le cas d'étude sur la concurrence, nous allons utiliser notre environnement pour modéliser et tester l'API IPC d'un système d'exploitation industriel appelé PikeOS.Notre environnement est implémenté en Isabelle / HOL. Ainsi, notre approche bénéficie directement des modèles, des outils et des preuves formelles de ce système. / Formal methods can be understood as the art of applying mathematical reasoningto the modeling, analysis and verification of computer systems. Three mainverification approaches can be distinguished: verification based on deductive proofs,model checking and model-based testing.Model-based testing, in particular in its radical form of theorem proving-based testingcite{brucker.ea:2012},bridges seamlessly the gap between the theory, the formal model, and the implementationof a system. Actually,theorem proving based testing techniques offer a possibility to directly interactwith "real" systems: via differentformal properties, tests can be derived and executed on the system under test.Suitably supported, the entire process can fully automated.The purpose of this thesis is to create a model-based sequence testing environmentfor both sequential and concurrent programs. First a generic testing theory basedon monads is presented, which is independent of any concrete program or computersystem. It turns out that it is still expressive enough to cover all common systembehaviours and testing concepts. In particular, we consider here: sequential executions,concurrent executions, synchronised executions, executions with abort.On the conceptual side, it brings notions like test refinements,abstract test cases, concrete test cases,test oracles, test scenarios, test data, test drivers, conformance relations andcoverage criteria into one theoretical and practical framework.In this framework, both behavioural refinement rules and symbolic executionrules are developed for the generic case and then refined and used for specificcomplex systems. As an application, we will instantiate our framework by an existingsequential model of a microprocessor called VAMP developed during the Verisoft-Project.For the concurrent case, we will use our framework to model and test the IPC API of areal industrial operating system called PikeOS.Our framework is implemented in Isabelle/HOL. Thus, our approach directly benefitsfrom the existing models, tools, and formal proofs in this system.

L'injection de faute est une méthode bien connue pour évaluer la robustesse et détecter les vulnérabilités des systèmes. La détection des vulnérabilités créées par injection de fautes a été approchée par différentes méthodes. Dans la littérature deux approches existent: les approches logicielles et les approches matérielles. Les approches logicielles peuvent fournir une large et rapide couverture, mais ne garantissent pas la présence de vulnérabilité dans le système. Les approches matérielles sont incontestables dans leurs résultats, mais nécessitent l’utilisation de matériaux assez coûteux et un savoir-faire approfondi, qui ne permet tout de même pas dans la majorité des cas de confirmer le modèle de faute représentant l'effet créé. Dans un premier lieu, cette thèse se concentre sur l'approche logicielle et propose une approche automatisée qui emploie les techniques de la vérification formelle pour détecter des vulnérabilités créées par injection de faute au niveau binaire. L'efficacité de cette approche est montrée en l'appliquant à des algorithmes de cryptographie implémentés dans les systèmes embarqués. Dans un second lieu, cette thèse établit un rapprochement entre les deux approches logicielles et matérielles sur la détection de vulnérabilité d'injection de faute en comparant les résultats des expériences des deux approches. Ce rapprochement des deux approches démontre que: toutes les vulnérabilités détectées par l'approche logicielle ne peuvent pas être reproduites dans le matériel; les conjectures antérieures sur le modèle de faute par des attaques d'impulsion électromagnétique ne sont pas précises ; et qu’il y a un lien entre les résultats de l’approche logicielle et l'approche matérielle. De plus, la combinaison des deux approches peut rapporter une approche plus précise et plus efficace pour détecter les vulnérabilités qui peuvent être créées par injection de faute. / Fault injection is a well known method to test the robustness and security vulnerabilities of systems. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. Software-based and hardware-based approaches have both been used to detect fault injection vulnerabilities. Software-based approaches can provide broad and rapid coverage, but may not correlate with genuine hardware vulnerabilities. Hardware-based approaches are indisputable in their results, but rely upon expensive expert knowledge, manual testing, and can not confirm what fault model represent the created effect. First, this thesis focuses on the software-based approach and proposes a general process that uses model checking to detect fault injection vulnerabilities in binaries. The efficacy and scalability of this process is demonstrated by detecting vulnerabilities in different cryptographic real-world implementations. Then, this thesis bridges software-based and hardware-based fault injection vulnerability detection by contrasting results of the two approaches. This demonstrates that: not all software-based vulnerabilities can be reproduced in hardware; prior conjectures on the fault model for electromagnetic pulse attacks may not be accurate; and that there is a relationship between software-based and hardware-based approaches. Further, combining both software-based and hardware-based approaches can yield a vastly more accurate and efficient approach to detect genuine fault injection vulnerabilities.

L’adaptation et l’application des méthodes formelles de vérification et de développement à des systèmes et algorithmes distribués est un domaine de recherche très actif. Un des défis principaux réside dans la variété des modèles calculatoires qui existent en algorithmique répartie : des encodages naïfs conduisent à des espaces d’états dont la taille dépasse les capacités des outils les plus puissants de vérification. D’autre part, la complexité intrinsèque de ces algorithmes fait que leur correction n’est pas évidente même pour leurs concepteurs. Dans cette thèse on s’intéresse à l’analyse formelle de protocoles de robots mobiles, un modèle de calcul particulièrement original car les agents ne disposent ni de mémoire (locale ou partagée) ni de la capacité de communiquer par échange de messages. Un cadre général permettant d'exprimer les modèles robotiques est présenté dans cette thèse. Ce modèle a permit d'utiliser à la fois la vérification par model checking d’algorithmes proposés dans la littérature et la synthèse formelle d’algorithmes (optimaux) pour un problème donné, quelque soit le niveau d'asynchronisme du modèle robotique étudié. / The topic of autonomous mobile robots continues to generate a lot of interest in the algorithmic community, both from a purely theoretical perspective and from a more applicative one. The model is now well understood, and the problems under investigation are becoming more and more complex. Correctness proofs are usually very intricate and elaborate, often leaving margin of doubts. This thesis focuses on a new approach to formally study correctness in robots systems and to automatically generate algorithmic solutions. In fact, we propose a general framework to express robot models, and where automated technics like model checking and algorithm synthesis can be used, moreover we show their applicability in robots models under all possible synchronicity levels (from fully synchronous to fully asynchronous).

Les implémentations cryptographiques sont vulnérables aux attaques physiques, et ont donc besoin d'en être protégées. Bien sûr, des protections défectueuses sont inutiles. L'utilisation des méthodes formelles permet de développer des systèmes tout en garantissant leur conformité à des spécifications données. Le premier objectif de ma thèse, et son aspect novateur, est de montrer que les méthodes formelles peuvent être utilisées pour prouver non seulement les principes des contre-mesures dans le cadre d'un modèle, mais aussi leurs implémentations, étant donné que c'est là que les vulnérabilités physiques sont exploitées. Mon second objectif est la preuve et l'automatisation des techniques de protection elles-même, car l'écriture manuelle de code est sujette à de nombreuses erreurs, particulièrement lorsqu'il s'agit de code de sécurité. / Implementations of cryptosystems are vulnerable to physical attacks, and thus need to be protected against them. Of course, malfunctioning protections are useless. Formal methods help to develop systems while assessing their conformity to a rigorous specification. The first goal of my thesis, and its innovative aspect, is to show that formal methods can be used to prove not only the principle of the countermeasures according to a model, but also their implementations, as it is where the physical vulnerabilities are exploited. My second goal is the proof and the automation of the protection techniques themselves, because handwritten security code is error-prone.

Cette thèse s'inscrit dans le domaine de la vérification de protocoles cryptographiques dans le modèle symbolique. Plus précisément, il s'agit de s'assurer à l'aide de méthodes formelles que de petits programmes distribués satisfont à des propriétés d'indistinguabilité, c'est-à-dire qu'un attaquant n'est pas capable de deviner quelle situation (parmi deux)il observe. Ce formalisme permet d'exprimer des propriétés de sécurité comme le secret fort, l'intraçabilité ou l'anonymat. De plus, les protocoles sont exécutés simultanément par un grand nombre d'agents, à plusieurs reprises si bien que nous nous heurtons très rapidement à des résultats d'indécidabilité. Dès lors, il faut ou bien tenir compte du nombre arbitraire de sessions et rechercher des méthodes de semi-décision ou identifier des classes décidables ;ou bien établir des procédures de décision pour un nombre fini de sessions. Au moment où nous avons commencé les travaux présentés dans cette thèse les outils de vérification de propriétés d'indistinguabilité pour un nombre borné de sessions ne permettaient de traiter que très peu de sessions :dans certains cas il était tout juste possible de modéliser un échange complet. Cette thèse présente des procédures de décision efficaces dans ce cadre. Dans un premier temps, nous établissons des résultats de petite attaque. Pour des protocoles déterministes nous démontrons qu'il existe une attaque si, et seulement s’il existe une attaque bien typée lorsque toute confusion entre les types des variables est évitée. De plus, nous prouvons que, lorqu'il existe une attaque l'attaquant peut la trouver en utilisant au plus trois constantes. Dans un second temps, nous traduisons le problème d'indistinguabilité en termes d'accessibilité dans un système de planification qui est résolu par l'algorithme du graphe de planification associé à un codage SAT. Nous terminons en confirmant l'efficacité de la démarche ,à travers l'implémentation de l'outil SAT-Equivet sa comparaison vis-à-vis des outils analogues. / This thesis presents methods to verify cryptographic protocolsin the symbolic model: formal methods allowto verify that small distributed programssatisfy equivalence properties.Those properties state that an attackercannot decide what scenario is beeing played.Strong secrecy, and privacy type properties, like anonymityand unlinkeability, can be modelled through this formalism.Moreover, protocols are executed simultaneouslyby an unbounded number of agents, for an unbounded numberof sessions,which leads to indecidability results.So, we have either to consider an arbitrary number of sessions,and search for semi-decision proceduresand decidable classes;or to establish decision procedures for a finite numberof sessions.When we started the work presented in this thesis,the existing equivalence checkers in the bounded modelwere highly limited. They could only handlea~very small number of sessions (sometimes no more than three).This thesis presents efficient decision proceduresfor bounded verification of equivalence properties.Our first step is to provide small attack results.First, for deterministic processes, there existsan attack if, and ony if, there is a well-typed attack,assuming that there is no confusion between variable types.Second, when there exists a flaw,the attacker needs at most three constants to find it.Then, our second step is to translatethe indistinguishability problem as a reachability problemin a planning system. We solve this second problemthrough planning graph algorithm and SAT encoding.In a final step, we present the implementation ofthe SAT-Equiv tool, which allows us to evaluate our approach.In particular, a benchmark with comparable tools provesthe efficiency of SAT-Equiv.