Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

L’introduction des nouvelles technologies de l’information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu’ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d’un réseau d’interactions entre ces constituants qui peut être à l’origine de comportements néfastes et difficiles à prévoir. Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées « système », qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s’assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences « système » formulées par les utilisateurs. Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l’identification, la formalisation et la structuration d’exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d’une part, sur un raffinement prouvé (par theroem proving) des exigences « système » permettant d’établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d’autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques. / Introduction of new information and communication technology in automated systems leads to a growth of safety functions complexity. System properties are not limited to components properties, they issued from an interactions network that can introduces bad behaviour. Our conviction is that a safe development of such system must involve system oriented approaches in order to apprehend system global behaviour and architecture and more formal approaches allowing verifying that components properties satisfy end users system requirements We define a methodological approach based on SysML formalism (System Modelling Language) allowing global system requirements identification; formalisation and structuring in order to project these requirements on the system components architecture and so obtain local components properties. Then safety requirements verification is based in one hand on proved refinement (using theorem proving) of system requirements to components properties; and, in the other hand, on the formal verification (using model checking) of these components properties.

Cette thèse étudie des formalismes logiques exprimant des propriétés sur des programmes. L'intention originale de ces logiques est de vérifier formellement la correction de programmes manipulant des pointeurs. Dans l'ensemble, il ne sera pas proposé de méthode de vérification applicable dans cette thèse- nous donnons plutôt un éclairage nouveau sur la logique de séparation, une logique pour triplets de Hoare. Pour certains fragments essentiels de cette logique, la complexité et la décidabilité du problème de la satisfiabilité n'étaient pas connus avant ce travail. Aussi, sa combinaison avec certaines autres méthodes de vérification était peu étudiée. D'une part, dans ce travail nous isolons l'opérateur de la logique de séparation qui la rend indécidable. Nous décrivons le pouvoir expressif de cette logique, en la comparant à des logiques du second ordre. D'autre part, nous essayons d'étendre des fragments décidables de la logique de séparation avec la une logique temporelle et avec l'aptitude à décrire les données. Cela nous permet de donner des limites à l'utilisation de la logique de séparation. En particulier, nous donnons des limites à la création de logiques décidables utilisant ce formalisme combiné à une logique temporelle ou à l'aptitude à décrire les données. / This thesis studies logics which express properties on programs. These logics were originally intended for the formal verification of programs with pointers. Overall, no automated verification method will be proved tractable here- rather, we give a new insight on separation logic. The complexity and decidability of some essential fragments of this logic for Hoare triples were not known before this work. Also, its combination with some other verification methods was little studied. Firstly, in this work we isolate the operator of separation logic which makes it undecidable. We describe the expressive power of this logic, comparing it to second-order logics. Secondly, we try to extend decidable subsets of separation logic with a temporal logic, and with the ability to describe data. This allows us to give boundaries to the use of separation logic. In particular, we give boundaries to the creation of decidable logics using this logic combined with a temporal logic or with the ability to describe data.

Dans une infrastructure logicielle, les systèmes critiques ont souvent besoin de garder des clés cryptographiques sur des HSM ou des serveurs consacrés à la gestion de clés. Ils ont pour but de séparer les opérations cryptographiques, très critiques, du reste du réseau, qui est plus vulnérable. L'accès aux clés est fourni au travers des APIs de sécurité, comme par exemple le standard PKCS#11 de RSA, CCA d'IBM, ou encore l'API du TPM, qui ne permettent qu'un accès indirect aux clés. Cette thèse est composée de deux parties. La première introduit des méthodes formelles qui ont pour but l'identification des configurations dans lesquelles les APIs de sécurité peuvent améliorer le niveau de sûreté des protocoles existants, par exemple en cas de compromission d'un participant. Un paradigme prometteur considère les APIs de sécurité comme des participants d'un protocole afin d'étendre l'emploi des méthodes traditionnelles d'analyse de protocole à ces interfaces. À l'opposé des protocoles réseau, les APIs de sécurité utilisent souvent une base de données interne. Ces outils traditionnels d'analyse ne sont adaptés que pour le cas où le nombre des clés est borné a priori. Nous exposons également des arguments pour l'utilisation de la réécriture de multi-ensembles (MSR), lors de la vérification. De plus, nous proposons un langage dérivant du pi-calcul appliqué possédant des opérateurs qui permettent la manipulation d'un état explicite. Ce langage se traduit en règles MSR en préservant des propriétés de sécurité qui s'expriment dans une logique de premier ordre. La traduction a été implémentée sous forme d'un prototype produisant des règles spécifiquement adapté au prouveur tamarin. Plusieurs études de cas, dont un fragment de PKCS#11, le jeton d'authentification Yubikey, et un protocole de signature de contrat optimiste ont été effectuées. Le deuxième partie de la présente thèse a pour but l'identification des propriétés de sécurité qui a) peuvent être établies indépendamment du protocole b) permettent de trouver des failles au niveau de la cryptographie b) facilitent l'analyse des protocoles utilisant cette API de sécurité. Nous adoptons ici l'approche plus générale de Kremer et al. dans un cadre qui permet la composition universelle, à travers une fonctionnalité de gestion de clés. La nouveauté de ce genre de définition est qu'elle dépend des opérations mises à disposition par l'API. Ceci est seulement possible grâce à la composition universelle. Une API de sécurité n'est sûre que si elle réalise correctement la gestion des clés (selon la fonctionnalité présentée dans ce travail) et les opérations utilisant les clés (selon les fonctionalités qui les définissent). Pour finir, nous présentons aussi une implémentation de gestion de clés définie par rapport à des opérations arbitraires utilisant des clés non concernées par la gestion des clés. Cette réalisation représente ainsi un modèle générique pour le design des APIs de sécurité. / Security critical applications often store keys on dedicated HSM or key-management servers to separate highly sensitive cryptographic operations from more vulnerable parts of the network. Access to such devices is given to protocol parties by the means of Security APIs, e.g., the RSA PKCS#11 standard, IBM's CCA and the TPM API, all of which protect keys by providing an API that allows to address keys only indirectly. This thesis has two parts. The first part deals with formal methods that allow for the identification of secure configurations in which Security APIs improve the security of existing protocols, e.g., in scenarios where parties can be corrupted. A promising paradigm is to regard the Security API as a participant in a protocol and then use traditional protocol analysis techniques. But, in contrast to network protocols, Security APIs often rely on the state of an internal database. When it comes to an analysis of an unbounded number of keys, this is the reason why current tools for protocol analysis do not work well. We make a case for the use of MSR as the back-end for verification and propose a new process calculus, which is a variant of the applied pi calculus with constructs for manipulation of a global state. We show that this language can be translated to MSR rules while preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a back-end. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and a contract signing protocol. The second part of this thesis aims at identifying security properties that a) can be established independent of the protocol, b) allow to catch flaws on the cryptographic level, and c) facilitate the analysis of protocols using the Security API. We adapt the more general approach to API security of Kremer et.al. to a framework that allows for composition in form of a universally composable key-management functionality. The novelty, compared to other definitions, is that this functionality is parametric in the operations the Security API allows, which is only possible due to universal composability. A Security API is secure if it implements correctly both key-management (according to our functionality) and all operations that depend on keys (with respect to the functionalities defining those operations). We present an implementation which is defined with respect to arbitrary functionalities (for the operations that are not concerned with key-management), and hence represents a general design pattern for Security APIs.

La thèse étudie des problèmes de vérification de modèles infini, en appliquant des techniques de combinaisons de solveurs de contraintes.

A cause de la complexité croissante des systèmes sur puce (SoC), la vérification devient un aspect très important : 70 - 80% du coût de conception est alloué à cette tâche. Plus de 60% des projets de développement d'ASIC doivent être repris à cause des erreurs fonctionnelles, environ 50% des erreurs de conception étant situées au niveau du module. Dans le monde industriel, la vérification est souvent synonyme de simulation - une méthode de vérification naturelle pour les concepteurs, mais qui ne garantit pas l'absence d'erreurs. Une alternative est fournie par la vérification formelle qui prouve mathématiquement qu'un circuit satisfait une spécification. Dans cette thèse, on s'intéresse aux méthodes déductives basées sur la démonstration de théorèmes. La démonstration de théorèmes permet de vérifier formellement des descriptions matérielles de haut niveau et des systèmes réguliers ou très complexes, car la taille de données n'a plus d'importance. Par contre la modélisation de la description matérielle se fait directement en logique, ce qui rend l'accès difficile pour les concepteurs. Notre travail a pour but de faciliter l'introduction des outils de démonstration de théorèmes dans le flot de conception. Nous proposons une méthode automatique de traduction d'un circuit VHDL vers un modèle sémantique basé sur des équations récurrentes par rapport au temps qui peut être l'entrée de tout outil de démonstration de théorèmes et nous définissons une approche de vérification adaptée au modèle. Afin de valider notre proposition, nous avons choisi le démonstrateur ACL2 pour vérifier une bibliothèque de circuits de cryptographie.

Suivant les recommandations de l'ITRS 2003, il convient de s'intéresser aux circuits numériques asynchrones pour préparer l'avenir de la conception des circuits numériques. Sur le plan théorique, nous établissons le théorème de l'insensibilité aux délais des circuits numériques asynchrones. Pour spécifier un circuit numérique asynchrone par un programme faisant abstraction des délais, il faut et il suffit que le circuit vérifie trois propriétés fondamentales, que nous appelons propriétés d'insensibilité aux délais, i.e. persistance, sûreté et vivacité. Sur le plan pratique, nous choisissons le standard SystemC v2.0.1 de conception de systèmes numériques pour élaborer le premier modèle de circuits numériques asynchrones instrumenté pour la vérification des propriétés d'insensibilité aux délais, intégré dans un standard de conception de systèmes numériques. Nous mettons ce modèle en œuvre sur des exemples de taille réduite, mais significatifs, avant d'élargir la perspective.

Pour satisfaire la demande du marché actuel, plusieurs outils commerciaux de vérification formelle sont apparus ces dernières années. Le niveau le plus abstrait de description accepté dans la plupart de ces outils est le niveau appelé transfert de registres, c'est-à-dire une description avec des cycles d'horloge explicitement définis. Pour rester compétitifs, néanmoins, les concepteurs sont obligés d'élever le niveau d'abstraction et commencent à utiliser des outils de synthèse de haut niveau. Cette thèse a pour objet la vérification formelle des résultats de synthèse de haut niveau par rapport à la spécification initiale décrite en VHDL. Nous proposons une méthodologie de vérification qui épouse le flot de conception et consiste en la vérification de deux étapes principales:<br />l'ordonnancement et l'allocation. La vérification de chaque étape est fondée sur un modèle de machine abstraite que nous avons défini: contrairement au modèle de machine d'états finis classique, il réduit<br />considérablement l'espace d'états d'où les registres de la partie opérative sont exclus. En outre, la machine abstraite est similaire aux descriptions VHDL utilisées lors de la synthèse et offre, par conséquent, un niveau d'abstraction plus élevé de représentation des<br />circuits. La preuve d'équivalence entre la machine abstraite et la machine d'états finis classique justifie la première et constitue une des contributions théoriques de la thèse. Un prototype d'outil basé sur la simulation symbolique a été développé et exécuté sur des benchmarks de la synthèse comportementale. La thèse<br />s'achève sur les problèmes ouverts et les axes de recherche à explorer.

L'utilisation d'un outil d'aide à la correction peut contribuer à faciliter et à accélérer la correction de travaux pratiques de programmation. Au fil des ans, plusieurs logiciels ont été développés à cette fin, mais souffraient souvent d'un manque de flexibilité et étaient limités à un seul langage cible. Face à cette situation, l'outil Oto, développé à l'UQAM en langage Ruby, se voulait générique et extensible, pouvant théoriquement appliquer n'importe quel test à n'importe quel travail pratique. Toutefois, l'utilisation d'Oto en situation réelle a permis de constater que l'outil souffrait de certains défauts susceptibles de nuire à son utilisation à grande échelle, notamment en raison du manque de flexibilité de ses scripts de correction et de ses performances relativement faibles. Dans ce mémoire, nous présentons les modifications que nous avons apportées à Oto pour en améliorer la flexibilité et les performances. D'abord, nous avons analysé l'outil pour en comprendre le fonctionnement et en localiser les faiblesses, qui provenaient principalement de choix architecturaux de coordination des tâches de correction. Nous nous sommes ensuite attardés sur les caractéristiques et les capacités qui devraient être offertes par Oto. Notre solution est passée par le remplacement du mécanisme de scripts Oto par un langage spécifique au domaine de type interne (internal DSL) basé sur Ruby. Au meilleur de nos connaissances, nous sommes les premiers à avoir eu recours à une telle approche dans le cadre d'un outil d'aide à la correction. Les résultats que nous avons obtenus avec le DSL Oto sont venus confirmer une hausse considérable de la flexibilité et une amélioration des performances de l'outil, particulièrement pour les scripts de correction ayant recours à un nombre élevé de courts tests et aux corrections intra-groupes. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Programmation, Correction automatisée, Outils d'aide à la correction, Oto, Ruby, Langages spécifiques au domaine, DSL.