Les problèmes logiciels sont frustrants et diminuent l’expérience utilisateur. Par exemple, la fuite de données bancaires, la publication de vidéos ou de photos compromettantes peuvent affecter gravement une vie. Comment éviter de telles situations ? Utiliser des tests est une bonne stratégie, mais certains bogues persistent. Une autre solution est d’utiliser des méthodes plus mathématiques, aussi appelées méthodes formelles. Parmi celles-ci se trouve la sémantique dénotationnelle. Elle met la sémantique extraite de vos logiciels préférés en correspondance avec des objets mathématiques. Sur ceux-ci, des propriétés peuvent être vérifiées. Par exemple, il est possible de déterminer, sous certaines conditions, si votre logiciel donnera une réponse. Pour répondre à ce besoin, il est nécessaire de s’intéresser à des théories mathématiques suffisamment riches. Parmi les candidates se trouvent le sujet de ce mémoire : la théorie des domaines. Elle offre des objets permettant de modéliser formellement les données et les instructions à l’aide de relations d’ordre. Cet écrit présente les concepts fondamentaux tout en se voulant simple à lire et didactique. Il offre aussi une base solide pour des lectures plus poussées et contient tout le matériel nécessaire à sa lecture, notamment les preuves des énoncés présentés. / Bugs in programs are definitively annoying and have a negative impact on the user experience. For example, leaks of bank data or leaks of compromising videos or photos have a serious effect on someone’s life. How can we prevent these situations from happening? We can do tests, but many bugs may persist. Another way is to use mathematics, namely formal methods. Among them, there is denotational semantics. It links the semantics of your favorite program to mathematical objects. On the latter, we can verify properties, e.g., absence of bugs. Hence, we need a rich theory in which we can express the denotational semantics of programs. Domain Theory is a good candidate and is the main subject of this master thesis. It provides mathematical objects for data and instructions based on order relations. This thesis presents fundamental concepts in a simple and pedagogical way. It is a solid basis for advanced readings as well as containing all the needed knowledge for its reading, notably proofs for all presented statements.

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.

Les systèmes informatiques offrent une grande flexibilité aux usagers en leur permettant l'accès, notamment par le biais de réseaux de télécommunication ou de l'Internet, à un vaste éventail de services. Toutefois, certains de ces services sont soumis à de fortes contraintes de sécurité, comme le télépaiement qui est au coeur du commerce électronique. Ainsi, les fournisseurs et les utilisateurs expriment des besoins croissants, et antagonistes, en sécurité. Répondre à ces deux besoins simultanément est un enjeu technologique transversal à de nombreux domaines de l'informatique. L'objectif de ce travail est de développer un mécanisme permettant de garantir la sécurité des systèmes, en s'appuyant sur l'expérience établie dans le domaine de la sécurité et des méthodes formelles. Pour se faire, nous définissons un nouveau cadre de vérification des propriétés de sécurité d'un programme informatique par l'analyse des flots de données et de contrôle construits à partir du code de ce dernier. L'idée principale consiste à définir un modèle pouvant abstraire la trace d'événements et les dépendances de ressources engendrés au moment de l'exécution du programme, et pouvant être soumis à des algorithmes de vérification de modèle (model-checking) pour l'analyse de la sûreté du programme vis-à-vis d'une propriété.

Se procurer les outils les plus récents et les plus performants liés à la sécurisation de réseaux informatique est loin d'être suffisant pour réduire les risques d'intrusions. En effet, le maillon le plus faible dans la chaîne de la sécurité informatique est souvent l'intervention humaine qui est parfois nécessaire pour installer et configurer ces outils. Limiter cette intervention humaine permettra sans doute de réduire à la fois les risques et les coûts engendrés par la sécurité. Il est important, par exemple, de développer des méthodes sûres permettant de configurer automatiquement un réseau informatique de sorte que son comportement soit conforme à une politique de sécurité donnée. C'est dans cet axe de recherche que se situe ce travail. En effet, nous proposons une méthode formelle permettant de générer à partir d'une politique de sécurité (spécifiée par une formule logique) et d'un réseau informatique (spécifié par un processus) une configuration sécuritaire de ce réseau.

Certains protocoles cryptographiques ont été développés spécifiquement pour assurer quelques propriétés de sécurité dans nos réseaux de communication. Dans le but de s'assurer qu'un protocole remplit ses propriétés de sécurité, des vérifications probabilistes y sont donc entreprises afin de confirmer s'il présente des failles lorsqu'on prend en compte leur comportement probabiliste. Nous avons voulu entreprendre une méthode probabiliste, mais aussi non-déterministe, de modélisation de protocoles afin de confirmer si cette méthode peut remplacer d'autres qui ont déjà été utilisées pour vérifier des failles sur des protocoles cryptographiques. Cela nous a motivé à envisager comme objectif de nos recherches scientifiques, des analyses quantitatives des possibilités de faille sur des protocoles cryptographiques. / Certain cryptographic protocols were specifically developed to provide some security properties in our networks of communication. For the purpose of assuring that a protocol fulfils its security properties, probabilistic model checkings are undertaken to confirm if it introduces a fault when its probabilistic behavior is considered. We wanted to use a probabilistic method (and also non-deterministic) of protocols modeling to confirm if this method may substitute others that were already used for checking faults in cryptographic protocols. It leads us to consider the objective of our scientific researches as: quantitative analysis of faults in cryptographic protocols.

Tableau d’honneur de la Faculté des études supérieures et postdoctorales, 2004-2005 / Dans les deux dernières décennies, l’Internet a apporté une nouvelle dimension aux communications. Il est maintenant possible de communiquer avec n’importe qui, n’importe où, n’importe quand et ce, en quelques secondes. Alors que certains systèmes de communication distribués, comme le courriel, le chat, . . . , sont plutôt informels et ne nécessitent aucune sécurité, d’autres comme l’échange d’informations militaires ou encore médicales, le commerce électronique, . . . , sont très formels et nécessitent de très hauts niveaux de sécurité. Pour atteindre les objectifs de sécurité voulus, les protocoles cryptographiques sont souvent utilisés. Cependant, la création et l’analyse de ces protocoles sont très difficiles. Certains protocoles ont été montrés incorrects plusieurs années après leur conception. Nous savons maintenant que les méthodes formelles sont le seul espoir pour avoir des protocoles parfaitement corrects. Ce travail est une contribution dans le domaine de l’analyse des protocoles cryptographiques de la façon suivante: • Une classification des méthodes formelles utilisées pour l’analyse des protocoles cryptographiques. • L’utilisation des systèmes d’inférence pour la mod´elisation des protocoles cryptographiques. • La définition d’une classe de systèmes d’inférence qui ont une theorie décidable. • La proposition d’une procédure de décision pour une grande classe de protocoles cryptographiques / In the last two decades, Internet brought a new dimension to communications. It is now possible to communicate with anyone, anywhere at anytime in few seconds. While some distributed communications, like e-mail, chat, . . . , are rather informal and require no security at all, others, like military or medical information exchange, electronic-commerce, . . . , are highly formal and require a quite strong security. To achieve security goals in distributed communications, it is common to use cryptographic protocols. However, the informal design and analysis of such protocols are error-prone. Some protocols were shown to be deficient many years after their conception. It is now well known that formal methods are the only hope of designing completely secure cryptographic protocols. This thesis is a contribution in the field of cryptographic protocols analysis in the following way: • A classification of the formal methods used in cryptographic protocols analysis. • The use of inference systems to model cryptographic protocols. • The definition of a class of theory-decidable inference systems. • The proposition of a decision procedure for a wide class of cryptographic protocols.

Nous étudions la modélisation et la validation hors-ligne des applications temps-réel en environnement monoprocesseur, qui prend explicitement en compte l'échange des messages, le partage des ressources et les instructions conditionnelles entre les tâches. Notre objectif est de mettre en évidence l'impact de ces paramètres sur l'analyse des applications. Classiquement, ces applications sont modélisées de façon linéaire, en encapsulant les blocs conditionnels, et les séquences sont utilisées pour leur validation. Nous proposons une approche de modélisation et de validation arborescente, qui permet de considérer de façon explicite les blocs conditionnels, et qui utilise les arbres d'ordonnancement pour la validation. Nous comparons ensuite ces deux approches, et prouvons que les premières sont parfois trop pessimistes, c'est à dire qu'elles peuvent conduire à déclarer certaines applications comme non ordonnançables, alors qu'en réalité elles le sont. Nous commençons par construire un générateur d'arbres d'ordonnancement valides. La complexité du générateur étant exponentielle en fonction du nombre de tâches, cette approche est di cile à mettre en ÷uvre dans la pratique. Nous proposons donc une approche de modélisation bas ée sur les réseaux de Petri. Ce réseau sera utilisé pour générer les arbres valides, par construction du graphe de marquages, et la complexité pourra être réduite grâce à des heuristiques.

Le sujet de ma thèse s’inscrit dans le domaine des preuves formelleset de la vérification des algorithmescryptographiques. L’implémentation des algorithmes cryptographiquesest souvent une tâche assez compliquée, parce qu’ils sont optimiséspour être efficaces et sûrs en même temps. Par conséquent, il n’estpas toujours évident qu’un programme cryptographique en tant quefonction, corresponde exactement à l’algorithme mathématique,c’est-à-dire que le programme soit correct. Les erreurs dans lesprogrammes cryptographiques peuvent mettre en danger la sécurité desystèmes cryptographiques entiers et donc, des preuves de correctionsont souvent nécessaires. Les systèmes formels et les assistants depreuves comme Coq et Isabelle-HOL sont utilisés pour développer despreuves de correction des programmes. Les courbes elliptiques sontlargement utilisées en cryptographie surtout en tant que groupecryptographique très efficace. Pour le développement des preuvesformelles des algorithmes utilisant les courbes elliptiques, unethéorie formelle de celles-ci est nécessaire. Dans ce contexte, nousavons développé une théorie formelle des courbes elliptiques enutilisant l’assistant de preuves Coq. Cette théorie est par la suiteutilisée pour prouver la correction des algorithmes de multiplicationscalaire sur le groupe des points d’une courbe elliptique.Plus précisément, mes travaux de thèse peuvent être divisées en deuxparties principales. La première concerne le développement de lathéorie des courbes elliptiques en utilisant l'assistant des preuvesCoq. Notre développement de plus de 15000 lignes de code Coqcomprend la formalisation des courbes elliptiques données par uneéquation de Weierstrass, la théorie des corps des fonctionsrationnelles sur une courbe, la théorie des groupes libres et desdiviseurs des fonctions rationnelles sur une courbe. Notre résultatprincipal est la formalisation du théorème de Picard; une conséquencedirecte de ce théorème est l’associativité de l’opération du groupedes points d’une courbe elliptique qui est un résultat non trivial àprouver. La seconde partie de ma thèse concerne la vérification del'algorithme GLV pour effectuer la multiplication scalaire sur descourbes elliptiques. Pour ce développement, nous avons vérifier troisalgorithmes indépendants: la multiexponentiation dans un groupe, ladécomposition du scalaire et le calcul des endomorphismes sur unecourbe elliptique. Nous avons également développé une formalisationdu plan projectif et des courbes en coordonnées projectives et nousavons prouvé que les deux représentations (affine et projective) sontisomorphes.Notre travail est à la fois une première approche à la formalisationde la géométrie algébrique élémentaire qui est intégré dans lesbibliothèques de Ssreflect mais qui sert aussi à la certification devéritables programmes cryptographiques. / This thesis is in the domain of formalization of mathematics and ofverification of cryptographic algorithms. The implementation ofcryptographic algorithms is often a complicated task becausecryptographic programs are optimized in order to satisfy bothefficiency and security criteria. As a result it is not alwaysobvious that a cryptographique program actually corresponds to themathematical algorithm, i.e. that the program is correct. Errors incryprtographic programs may be disastrous for the security of anentire cryptosystem, hence certification of their correctness isrequired. Formal systems and proof assistants such as Coq andIsabelle-HOL are often used to provide guarantees and proofs thatcryptographic programs are correct. Elliptic curves are widely usedin cryptography, mainly as efficient groups for asymmetriccryptography. To develop formal proofs of correctness forelliptic-curve schemes, formal theory of elliptic curves is needed.Our motivation in this thesis is to formalize elliptic curve theoryusing the Coq proof assistant, which enables formal analysis ofelliptic-curve schemes and algorithms. For this purpose, we used theSsreflect extension and the mathematical libraries developed by theMathematical Components team during the formalization of the FourColor Theorem. Our central result is a formal proof of Picard’stheorem for elliptic curves: there exists an isomorphism between thePicard group of divisor classes and the group of points of an ellipticcurve. An important immediate consequence of this proposition is theassociativity of the elliptic curve group operation. Furthermore, wepresent a formal proof of correctness for the GLV algorithm for scalarmultiplication on elliptic curve groups. The GLV algorithm exploitsproperties of the elliptic curve group in order to acceleratecomputation. It is composed of three independent algorithms:multiexponentiation on a generic group, decomposition of the scalarand computing endomorphisms on algebraic curves. This developmentincludes theory about endomorphisms on elliptic curves and is morethan 5000 lines of code. An application of our formalization is alsopresented.

Les problèmes militaires sont très complexes et plusieurs d'entre eux ne peuvent être résolues en utilisant les techniques d'optimisation classiques. Le problème visé par ce travail de maîtrise, est celui de la gestion en temps réel des ressources d'une frégate. Ces ressources doivent être assignées convenablement et dans les délais requis de manière à contrer les menaces et augmenter ainsi la probabilité de survie de la frégate. Pour contribuer à résoudre un tel problème, nous avons convenu tout d'abord, d'analyser les menaces une à une et de déterminer lesquelles sont les plus importantes et quel plan d'attaque il convient d'élaborer pour les contrer. Nous avons introduit à cet effet, l'évaluation de ``l'engageabilité'' qui permet de considérer différents facteurs déterminants dans l'allocation des ressources. Nous avons ensuite formalisé le problème en question, en utilisant un modèle formel emprunté à la satisfaction des contraintes (CSP=constraint Satisfaction problem). Finalement, nous avons montré dans quelles circonstances il est avantageux d'utiliser cette évaluation de l'engageabilité dans un processus d'allocation de ressources en temps réel et dans un environnement stochastique, le tout relativement à la survie de la frégate. / Military problems are very complex and they can be solved by different artificial intelligence techniques. In this thesis, we address the problem of weapon-targets assignment for a frigate. To defend efficiently the ship, we have to analyze each threat and determine which resource assigns against it. For that purpose, we utilize the engageability assessment to consider different characteristics; useful in the resources assignment. To this end, a mathematical model named Constraint Satisfaction Problem (CSP) is employed. This framework allows formalizing the problem to ensure the constraint consistency and to sort threats in importance order. We tried this algorithm on different types of weapon-target assignment problems. Finally, we demonstrate the advantage of engageability assessment on the weapon-target assignment problem in real time and stochastic environment.

Le sujet central de cette thèse est le développement d'une méthode dédiée à la preuve de structures de données sans verrou. La motivation première vient du constat que les programmes concurrents sont devenu monnaie courante. Ceci a été possible par l'apparition de nouvelles primitives de synchronisation dans les nouvelles architectures matérielles. La seconde motivation est la quête de logiciel prouvé et donc correct. La sûreté des logiciels est en effet devenue primordiale de par la diffusion des systèmes embarqués et enfouis. La méthode proposée est basée sur le raffinement et dédiée à la conception et la vérification d'algorithme non-bloquant, en particulier ceux sans verrou. La méthode a été formalisée et sa correction prouvée en Isabelle/HOL. Un outil a par ailleurs été développé afin de générer des obligations de preuves à destination des solveurs SMT et des prouveurs de théorèmes du premier ordre. Nous l'avons utilisé afin de vérifier certains de ces algorithmes.