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é.
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).
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.
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
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
