Description
Date depot: 5 novembre 2020
Titre: Analyse statique par interprétation abstraite de smart contracts en Michelson
Directeur de thèse:
Antoine MINE (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé: 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. Commentaire sur le financement Le candidat est ingénieur en CDI dans l'entreprise Nomadic Lab. Une convention d'encadrement de thèse débutant au 1/10/2020 entre Sorbonne Université et Nomadic Lab est en cours de signature.
Doctorant.e: Bau Guillaume