Soutenance mémoire
Choix d’une approche sceptique
Mes travaux de thèse ont pour objectif de renforcer la confiance que l’on peut accorder aux transformations logiques. Nous nous intéressons aux transformations logiques des outils de vérification déductive, et nous appliquons notre méthode aux transformations logiques de Why3. L’intérêt que l’on porte à la correction de ces transformations s’explique par deux observations. D’une part les transformations logiques, nécessaires à chaque appel de prouveur automatique, sont omniprésentes dans les développements en Why3. D’autre part, leur implémentation comporte déjà plus de 17000 lignes de code OCaml, code qui est dans la base de confiance de Why3 et que nous souhaitons vérifier.
Mon approche est fondée sur l’utilisation de certificats vérifiables par une tierce partie, selon l’approche dénommée sceptique par Harrison [61]. L’idée est d’instrumenter le code des transformations afin qu’il génère un certificat de preuve, celui-ci permettant d’assurer a posteriori la correction de chaque exécution de l’outil. Ce certificat peut être vérifié par un outil externe qui, lui, peut avoir une base de confiance réduite. L’approche sceptique est particulièrement indiquée lorsque l’on souhaite instrumenter petit à petit le code à vérifier ou lorsque l’on veut pouvoir prouver plus de propriétés par la suite, comme par exemple dans les travaux sur SMTCoq [3,17]. Je mettrai donc l’accent sur l’aspect incrémental et modulaire de l’utilisation des certificats. On peut distinguer, au sein de l’approche sceptique, le travail de production de certificats du travail de vérification de ces certificats. Premièrement, celui qui instrumente la transformation doit expliciter, pour chaque cas d’application et sous la forme d’un certificat, la raison pour laquelle la transformation est correcte. Deuxièmement, la vérification de l’application d’une transformation peut s’appuyer sur un certificat, ce qui facilite grandement cette vérification. Similairement à l’approche FVDP de Boulmé [24], nous pouvons donc argumenter en faveur de la facilité de la vérification.
À l’inverse, une approche autarcique , selon la formulation de Barendregt et Barendsen [6], aurait cherché à prouver le code fourni. Par exemple, l’approche autarcique appliquée par Lescuyer à la vérification du prouveur Alt-Ergo [68] a mené à une version formalisée en Coq du noyau de ce prouveur. Cette approche permet de vérifier des propriétés du code autres que les propriétés fonctionnelles : il est par exemple possible de vérifier la terminaison ou de borner sa complexité. Un autre avantage est donné par le fait que la vérification d’une fonction est effectuée une fois lors de sa définition, et non à chacun de ses appels. Cette deuxième approche est cependant plus rigide car modifier le programme oblige également à adapter sa preuve de correction.
Faisons aussi la distinction entre les outils de vérification de programmes qui se fondent sur un assistant de preuve et ceux pour lesquels ce n’est pas le cas. Dans le premier cas, le langage de programmation et sa sémantique sont tous deux définis dans l’assistant de preuve considéré et le développement du langage se fait à travers l’implémentation de bibliothèques dédiées. C’est le cas notamment de la bibliothèque Iris [65] implémentée en Coq et développée pour la vérification de programmes impératifs et concurrents. Un autre exemple est donné par la bibliothèque AutoCorres [56, 57] qui permet de vérifier des programmes C en Isabelle. Dans ce contexte, la correction de la méthode repose sur la définition formelle de la sémantique des programmes et sur les règles de déduction qui doivent être établies une fois pour toutes. Cela demande de fournir un effort de preuve important, ce qui limite la flexibilité du langage. Dans le deuxième cas, la vérification ne s’appuie plus sur les prouveurs interactifs mais sur les tâches de preuve (aussi appelées obligations de preuve) dérivées à partir des annotations des programmes, et qui peuvent ensuite être validées par des prouveurs automatiques. Nous pouvons donner des exemples de tels outils de vérification de programmes en citant Why3 mais aussi Dafny [66], Viper [69], Frama-C [63], etc. Bien que la correction de ces outils repose sur des fondements théoriques solides, l’implémentation en elle-même de chacun d’entre eux, et en particulier l’encodage des tâches de preuve dansla logique des prouveurs automatiques appelés, n’est pas garantie. Une exception est donnée par F* [79], dont la correction de l’encodage dans la logique d’un prouveur SMT a été partiellement établie en Coq par Aguirre [2].
Encodage profond et encodage superficiel
Nous faisons mention, à divers endroits dans ce manuscrit, d’encodages profonds et d’encodages superficiels . En effet, au moment de vérifier nos certificats, nous avons le choix de l’outil de vérification que l’on utilise, de l’encodage des certificats dans cet outil et donc de la façon dont leur sémantique y est reflétée. D’un côté, l’encodage profond d’un langage (resp. d’une logique) Lsource dans un langage (resp. dans une logique) consiste à déclarer de nouveaux symboles dans Lcible permettant de traduire les symboles de Lsource, et à donner la sémantique de ces nouveaux symboles, par exemple à l’aide de nouveaux axiomes. Un encodage profond permet de raisonner sur Lsource vu comme des objets de Lcible. Par exemple, dans la lignée du compilateur certifié CompCert [67], Blazy [16] propose un encodage profond d’un sous-ensemble de C en Coq, ce qui permet d’énoncer et de prouver la correction de sa traduction vers un langage intermédiaire. D’un autre côté, l’encodage superficiel de Lsource dans Lcible consiste en une traduction syntaxique des symboles de Lsource comme une combinaison de symboles de Lcible . La sémantique de l’encodage de Lsource dans Lcible découle de la sémantique donnée à Lcible. De même, comme le remarque Cauderlier [26], les propriétés et les fonctionnalités de Lcible peuvent être directement mises à profit, facilitant ainsi les développements s’appuyant sur un encodage superficiel.
Dans cette thèse, nous utilisons les deux techniques d’encodage pour la vérification des certificats (chapitre 5). Nous avons également défini deux types de certificat, le premier étant encodé de manière superficielle dans le second (voir le 6.4), ceux-ci pouvant être encodés de manière profonde. Cela représente donc un moyen de combiner les deux types d’encodage en définissant des derived constructs comme le montre Svenningsson [78]. Par ailleurs, les certificats de surface font usage de la syntaxe abstraite d’ordre supérieur proposée par Pfenning [73] afin de réutiliser les lieurs du langage ambiant pour décrire ceux du langage que l’on définit. Puisque les autres constructions du langage sont définies de manière profonde, cela représente aussi un travail à mi-chemin entre l’encodage profond et l’encodage superficiel.
Contributions
Nous commençons, dans le chapitre 2, par définir le cadre logique dans lequel nous nous plaçons : les transformations logiques sont définies comme des fonctions partielles sur les tâches de preuve, elles-mêmes définies à partir de termes typés. Les transformations sont ensuite instrumentées, dans le chapitre 3, afin qu’elles renvoient un certificat à chacune de leurs applications. Le format de certificat choisi, celui des certificats de noyau, facilite la vérification et permet de certifier des transformations dans une logique d’ordre supérieur avec polymorphisme. Nous étendons notre formalisme dans le chapitre 4 en permettant l’ajout de théories interprétées telles que l’égalité et l’arithmétique entière. Nous expliquons au passage le mécanisme générique pour ajouter une théorie à notre formalisme. La vérification de certificats du chapitre 5 est modulaire. En effet, nous définissons deux vérificateurs. Le premier suit une approche calculatoire efficace de la vérification de certificats qui manipule l’encodage profond des tâches de preuve. Le second vérificateur se fonde sur un prouveur interactif dans lequel nous encodons notre formalisme de façon superficielle. Afin de simplifier l’instrumentation des transformations, nous définissons un deuxième format de certificat dans le chapitre 6, celui des certificats de surface. Ces derniers sont de plus haut niveau que les certificats de noyau, ce qui facilite leur génération et améliore leur modularité. Les certificats de surface sont traduits en des certificats de noyau avant leur vérification. Nous appliquons ensuite notre méthode aux transformations de Why3 dans le chapitre 7. Cela nécessite de traduire le formalisme de Why3 dans le nôtre. Nous donnons ensuite des garanties du bienfondé et de l’efficacité de notre méthode. En conclusion de cette thèse, dans le chapitre 8, nous rappelons nos contributions, nous les comparons avec des travaux connexes et nous donnons les améliorations que nous envisageons.
Cadre logique
Nous souhaitons décrire les transformations logiques, nous nous plaçons pour cela dans la logique d’ordre supérieur classique [10] à l’exception du fait que les types peuvent être polymorphes, la quantification de type étant en forme prénexe. Ce formalisme est suffisamment général pour permettre la certification des transformations logiques que nous considérons.
Dans ce chapitre, nous commençons, au paragraphe 2.1, par introduire les notations utilisées tout au long du manuscrit. Ces notations visent à faciliter l’écriture des termes et des tâches de preuve qui apparaissent à de nombreuses reprises. Nous explicitons ensuite, dans les paragraphes 2.2 à 2.4, la grammaire des termes, celle de leurs types et les substitutions que nous considérons. Cela nous permet, dans les paragraphes 2.5 à 2.7, d’expliciter le typage des termes, de définir les tâches de preuve et de leur donner une sémantique. Enfin, dans le paragraphe 2.8, nous donnons la définition des transformations logiques ainsi que celle de la correction de leurs applications.
Définition des tâches de preuve
Une tâche de preuve représente un séquent dans la logique d’ordre supérieur, nous explicitons la sémantique d’un tel séquent dans le paragraphe 2.7. Une tâche de preuve est donc un énoncé logique donné sous la forme de buts où il s’agit de prouver l’un d’entre eux à partir d’hypothèses, chaque but ou hypothèse étant une formule. Une déclaration de formule est une paire de la forme ’P : t’ où P est un identifiant et t est une formule. Les hypothèses et les buts forment des dictionnaires associant une formule à un identifiant, ce sont donc des ensembles de déclarations de formules. Une tâche de preuve regroupe une signature de type, une signature, des hypothèses et des buts.
Définition 2.21 (Tâche de preuve). Soit I une signature de type, Σ une signature, Γ et ∆ des ensembles de déclarations de formules. La tâche de preuve I | Σ | Γ ⊢ ∆ représente le séquent où il s’agit de prouver la disjonction des formules de ∆ à partir de la conjonction des formules de Γ dans la signature Σ et dans la signature de type I.
Sémantique des tâches de preuve
Nous définissons l’interprétation d’une signature de type, d’une signature et d’un ensemble de formules. Cela nous permet ensuite de définir la validité d’une tâche de preuve.
Notre formalisme s’inspire de THF0 [11], un langage pour la logique d’ordre supérieur, et de TFF1 [13], un langage pour la logique du premier ordre avec polymorphisme. En effet, nous nous plaçons dans une logique d’ordre supérieur classique où il est possible de définir des symboles de fonction polymorphes et des formules polymorphes. En revanche, dans un terme bien typé donné, on impose que les variables de terme qui sont liées soient monomorphes (condition V α (τ ) = ∅). Nous avons donc une hiérarchie de types implicite : les types monomorphes et, au-dessus, les types où les variables de type sont implicitement quantifiées universellement. Ainsi, notre formalisme, tel un système avec polymorphisme prédicatif [33], ne permet pas d’exprimer le paradoxe de Girard.
Notre formalisme peut aussi être vu comme une application du système STT∀ [81]. Au lieu de définir une logique minimale, nous cherchons à faciliter la définition de tâches de preuve, notamment en rendant accessibles les opérateurs propositionnels habituels et en étendant notre formalisme avec des théories interprétées (voir le chapitre 4). Une autre différence notable est que dans STT∀ la spécialisation des symboles polymorphes se fait par application à un type alors que cette application est implicite dans notre formalisme.
Notre sémantique cible est donc la sémantique standard de la logique d’ordre supérieur [10], où les fonctions peuvent également prendre des arguments de type. Les modèles considérés admettent l’extensionnalité de fonctions. De cette façon deux fonctions sont égales lorsqu’elles sont égales point à point. De même, les modèles admettent l’extensionnalité booléenne où l’on ne peut pas distinguer une formule vraie d’une autre. Il est donc possible de remplacer une formule par une formule équivalente.
Transformations logiques et correction
Correction d’une application d’une transformation logique
Définition 2.30 (Transformation logique). Une transformation logique est une fonction partielle qui prend une tâche en argument et renvoie une liste de tâches. On dit qu’une transformation logique s’applique à une tâche initiale et produit une liste de tâches résultantes. Informellement, la liste des tâches résultantes contient les tâches qu’il nous reste à valider pour nous assurer que la tâche initiale est valide. Nous n’avons plus d’autre preuve à faire lorsque la liste est vide, on dit dans ce cas que la transformation clôt la tâche initiale. Une transformation logique peut ne pas être définie sur une tâche initiale et ne pas renvoyer de tâches résultantes. Dans ce cas on dit que l’application de la transformation échoue. Cette application ne nous donne pas plus d’informations sur les conditions de validité de la tâche initiale et il ne faut pas confondre ce cas avec le cas où la liste de tâches résultantes est vide.
Définition 2.31 (Correction d’une application d’une transformation logique). Une application d’une transformation à une tâche initiale T est dite correcte si, lorsqu’elle produit la liste de tâches résultantes L (et donc lorsqu’elle n’échoue pas), alors la validité de toutes les tâches de L implique la validité de T.
Vérification de certificats
La vérification d’une application d’une transformation certifiante se fait à l’aide d’un vérificateur, procédure qui indique si la correction d’une application donnée est garantie.
La confiance apportée par cette approche (l’approche sceptique) peut être renforcée lorsque le vérificateur est lui-même formellement vérifié ou suffisamment réduit et simple pour que l’inspection de son code soit envisageable.
L’utilisation de certificats offre une grande flexibilité par rapport au code des transformations car ce code n’est pas directement lié à une preuve de sa correction et peut changer sans que cela ne requiert nécessairement de modifier également cette preuve. Par ailleurs, cette approche offre également une flexibilité au niveau de la vérification effectuée. En effet, les certificats sont à voir comme des indications pour la vérification d’une application d’une transformation, indication que les vérificateurs peuvent suivre de la manière qui leur convient. Nous utilisons à profit, dans ce chapitre, ce deuxième aspect de la flexibilité offerte par les certificats.
Nous commençons, dans le paragraphe 5.1, par donner le cadre général des vérificateurs puis nous expliquons comment ils s’intègrent à notre travail dans le paragraphe 5.2. Nous détaillons ensuite, dans les paragraphes 5.3 et 5.5, les deux vérificateurs que nous avons définis, le deuxième s’appuyant sur l’encodage présenté au paragraphe 5.4.
Approche calculatoire de la vérification de certificats
Le premier vérificateur proposé est implémenté en OCaml. Dans cette première approche, j’ai implémenté une version modifiée et exécutable du jugement T ↓ c sous la forme d’unefonction OCaml ccheck qui, à partir d’une tâche T et d’un certificat c, calcule une liste de tâches telle que la validité de toutes ces tâches implique la validité de la tâche initiale.
Une transformation certifiante produit un certificat, ce qui permet de vérifier son résultat.
Dans le cas du vérificateur en OCaml cette vérification se fait en appelant la fonction ccheckselon la figure 5.3, puis en vérifiant que la liste des tâches calculée est incluse dans à la liste des tâches résultantes.
Encodage superficiel dans un système de type pur
La deuxième approche de la réalisation d’un vérificateur vise à se passer d’une preuve formalisée d’un théorème de correction comme le théorème 5.5. Mon implémentation d’un telvérificateur utilise, en son cœur, le framework logique Lambdapi [4] avec un encodage d’un système de type pur [5, 35]. Par ailleurs, dans ce paragraphe, nous proposons un encodage superficiel de notre formalisme dans un système de type pur et nous montrons que, dans un tel système, nous avons besoin de toutes les quantifications qui caractérisent le Calcul des Constructions (CoC) [34]. Nous verrons dans le paragraphe 5.5 suivant comment nous définissons le plongement profond de CoC dans Lambdapi et comment nous pouvons le combiner avec l’encodage proposé ici afin de définir un vérificateur de certificats en Lambdapi.
|
Table des matières
1 Introduction
1.1 Méthodes formelles
1.1.1 Formules mathématiques et transformations logiques
1.1.2 Preuve formelle
1.2 Vérification de programmes
1.2.1 Vérification déductive
1.2.2 Présentation de Why3
1.3 Choix d’une approche sceptique
1.4 Encodage profond et encodage superficiel
1.5 Contributions
2 Cadre logique
2.1 Définitions générales et notations
2.2 Syntaxe des types
2.3 Syntaxe des termes
2.4 Substitutions
2.5 Typage des termes
2.6 Définition des tâches de preuve
2.7 Sémantique des tâches de preuve
2.8 Transformations logiques et correction
2.8.1 Correction d’une application d’une transformation logique
2.8.2 Discussion sur la correction des transformations
2.9 Conclusion
3 Certificats de noyau
3.1 Langage des certificats de noyau
3.2 Sémantique des certificats
3.2.1 Groupe identité et groupe structurel
3.2.2 Certificat pour la conversion
3.2.3 Groupe propositionnel
3.2.4 Certificats pour les quantificateurs
3.3 Notation et nommage des certificats
3.4 Correction des certificats
3.5 Expressivité des certificats
3.6 Transformations certifiantes
3.7 Limitations des certificats de noyau
3.8 Conclusion
4 Théories interprétées
4.1 Définition de nouvelles théories
4.1.1 Axiomatisation d’une théorie
4.1.2 Intérêt des théories interprétées
4.1.3 Ajustement de la notion de correction
4.1.4 Définition d’une théorie interprétée
4.2 Théorie de l’égalité polymorphe
4.3 Théorie de l’arithmétique entière des entiers relatifs
4.3.1 Transformations arithmétiques et conversions
4.3.2 Transformations d’induction sur les entiers relatifs
4.4 Théories interprétées et formalisme logique
5 Vérification de certificats
5.1 Cadre général des vérificateurs
5.2 Intégration des vérificateurs
5.3 Approche calculatoire de la vérification de certificats
5.3.1 Réalisation et correction de la fonction ccheck
5.3.2 Réécriture et certificat Conv en OCaml
5.3.3 Vers une preuve vérifiée par ordinateur
5.4 Encodage superficiel dans un système de type pur
5.4.1 Choix d’un système de type pur
5.4.2 Encodage dans le Calcul des Constructions
5.4.3 Incomplétude de la traduction vers CoC
5.5 Vérification par encodage dans le λΠ-calcul
5.5.1 Présentation de Lambdapi
5.5.2 Encodage du Calcul des Constructions dans Lambdapi
5.5.3 Encodage des tâches de preuve en Lambdapi
5.5.4 Traduction du certificat
5.5.4.1 Traduction des différents constructeurs de certificat
5.5.4.2 Traduction d’un certificat complet
5.5.4.3 Sémantique des certificats en Lambdapi
5.5.5 Théories interprétées en Lambdapi
5.5.5.1 Théorie de l’égalité polymorphe
5.5.5.2 Théorie des entiers relatifs
5.6 Certificats de noyau et vérificateurs
6 Certificats de surface
6.1 Définitions et notations
6.1.1 Nœuds de certificat de surface
6.1.1.1 Sémantique
6.1.1.2 Correction
6.1.2 Certificats de surface
6.1.2.1 Sémantique
6.1.2.2 Définition syntaxique
6.1.2.3 Correction
6.1.3 Notation
6.2 Abstraction dans les certificats
6.2.1 Abstraction des tâches
6.2.2 Composition des transformations
6.2.2.1 Composition de transformations logiques
6.2.2.2 Composition de certificats
6.2.2.3 Composition de transformations certifiantes
6.3 Réordonner et retirer des tâches résultantes
6.4 Élaboration de certificats
6.4.1 Abstraction des tâches
6.4.2 Retrouver les champs manquants des certificats
6.4.3 Distinguer les certificats de surface
6.4.4 Mécanisme générique pour créer de nouveaux certificats de surface
6.5 Résultats et applications des certificats de surface
7 Application aux transformations de Why3
7.1 Formalisme logique de Why3
7.1.1 Tâches et transformations en Why3
7.1.2 Traduction des tâches de Why3
7.1.2.1 Différence de syntaxe et de sémantique des tâches de preuve
7.1.2.2 Différences d’implémentation
7.2 Transformation rewrite
7.3 Transformation compute
7.4 Transformation blast
7.4.1 Élimination de l’implication et de l’équivalence
7.4.2 Élimination de la conjonction et de la disjonction
7.4.3 Traitement de la négation
7.4.4 Définition récursive de blast
7.4.5 Terminaison de blast
7.5 Transformation induction sur Z
7.6 Transformation split
7.6.1 Cas où la formule de départ est une négation
7.6.2 Cas où la formule de départ est une conjonction
7.7 Élimination du polymorphisme
7.7.1 Élimination du polymorphisme du but
7.7.2 Instanciation des déclarations polymorphes
7.7.3 Introduction et réécriture des symboles monomorphes
7.8 Implémentation et expérimentation
7.8.1 Validation de notre méthode
7.8.2 Implémentation
8 Conclusion
8.1 Vérification de certificats
8.2 Génération de certificats
8.3 Comparaison avec des travaux connexes
8.3.1 Identification du noyau d’un prouveur et approche autarcique
8.3.2 Définition de certificats dans les prouveurs automatiques
8.3.3 Vérification de certificats
8.3.4 Combiner la production et la vérification de certificats
8.4 Perspectives
Liste des symboles
Index
