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

La vérification formelle des contrats intelligents permet d’éviter qu’ils présentent des erreurs, des vulnérabilités ou d’autres situations défavorables. Dans ce processus, des experts humains transforment la logique du contrat intelligent en énoncés mathématiques, puis utilisent des processus automatisés pour comparer ces énoncés à un modèle de comportement attendu du contrat afin de vérifier sa logique réelle. En combinant vérification formelle et audit manuel, nous pouvons réaliser une évaluation complète de la sécurité des contrats intelligents.

Introduction

Les contrats intelligents sont des programmes informatiques déployés sur la blockchain, qui s’exécutent automatiquement lorsque certaines conditions sont remplies. Ils peuvent être très simples ou extrêmement complexes, et peuvent détenir des actifs d’une valeur de plusieurs millions, voire de plusieurs milliards de dollars.

Si le code d’un contrat intelligent comporte une vulnérabilité de sécurité, cela peut entraîner des conséquences dévastatrices, comme le vol de tous ses actifs par des acteurs malveillants. En 2021, en raison d’une erreur d’orthographe dans un contrat intelligent, le Automated Market Maker (AMM) (Uranium Finance a été piraté pour 50 millions de dollars.

De même, en 2021, une erreur dans un seul morceau de code a permis à Compound Finance de distribuer par erreur 80 millions de dollars en récompenses. En 2022, une erreur dans un contrat intelligent a permis de voler 320 millions de dollars via le Wormhole Bridge.

Il est donc crucial de s’assurer que le code des contrats intelligents est correct dès le départ. Les contrats intelligents sont généralement open source, ce qui signifie qu’une fois déployés, leur code devient public. Si un hacker découvre une erreur, il peut l’exploiter immédiatement. De plus, avec le temps, les opérations de correction des vulnérabilités de sécurité deviennent inefficaces, car le code des contrats intelligents ne peut généralement pas être modifié après déploiement.

Comment fonctionne la vérification des contrats intelligents ?

La vérification formelle des contrats intelligents consiste à représenter leur logique et leur comportement attendu sous forme d’énoncés mathématiques. Ensuite, des outils automatisés sont utilisés par des auditeurs pour vérifier si ces énoncés sont corrects.

Ce processus implique :

• La définition formelle des spécifications et des propriétés attendues du contrat.

• La conversion du code du contrat en déclarations formelles, telles que des modèles mathématiques ou logiques.

• L’utilisation de preuves automatiques ou de la détection de modèles pour vérifier la conformité du contrat aux spécifications et propriétés.

• La répétition de ces vérifications pour identifier et corriger toute erreur ou divergence par rapport aux propriétés attendues.

Pourquoi la vérification des contrats intelligents est-elle importante ?

En utilisant le raisonnement mathématique, la vérification formelle aide à garantir que les contrats intelligents vérifiés formellement sont exempts d’erreurs, de vulnérabilités ou d’autres situations indésirables. Elle contribue également à renforcer la confiance et la fiabilité du contrat, car ses propriétés ont été rigoureusement testées.

Voici quelques exemples illustrant comment la vérification des contrats intelligents peut aider à prévenir des pertes financières importantes et d’autres conséquences catastrophiques.

Uniswap

Uniswap est un AMM bien connu. Lors du développement de la version 1 d’Uniswap, une vérification formelle a été effectuée. Avant sa sortie, cette vérification a permis de détecter et de corriger des erreurs d’arrondi, évitant ainsi que les fonds d’Uniswap V1 soient entièrement siphonnés.

Balancer

Balancer V2 est également un AMM vérifié. La vérification formelle a permis de découvrir et de corriger une erreur de calcul des frais dans la fonction de prêt flash, une erreur qui aurait pu rendre la plateforme vulnérable au vol.

SafeMoon

SafeMoon V1, après déploiement, a révélé une erreur extrêmement mineure grâce à la vérification formelle. Si cette erreur n’avait pas été détectée, le propriétaire du contrat aurait pu, en abandonnant la propriété, la récupérer ultérieurement en effectuant certaines opérations.

La plupart des audits manuels des forks de SafeMoon V1 ont omis cette erreur, car il fallait analyser des combinaisons spécifiques de valeurs de variables pour la détecter. Les humains peuvent facilement passer à côté de ce problème, mais les machines peuvent le repérer rapidement.

Comment la vérification formelle et l’audit manuel collaborent-ils ?

La vérification formelle offre une méthode systématique et automatisée pour examiner la logique et le comportement du contrat en fonction de ses propriétés attendues. Cela facilite l’identification et la correction de toute erreur ou vulnérabilité potentielle, en particulier pour des problèmes complexes ou subtils difficiles à détecter lors d’un contrôle manuel.

L’audit manuel, quant à lui, consiste en une revue par des experts du code, de la conception et du déploiement du contrat. Les auditeurs utilisent leur expérience et leur expertise pour identifier les risques de sécurité et évaluer la sécurité globale du contrat. Ils peuvent également vérifier si le processus de vérification formelle a été correctement exécuté et détecter tout problème que les outils automatisés pourraient ne pas repérer.

En combinant vérification formelle et audit manuel, nous pouvons réaliser une évaluation complète de la sécurité des contrats intelligents. Cela augmente la probabilité de détecter et de corriger toute vulnérabilité. En somme, cela constitue une approche de défense en profondeur, combinant les forces humaines et machine.

Conclusion

Pour garantir la sécurité des contrats intelligents, il est essentiel de combiner vérification formelle et audit manuel, afin d’obtenir une évaluation exhaustive et rigoureuse de leur sécurité.

Bien que la vérification formelle soit gourmande en ressources, elle constitue un investissement précieux pour les contrats de grande valeur ou à haut risque. En fin de compte, la sécurité prime sur tout, et il faut donner la priorité à la sécurité pour éviter erreurs, vulnérabilités et comportements indésirables dans les contrats intelligents. )$BROCCOLI