Avec le développement des réseaux de communications comme Internet, le besoin d'assurer la sécurité des échanges a considérablement augmenté. Les communications " sécurisées " sont réalisées par l'utilisation de petits programmes appelés protocoles cryptographiques qui peuvent être attaqués même en présence d'un chiffrement parfait. De telles failles, qualifiées de " failles logiques ", sont souvent subtiles et difficiles à déceler à la simple vue du texte du protocole. Dans cette thèse, nous poussons les limites de l'analyse des protocoles au delà de cette hypothèse. En particulier, nous proposons des procédures de décision, pour le problème de la recherche d'attaques en présence d'opérateurs satisfaisant des propriétés algébriques.

La conception d'un protocole cryptographique obéit à de nombreux impératifs : algorithmes à utiliser, propriétés à garantir, moyen d'identification, etc. Il apparaît donc régulièrement de nouveaux protocoles qu'il convient de vérifier. Malgré l'apparente simplicité, concevoir un protocole cryptographique est une tâche difficile et sujette à de nombreuses erreurs. Des failles pour certains protocoles ont été découvertes des années après leur conception. La plupart des travaux existants se basent uniformément sur l'intrus de Dolev Yao et ne se généralisent pas automatiquement à un intrus disposant de capacités supplémentaires ou différentes. Dans cette thèse, nous allons présenter un système de déduction prenant le pouvoir de l'intrus comme paramètre. De plus, les règles de protocole seront vues comme une capacité additionnelle pour l'intrus. Le résultat principal est un théorème de normalisation de preuve permettant de réduire l'espace de recherche des attaques.

Les protocoles de communication asynchrones sont naturellement modélisés par des automates communicants via des canaux FIFO non bornés. Dans cette thèse nous nous intéressons aux variantes des Lossy Channel Systems pour lesquelles les pertes de messages dans les canaux sont probabilistes. Plus précisément, on considère des sémantiques sous forme de chaînes de Markov et de processus de décision markoviens. Un théorème général de convergence de points fixes dans les systèmes de transition bien structurés, permet de prouver pour les PLCS et NPLCS de nombreux résultats de décidabilité pour la vérification de propriétés du temps linéaire. Nous donnons également les limites des modèles par l'intermédiaire de résultats d'indécidabilité. Un prototype a fait l'objet de l'implémentation des algorithmes développés dans la thèse. Malgré la grande complexité des problèmes cet outil a permis de prouver des propriétés de vivacité sur des protocoles tels que le Bit Alterné et le protocole de Pachl.

Nous etendons les logiques temporelles du temps alternant ATL et ATL* au moyen de contextes strategiques et de contraintes sur la memoire : la premiere extension permet aux agents de s'en tenir a leurs strategies lors de l'evaluation des formules, contrairement a ATL ou chaque quantificateur de strategies ecrase les strategies anterieurement selectionnees. La seconde extension permet aux quantificateurs de strategies de se restreindre aux strategies sans memoire ou avec memoire bornee. Nous avons l'etudie l'expressivite de nos logiques. Nous montrons qu'elles expriment des proprietes importantes comme l'exstence d'equilibres, et nous les comparons formellement a d'autres formalismes proches (ATL, ATL*, Game Logic, Strategy Logic, ...). Nous avons aborde les problemes de model-checking. Nous donnons un algorithme PSPACE pour la logique n'impliquant que des strategies sans memoire, et un algorithme EXPSPACE pour le cas des strategies a memoire bornee. Dans le cas general, malgre leur forte expresssivite, nous prouvons que leur model-checking reste decidable par un algorithme a base d'automates d'arbres alternants qui permet d'evaluer une formule sur la classe complete des CGS avec n joueurs.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal

Le développement d'un système a pour objectif de répondre à des exigences. Aussi, le succès de sa réalisation repose en grande partie sur la phase de spécification des exigences qui a pour vocation de décrire de manière précise et non ambiguë toutes les caractéristiques du système à développer.Les spécifications d'exigences sont le résultat d'une analyse des besoins faisant intervenir différentes parties. Elles sont généralement rédigées en langage naturel (LN) pour une plus large compréhension, ce qui peut mener à diverses interprétations, car les textes en LN peuvent contenir des ambiguïtés sémantiques ou des informations implicites. Il n'est donc pas aisé de spécifier un ensemble complet et cohérent d'exigences. D'où la nécessité d'une vérification formelle des spécifications résultats.Les spécifications LN ne sont pas considérées comme formelles et ne permettent pas l'application directe de méthodes vérification formelles.Ce constat mène à la nécessité de transformer les spécifications LN en spécifications formelles.C'est dans ce contexte que s'inscrit cette thèse.La difficulté principale d'une telle transformation réside dans l'ampleur du fossé entre spécifications LN et spécifications formelles.L'objectif de mon travail de thèse est de proposer une approche permettant de vérifier automatiquement des spécifications d'exigences utilisateur, écrites en langage naturel et décrivant le comportement d'un système.Pour cela, nous avons exploré les possibilités offertes par un modèle de représentation fondé sur un formalisme logique.Nos contributions portent essentiellement sur trois propositions :1) une ontologie en OWL-DL fondée sur les logiques de description, comme modèle de représentation pivot permettant de faire le lien entre spécifications en langage naturel et spécifications formelles; 2) une approche d'instanciation du modèle de représentation pivot, fondée sur une analyse dirigée par la sémantique de l'ontologie, permettant de passer automatiquement des spécifications en langage naturel à leur représentation conceptuelle; et 3) une approche exploitant le formalisme logique de l'ontologie, pour permettre un passage automatique du modèle de représentation pivot vers un langage de spécifications formelles nommé Maude.

Les systèmes à canaux non fiables ont été introduits à l'origine comme un modèle de communication. Ils ont donné naissance à une classe de complexité restée mal comprise pendant longtemps. Dans cette thèse, nous étudions et comblons certaines des plus importantes lacunes dans la connaissance de cette classe. Nous fournissons entre autres des bornes inférieure et supérieure qui se rejoignent pour la complexité en temps. Puis nous proposons un nouvel outil de preuve : le Problème de Sous Mot de Post (PEP). C'est un problème simple, inspiré du Problème de Correspondance de Post, et complet pour cette classe de complexité. Nous étudions ensuite PEP et ses variantes, ainsi que les langages de solutions de PEP sur lesquels nous avons fourni des résultats de complexité et des outils de preuve tels que des lemmes de pompage. / Lossy channel systems were originally introduced to model communication protocols. It gave birth to a complexity class wich remained scarcely undersood for a long time. In this thesis we study some of the most important gaps. In particular, we bring matching upper and lower bounds for the time complexity. Then we describe a new proof tool : the Post Embedding Problem (PEP) which is a simple problem, closely related to the Post Correspondence Problem, and complete for this complexity class. Finally, we study PEP, its variants and the languages of solutions of PEP on which we provide complexity results and proof tools like pumping lemmas.

Le développement des réseaux de communication digitaux tel Internet a rendu omniprésents les protocoles de communication. Les différents appareils électroniques que nous utilisons au quotidien doivent interagir les uns avec les autres afin de réaliser les taches nombreuses et variées qui sont devenues courantes, comme d'utiliser d'un téléphone portable, envoyer ou recevoir des messages électroniques, faire des achats en ligne et ainsi de suite. Pour ces applications, la sécurité est une notion cruciale. Par exemple, dans le cas des achats en ligne, il faut que la transaction ait lieu sans divulguer les informations personnelles de l'acheteur à un tiers. Les protocoles de communications contiennent les règles qui régissent ces interactions. Afin de s'assurer qu'ils garantissent un certain niveau de sécurité, on souhaite pouvoir les analyser. Une analyse manuelle, ou leur faire subir des tests, n'est pas suffisant, les attaques pouvant se révéler subtiles. Certains protocols ont été utilisés pendant des années avant qu'une attaque soit découverte contre eux. Étant donnée leur ubiquité croissante dans de nombreuses applications importantes, comme le commerce électronique, un des défis importants auquel la recherche doit faire face consiste à développer des méthodes et des outils de vérification pour augmenter notre confiance dans les protocoles sécurisés, et dans les applications qui dépendent de ces protocoles. Par exemple, plus de 28 milliards d'euros sont dépensés en France au cours de transactions sur Internet, et cette quantité ne cesse d'augmenter. De plus, de nouveaux types de protocoles apparaissent continuellement afin de relever de nouveaux défis technologiques et de société, e.g. le vote électronique, le passeport numérique pour n'en citer que quelques-uns. / With the development of digital networks, such as Internet, communication protocols are omnipresent. Digital devices have to interact with each other in order to perform the numerous and complex tasks we have come to expect as commonplace, such as using a mobile phone, sending or receiving electronic mail, making purchases online and so on. In such applications, security is important. For instance, in the case of an online purchase, the right amount of money has to be paid without leaking the buyer personal information to outside parties. Communication protocols are the rules that govern these interactions. In order to make sure that they guarantee a certainlevel of security, it is desirable to analyze them. Doing so manually or by testing them is not enough, as attacks can be quite subtle. Some protocols have been used for years before an attack was discovered. Because of their increasing ubiquity in many important applications, e.g. electronic commerce, a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them. For example, more than 28 billion Euros were spent in France using Internet transactions, and the number is growing. Moreover, new types of protocols are continuously appearing in order to face new technological and societal challenges, e.g. electronic voting, electronic passport to name a few.

La prise de conscience générale de l'importance de vérifier plus scrupuleusement les programmes a engendré une croissance considérable des efforts de vérification formelle de programme durant cette dernière décennie. Néanmoins, le code qu'exécute l'ordinateur, ou code exécutable, n'est pas le code écrit par le développeur, ou code source. La vérification formelle de compilateurs est donc un complément indispensable à la vérification de code source.L'une des tâches les plus complexes de compilation est l'allocation de registres. C'est lors de celle-ci que le compilateur décide de la façon dont les variables du programme sont stockées en mémoire durant son exécution. La mémoire comporte deux types de conteneurs : les registres, zones d'accès rapide, présents en nombre limité, et la pile, de capacité supposée suffisamment importante pour héberger toutes les variables d'un programme, mais à laquelle l'accès est bien plus lent. Le but de l'allocation de registres est de tirer au mieux parti de la rapidité des registres, car une allocation de registres de bonne qualité peut conduire à une amélioration significative du temps d'exécution du programme.Le modèle le plus connu de l'allocation de registres repose sur la coloration de graphe d'interférence-affinité. Dans cette thèse, l'objectif est double : d'une part vérifier formellement des algorithmes connus d'allocation de registres par coloration de graphe, et d'autre part définir de nouveaux algorithmes optimisants pour cette étape de compilation. Nous montrons tout d'abord que l'assistant à la preuve Coq est adéquat à la formalisation d'algorithmes d'allocation de registres par coloration de graphes. Nous procédons ainsi à la vérification formelle en Coq d'un des algorithmes les plus classiques d'allocation de registres par coloration de graphes, l'Iterated Register Coalescing (IRC), et d'une généralisation de celui-ci permettant à un utilisateur peu familier du système Coq d'implanter facilement sa propre variante de cet algorithme au seul prix d'une éventuelle perte d'efficacité algorithmique. Ces formalisations nécessitent des réflexions autour de la formalisation des graphes d'interférence-affinité, de la traduction sous forme purement fonctionnelle d'algorithmes impératifs et de l'efficacité algorithmique, la terminaison et la correction de cette version fonctionnelle. Notre implantation formellement vérifiée de l'IRC a été intégrée à un prototype du compilateur CompCert.Nous avons ensuite étudié deux représentations intermédiaires de programmes, dont la forme SSA, et exploité leurs propriétés pour proposer de nouvelles approches de résolution optimale de la fusion, l'une des optimisations opéréeslors de l'allocation de registres dont l'impact est le plus fort sur la qualité du code compilé. Ces approches montrent que des critères de fusion tenant compte de paramètres globaux du graphe d'interférence-affinité, tels que sa largeur d'arbre, ouvrent la voie vers de nouvelles méthodes de résolution potentiellement plus performantes. / The need for trustful programs led to an increasing use of formal verication techniques the last decade, and especially of program proof. However, the code running on the computer is not the source code, i.e. the one written by the developper, since it has to betranslated by the compiler. As a result, the formal verication of compilers is required to complete the source code verication. One of the hardest phases of compilation is register allocation. Register allocation is the phase within which the compiler decides where the variables of the program are stored in the memory during its execution. The are two kinds of memory locations : a limited number of fast-access zones, called registers, and a very large but slow-access stack. The aim of register allocation is then to make a great use of registers, leading to a faster runnable code.The most used model for register allocation is the interference graph coloring one. In this thesis, our objective is twofold : first, formally verifying some well-known interference graph coloring algorithms for register allocation and, second, designing new graph-coloring register allocation algorithms. More precisely, we provide a fully formally veri ed implementation of the Iterated Register Coalescing, a very classical graph-coloring register allocation heuristics, that has been integrated into the CompCert compiler. We also studied two intermediate representations of programs used in compilers, and in particular the SSA form to design new algorithms, using global properties of the graph rather than local criteria currently used in the litterature.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.