Direction de recherche : Antoine MINÉ

Analyse statique par interprétation abstraite de smart-contrats Michelson

Le but de cette thèse est de développer, prouver correct et implanter des nouvelles analyses statiques par interprétation abstraite pour vérifier les smart contracts écrits dans le langage Michelson et déployés sur la blockchain Tezos.
Tezos est une plateforme permettant de développer et déployer des blockchains. Une particularité de Tezos est le support pour un langage Turing-complet, Michelson, permettant d’écrire des smart contracts. L'application des méthodes formelles aux smart contracts est relativement récente, et la théorie de l’interprétation abstraite a été peu exploitée dans ce contexte. Pourtant, la montée en puissance des smart contracts et leur utilisation dans des domaines économiquement sensibles, comme l’automatisation des transactions financières, montre la grande utilité qu'auraient des outils de vérification automatique ayant des garanties formelles de correction.
Un premier travail consistera à développer une analyse statique inférant des invariants dans des programmes Michelson. Une propriété cible est l'inférence de bornes sûres des variables numériques, puisque le type des entiers est par défaut non-borné. Une deuxième cible, spécifique à Michelson, est l'inférence des clés utilisées dans les structures de table. Un deuxième travail, basé sur l'analyse d'invariants, consiste à développer une analyse de consommation de gaz, c'est à dire de coût. Cette analyse devra permettre de déterminer si un contrat respecte son budget en gaz, ainsi que d’optimiser ce budget pour réduire son coût économique. Au-delà des propriétés non-fonctionnelles développées dans les travaux ci-dessus, la thèse pourra considérer des propriétés fonctionnelles, c’est à dire liées à une spécification du contrat fournie par l'utilisateur. La suite de la thèse étendra certaines de ces analyses d'invariance, de coût ou de propriétés fonctionnelles pour tenir compte de l’état du store maintenu dans la blockchain. Le projet mêlera des aspects théoriques et fondamentaux ainsi que des aspects appliqués. Les méthodes développées devront être bien définies formellement, ainsi que prouvées correctes en utilisant le cadre théorique de l'interprétation abstraite. Elles devront être motivées par l’analyse de cas d’étude réels. Les méthodes feront l'objet d'une implantation logicielle, qui pourra s'intégrera à la plateforme ouverte Mopsa développée au LIP6.

Publications 2022

• 2022
  • G. Bau, A. Miné, V. Botbol, M. Bouaziz : “Abstract interpretation of Michelson smart-contracts”, SOAP '22: 11^th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, San Diego, CA, United States, pp. 36-43, (ACM) (2022)