La sûreté de fonctionnement occupe une place prépondérante dans la conception de systèmes critiques, puisqu'un dysfonctionnement peut être dangereux pour les utilisateurs ou l'environnement. Les concepteurs doivent également démontrer aux autorités de certification que les risques encourus sont acceptables. Pour cela, le concepteurs définissent une architecture contenant un ensemble de mécanismes de sûreté permettant de mitiger ou tout du moins limiter la probabilité d’occurrence des risques identifiés. L'objectif de ce travail est de développer une méthode automatique et générique de synthèse d’architecture assurant formellement le respect d’exigences de sûreté. Cette activité de synthèse est formalisée comme un problème d'exploration de l'espace des architectures c'est-à-dire trouver un candidat appartenant à un espace de recherche fini, respectant les exigences de sûreté. Ainsi nous proposons un processus de résolution complet et correct des problèmes d'exploration basé sur l'utilisation des solveurs SMT. Les contributions principales sont:1- La formalisation de la synthèse comme un problème de Satisfiabilité Modulo Théorie (SMT) afin d’utiliser les solveurs existants pour générer automatiquement une solution assurant formellement le respect des exigences;2- Le développement de méthodes d’analyse spécialement conçues pour évaluer efficacement la conformité d’une architecture vis-à-vis d’un ensemble d’exigences;3- La définition d'un langage KCR permettant de formuler les problèmes d'exploration et l'implantation des méthodes de résolution au sein de l'outil KCR Analyser. / Safety is a major issue in the design of critical systems since any failure can be hazardous to the users or the environment of such systems. In some areas, such as aeronautics, designers must also demonstrate to the certification authorities that the risks are acceptable. To do so, the designers define an architecture containing a set of security mechanisms to mitigate or at least limit the probability of occurrence of the identified risks. The objective of this work is to develop an automatic and generic method of architectural synthesis which formally ensures compliance with the safety requirements. This synthesis activity is then formalized as a design space exploration problem, i.e. find a candidate belonging to a finite set of architectures, fulfilling the safety requirements. Thus, we propose in this document a complete and correct resolution process of the design space exploration problem based on the use of SMT solvers. The main contributions are:1- the formalization of the synthesis as a problem of Satisfiability Modulo Theory (SMT) in order to use existing solvers to automatically generate a solution formally ensuring safety requirements;2- the development of analytic methods specially designed to efficiently assess the conformity of an architecture with respect to a set of safety requirements;3- the definition of a language named, KCR, allowing to formulate the design space exploration problem and the implementation of the methods of resolution presented in this work within the tool KCR Analyser.

En analyse de risques, les arbres d’attaque sont utilisés pour évaluer les menaces sur un système. Les méthodes formelles permettent leur analyse quantitative et leur synthèse, mais les propriétés exprimant la qualité des arbres d’attaque par rapport au système n’ont pas été formalisées. Dans ce document, nous définissons un nouveau cadre formel pour les arbres d’attaque prenant en compte un modèle opérationnel du système, et dotant les arbres d’une sémantique de chemins. Nous définissons les propriétés de correction des raffinements, et étudions leurs complexités. A partir d’une attaque optimale dans un modèle de système quantitatif, nous guidons la conception d’un arbre d’attaque, en indiquant ses feuilles qui contribuent à l’attaque optimale considérée. / In risk analysis, attack trees are used to assess threats to a system. Formal methods allow for their quantitative analysis and synthesis, but the properties expressing the quality of the attack trees with respect to the system have not been formalized. In this document, we define a new formal framework for attack trees that takes an operational model of the system into account, and provides the trees with a path semantics. We define the correctness properties of refinements, and study their computational complexity. Given an optimal attack in a quantitative system model, we guide the design of a attack tree, indicating its leaves that contribute to considered the optimal attack.

Les protocoles de sécurité modernes peuvent impliquer un participant humain de façon à ce qu'il compare ou copie de courtes chaines de caractères faisant le pont entre différents appareils. C'est par exemple le cas des protocoles basés sur une authentification à facteur multiples comme les protocoles Google 2 factor ou 3D-Secure.Cependant, de telles chaines de caractères peuvent être sujettes à des attaques par force brute. Dans cette thèse nous proposons un modèle symbolique qui inclut les capacités de l'attaquant à deviner des secrets faibles et à produire des collisions avec des fonctions de hachage dont de l'application résulte une courte chaine de caractères. Nous proposons une nouvelle procédure de décision pour analyser un protocole (restreint à un nombre borné de sessions) qui se base sur de courtes chaines de caractères. Cette procédure a été intégré dans l'outil AKISS et testé sur les protocoles du standard ISO/IEC 9798-6:2010 / Modern security protocols may involve humans in order to compare or copy short strings betweendifferent devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-Secure are typical examplesof such protocols. However, such short strings may be subject to brute force attacks. In this thesis we propose asymbolic model which includes attacker capabilities for both guessing short strings, and producing collisions whenshort strings result from an application of weak hash functions. We propose a new decision procedure for analyzing(a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in theAKISS tool and tested protocols from the ISO/IEC 9798-6:2010 standard

La préservation de propriétés établies sur le programme source jusqu'au code exécutable est un point important dans les méthodes formelles. Cette propriété de préservation est établie par la vérification formelle du proccessus de compilation. Un compilateur est formellement vérifié s'il est accompagné d'une preuve de préservation sémantique : "si la compilation réussit, le code compilé se comporte comme le code source le prédit." Le projet CompCert étudie la vérification formelle de compilateurs réalistes utilisable dans l'embarqué-critique. Il s'agit de développer et formellement vérifier de tels compilateur via l'assistant de preuve Coq. Un compilateur pour le langage C vers l'assembleur PowerPC a déjà ainsi été produit. Le code exécutable du compilateur a été obtenu en deux étapes non vérifiés : la génération automatique de code Ocaml par le mécanisme d'extration de Coq et la compilation du de ce code extrait par le système Objective Caml. En fait, cette lacune est commune à tous les développements spécifiés dans l'assistant de preuve Coq et destinés à produire un éxécutable. Cette thèse décrit l'étude, le développement et la vérification formelle, dans l'assistant de preuve Coq, d'un compilateur pour le fragment purement fonctionnel du langage ML : le langage cible du mécanisme d'extraction de Coq. Concrètement, il s'git d'une chaîne de compilation en amont pour mini-ML (lambda calcul, let, letrec et filtrage) vers le premier langage intermédiaire de la chaîne de compilation en aval du compilateur CompCert. Ce langage, Cminor, est un langage de bas niveau à la C. L'expressivité du langage source traité rend ce compilateur réaliste. Il comporte aussi des optimisations classiques propre à la compilation de langages fonctionnels : la décurryfication, comme celle implémentée dans le compilateur OCaml ; la représentation uniforme des données, explicitation des fermetures, numérotation des constructeurs et une mise en style par passage de continuation (CPS) optimisée. Le point fort de ce compilateur et que, comme les compilateurs modernes pour langage de haut niveau, il peut interagir avec un gestionnaire de mémoire automatique. Cette interaction a aussi été formellement vérifiée.

Dans les domaines critiques d'application de l'informatique, il peut être vital de disposer d'un génie logiciel qui soit capable de garantir le bon fonctionnement des systèmes produits. Dans ce contexte, la méthode B évènementielle promeut le développement de modèles abstraits du système à concevoir et l'utilisation de démonstrations formelles ainsi que de la relation de raffinement entre les modèles. Notre but est de pouvoir travailler sur des systèmes ayant des aspects temporels quantitatifs (propriétés et contraintes de temps) en restant au sein du cadre défini par la méthode B qui a déjà montré son efficacité par ailleurs, mais qui ne dispose pas de concepts spécifiques pour le temps. C'est ainsi que nous proposons l'introduction des contraintes de temps par le raffinement, ceci permet de respecter la philosophie de la méthode B et de systématiser cette approche par la formalisation de patrons de raffinement. Nos différentes modélisations du temps sont proposées sous la forme de patron à réappliquer sur le système à étudier. Nous pouvons donc étudier progressivement le système à partir d'une abstraction non-temporelle afin de le valider progressivement et de distribuer la difficulté de la preuve en plusieurs étapes. L'introduction des aspects temporels ne se fait que lorsque cela est nécessaire lors du processus de développement prouvé. Nous avons validé cette approche sur des études de cas réalistes en utilisant les outils logiciels de démonstration formelle de la méthode B.

Cette thèse se situe au croisement de deux domaines : la sûreté de fonctionnement des systèmes critiques et les méthodes formelles. Nous cherchons à établir la cohérence des analyses de sûreté de fonctionnement réalisées à l'aide de modèles représentant un même système à des niveaux de détail différents. Pour cela, nous proposons une notion de raffinement dans le cadre de la conception de modèles AltaRica : un modèle détaillé raffine un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vérification du raffinement de modèles AltaRica est supportée par l'outil de model-checking MecV. Ceci permet de réaliser des analyses multi-systèmes à l'aide de modèles à des niveaux de détail hétérogènes : le système au centre de l'étude est détaillé tandis que les systèmes en interface sont abstraits. Cette approche a été appliquée à l'étude d'un système de contrôle de gouverne de direction d'un avion connecté à un système de génération et distribution électrique.

Nous nous intéressons dans ce document à la génération automatique de tests de conformité pour des implémentations réactives. Nous nous attachons dans un premier temps à étendre la méthode de génération de tests, basée sur la théorie du test de conformité à la ioco, en reliant trois niveaux de description (propriétés, spécification et implémentation). Nous combinons pour cela vérification formelle et test de conformité. Nous obtenons ainsi, lors de l'exécution du cas de test sur l'implémentation, des verdicts pouvant indiquer la non-conformité de l'implémentation, mais également la satisfaction/violation de la propriété par l'implémentation et/ou la spécification. Nous étendons dans un deuxième temps la génération de tests par l'expressivité du modèle de spécification en nous intéressant aux spécifications interprocédurales récursives. Notre méthode est basée sur une analyse exacte de co-accessibilité permettant de décider si et comment un objectif de test pourra être atteint. Cependant, l'incapacité des cas de test récursifs à connaître leur propre pile d'exécution ne permet pas d'utiliser la totalité des résultats de l'analyse. Nous discutons de ce problème d'observation partielle et de ses conséquences puis nous proposons un moyen de minimiser son impact. Enfin, nous expérimentons ces méthodes de génération de tests sur quelques exemples et une étude de cas

Nous nous sommes intéressé à la logique équationnelle en tant que support de la vérification des programmes impératifs. Notre approche vise le double objectif d'automatiser la vérification des propriétés de programmes et de proposer un formalisme pour raisonner sur les programmes adapté aux acteurs du développement des logiciels. Précisément, les travaux de cette thèse portent sur la traduction automatique des programmes impératifs vers la logique équationnelle. Nous avons considéré deux classes de programmes. Dans la première, la seule instruction avec effet de bord du langage est l'affectation. Nous présentons l'algorithme de traduction d'un programme en un ensemble d'équations sous la forme d'un système de réécriture définissant la sémantique du langage. Nous montrons la convergence du système de réécriture à l'aide d'un démonstrateur de théorèmes. Pour la seconde classe, nous ajoutons au langage appel par référence et listes mutables. Ces deux mécanismes introduisent la possibilité de manipuler des alias dans les programmes. Nous énonçons des restrictions sur l'utilisation des alias moyennant lesquelles nous proposons un algorithme pour la traduction en équations des programmes de cette seconde classe. La définition équationnelle obtenue ne s'appuie pas sur un modèle de la mémoire. Les équations produites par la traduction d'un programme peuvent alors être utilisées dans des systèmes de preuve afin de vérifier des propriétés du programme, elles-mêmes exprimées par des équations. Nous validons notre approche par une implantation des algorithmes et par la preuve de propriétés de programmes non triviales à l'aide des équations produites par notre méthode.

Cette thèse propose des méthodes assistant la modélisation et l'évaluation qualitative de l'architecture de sûreté de fonctionnement des systèmes embarqués complexes. Ces architectures sont souvent construites à partir de motifs généraux d'architectures de systèmes correspondant à des mécanismes de sûreté récurrents comme des redondances, des détections, etc. En s'inspirant des principes des "patrons de conception" développés en génie logiciel, nous avons proposé une modélisation de ces mécanismes et des attributs permettant leur réutilisation lors des analyses de sûreté de fonctionnement. Ces analyses nécessitent de raisonner sur le comportement des systèmes en présence de pannes qui peut être modélisé à l'aide de langages formels comme AltaRica. Dans notre cas, les motifs correspondent à des abstractions d'architectures concrètes et donc requièrent une modélisation plus déclarative. Les propriétés étudiées étant en général dynamiques, nous avons choisi d'utiliser une logique temporelle pour les exprimer. Les motifs sont donc constitués d'une partie AltaRica et d'une partie propriétés. Ce type de modélisation mixte possède plusieurs intérêts, notamment lors de la conception en phase amont d'architectures de systèmes où il est possible de manipuler à la fois des parties d'un système conçues de manière détaillée et des spécifications. Elle a également pour buts de faciliter l'allocation d'exigences pour la validation d'architectures ainsi que le prototypage. Nous avons donc défini une notation mixant ces aspects opérationnels et déclaratifs.

Notre thèse se situe dans le domaine des méthodes formelles appliquées aux systèmes réactifs. Nous modélisons et traitons ces systèmes, en continuelle interaction avec leur environnement, grâce au langage<br />synchrone Lustre.<br /><br />D'abord, sur la base d'un travail précurseur, nous établissons pour Lustre une méthode de preuve inductive des propriétés de sûreté. Cette méthode est optimisée, afin de prendre en compte au mieux la dynamique des systèmes. Elle est implémentée dans un outil de preuve, Gloups.<br /><br />Ensuite, suivant le modèle de la méthode B, nous définissons un calcul de raffinement pour Lustre. Ce calcul est à la fois adapté à Lustre et exprimé en ce langage. Les obligations de preuve qui assurent la<br />correction du raffinement peuvent être traitées par Gloups. Pour faciliter le développement, un autre outil, Flush, génère automatiquement les obligations pour Gloups.<br /><br />Ainsi, nous utilisons Lustre à la fois comme langage de programmation et comme cadre formel d'un développement maîtrisé. L'intérêt de ce<br />procédé réside dans la simplicité du langage et dans son adaptation aux systèmes réactifs : en ce domaine, notre méthode de raffinement est suffisamment expressive, sans être inutilement compliquée. Des exemples viennent démontrer l'intérêt de la méthode.