LIP6 CNRS Sorbonne Université
Direct Link LIP6 » News » PhD students

BAU Guillaume

PhD student
Team : APR
Arrival date : 12/01/2020
Localisation : Campus Pierre et Marie Curie
    Sorbonne Université - LIP6
    Boîte courrier 169
    Couloir 25-26, Étage 3, Bureau 303
    4 place Jussieu
    75252 PARIS CEDEX 05
    FRANCE
Tel: +33 1 44 27 88 16, Guillaume.Bau (at) nulllip6.fr

Supervision : 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.

 Mentions légales
Site map |