Méthodes formelles, Vérification de modèles, Démonstration automatique de théorèmes, Systèmes distribués, Blockchain, Smart contracts, Cross-Chain swap, Why3, Tla+

Une blockchain est un système distribué qui permet de stocker des données ne pouvant être ni modifiées ni supprimées. Les applications blockchain sont très complexes, car elles se constituent de plusieurs programmes, souvent tous liés les uns aux autres. Une caractéristique qui a suscité un fort intérêt pour les blockchains est la possibilité d'écrire des smart contracts. Ces derniers sont des programmes dans lesquels des règles de transaction peuvent être définies, révolutionnant ainsi l'utilisation de la blockchain. Cependant, l'utilisation croissante de la blockchain a fait émerger les limites de cette technologie. En effet, l'augmentation du nombre de blockchains, a fait naître auprès des utilisateurs l'envie d'échanger avec d'autres utilisateurs n'étant pas sur la même blockchain qu'eux. Pour répondre à ce cas d'utilisation, les applications appelées Cross-Chain Swap ont été développées. Leur but est d'échanger des biens entre différents utilisateurs se trouvant sur différentes blockchains. Ces applications sont souvent basées sur l'utilisation des smart contracts pour établir les règles de transfert. Bien qu'étant une technologie qui se popularise, la blockchain souffre d'un manque de formalisme de ses systèmes tels que les langages de smart contract. Par exemple, le langage Solidity possède une sémantique non-formelle, rendant les smart contracts rédigés dans ce langage vulnérable aux attaques. De plus, la blockchain souffre également de la présence de participants malveillants, appelés Byzantins. Ces participants ont un comportement aléatoire, et sont susceptibles de ne pas suivre les règles du système. Ainsi, les systèmes, comme les Cross-Chain Swap, ont nécessairement besoin d'employer des moyens pour assurer leur bon fonctionnement malgré la présence de Byzantins. Un moyen d'y parvenir est l'utilisation des méthodes formelles. Ces techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique, afin de démontrer leur validité par rapport à une certaine spécification. Dans cette thèse, nous proposons d'appliquer ces méthodes de vérification aux systèmes que nous avons cités, à savoir les smart contracts et les applications Cross-Chain Swap. Dans un premier temps, nous proposons le langage WhyML, dédié à la vérification formelle de programme, comme langage d'écriture de smart contract. Le langage WhyML, se base sur de la logique mathématique pour prouver l'exactitude du programme. L'approche est de définir un smart contract sous forme de formules mathématiques et ensuite d'appliquer des outils qui permettent de prouver que les formules sont vraies. En appliquant cette approche, on s'assure de la correction des contracts avant leur stockage dans la blockchain. Les résultats obtenus à l'issue de cette première étude ont montré que WhyML convenait comme langage d'écriture de smart contracts, permettant ainsi d'avoir des programmes correct par construction. Dans un second temps, nous appliquons des méthodes de formalisme à des applications Cross-Chain Swap. La première étape de cette formalisation est de définir une spécification formelle du problème des Cross-Chain Swap. L'approche consiste à définir les propriétés qui caractérisent la spécification du problème, par exemple, la spécification se doit d'être résiliente aux participants Byzantins. La seconde étape est la construction d'un algorithme qui satisfait la spécification du Cross-Chain Swap. Une fois ces deux étapes accomplies, nous appliquons des méthodes formelles à l'algorithme pour prouver sa correction. Pour cette approche, nous avons modélisé notre algorithme en TLA+ qui est un langage spécifique pour modéliser des systèmes distribués. Nous avons ensuite vérifié si le modèle obtenu satisfait bien les propriétés du problème étudié. Les résultats obtenus ont montré que l'algorithme que nous avons construit satisfaisait bien les propriétés de la spécification du Cross-Chain Swap.