Qu’est-ce que la vérification formelle de smart contracts ?

Cet article est une soumission de la communauté. L’auteur est David Tarditi, vice-président de l’ingénierie chez CertiK, un cabinet d’audit de smart contracts Web3.

Résumé

La vérification formelle de smart contracts garantit qu’ils sont exempts de bogues, de vulnérabilités et d’autres comportements involontaires. Cela implique qu’un expert humain présente la logique du smart contract sous forme d’énoncés mathématiques, puis les exécute à travers un processus automatisé qui vérifie la logique réelle par rapport aux modèles du comportement attendu du contrat. La combinaison de la vérification formelle et de l’audit manuel fournit une évaluation complète de la sécurité d’un smart contract.

Introduction

Les smart contracts sont des programmes informatiques déployés sur une blockchain qui exécutent automatiquement une action lorsque certaines conditions sont remplies. Ces actions peuvent aller de la plus simple à la plus complexe, et peuvent contenir des actifs valant des millions, voire des milliards de dollars.  

Les failles de sécurité dans le code des smart contracts peuvent avoir des conséquences dévastatrices, dont le vol de tous les actifs détenus par un smart contract. En 2021, le market maker automatisé (AMM) Uranium Finance s’est fait voler 50 millions de dollars en raison d’une simple faute de frappe dans un smart contract.

Toujours en 2021, Compound Finance a distribué 80 millions de dollars en récompenses non gagnées en raison d’une erreur d’un caractère. En 2022, 320 millions de dollars ont été volés à la passerelle Wormhole en raison d’un bogue dans l’un de ses smart contracts.

Il est important de ne pas faire d’erreur dans la définition initiale du smart contract. Les smart contracts sont disponibles en libre accès (open-source), ce qui signifie que le code est accessible au public une fois qu’un contrat est déployé. Si un pirate trouve un bogue, il peut en profiter immédiatement. En outre, l’application de correctifs aux vulnérabilités de sécurité au fil du temps n’est pas une option, car le code d’un smart contract ne peut généralement pas être modifié après son déploiement.

Comment fonctionne la vérification des smart contracts ?  

La vérification formelle des smart contracts fonctionne en présentant la logique et le comportement souhaité des smart contracts sous forme d’énoncés mathématiques. Les auditeurs utilisent ensuite des outils automatisés pour vérifier si ces comportements sont respectés.

Le processus comprend :

1. La définition des spécifications et des propriétés souhaitées d’un contrat en langage formel.

2. La traduction du code du contrat en une représentation formelle, telle que des modèles mathématiques ou logiques.

3. L’utilisation de vérificateurs de théorèmes automatisés ou des vérificateurs de modèles pour valider les spécifications et les propriétés du contrat.

4. La répétition du processus de vérification pour trouver et corriger les erreurs ou les écarts par rapport aux propriétés souhaitées.

Pourquoi la vérification des smart contracts est importante ?

L’utilisation du raisonnement mathématique permet de s’assurer que les smart contracts formellement vérifiés sont exempts de bogues, de vulnérabilités et d’autres comportements involontaires. Cela contribue également à accroître la confiance dans le contrat, car ses propriétés ont été rigoureusement prouvées comme étant correctes. 

Vous trouverez ci-dessous quelques exemples de la façon dont la vérification des smart contracts a permis d’éviter des pertes financières importantes et d’autres résultats désastreux.  

Uniswap

Uniswap est un AMM bien connu. Lorsque le smart contract Uniswap V1 a été développé, il a été formellement vérifié. Avant sa publication, cette vérification formelle a permis de trouver et de corriger des erreurs d’arrondi qui auraient pu entraîner le vol des fonds d’Uniswap V1. 

Balancer

Balancer V2 est également un AMM qui a été formellement vérifié. Une vérification formelle a permis de trouver et de corriger un calcul incorrect des frais impliquant une fonctionnalité de prêt flash dans le smart contract, ce qui aurait pu rendre l’exchange vulnérable au vol.

SafeMoon

SafeMoon V1 contenait un bogue subtil trouvé par vérification formelle après son déploiement. Il était possible pour un propriétaire de renoncer à la propriété du contrat et de la récupérer, si certaines opérations étaient effectuées avant de renoncer à la propriété.

Ce bogue a été omis dans la plupart des audits manuels des forks SafeMoon V1 car sa découverte nécessitait l’analyse de combinaisons spécifiques de valeurs de variables du programme. C’est quelque chose qu’il est difficile de détecter pour les humains, mais facile à identifier pour une machine.

Comment la vérification formelle et l’audit manuel fonctionnent ensemble ?

La vérification formelle fournit un moyen systématique et automatisé de vérifier la logique et le comportement d’un contrat par rapport aux propriétés souhaitées. Cela facilite l’identification et la correction des erreurs ou des bogues potentiels. Cette méthode est particulièrement utile pour trouver des problèmes complexes et subtils qui peuvent être difficiles à détecter par une inspection manuelle.

L’audit manuel implique l’examen par un expert, du code, de la conception et du déploiement d’un contrat. L’auditeur utilise son expérience et son expertise pour identifier les risques de sécurité et évaluer le niveau de sécurité général du contrat. Ils peuvent également confirmer que le processus de vérification formelle a été effectué correctement et vérifier les problèmes qui peuvent ne pas être détectables par les outils automatisés. 

La combinaison de la vérification formelle et de l’audit manuel fournit une évaluation complète de la sécurité d’un smart contract. Cela augmente les chances de trouver et de corriger des vulnérabilités. Le résultat est une approche défensive en profondeur de la sécurité qui exploite les capacités uniques des humains et des machines. 

Conclusion

Pour assurer la sécurité des smart contracts, il est essentiel d’utiliser à la fois une vérification formelle et un audit manuel pour assurer une évaluation complète et approfondie du niveau de sécurité d’un smart contract.

Bien que la vérification formelle puisse exiger beaucoup de ressources, il s’agit d’un investissement rentable pour les contrats gérant d’importantes sommes d’argent, ou à risque élevé. En fin de compte, il est essentiel de donner la priorité à la sécurité et de s’assurer que les smart contracts sont exempts de bogues, de vulnérabilités et de comportements involontaires.

Plus d’informations

• Qu’est-ce qu’un smart contract ?

• Qu’est-ce que l’audit de sécurité d’un smart contract ?

Clause de non-responsabilité et avertissement concernant les risques : ce contenu vous est présenté « tel quel » à des fins d’information générale et éducative uniquement, sans représentation ni garantie d’aucune sorte. Il ne doit pas être interprété comme un conseil financier, ni comme un moyen de recommander l’achat d’un produit ou d’un service spécifique. Les prix des actifs numériques peuvent être volatils. La valeur de votre investissement peut varier à la baisse ou à la hausse, et vous ne récupérerez peut-être pas le montant que vous avez investi. Vous êtes seul(e) responsable de vos décisions d’investissement et Binance Academy n’est pas responsable des pertes que vous pourriez subir. Ce contenu ne doit pas être interprété comme un conseil financier.