Introduction

Alors que la valeur des actifs sur la chaîne de blocs augmente rapidement avec plusieurs projets se succédant pour lancer différents cas d'utilisation au sein de l'économie crypto, rester en avance sur les éventuelles failles et menaces est plus impératif que jamais.

Bitcoin a été inventé pour remplacer les banques, mais la technologie sous-jacente, la blockchain, a prouvé qu'elle pouvait remplacer presque n'importe quel intermédiaire. En avançant, cela ne s'est pas arrêté là en voyant le potentiel énorme que l'argent numérique possédait et que l'argent papier ne pouvait jamais avoir, à savoir la possibilité de programmer de l'argent. Soudain, les avocats et les contrats pouvaient être remplacés dans les transactions financières. Cette forme de monnaie numérique a favorisé la décentralisation en permettant l'exécution automatique de contrats avec une transparence totale et sans intervention humaine. Cependant, comment les contrats intelligents fonctionnent-ils exactement ? Peut-on vraiment faire confiance à ces systèmes qui manquent de confiance ?

Dans cet article, nous explorerons les nombreuses questions sur la vérification formelle des smart contracts, en discutant de ses avantages, de ses inconvénients, de son impact sur l'écosystème crypto, et plus encore, en mettant l'accent sur Ethereum.

Brève histoire des smart contracts

Source: CryptoSlate

Nick Szabo, un informaticien et cryptographe américain souvent spéculé être Satoshi Nakamoto, a été le pionnier des smart contracts, introduisant pour la première fois le concept en 1994. Szabo a décrit les smart contracts comme des protocoles de transaction numériques conçus pour appliquer automatiquement les termes d'un accord. Son objectif était d'améliorer les méthodes de transaction électronique, telles que les systèmes de point de vente, et d'étendre leurs capacités dans le monde numérique.

Szabo a imaginé un avenir où les accords pourraient fonctionner comme des distributeurs automatiques - automatisés, fiables et inviolables. Bien que la technologie de son époque ne soit pas assez avancée pour réaliser pleinement sa vision, les idées de Szabo ont jeté les bases de ce qui révolutionnerait plus tard l'industrie de la blockchain. Quand Ethereum lancéen 2015, il a mis en pratique les smart contracts, transformant les concepts théoriques de Szabo en composants essentiels des applications décentralisées.

Sa vision était de créer des contrats capables de gérer des relations avec des termes précis et automatisés, réduisant ainsi le besoin d'intervention et de supervision humaines. Cette approche visait à créer une manière plus sécurisée et efficace de gérer les accords, ouvrant la voie à l'évolution des smart contracts en des outils puissants dans l'écosystème de la blockchain. Les premières intuitions de Szabo continuent d'influencer le paysage des transactions numériques et du développement des smart contracts aujourd'hui.

Qu'est-ce que la vérification formelle?

Source : Moyen

La vérification formelle est le processus d'évaluation rigoureuse de savoir si un système, comme un contrat intelligent, fonctionne selon un ensemble défini de règles ou de spécifications. En essence, il vérifie si le système se comporte comme prévu, garantissant qu'il satisfait aux conditions requises et exécute les fonctions prévues sans erreurs.

Pour y parvenir, les comportements attendus du système sont décrits à l’aide de modèles formels, tandis que des langages de spécification sont utilisés pour définir les propriétés exactes que le contrat doit satisfaire et nous verrons des scénarios plus pratiques au fur et à mesure que l’article progresse. Les techniques de vérification formelle font ensuite correspondre la mise en œuvre du contrat à ses spécifications, fournissant ainsi une preuve mathématique de son exactitude. Lorsqu’un contrat répond à ces spécifications, il est considéré comme « fonctionnellement correct » ou « correct dès la conception », ce qui confirme sa fiabilité et sa sécurité dans l’environnement de la blockchain.

Types de spécifications formelles pour les contrats intelligents

Source: Ever Scale

Les spécifications formelles fournissent une manière structurée d'utiliser le raisonnement mathématique pour vérifier l'exactitude de l'exécution d'un programme. Ces spécifications peuvent décrire soit des propriétés de haut niveau, qui se concentrent sur le comportement global, soit des détails de bas niveau sur le fonctionnement interne d'un contrat. En définissant ces comportements mathématiquement, les spécifications formelles garantissent que le contrat fonctionne comme prévu.

Spécifications de haut niveau

Les spécifications de haut niveau, également connues sous le nom de spécifications orientées modèle, décrivent le comportement global d'un contrat intelligent, le traitant comme une machine à états finis (MEF) qui passe entre différents états à travers des opérations spécifiques. La logique temporelle est souvent utilisée pour définir les règles formelles qui régissent ces transitions, détaillant comment le contrat se déplace entre les états au fil du temps et les conditions qu'il doit remplir pour le faire correctement.

Ces spécifications capturent deux propriétés essentielles : la sûreté et la vivacité. La sûreté garantit que des événements indésirables ne se produisent pas, tels que la prévention d'une diminution du solde de l'expéditeur en dessous du montant nécessaire pour une transaction. La vivacité, à l'inverse, garantit que le contrat continue de fonctionner et de progresser, comme maintenir la liquidité pour que les utilisateurs puissent retirer des fonds lorsqu'ils le demandent. Les deux propriétés garantissent que les smart contracts fonctionnent de manière sécurisée et fiable, protégeant les interactions et les actifs des utilisateurs.

Spécifications de bas niveau

Les spécifications de bas niveau, également connues sous le nom de spécifications orientées propriété, se concentrent sur la définition du comportement correct des contrats intelligents en analysant leurs processus d'exécution internes. Contrairement aux spécifications de haut niveau qui modélisent les contrats en tant que machines à états finis, les spécifications de bas niveau considèrent les contrats intelligents comme des systèmes de fonctions mathématiques et examinent les séquences d'exécution de fonctions, appelées traces, qui modifient l'état du contrat.

Techniques de vérification formelle des contrats intelligents

Source: Ever Scale

Vérification de modèle

La vérification de modèle est une méthode de vérification formelle qui utilise des algorithmes pour évaluer si le modèle d'un smart contract correspond à ses spécifications. Les smart contracts sont généralement représentés sous forme de systèmes de transition d'états, et leurs propriétés sont définies à l'aide de la logique temporelle.logiqueCe processus consiste à créer un modèle mathématique du contrat et à exprimer ses propriétés à travers des formules logiques, permettant à l'algorithme de vérifier si le modèle répond à ces spécifications.

Démonstration de théorème

Contrairement à la vérification de modèle, la démonstration de théorème est une approche mathématique utilisée pour établir la justesse des programmes, y compris des contrats intelligents. Cette méthode consiste à convertir le modèle et les spécifications d'un contrat en formules logiques pour vérifier leur équivalence logique, c'est-à-dire qu'une déclaration est vraie si l'autre est vraie. En formulant cette relation comme un théorème, un prouveur de théorème automatisé peut valider la justesse du modèle de contrat par rapport à ses spécifications.

En contraste marqué avec la vérification de modèles, qui est limitée aux systèmes à états finis, la vérification de théorèmes peut analyser des systèmes à états infinis mais nécessite souvent l'aide humaine pour naviguer dans des problèmes logiques complexes. Par conséquent, la vérification de théorèmes a tendance à être plus gourmande en ressources que le processus de vérification de modèles entièrement automatisé.

Exécution symbolique

L'exécution symbolique est une méthode d'analyse puissante pour les smart contracts qui consiste à exécuter des fonctions avec des valeurs symboliques plutôt qu'avec des entrées spécifiques. Cette technique de vérification formelle permet de raisonner sur les propriétés au niveau de la trace dans le code d'un contrat en représentant les chemins d'exécution sous forme de formules mathématiques, appelées prédicats de chemin. Un solveur SMT est ensuite utilisé pour déterminer si ces prédicats sont satisfaisants, c'est-à-dire s'il existe une entrée qui satisfait les conditions.

Par exemple, si une fonction de contrat renvoie lorsqu'une valeur est entre 5 et 10, l'exécution symbolique peut identifier efficacement de telles valeurs déclenchantes en évaluant la condition comme X > 5 ∧ X < 10. Cette méthode est souvent plus efficace que les tests traditionnels, produisant moins de faux positifs et générant directement des valeurs concrètes qui reproduisent tout résolveur SMT est alors utilisé pour déterminer les erreurs trouvées, en en faisant un outil précieux pour garantir la fiabilité des contrats intelligents.

Quels sont les smart contracts?

Source: Tendrement

Les smart contracts sont des programmes informatiques automatisés qui fonctionnent sur une chaîne de blocs, exécutant des actions lorsque des conditions spécifiques sont remplies. Ils peuvent varier d'accords simples à des processus très complexes et peuvent gérer des actifs valorisés à des millions, voire des milliards de dollars.

Alors que les smart contracts ont le potentiel de révolutionner divers secteurs tels que le vote politique, la gestion de la chaîne d'approvisionnement, les soins de santé et l'immobilier, cet article maintient toujours son focus sur leur impact dans le domaine des cryptomonnaies. Leur conception permet à plusieurs parties de collaborer sans risque de manipulation, offrant un cadre transparent et sécurisé qui améliore l'efficacité et l'innovation. Cependant, il est important de reconnaître que les smart contracts comportent également des vulnérabilités et des défis.

Vulnérabilités avec les contrats intelligents

Vulnérabilités de sécuritéDans le code de contrat intelligent, une erreur peut entraîner des conséquences catastrophiques, telles que la perte totale des actifs stockés dans le contrat, comme l'ont démontré des incidents récents.

• En 2021, l'automate de marché Uranium Financeont subi un vol de 50 millions de dollarsen raison d'une simple faute de frappe dans son smart contract.
• Aussi en 2021, Compound Finance a distribué accidentellement 80 millions de dollarsdans les récompenses non méritées, encore une fois à cause d'une erreur de caractère unique.
• Une violation plus importante s'est produite en 2022lorsque 320 millions de dollars ont été volés du pont Wormholeen raison d'un bogue dans l'un de ses contrats intelligents.

Compte tenu de ces exemples, il est crucial de s'assurer que les smart contracts sont codés avec précision dès le départ. Une fois déployés, les smart contracts sont open source, ce qui signifie que leur code est accessible au public, facilitant ainsi l'exploitation de toutes les vulnérabilités découvertes par les pirates. De plus, la nature immuable des smart contracts signifie que leur code ne peut généralement pas être modifié pour corriger les failles de sécurité une fois qu'ils sont lancés, les laissant ainsi constamment exposés aux risques s'ils ne sont pas développés avec la plus grande précision.

Comment fonctionne la vérification des contrats intelligents?

Source: Certik

Le processus comprend:

• Définir les spécifications et les propriétés souhaitées du contrat en utilisant un langage formel.
• Traduire le code du contrat en une représentation formelle, telle que des modèles mathématiques ou des expressions logiques.
• Les prouveurs de théorèmes automatisés ou les vérificateurs de modèles sont employés pour confirmer la validité des spécifications et des propriétés du contrat.
• Répéter de manière itérative le processus de vérification pour identifier et corriger les erreurs ou les écarts par rapport aux propriétés prévues.

Caractéristiques clés des smart contracts

Source: Certik

Pensez aux smart contracts comme des accords gravés dans la pierre une fois créés, ils ne peuvent pas être modifiés. Fonctionnant sur le registre immuable d'une blockchain, ces contrats appliquent automatiquement les termes sans avoir besoin d'intermédiaires, ce qui accélère les transactions et réduit les coûts. Cette nature fixe renforce la sécurité et décentralise le contrôle, réduisant considérablement les risques de fraude et de corruption.

Pourquoi la vérification des contrats intelligents est importante

Le raisonnement mathématique joue un rôle crucial dans le fait de garantir que les contrats intelligents vérifiés formellement sont exempts de bugs, de vulnérabilités et de comportements inattendus. Ce processus rigoureux renforce la confiance dans le contrat, car ses propriétés ont été rigoureusement validées.

Les exemples réussis de vérification de contrats intelligents mettent en évidence son importance dans la prévention de pertes financières importantes.

Uniswap

Par exemple, Uniswap, un fournisseur de liquidité automatisé (AMM) bien connu, a fait l'objet d'une vérification formelle lors du développement de son contrat intelligent V1, ce qui a permis d'identifier et de corriger les erreurs d'arrondi.qui aurait pu vider les fonds.

Balancer

De même, Balancer V2, un autre AMM, a bénéficié de la vérification formelle qui a découvert un calcul de frais incorrect liés aux prêts flash, prévenant tout vol potentiel.

SafeMoon

SafeMoon V1 avait un bug subtilidentifié par vérification formelle après le déploiement. Ce bogue permettait au propriétaire de renoncer à la possession et de la récupérer dans certaines conditions, un détail que la plupart des audits manuels ont manqué en raison de sa complexité. La capacité de la vérification formelle à analyser des combinaisons spécifiques de valeurs de variables en fait un outil efficace pour détecter des problèmes que les auditeurs humains pourraient négliger.

Comment la vérification formelle et l'audit manuel travaillent ensemble

La vérification formelle offre une méthode systématique et automatisée pour vérifier la logique et le comportement d'un contrat intelligent par rapport à ses propriétés prévues. Cette approche simplifie l'identification et la correction d'erreurs ou de bogues potentiels, en particulier des problèmes complexes que les inspections manuelles pourraient négliger.

D'autre part, l'audit manuel implique une revue approfondie du code, de la conception et du déploiement du contrat par un expert. L'auditeur utilise son expérience pour identifier les risques de sécurité et évaluer la posture de sécurité globale du contrat. Il peut également valider la précision du processus de vérification formelle et identifier les problèmes que les outils automatisés pourraient ne pas détecter. La combinaison de la vérification formelle et de l'audit manuel permet une évaluation de sécurité complète, augmentant ainsi les chances de découvrir et de résoudre les vulnérabilités, et établissant une stratégie de défense solide qui exploite les points forts de l'expertise humaine et de l'analyse automatisée.

Avantages et inconvénients des contrats intelligents

Source : Blockonomi

Les contrats intelligents ne sont pas parfaits, mais leurs avantages l'emportent largement sur les inconvénients. Ils simplifient les transactions complexes, économisent du temps et de l'argent tout en favorisant la transparence et en réduisant les litiges. Comme ils fonctionnent sur du code, ils minimisent les erreurs humaines. Leur sécurité est robuste, grâce à des protections cryptographiques. Cependant, les contrats intelligents peuvent être rigides et avoir du mal à s'adapter à des situations inattendues. De plus, leur mise en place nécessite des compétences en codage spécialisées, ce qui peut être un obstacle pour certains. Malgré ces défis, les contrats intelligents transforment les industries.

Avantages des smart contracts

• Améliorez l'efficacité en automatisant les tâches, en gagnant du temps et de l'argent.
• Accroître la transparence en donnant à toutes les parties accès aux mêmes informations, réduisant ainsi les litiges.
• Réduisez les erreurs en vous appuyant sur le code, ce qui élimine les erreurs humaines.
• Renforcez la sécurité avec des protections cryptographiques, rendant la falsification difficile.

Inconvénients des contrats intelligents

• Manque de flexibilité pour s’adapter aux situations imprévues en raison de leur nature rigide.
• Nécessite des connaissances en codage spécialisées, limitant l'adoption généralisée.

Outils de vérification formelle pour les smart contracts Ethereum

Source: Calibraint

Langages de spécification pour créer des spécifications formelles

• Act: Act permet aux utilisateurs de définir des mises à jour de stockage, des pré et post-conditions et des invariants de contrat. Sa suite d'outils comprend des arrière-plans de preuve qui peuvent valider différentes propriétés à l'aide de Coq, de solveurs SMT ou de hevm.

GitHub

Documentation

• Scribble : Scribble convertit les annotations de code écrites dans son langage de spécification en assertions spécifiques qui vérifient les spécifications.

Documentation

• Dafny : Dafny est un langage de programmation conçu pour la vérification, utilisant des annotations de haut niveau pour aider à raisonner et confirmer la correction du code.

GitHub

Vérificateurs de programme pour vérifier la correction

• Certora Prover : Certora Prover est un outil de vérification formelle automatisé qui vérifie la correction des codes de contrat intelligents. Les spécifications sont créées à l'aide du langage de vérification Certora (CVL), et il détecte les violations de propriétés grâce à une combinaison d'analyse statique et de techniques de résolution de contraintes.

Site web

Documentation

• SMTChecker Solidity : Le SMTChecker de Solidity est un vérificateur de modèle intégré qui utilise la résolution de satisfiabilité modulo théories (SMT) et les résolutions de Horn. Il vérifie si le code source d'un contrat est conforme aux spécifications lors de la compilation et vérifie les violations des propriétés de sécurité.

GitHub

• Solc-verify: Solc-verify est une version améliorée du compilateur Solidity qui permet la vérification formelle automatisée du code Solidity grâce à des annotations et à la vérification de programmes modulaires.

GitHub

• KEVM : KEVM représente formellement la Machine Virtuelle Ethereum(EVM)créé à l'aide du framework K. Il est exécutable et peut vérifier des revendications spécifiques liées à des propriétés grâce à la logique de l'accessibilité.

GitHub (en anglais seulement)

Documentation

Cadres logiques pour la démonstration de théorèmes

• Isabelle: Isabelle/HOL est un assistant de preuve qui aide les utilisateurs à exprimer des formules mathématiques dans un langage formel et fournit des outils pour les prouver. Son utilisation principale est la formalisation des preuves mathématiques, en particulier pour vérifier la correction du matériel informatique et des logiciels, ainsi que les propriétés des langages de programmation et des protocoles.

GitHub

Documentation

• Coq - Coq est un prouveur de théorèmes interactif qui vous permet de définir des programmes avec des théorèmes et de créer des preuves vérifiées par machine de leur exactitude grâce à un processus interactif.

GitHub

Documentation

Outils basés sur l'exécution symbolique pour détecter des motifs vulnérables dans les contrats intelligents

• Manticore - Un outil qui analyse le bytecode EVM en utilisant l'exécution symbolique.

GitHub (en anglais seulement)

Documentation

• Hevm - hevm est un moteur d'exécution symbolique qui vérifie l'équivalence du bytecode EVM.

GitHub (en anglais seulement)

• Mythril - Un outil d'exécution symbolique utilisé pour trouver des vulnérabilités dans les smart contracts Ethereum.

GitHub

Documentation

Conclusion

Pour protéger les contrats intelligents, il est crucial de combiner la vérification formelle avec une vérification manuelle pour une évaluation complète de leur sécurité. Bien que la vérification formelle puisse être gourmande en ressources, c'est un investissement précieux pour les contrats impliquant des enjeux élevés ou des risques importants. Les contrats intelligents sont plus qu'un concept à la mode ; ils transforment les opérations commerciales mondiales, et bien qu'ils présentent des défis, leur capacité inégalée à accroître l'efficacité, à minimiser les erreurs et à renforcer la sécurité ne peut être ignorée. Les contrats intelligents ont un énorme potentiel pour simplifier les processus et favoriser la confiance dans les transactions numériques. À cette fin, les organisations qui adoptent cette technologie aujourd'hui seront prêtes à prospérer dans un avenir qui privilégie la transparence et la fiabilité.