Garantir le fonctionnement correct des systèmes informatisés est un enjeu chaque jour plus important. La vérification formelle est un ensemble de techniquespermettant d’établir la correction d’un modèle mathématique du système par rapport à des propriétés exprimées dans un langage formel.Le "Regular model checking" est une technique bien connuede vérification de systèmes infinis. Elle manipule des ensembles infinis de configurations représentés de façon symbolique. Le "Regular model checking" de systèmes à canaux non fiables (LCS) soulève des questions fondamentales de décision et de complexité concernant l’ordre sous-mot qui modélise la perte de messages. Nous abordons ces questions et résolvons un problème ouvert sur l’index de la congruence de Simon pour les langages testables par morceaux.L’accessibilité pour les LCS est décidable mais de complexité F_{omega^omega} très élevée, bien au delà des complexités primitives récursives. Plusieurs problèmes de complexité équivalente ont été découverts récemment, par exemple dans la vérification de mémoire faibles ou de logique temporelle métrique. Le problème de plongement de Post (PEP) est une abstraction de l’accessibilité des LCS, lui aussi de complexité F_{omega^omega}, et qui nous sert de base dans la définition d’une classe de complexité correspondante. Nous proposons une généralisation commune aux deux variantes existantes de PEP et donnons une preuve de décidabilité simplifiée. Ceci permet d’étendre le modèle des systèmes à canaux unidirectionnels (UCS) par des tests simples tout en préservant la décidabilité de l’accessibilité. / The increasing use of software and automated systems has made it important to ensure their correct behaviour. Formal verification is the technique that establishes correctness of a system or a mathematical model of the system with respect to properties expressed in a formal language.Regular model checking is a common technique for verification of infinite-state systems - it represents infinite sets of configurations symbolically in a finite manner and manipulates them using these representations. Regular model checking for lossy channel systems brings up basic automata-theoretic questions concerning the subword relation on words which models the lossiness of the channels. We address these state complexity and decision problems, and also solve a long-standing problem involving the index of the Simon's piecewise-testability congruence.The reachability problem for lossy channel systems (LCS), though decidable, has very high F_{omega^omega} complexity, well beyond primitive-recursive. In recent times several problems with this complexity have been discovered, for example in the fields of verification of weak memory models and metric temporal logic. The Post Embedding Problem (PEP) is an algebraic abstraction of the reachability problem on LCS, with the same complexity, and is our champion for a "master" problem for the class F_{omega^omega}. We provide a common generalization of two known variants of PEP and give a simpler proof of decidability. This allows us to extend the unidirectional channel system (UCS) model with simple channel tests while having decidable reachability.

Cette these concerne la verification formelle et la composition de protocoles de securite, motivees en particulier par l'analyse des protocoles de vote electronique. Les chapitres 3 a 5 ont comme sujet la verification de protocoles de securite et le Chapitre 6 vise la composition.Nous montrons dans le Chapitre 3 comment reduire certains problemes d'une algebre quotient des termes a l'algebre libre des termes en utilisant des ensembles fortement complets de variants. Nous montrons que, si l'algebre quotient est donnee par un systeme de reecriture de termes convergent et optimalement reducteur (optimally reducing), alors des ensembles fortement complets de variants existent et sont finis et calculables.Dans le Chapitre 4, nous montrons que l'equivalence statique pour (des classes) de theories equationnelles, dont les theories sous-terme convergentes, la theorie de l'engagement a trappe (trapdoor commitment) et la theorie de signature en aveugle (blind signatures), est decidable en temps polynomial. Nous avons implemente de maniere efficace cette procedure.Dans le Chapitre 5, nous etendons la procedure de decision precedente a l'equivalence de traces. Nous utilisons des ensembles fortement complets de variants du Chapitre 3 pour reduire le probleme a l'algebre libre. Nous modelisons chaque trace du protocole comme une theorie de Horn et nous utilisons un raffinement de la resolution pour resoudre cette theorie. Meme si nous n'avons pas reussi a prouver que la procedure de resolution termine toujours, nous l'avons implementee et utilisee pour donner la premiere preuve automatique de l'anonymat dans le protocole de vote electronique FOO.Dans le Chapitre 6, nous etudions la composition de protocoles. Nous montrons que la composition de deux protocoles qui utilisent des primitives cryptographiques disjointes est sure s'ils ne revelent et ne reutilisent pas les secrets partages. Nous montrons qu'une forme d'etiquettage de protocoles est suffisante pour assurer la disjonction pour un ensemble fixe de primitives cryptographiques. / This thesis is about the formal verification and composition of security protocols, motivated by applications to electronic voting protocols. Chapters 3 to 5 concern the verification of security protocols while Chapter 6 concerns composition.We show in Chapter 3 how to reduce certain problems from a quotient term algebra to the free term algebra via the use of strongly complete sets of variants. We show that, when the quotient algebra is given by a convergent optimally reducing rewrite system, finite strongly complete sets of variants exist and are effectively computable.In Chapter 4, we show that static equivalence for (classes of) equational theories including subterm convergent equational theories, trapdoor commitment and blind signatures is decidable in polynomial time. We also provide an efficient implementation.In Chapter 5 we extend the previous decision procedure to handle trace equivalence. We use finite strongly complete sets of variants introduced in Chapter 3 to get rid of the equational theory and we model each protocol trace as a Horn theory which we solve using a refinement of resolution. Although we have not been able to prove that this procedure always terminates, we have implemented it and used it to provide the first automated proof of vote privacy of the FOO electronic voting protocol.In Chapter 6, we study composition of protocols. We show that two protocols that use arbitrary disjoint cryptographic primitives compose securely if they do not reveal or reuse any shared secret. We also show that a form of tagging is sufficient to provide disjointness in the case of a fixed set of cryptographic primitives.

Les multiprocesseurs et microprocesseurs multicœurs modernes mettent en oeuvre des modèles mémoires dits faibles ou relâchés, dans dans lesquels l'ordre apparent des opérations mémoire ne suit pas la cohérence séquentielle (SC) proposée par Leslie Lamport. Tout programme concurrent s'exécutant sur une telle architecture et conçu avec un modèle SC en tête risque de montrer à l'exécution de nouveaux comportements, dont certains sont potentiellement des comportements incorrects. Par exemple, un algorithme d'exclusion mutuelle correct avec une sémantique par entrelacement pourrait ne plus garantir l'exclusion mutuelle lorsqu'il est mis en oeuvre sur une architecture plus relâchée. Raisonner sur la sémantique de tels programmes s'avère très difficile. Par ailleurs, bon nombre d'algorithmes concurrents sont conçus pour fonctionner indépendamment du nombre de processus mis en oeuvre. On voudrait donc pouvoir s'assurer de la correction d'algorithmes concurrents, quel que soit le nombre de processus impliqués. Pour ce faire, on s'appuie sur le cadre du Model Checking Modulo Theories (MCMT), développé par Ghilardi et Ranise, qui permet la vérification de propriétés de sûreté de programmes concurrents paramétrés, c'est-à-dire mettant en oeuvre un nombre arbitraire de processus. On étend cette technologie avec une théorie permettant de raisonner sur des modèles mémoires faibles. Le résultat ce ces travaux est une extension du model checker Cubicle, appelée Cubicle-W, permettant de vérifier des propriétés de systèmes de transitions paramétrés s'exécutant sur un modèle mémoire faible similaire à TSO. / Modern multiprocessors and microprocesseurs implement weak or relaxed memory models, in which the apparent order of memory operation does not follow the sequential consistency (SC) proposed by Leslie Lamport. Any concurrent program running on such architecture and designed with an SC model in mind may exhibit new behaviors during its execution, some of which may potentially be incorrect. For instance, a mutual exclusion algorithm, correct under an interleaving semantics, may no longer guarantee mutual exclusion when implemented on a weaker architecture. Reasoning about the semantics of such programs is a difficult task. Moreover, most concurrent algorithms are designed for an arbitrary number of processus. We would like to ensure the correctness of concurrent algorithms, regardless of the number of processes involved. For this purpose, we rely on the Model Checking Modulo Theories (MCMT) framework, developed by Ghilardi and Ranise, which allows for the verification of safety properties of parameterized concurrent programs, that is to say, programs involving an arbitrary number of processes. We extend this technology with a theory for reasoning about weak memory models. The result of this work is an extension of the Cubicle model checker called Cubicle-W, which allows the verification of safety properties of parameterized transition systems running under a weak memory model similar to TSO.

À mesure que le nombre d’objets capables de communiquer croît, le besoin de sécuriser leurs interactions également. La conception des protocoles cryptographiques nécessaires pour cela est une tâche notoirement complexe et fréquemment sujette aux erreurs humaines. La vérification formelle de protocoles entend offrir des méthodes automatiques et exactes pour s’assurer de leur sécurité. Nous nous intéressons en particulier aux méthodes de vérification automatique des propriétés d’équivalence pour de tels protocoles dans le modèle symbolique et pour un nombre non borné de sessions. Les propriétés d’équivalences ont naturellement employées pour s’assurer, par exemple, de l’anonymat du vote électronique ou de la non-traçabilité des passeports électroniques. Parce que la vérification de propriétés d’équivalence est un problème complexe, nous proposons dans un premier temps deux méthodes pour en simplifier la vérification : tout d’abord une méthode pour supprimer l’utilisation des nonces dans un protocole tout en préservant la correction de la vérification automatique; puis nous démontrons un résultat de typage qui permet de restreindre l’espace de recherche d’attaques sans pour autant affecter le pouvoir de l’attaquant. Dans un second temps nous exposons trois classes de protocoles pour lesquelles la vérification de l’équivalence dans le modèle symbolique est décidable. Ces classes bénéficient des méthodes de simplification présentées plus tôt et permettent d’étudier automatiquement des protocoles taggués, avec ou sans nonces, ou encore des protocoles ping-pong. / As the number of devices able to communicate grows, so does the need to secure their interactions. The design of cryptographic protocols is a difficult task and prone to human errors. Formal verification of such protocols offers a way to automatically and exactly prove their security. In particular, we focus on automated verification methods to prove the equivalence of cryptographic protocols for a un-bounded number of sessions. This kind of property naturally arises when dealing with the anonymity of electronic votingor the untracability of electronic passports. Because the verification of equivalence properties is a complex issue, we first propose two methods to simplify it: first we design a transformation on protocols to delete any nonce while maintaining the soundness of equivalence checking; then we prove a typing result which decreases the search space for attacks without affecting the power of the attacker. Finally, we describe three classes of protocols for which equivalence is decidable in the symbolic model. These classes benefit from the simplification results stated earlier and enable us to automatically analyze tagged protocols with or without nonces, as well as ping-pong protocols.

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

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.

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.

Thèse en cotutelle Université Laval, Québec, Canada, Philosophiæ doctor (Ph. D.) et Ghent University, Gent, Belgique / Comment les fonctionnaires publics conçoivent-ils les mécanismes de mise en œuvre applicables aux accords multilatéraux sur l'environnement (AME) ? Depuis les années 1990, ces mécanismes sont progressivement devenus essentiels au fonctionnement d'un nombre important d'AME, servant d'alternative coopérative au règlement juridique des différends pour répondre à des cas potentiels de non-conformité avec les accords. La littérature dominante sur la conception des traités (treaty design) suggère que les États identifient rationnellement leurs préférences et négocient les dispositions des accords afin de maximiser leur utilité. Pourtant, la forme que revêtent les mécanismes de mise en œuvre dans les AME ne cadre pas avec cette proposition. Alors qu'une lecture rationnelle de leur conception voudrait que des circonstances de négociations similaires conduisent systématiquement à un mécanisme similaire, la conception des mécanismes de conformité dans les AME a plutôt convergé au fil du temps. Ma thèse vise à éclairer cette divergence entre les prédictions théoriques dominantes et la réalité empirique, en étudiant le processus par lequel les fonctionnaires conçoivent les mécanismes de mise en œuvre des AME. Je soutiens que les explications rationnelles de la conception des traités ont trois limites inhérentes : elles se focalisent sur les États en tant qu'acteurs principaux, elles étudient les résultats plutôt que les processus de conception, et elles sont limitées par leur postulat initial de rationalité. En réponse, je propose un nouveau cadre théorique qui articule comment les liens interpersonnels entre les fonctionnaires gouvernementaux influencent les résultats des négociations. Je suggère qu'au travers d'interactions répétées lors de réunions internationales, les fonctionnaires publics viennent à former une communauté transnationale de politiques qui s'articule autour de leur identité professionnelle partagée. Les membres de cette communauté partagent des normes, des récits, une connaissance mutuelle les uns des autres, et une certaine confiance. Je construis un mécanisme causal mixte qui conceptualise la conception des AME comme un processus partiellement rationnel, mais qui est également influencé par l'appartenance des fonctionnaires publics à une communauté. Je teste cette proposition grâce à une stratégie empirique en trois volets. Tout d'abord, je caractérise les résultats potentiels du mécanisme causal en explorant les formes que prennent les mécanismes de mise en œuvre dans un ensemble d'AME déjà en vigueur. Ensuite, grâce à un sondage auprès de 307 fonctionnaires, je vérifie que la condition initiale selon laquelle une communauté de fonctionnaires existe dans le domaine des AME est remplie. Finalement, je réalise une étude de cas de la Convention de Minamata sur le mercure. Grâce à des entretiens semi-structurés et à l'analyse de documents officiels de négociation, je retrace le processus par lequel les fonctionnaires publics ont sélectionné le mécanisme de mise en œuvre de la Convention. Cette thèse contribue à la littérature en élargissant le pouvoir explicatif des théories de conception rationnelle des traités. Elle propose d'ouvrir la « boîte noire » de l'État en tenant compte des liens interpersonnels entre les individus comme facteur influençant les décisions étatiques. Elle approfondit la compréhension du choix de dispositions des traités internationaux en construisant un mécanisme causal qui éclaire leur processus de négociation. Enfin, elle va au-delà de la rationalité en théorisant l'impact qu'ont les structures sociales sur la conception des traités. Dans l'ensemble, elle offre une analyse plus complète des processus de conception, qui explique ainsi une gamme étendue de résultats. En étudiant le processus par lequel les acteurs conçoivent les mécanismes de mise en œuvre des AME, j'entends offrir une nouvelle perspective sur la conception des traités au sens large, qui peut éventuellement être étendue à des cas similaires non seulement dans la sphère environnementale, mais aussi dans d'autres domaines. / How do public officials design compliance mechanisms in multilateral environmental agreements (MEAs)? Since the 1990s, such mechanisms have progressively become a staple in a large number of MEAs. They serve as a cooperative alternative to adversarial dispute settlement procedures, with the same overarching purpose of responding to suspected instances of non-compliance. Much of the literature on treaty design starts from the assumption that states rationally identify and bargain for the set of provisions that best serves their interests. Yet, the form that compliance mechanisms take in MEAs does not fit with this proposition: where the rational design literature would expect similar circumstances to lead to a similar, utility-maximizing design every time, the design of compliance mechanisms in MEAs has instead converged over time. My thesis aims to shed light on this divergence from theoretical expectations by studying the process through which public officials design compliance mechanisms. I argue that rational explanations of treaty design face three inherent limits: their focus on states as main actors, their focus on outcomes as opposed to processes, and their very assumption of rationality. In response, I introduce a theoretical framework that highlights how interpersonal ties between public officials influence negotiation outcomes. I suggest that, through repeated interactions at international meetings, public officials can come to form a transnational policy community centered around their shared professional identity. I expect members of this community to share norms, policy narratives, knowledge of one another, and trust. I build a mixed causal mechanism that conceptualizes treaty design as a process that is partially rational, but is also influenced by public officials' membership in a community. I test this proposition through a three-pronged empirical strategy. I first characterize the causal mechanism's potential outcomes, by exploring the forms that compliance mechanisms take in a set of existing MEAs. Through a survey of 307 public officials, I then verify that the initial condition that a community of public officials exists in the MEA sphere is met. Finally, I conduct a case study of the design of the Minamata Convention on Mercury. Based on semi-structured interviews and official negotiation documents, I trace the process through which public officials selected its compliance mechanism. This thesis contributes to the literature by extending rational design's explanatory power. It opens up the “black box” of the state by considering interpersonal ties between individuals. It deepens our understanding of design outcomes by building a causal mechanism that provides a plausible account of negotiation processes. Finally, it looks beyond rationality by theorizing the impact that social structures have on treaty design. All in all, this provides a fuller account of design processes that explains an extended array of outcomes. By studying the process through which actors design these mechanisms, I set out to gain new insights into treaty design more broadly, that can eventually be extended to similar cases both within and outside of the MEA sphere.

Titre de l'écran-titre (visionné le 5 septembre 2023) / Le mandat des institutions supérieures de contrôle (ISC) est d'assurer une saine gestion des finances publiques. Leurs activités d'audit exigent l'imputabilité (accountability) et la transparence de la part des agents publics. Le respect de ces deux valeurs de gestion publique participe à réduire un fléau d'envergure mondiale qu'est la corruption. La lutte contre la corruption est ancienne, et pourtant demeure un enjeu majeur de gouvernance. Diverses institutions publiques nationales et internationales travaillent à réduire ce fléau. L'implication des institutions supérieures de contrôle des finances publiques dans cette lutte est plutôt récente. Leur responsabilité en la matière n'est pas clairement définie, ni la façon dont elles doivent interagir avec les organisations qui les ont précédées dans ce combat, afin d'assurer un cadre efficace contre la corruption. Cette thèse se base sur la notion de « système national d'intégrité » de l'organisation Transparency International, place les ISC au centre du système, et contribue à l'avancement des connaissances en répondant à trois questions : 1) Au-delà des éléments généraux rapportés dans la littérature, quel est le rôle concret des ISC dans la lutte contre la corruption ? 2) Quels sont les principes à respecter dans les relations entre les ISC et les autres institutions de gouvernance pour renforcer leur efficacité en matière de lutte contre la corruption ? 3) Quel est l'impact d'un dispositif institutionnel anticorruption centré sur les ISC sur le niveau de perception de corruption ? Le chapitre premier présente une revue de littérature sur la corruption et le rôle des ISC pour la réduire. Les chapitres deuxième, troisième et quatrième mobilisent les méthodologies qualitatives et quantitatives pour répondre à chacune des trois questions de recherche. Chacun des chapitres est rédigé sous forme d'article. Pour la méthode qualitative, des entretiens semi-directifs ont été effectués avec treize membres d'ISC de France, du Sénégal et du Québec. Les analyses de régression ont été réalisées pour la méthode quantitative. Les résultats démontrent une implication effective des ISC dans le combat contre la corruption, même si ce rôle ne fait pas partie de leur mandat officiel. Ensuite, les principes devant gouverner les relations entre les ISC et les autres institutions publiques nécessitent des améliorations pour une lutte efficace contre la corruption. Ces améliorations sont notamment nécessaires au niveau de leur indépendance et de leur collaboration avec les acteurs sociaux. Enfin, la qualité d'un dispositif institutionnel anticorruption centré sur l'ISC démontre un effet réducteur sur le niveau de perception de la corruption. / The mandate of supreme audit institutions (SAIs) is to ensure sound management of public finances. Their audit activities require accountability and transparency from public officials. Respect of these two public management values contributes to reducing the global scourge that is corruption. The fight against corruption is old, yet it remains a major issue for governance. Various national and international public institutions are working to reduce this scourge. SAIs' involvement in this fight is rather recent. Their responsibility in this matter is not clearly defined, nor is the way in which they should interact with the organizations that preceded them in this fight, to ensure an effective framework against corruption. This thesis draws on Transparency International's concept of a "national integrity system", places SAIs at the center of the system, and contributes to the advancement of knowledge by answering three questions: 1) Beyond the general elements reported in the literature, what is SAIs' actual role in fighting corruption? 2) What principles should be observed in relations between SAIs and other governance institutions to enhance their effectiveness in the fight against corruption? 3) What is the impact of an institutional anticorruption system centered on SAIs on the perceived level of corruption? The first chapter presents a literature review on corruption and the role of SAIs in its fight. The second, third and fourth chapters mobilize qualitative and quantitative research methodologies to answer each of the three research questions. Each of these chapters is a manuscript article. For the qualitative analysis, semi-structured interviews were carried out with thirteen members of SAIs in France, Senegal, and Quebec. Regression analyses were performed for the quantitative method. The results demonstrate that involving SAIs in the fight against corruption is effective, even if this is not part of their official mandate. Also, principles that should govern the relations between SAIs and other public institutions must be improved to fight corruption more efficiently. These improvements are particularly necessary in terms of SAIs' independence and their collaboration with social actors. Finally, the quality of an institutional anticorruption system centered on SAIs demonstrates a reducing effect on the perceived level of corruption.