Tezos - Vérification formelle
Introduction
Cet article est une brève introduction à la vérification formelle dans le cadre de smart contract de la blockchain Tezos [11]. Cet article a pour but de donner un aperçu du concept de vérification formelle et de donner un exemple d’application à un smart contract.
Bien que la vérification formelle ait été utilisée depuis les années 1960 sur des industries “critiques” (aérospatial), il n’y a pas eu d’émergence sur les autres industries. Il a fallu attendre plusieurs décennies avant de voir apparaître l’utilisation de la vérification formelle dans le réseau ferroviaire, l’énergie ou la construction automobile.
Récemment, Tezos, une nouvelle blockchain de 3e génération, a été conçue pour permettre l’utilisation de la vérification formelle sur des “smart contracts”. Le but étant d'apporter de la confiance.
Durée de lecture
Temps de lecture: 30 min
Pré-requis
Pour une compréhension détaillée sur l’assistant de preuve Coq (en Annexe), il est recommandé d’avoir des notions de théorie de la preuve, et formalisme mathématique, ainsi que des notions de lambda-calcul.
Vérification formelle
Généralités
La vérification du bon comportement d’un programme est généralement effectuée par des tests, c’est-à-dire en exécutant une partie du code du programme dans un contexte bien spécifié. L'exhaustivité des tests apporte ainsi l’assurance du bon fonctionnement du programme.
Au lieu de vérifier tous les cas possibles d'exécution d’un programme, la démarche de la vérification formelle propose de vérifier sémantiquement l'exécution d’un programme et ainsi d’éviter l’écriture d’une multitude de tests. L’apport serait considérable car elle remplacerait la majorité des tests unitaires et scénarisés d’un programme. Par contre, l’écriture de la preuve (vérification sémantique) est un exercice plus complexe que celle d’un test.
Définition
La vérification formelle est l’utilisation de méthodes formelles (permettant un raisonnement logique/mathématique) dans le cadre de la vérification de la validité d’un programme. Il s’agit d’une analyse sémantique; c’est-à-dire la vérification de la cohérence d’un système de règle.
Pour s’assurer de cette cohérence, il faut prouver formellement (“mathématiquement”) que les règles sont vraies et qu’elles sont cohérentes entre elles.
Le raisonnement mathématique nécessaire à la preuve de théorèmes peut être assisté de logiciels d'assistants de preuve.
Démarche
Pour pouvoir appliquer une analyse formelle sur un programme, on peut suivre la démarche suivante :
On écrit un programme dans un langage Turing-complet [12].
L’isomorphisme Curry-Howard [7] permet de transformer un programme (turing-complet) en une expression formelle équivalente à son exécution. (rappel: un isomorphisme est une transformation de structure qui peut être réversible).
En s’appuyant sur l’isomorphisme Curry-Howard qui assure la correspondance entre un programme et une modélisation formelle (théorème), on peut écrire un théorème équivalent à notre smart contract.
Ainsi, l’énoncé du théorème est la traduction du programme en langage formel.
On démontre la véracité du théorème (prouve le théorème) ce qui implique que le programme fait effectivement ce qui est demandé.
Assistant de preuve
La création d’outil permettant de faire des preuves a été et est toujours un sujet de recherche en informatique. Beaucoup de projets ont été lancés pour formaliser les mathématiques, en 1966, le projet Automath aux Pays-bas, puis le projet Mizar en Pologne, HOL (Grande-bretagne), Isabelle (USA), Matita en (Italie) et le projet Coq en France.
Par exemple, l’utilisation d’assistant de preuve a permis de démontrer des théorèmes mathématiques :
- Le théorème des quatre couleurs, en 2005 ;
- la conjecture de Kepler, proposée en 1998, et finalement certifiée le 10 août 2014
- le théorème de Feit-Thompson, un théorème important de la théorie des groupes, en 20127.
Coq
Développé par l’INRIA, Coq [2] est un moteur de preuve formelle; c’est-à-dire un logiciel permettant l'écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques.
Initialement développé par Thierry Coquand, le calcul des constructions [13] (CoC de l'anglais Calculus Of Constructions) est un lambda-calcul (un système formel) typé d'ordre supérieur. Le CoC est utilisé comme langage typé de programmation. Plusieurs variantes de CoC ont été créées pour pouvoir gérer les type de données inductives, co-inductives et prédicats.
Le calcul des constructions inductives (CiC de l’anglais Calculus of Inductive Constructions) est une extension du CoC qui intègre des types de données inductives.
L’assistant de preuve Coq est construit à partir de CiC.
Les objets logiques (théorème, axiome) sont écrits en langage Gallina (Term) qui suit les principes du Cic. Les scripts de preuve sont écrits en langage Gallina (Vernaculaire) qui fournit les tactics. Ces script de preuve sont exécutés par le moteur d’inférence (Coq).
Pour plus d’information sur Coc ou Cic, il est conseillé de consulter les références [13][16]. Il est nécessaire de connaître le lambda-calcul [17] pour comprendre les notations mathématiques utilisées dans CoC ou Cic.
Pour plus d’information sur Gallina, le langage de définition de théorème et le langage de tactics pour la résolution de preuve, il est conseillé de consulter l’Annexe à la fin de l’article.
Tezos & Mi-cho-coq
Généralités
La blockchain Tezos apporte plusieurs innovations notamment en rendant possible de la vérification formelle. La blockchain Tezos utilise un langage de smart contract (Michelson) qui a été formellement prouvé. Cette preuve du langage Michelson est une librairie appelée Mi-cho-coq.
En s’appuyant sur l’isomorphisme Curry-Howard [5], qui assure la correspondance entre un programme et un théorème), on peut traduire un script Michelson en une forme logique équivalente (un théorème).
La vérification sémantique d’un smart contract se fait en démontrant ce théorème, c’est-à-dire en fournissant une preuve formelle pour ce théorème.
Michelson
Dans la blockchain Tezos, le langage de smart contract est le Michelson [9]. Ce langage est basé sur une pile (stack), est fortement typé et turing-complet.
Une petite introduction à l'écosystème de Tezos et Michelson est disponible ici sur le blog d’Octo.
Mi-cho-coq
Mi-cho-coq [8] est la spécification du langage Michelson en Coq pour prouver des propriétés de smart contract. Concrètement c’est une librairie de preuve des instructions du langage Michelson, (codée en Cic pour l’assistant de preuve Coq) permettant la vérification formelle sur des smart contract Tezos.
Une section à la fin de l’article fournit plus de détail à propos de l’assistant de preuve Coq, son langage (Gallina) de définition de théorème Cic, et des tactics du Vernaculaire pour la preuve.
Démarche
Pour valider un smart contract écrit en Michelson, il faut s’assurer que le code du smart contract fait effectivement ce qui est demandé. Ceci est fait en formulant un théorème et en fournissant une démonstration pour ce théorème.
La prochaine section “Exemple” détaillera la formalisation du théorème (ici). La section Vernacular détaille les Tactics utilisables (ici).
Cette démonstration est vérifiée par Coq (le moteur d’inférence) en s’appuyant sur mi-cho-coq et l’univers de Coq (définition de domaines et théorèmes associés).
La validation du théorème équivaut à la vérification formelle, c’est-à-dire la vérification sémantique que le code du smart contract fait ce qui est demandé.
Démarche de vérification formelle pour un smart contract Michelson
Exemple (de modélisation en théorème)
Voici un exemple de modélisation en théorème pour un smart contract de vote. Nous allons voir comment un code de smart contract Tezos est traduit en théorème mathématique dans coq.
Le code de preuve formelle pour notre smart contract consiste en 2 scripts Coq qui ont pour but d’énoncer un théorème équivalent à l’exécution du code du smart contract et de prouver ce théorème. Ces scripts Coq sont écrits en Gallina - Calculus of Inductive Constructions pour la définition du théorème et en Gallina - Vernaculaire pour la preuve.
Script Michelson (le code du smart contract)
Voici le code du smart contract de vote. Vous pouvez remarquer que ce script contient :
- la définition du type de paramètre,
- la définition du type de storage,
- les instructions à exécuter lors de l’invocation de l’entrypoint vote
Rappel sur le smart contract
Pour rappel, un smart contract est un ensemble de définition de structures de données et d’instructions. En d’autres termes, c’est la définition et l’implémentation d’un service décentralisé. Il définit quelles parties du code peuvent être appelées (appelés “entry point”) et comment exécuter ces entrypoints (quels sont les paramètres). Une fois enregistré (“déployé”) sur une blockchain, un smart contract peut être invoqué. L’invocation d’un smart contract nécessite de connaître l’adresse du contrat ainsi que de spécifier un entrypoint et ses paramètres. Comme par exemple, la 1ere ligne de code ci-dessus.
Le storage est un espace persistant (dans le ledger) associé à un smart contract. Le smart contract se doit de définir la structure de données qui lui est associé. Comme par exemple, la 2e ligne de code ci-dessus.
La 3e ligne de code débute la définition de la séquence d’instructions michelson (avec le mot clé code). Comme vous pouvez le remarquer, il s’agit d’un langage à pile.
Rappel sur l’invocation d’un smart contract
Rappelons que dans la blockchain Tezos, et plus particulièrement, les entrypoints d’un smart contract Tezos ont pour rôle de modifier le storage associé au smart contract. Pour rappel, le storage d’un smart contract est une zone mémoire persistante associée à un smart contrat contenant donc toutes les informations liées à un contrat. L’invocation d’un smart contract déclenche l’exécution d’un entrypoint du smart contract. Lors de l’exécution d’un entrypoint, la VM prend en paramètre l’état actuel du storage, exécute les instructions Michelson du smart contract et produit un nouvel état du storage (et une liste d’opération).
Exécution d'un entry point de smart contrat
Définition logique du smart contract
Mi-cho-coq (qui contient la spécification coq du Michelson) fournit la correspondance entre une instruction Michelson et une proposition logique équivalente. Il est donc possible de produire une “définition” en Cic du script Michelson.
On peut remarquer les annotations qui permettent de typer les différentes propositions logiques (en Cic , tous les terms sont typés).
Par exemple, on peut voir par comparaison avec le code Michelson que l’instruction GET est annotée de (i := get_map string int).
Définition logique des conditions de validation du smart contract
Il est possible de définir une proposition logique représentant des conditions à vérifier sur les propriétés d’un smart contrat (de son storage).
Le schéma ci-dessous montre comment on peut former des conditions logiques par rapport à des propriétés/paramètres du smart contract.
Conditions logiques de validation de l’exécution d'un smart contract
La condition B s’écrit :
La condition A & C s’écrit :
La condition D s’écrit :
La condition E s’écrit :
Le code ci-dessous exprime ces conditions logiques en fonction de:
- storage initial
- storage final
- le paramètre d’invocation
- la liste d’opérations générées.
Définition logique du théorème
Il s’agit d’exprimer “l’exécution du smart contract “ comme un théorème (une expression logique).
Comme on peut le voir la proposition logique est une équivalence entre l’exécution du smart contract et les conditions logiques de validation (vue dans la section précédente).
Il faut comprendre ce théorème comme une proposition logique:
l’exécution du smart contract est équivalente à la vérification des conditions logiques
Illustration du théorème
Preuve du théorème
En utilisant des Tactics (du Vernacular de Gallina), il est possible de démontrer le théorème. Pour faire avancer la preuve, il faut décomposer le problème en sous propositions logiques qui seront plus simples à prouver séparément.
Ce script de preuve s’appuie sur:
- les commandes du Vernacular de Gallina,
- des types induits et des théorèmes (prouvés) de mi-cho-coq concernant les propriétés liées aux contrat Tezos (fuel, par exemple)
- L’univers de coq qui définit les domaines/ensembles des nombres et divers théorèmes associés. Par exemple, l’ensemble des entiers naturels est défini sur l’arithmétique de Peano [12].
Pour comprendre comment faire une preuve comme celle-ci, il faudrait un article complet sur Coq. Heureusement pour les plus curieux d’entre vous, il existe un livre : le Coq’Art [15].
Plus d’informations sur les Tactics sont présentes dans la partie Annexe (Vernaculaire).
Conclusion
La vérification formelle apporte une vraie confiance dans le code et cette confiance est essentielle en matière de smart contract sur des blockchains publiques.
La vérification formelle apporte un côté "exhaustif" en terme de tests en comparaison aux tests unitaires.
La suite de nos investigations sur le sujet de la vérification formelle dans les blockchain mérite un deuxième article pour creuser un peu plus la preuve et décrire plus en détail le Vernacular de Gallina.
Plus d’informations sur l’assistant de preuve Coq et du langage Gallina sont présentes dans la partie Annexe.
Référence
[1] Calculus of Inductive Constructions - https://coq.inria.fr/distrib/current/refman/language/cic.html
[2] Coq - https://coq.inria.fr/distrib/current/refman/index.html
[3] Introduction to Coq - http://www-sop.inria.fr/members/Yves.Bertot/courses/introcoq.pdf
[4] Gallina - https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html
[5] Lambda-Calculus and Isomorphism Curry-Howard - http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
[6] Isomorphism Curry-Howard for Dummies - https://www.pédrot.fr/slides/inria-junior-02-15.pdf
[7] Isomorphism Curry-Howard (small) - https://www.seas.harvard.edu/courses/cs152/2015sp/lectures/lec15-curryhoward.pdf
[8] Mi-cho-coq repository - https://gitlab.com/nomadic-labs/mi-cho-coq
[9] Michelson - https://www.michelson-lang.com/why-michelson.html
[10] Logique formelle - https://www.irif.fr/~roziere/2ord/2ndordre.pdf
[11] Tezos ecosystem - https://blog.octo.com/tezos-ecosystem-october-2019/
[12] Axomes de Peano - https://fr.wikipedia.org/wiki/Axiomes_de_Peano
[13] Calculus of constructions - https://fr.wikipedia.org/wiki/Calcul_des_constructions
[14] Mini-guide Coq - https://www.lri.fr/~paulin/MathInfo/coq-survey.pdf
[15] Coq’Art - https://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf
[16] The calculus of constructions (1988) by Thierry Coquand - https://www.sciencedirect.com/science/article/pii/0890540188900053
[17] Lambda-calcul - https://fr.wikipedia.org/wiki/Lambda-calcul
Annexe:
Gallina - Terms et Vernaculaire
Le langage de spécification de Coq est Gallina [4]. Il permet de développer des théories mathématiques sur le paradigm du Cic (Calculus of Inductive Constructions), et de prouver des théorèmes sur celles-ci. Les théories sont construites à partir d’hypothèses, d'axiomes, de lemmes, ... . Ce langage permet de modéliser ces objets logiques (Terms) et fournit des commandes permettant de prouver des propositions logiques (Vernaculaire).
À des fins d’illustration, la section “Terms” de l’article donne un aperçu de la syntaxe et des règles pour définir des objets logiques ( mais ne rentrera pas dans le détail ni du langage Gallina, ni comment construire des théories).
Et enfin, la section “Vernaculaire” de l’article donne un aperçu des Tactics et un exemple de preuve.
Terms
Les Terms ou objets logiques (hypothèses, axiome, lemme, définition de type induit, ...) permettent de construire des théories.
Toutes les expressions en Cic sont des terms et les terms sont typés. Il existe des types pour :
- les function (ou programmes),
- les types de données,
- les preuves
- les types eux-mêmes (méta-type)
Les Terms sont construits à partir de propositions (sorts), variables, constantes, abstractions, applications, définitions locales, de produits (“forall”).
Règle de typage
Les terms sont soumis au typage qui dépend d’un environnement global et d’un contexte local. Un contexte local est une liste ordonnée de déclarations locales de noms (appelées variables). Un environnement global est une liste ordonnée d’assomptions globales ou de définitions globales ou déclaration de type induits.
Cic permet également de définir des assomptions c’est-à-dire étendre l'environnement avec des axiomes, paramètres, hypothèses, variables
Définition
Cic permet également d’étendre l'environnement en associant des noms aux Terms.
Définition de types induits
Cic permet d’étendre l'environnement en définissant des définitions inductives. Formellement, on représente une définition inductive par la relation
Ind [p] (Ri := Rc)
ou:
- Ri représente les noms et types des types induits
- Rc représente les noms et types des constructeurs des types induits
- p représente le nombre de paramètres des types induits
Exemple de définition de type induit pour une liste paramétrée.
Exemple de définition de type induit pour la distinction des nombres pairs et impairs.
Fixpoint
Cette commande permet d’appliquer du pattern matching sur des objets induits.
Exemple de définition d’un fixpoint pour l’addition
Axiome
Exemple de définition d’axiome
Theorem
On déclare les théorèmes de la même manière que les axiomes, mais il faut en fournir la preuve
Règle de conversion
Cic intègre un mécanisme interne de réduction permettant de décider si deux programmes sont “intentionnellement” (ou sémantiquement) équivalents. Plusieurs réductions sont possibles :
- β-reduction (il s’agit de la fermeture réflexive symétrique et transitive)
- ι-reduction (Coq permet d’associer d’une règle de conversion à un objet inductif)
- δ-reduction
- ζ-reduction (Coq permet de supprimer des définitions locales d’un term en remplaçant la variable par sa valeur)
- η-expansion
Vernacular
Le vernaculaire est le langage de commande de Gallina. Ces commandes (ou tactiques) manipulent des Terms qui doivent être bien typés.
Exemple de preuve
Voici un exemple de définition d’une proposition et de preuve utilisant des Tactics.
Dans cet exemple, un lemme définit la règle vérifiant si une fonction est injective. Rappel de la définition formelle de l’injectivité:
Une application f : X → Y est injective si pour tout y ∈ Y, il existe au plus un x ∈ X tel que f(x) = y, ce qui s'écrit :
Le but est défini sous la forme d’un lemme en utilisant le mot clé Lemma.
La preuve du lemme est fournie entre les terms Proof et Qed.
Assertions and proofs
Une assertion postule une proposition dont la preuve est interactivement construite en utilisant des Tactics.
Lors de la preuve, l'exécution de tactiques permet d’introduire (d’ajouter) des variables, hypothèses mais aussi d’éliminer des quantifieurs ∀, ∃, et implications. Voici un petit pense-bête de tactiques à appliquer en fonction de la proposition que l’on souhaite introduire ou éliminer.
Tactics
Cet ensemble de tactiques (outil de démonstration) permettant de construire une preuve incrémentalement. La proposition à démontrer (appelé but) pourra être décomposé en sous but , chacun prouvable grâce à ces tactiques. Cette liste n’est pas exhaustive mais peut donner une idée des concepts manipulés par Coq.
Intro: permet de spécifier le nom à assigner aux variables et hypothèses introduites par une tactique.
assumption: Cette tactique correspond à la règle axiome de la déduction naturelle. On peut donc l’utiliser pour finir la preuve quand la conclusion du but courant se trouve dans les hypothèses.
intros: spécifie une ou plusieurs variables ou hypothèses à partir du but. Par exemple, considérons le but: ∀x, p(x)⇒∃y, p(y), (en français: pour tout entier “x”, “p” de “x” implique qu’il existe un entier “y” tel que “p” de “y”), la commande intros va créer une hypothèse et une variable.
revert: bouge une hypothèse (potentiellement définie) dans le but (si les dépendances sont respectées). Cette tactique est l’inverse de intro.
exists : Pour prouver une formule quantifiée existentiellement comme exists y:nat, p y, l’utilisateur doit fournir à Coq à la fois le témoin et la preuve que ce témoin vérifie le prédicat p (ce qui correspond à la règle d’introduction de ∃). La tactique exists permet de faire cela.
move {id1} after {h2}: cette tactique bouge une hypothèse nommée {id1} dans le contexte local après l’hypothèse nommée {h2}
set ({ident} := {term}) : remplace {term} par {ident} dans la conclusion du but courant et ajoute la nouvelle définition dans contexte local.
destruct: Cette tactique permet d’éliminer des conjonctions, disjonctions, négations, contradictions et existentiels en hypothèse. Dans le cas d’une disjonction, on obtient deux sous-but.
injection: Cette tactique exploite la propriété que les constructeurs de type induits sont injectifs. C’est-à-dire , si on considère c un constructeur d’un type induit,
c(t1) = c(t2) ⇒ t1 = t2
apply: Cette tactique permet d’utiliser une formule que l’on a en hypothèse.