De nos jours, la présence de réseaux à grande échelle dans notre société bouleverse nos habitudes avec l'apparition de nouveaux services distants avec des besoins en matière de sécurité de plus en plus important. Nous abordons dans cette thèse la problématique de la composition des protocoles de sécurité, nous nous focalisons notamment sur les protocoles cryptographiques ainsi que sur les politiques de contrôle d'accès. La première partie de la thèse est consacrée à la composition des protocoles cryptographiques ainsi que leurs intégration avec d'autres types de protocoles. Nous introduisons notamment la notion de mécanismes cryptographiques qui sont des protocoles cryptographiques simples qui peuvent être composés pour obtenir des protocoles plus complexes sous réserve de faire les preuves nécessaires. Nous proposons également une méthode pour la reconstitution d'éventuelles attaques. La seconde partie de la thèse est consacrée à l'implémentation des politiques de contrôle d'accès par le raffinement, l'idée consiste à partir de politiques de sécurité abstraites et de les raffiner afin d'obtenir des politiques plus concrètes. Nous proposons également de combiner la technique de raffinement avec la technique de composition pour rendre plus efficace la procédure d'implémentation des politiques de contrôle d'accès / The presence of big scale networks in our modern society is affecting our usual practice, which as a result is generating the need to introduce a more and more important level of remote security services. We address in this thesis the problem of security protocols composition, we focus in particular on cryptographic protocols as well as access control policies. The first part of the thesis is dedicated to the composition of cryptographic protocols and to their integration other classes of protocols. We introduce the notion of cryptographic mechanisms. Mechanisms are simple cryptographic protocols that can be composed to obtain more complex protocols if the necessary proof obligations are discharged. We also introduce a technique for a proof based attack reconstruction. The second part of the thesis is dedicated to the deployment of access control policies using refinement, the idea consists in refining abstract policies to obtain a more concrete access control policies. We also propose to combine the refinement technique with the composition technique to obtain a more efficient access control policies deployment techniques

Le champ de notre projet de recherche est la vérification des systèmes probabilistes interactifs. Étant donnée une formule de la logique PCTL, qui décrit les spécifications d'un système probabiliste, et un modèle, nous nous intéressons à vérifier si celui-ci satisfait la formule donnée. Ceci est fait à l'aide d'une méthode formelle appelée le model-checking. Nous nous restreindrons dans ce travail aux systèmes probabilistes finis ayant une structure particulière sans cycle qu'on appellera systèmes par niveaux. Les systèmes considérés ont un nombre fini d'états et les transitions sont quantifiées avec une mesure de probabilité. Nous désirons déterminer si le model-checking d'une telle structure pourrait être amélioré en utilisant la particularité de cette structure. L'application d'un tel algorithme serait de permettre le model-checking efficace pour les systèmes continus. À cet effet, nous avons élaboré une nouvelle méthode de vérification par modelchecking adaptée aux systèmes par niveaux. Celle-ci consiste, étant donné un modèle représentant un système par niveaux et une formule logique PCTL, à déterminer si ce modèle satisfait cette formule à un niveau i donné du système considéré. À partir de cette méthode, nous avons également étudié la complexité qui lui est associée. Celle-ci a été comparée à la complexité de la méthode de vérification classique. Nous en avons conclu que la méthode élaborée est légèrement plus avantageuse en terme de temps que la méthode classique.

Dans ce mémoire nous nous intéressons à une branche de la vérification qui consiste à comparer une spécification (fonctionnement idéal) à son implémentation (système réel). Tous les deux sont sous forme de systèmes probabilistes, c’est-à-dire des systèmes dont le comportement est incertain mais quantifié par des distributions de probabilité. Il y a plusieurs méthodes disponibles pour comparer les systèmes : la bisimulation, la simulation, l’équivalence de traces, ou bien les distances qui s’adaptent au comportement probabiliste auquel nous nous intéressons. En effet, plutôt que de dire si oui ou non les deux systèmes à comparer sont « équivalents » une distance nous donne une valeur qui quantifie leur différence. Si la distance est 0 les deux systèmes sont équivalents. Il y a plusieurs notions de distances pour les systèmes probabilistes, le but de ce mémoire est de comparer trois d’entre elles : -distance, K-moment et Desharnais et al. Le principal résultat de cette comparaison est que les trois méthodes ont des résultats qui ne sont pas fondamentalement différents, bien qu’elles soient conçues de façon difficilement comparable. Il arrive souvent que les distances se suivent. Les principales différences se manifestent dans le temps de calcul, la capacité de traitement et l’atténuation du futur. Nous démontrons que les performances de chaque distance varient selon le type de système traité. Cela signifie que pour choisir la meilleure méthode, il faut déterminer le type de système que nous avons. En prenant par exemple un système dont nous n’avons pas le modèle, c’est la famille K-moment qui sera la seule capable de calculer une distance. Par ailleurs, nous avons pu intégrer dans la -distance un facteur qui atténue les différences les plus lointaines par rapport à celles plus proches. Cela nous a amené à définir une nouvelle distance : -distance atténuée.

Ce mémoire traite en premier lieu des avantages et des désavantages des différentes approches visant à assurer la sûreté et la sécurité des logiciels. En second lieu, il présente une nouvelle approche pour combiner l'analyse statique et l'analyse dynamique afin de produire une architecture de sécurité plus puissante. Les premiers chapitres du mémoire comportent une revue analytique des différentes approches statiques, dynamiques et hybrides qui peuvent être utilisées afin de sécuriser le code potentiellement malicieux. L'exposé identifie alors les avantages et les inconvénients de chaque approche ainsi que le champ des politiques de sécurité dans lesquels on peut l'appliquer. Le dernier chapitre traite de la possibilité de combiner l'analyse statique et l'analyse dynamique par une nouvelle approche hybride. Cette approche consiste à instrumenter le code seulement là où c'est nécessaire pour assurer satisfaire une politique de sécurité définie par l'usager et exprimée en un ensemble de propriétés exprimées μ-calcul modal. Cette instrumentation est guidée par une analyse statique effectuée à priori et basée sur un système de type à effets. Les effets représentent les accès aux ressources protégées du système. / The purpose of this thesis is twofold. In the first place it presents a comparative study of the advantages and drawbacks of several approaches to insure software safety and security. It then focuses more particularly on combining static analyses and dynamic monitoring in order to produce a more powerful security architecture. The first chapters of the thesis present an analytical review of the various static, dynamic and hybrid approaches that can be used to secure a potentially malicious code. The advantages and drawbacks of each approach are thereby analyzed and the field of security properties that can be enforced by using it are identified. The thesis then focuses on the possibility of combining static and dynamic analysis through a new hybrid approach. This approach consists in a code instrumentation, that only alters those parts of a program where it is necessary to do so to insure the respect of a user-defined security policy expressed in a set of modal μ-calculus properties. this instrumentation is guided by a static analysis based on a type and effect system. The effects represent the accesses made to pretested system ressources.

Ce mémoire présente une nouvelle approche pour sécuriser du code potentiellement malicieux à l'aide d'un moniteur incorporé au code. Les premiers chapitres du mémoire introduisent les notions préliminaires à la présentation de l'approche. Plus précisément, les concepts fondamentaux de la vérification de modèle et du contrôle des systèmes à événements discrets. Le dernier chapitre présente les fondements théoriques de l'approche en généralisant les résultats de Ligatti, Bauer et Walker, et montre une classe de moniteurs qui est plus puissante lorsqu'on précise son contexte d'application. Cette observation mène à l'élaboration d'une approche consistant à instrumenter un programme, dans le but de le rendre sécuritaire, à partir d'un modèle du programme et d'une propriété de sécurité représentée par un automate de Rabin.

Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2006-2007 / La vérification de modèle est une technique permettant de faire un modèle représentant le comportement d'un système ou d'un programme, de décrire une propriété à vérifier sur ce dernier et de faire la vérification au moyen d'un algorithme. Dans ce mémoire, nous décrivons notre propre méthode de vérification de modèle basée sur les algèbres de Kleene. Plus particulièrement, nous utilisons une extension appelée omégaalgèbre avec domaine. Cette méthode algébrique permet de vérifier des propriétés pouvant être exprimées au moyen de la logique CTL* basée sur les états et les actions du modèle à vérifier. Nous représentons ces propriétés au moyen d'expressions sur une oméga-algèbre avec domaine. / Les modèles que nous pouvons vérifier sont les systèmes à pile, une classe de systèmes de transitions pouvant avoir un nombre infini d'états. Les systèmes à pile peuvent représenter le flot de contrôle des programmes avec appels de procédures, incluant les appels récursifs. Des matrices sur une oméga-algèbre avec domaine sont utilisées pour représenter ces systèmes de transitions. Notre méthode génère, à partir de la matrice représentant le système à pile à vérifier et de l'expression représentant la propriété à vérifier sur ce dernier, une équation qu'il faut démontrer de façon axiomatique afin de conclure que le système satisfait la propriété.

L'analyse statique des programmes consiste en un ensemble de techniques permettant de déterminer des propriétés des programmes sans avoir à les exécuter. Parmi les applications de l'analyse statique des programmes, nous retrouvons l'optimisation du code source par des compilateurs et la détection de code malveillant ou de code qui pourrait être exploité à des fins malveillantes. L'évidente pertinence et l'importance (parfois critique) de telles applications expliquent les nombreuses tentatives de compréhension du cadre théorique général de l'analyse statique des programmes. Les algèbres de Kleene sont la théorie algébrique des automates finis et des expressions régulières. Cet outil algébrique s'est avéré très approprié pour l'analyse statique et la vérification des programmes. Le but de cette thèse est de développer un cadre algébrique basé sur les algèbres de Kleene pour calculer les solutions d'une classe générale de problèmes intraprocéduraux d'analyse de flot de données. Ce cadre permet de représenter les programmes, ainsi que leurs propriétés, d'une manière homogène, compacte et expressive. Les algorithmes traditionnels employés pour calculer le résultat d'une analyse sont alors remplacés par des manipulations algébriques des éléments d'une algèbre de Kleene. / Static program analysis consists of techniques for determining properties of programs without actually running them. Among the applications of static program analysis are the optimization by compilers of object code and the detection of malicious code or code that might be maliciously exploited. The obvious relevance and (sometimes critical) importance of such applications explain the many attempts to try to understand the general theoretical framework of static program analysis. Kleene algebra is the algebraic theory of finite automata and regular expressions. This algebraic tool has proven to be very suitable for the purpose of static analysis and verification of programs. The goal of this thesis is to develop an algebraic framework based on Kleene algebra to compute the solutions to a general class of intraprocedural dataflow analysis problems. The framework allows one to represent both the programs and the relevant properties in an homogeneous, compact and readable way. Traditional algorithms used to compute the result of an analysis are then replaced by algebraic manipulations of elements of a Kleene algebra.

Les systèmes informatiques occupent une place grandissante dans notre société actuelle hautement informatisée. À mesure que les systèmes transactionnels traditionnels sont informatisés, une composante de confidentialité vient s'ajouter aux systèmes informatiques. Ces systèmes gagnant en complexité, la vérification manuelle par des êtres humains devient rapidement impraticable. Nous présentons des methods traditionnelles de verification automatique de la conformité d'un programme à une propriété de sécurité. Ensuite, nous présentons une approche originale de Hugues Chabot et al. utilisant des omega-automates, qui permettent de verifier des programmes pour lesquels une execution peut ne jamais se terminer. Nous proposons quelques optimisations puis procédons a son implantation pour en mesurer la performance. Nous présentons finalement une approche alternative, base sur la théorie des transactions logicielles, qui permet de corriger un programme deviant plutôt que de le rejetter. Nous terminons en posant un regrard critique sur le travail accompli.

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

L'analyse statique des programmes permet d'étudier les comportements possibles des programmes sans les exécuter. Les analyseurs statiques sont employés par exemple pour garantir que l'exécution d'un programme ne peut pas produire d'erreurs. Ces outils d'analyse étant eux-mêmes des programmes, ils peuvent être incorrects. Pour accroître la confiance que l'on peut accorder aux résultats d'une telle analyse, nous étudions dans cette thèse comment on peut formellement établir la correction de l'implantation d'un tel analyseur statique. En particulier, nous construisons au moyen de l'assistant à la preuve Coq des interpréteurs abstraits et prouvons qu'ils sont corrects ; c'est-à-dire nous établissons formellement que le résultat de l'analyse d'un programme caractérise bien toutes les exécutions possibles de ce programme. Ces interpréteurs abstraits s'intègrent, dans la mesure du possible, au compilateur vérifié CompCert, ce qui permet de garantir que les propriétés de sûreté prouvées sur le code source d'un programme sont aussi valides pour la version compilée de ce programme. Nous nous concentrons sur l'analyse de programmes écrits dans des langages de bas niveau. C'est-à-dire des langages qui ne fournissent que peu d'abstractions (variables, fonctions, objets, types…) ou des abstractions que le programmeur a loisir de briser. Cela complexifie la tâche d'un analyseur qui ne peut pas s'appuyer sur ces abstractions pour être précis. Nous présentons notamment comment reconstruire automatiquement le graphe de flot de contrôle de programmes binaires auto-modifiants et comment prouver automatiquement qu'un programme écrit en C (où l'arithmétique de pointeurs est omniprésente) ne peut pas produire d'erreurs à l'exécution. / Static analysis of programs enables to study the possible behaviours of programs without running them. Static analysers may be used to guarantee that the execution of a program cannot result in a run-time error. Such analysis tools are themselves programs: they may have bugs. So as to increase the confidence in the results of an analysis, we study in this thesis how the implementation of static analysers can be formally proved correct. In particular, we build abstract interpreters within the Coq proof assistant and prove them correct. Namely, we formally establish that analysis results characterize all possible executions of the analysed program. Such abstract interpreters are integrated to the formally verified CompCert compiler, when relevant ; this enables to guarantee that safety properties that are proved on source code also hold for the corresponding compiled code. We focus on the analysis of programs written in low-level languages. Namely, languages which feature little or no abstractions (variables, functions, objects, types…) or abstractions that the programmer is allowed to break. This hampers the task of a static analyser which thus cannot rely on these abstractions to yield precise results. We discuss in particular how to automatically recover the control-flow graph of binary self-modifying programs, and how to automatically prove that a program written in C (in which pointer arithmetic is pervasive) cannot produce a run-time error.