Cet article a été publié par un membre de la communauté. L'auteur est David Tarditi, vice-président de l'ingénierie chez CertiK, une société d'audit de contrats intelligents Web3.
Résumé
La vérification formelle des contrats intelligents les protège des erreurs, des vulnérabilités et d'autres conditions défavorables. Dans ce processus, des experts humains convertissent la logique du contrat intelligent en déclarations mathématiques, puis utilisent un processus automatisé pour vérifier la logique réelle par rapport à un modèle du comportement attendu du contrat. En combinant vérification formelle et audit manuel, nous pouvons procéder à 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. Les contrats intelligents peuvent être très simples ou extrêmement complexes et peuvent détenir des actifs valant des millions, voire des milliards de dollars.
S’il y a des failles de sécurité dans le code des contrats intelligents, cela peut avoir des conséquences dévastatrices, comme le vol de tous les actifs détenus par des criminels. En 2021, 50 millions de dollars ont été volés au teneur de marché automatisé (AMM) Uranium Finance en raison d'une faute de frappe dans un contrat intelligent.
Également en 2021, Compound Finance a émis par erreur 80 millions de dollars de récompenses en raison d'une seule erreur de codage. En 2022, 320 millions de dollars ont été volés à Wormhole Bridge en raison d'une erreur dans le contrat intelligent.
Par conséquent, il est important de mettre en place votre programme de contrats intelligents dès le début. Les contrats intelligents adoptent un modèle open source, ce qui signifie qu'une fois le contrat déployé, le code est rendu public. Si un hacker découvre un bug, il peut immédiatement l’exploiter. De plus, la pratique normale consistant à corriger les vulnérabilités de sécurité au fil du temps est inefficace car le code des contrats intelligents ne peut souvent pas être modifié après le déploiement.
Comment fonctionne la vérification des contrats intelligents ?
La vérification formelle des contrats intelligents est réalisée en présentant la logique et le comportement attendu du contrat intelligent sous forme d'énoncés mathématiques. Les auditeurs utilisent ensuite des outils automatisés pour vérifier si ces déclarations sont correctes.
Le processus implique :
Définir le cahier des charges et les caractéristiques attendues du contrat dans un langage formel.
Convertissez le code d'un contrat en une déclaration formelle, telle qu'un modèle mathématique ou logique.
Vérifiez les spécifications et les propriétés du contrat à l’aide de la preuve automatisée de théorèmes ou de la vérification de modèles.
Répétez le processus de validation pour rechercher et corriger les erreurs ou les écarts par rapport aux caractéristiques attendues.
Pourquoi la vérification des contrats intelligents est importante
En appliquant un raisonnement mathématique, cela permet de garantir que les contrats intelligents formellement vérifiés sont exempts d'erreurs, de vulnérabilités et d'autres situations défavorables. La vérification contribue également à accroître la confiance dans le contrat car ses propriétés ont été rigoureusement testées et sont correctes et fiables.
Les exemples ci-dessous illustrent comment la vérification intelligente des contrats peut aider à prévenir des pertes financières importantes et d'autres conséquences catastrophiques.
Uniswap
Uniswap est un AMM bien connu. Le contrat intelligent Uniswap V1 a subi une vérification formelle pendant le processus de développement. Avant la publication, cette vérification formelle a détecté et corrigé certaines erreurs d'arrondi, empêchant Uniswap V1 d'être vidé de ses fonds.
Balancier
Balancer V2 est également un AMM éprouvé. Une vérification formelle a découvert et corrigé une erreur de calcul des frais dans la fonction de prêt flash du contrat intelligent, qui rendait la plateforme de trading vulnérable au vol.
Lune sûre
Après le déploiement de SafeMoon V1, une très petite erreur a été découverte grâce à une vérification formelle. Si l'erreur n'était pas découverte, si le propriétaire du contrat effectuait certaines opérations avant de renoncer à la propriété, il pourrait la récupérer après avoir abandonné le contrat.
La plupart des audits manuels du fork SafeMoon V1 manquent ce bug car des combinaisons spécifiques de valeurs de variables de programme doivent être analysées pour le trouver. Les humains peuvent facilement ignorer ce problème, mais les machines peuvent le détecter à temps.
Comment la vérification formelle et l’audit manuel fonctionnent ensemble
La vérification formelle offre un moyen systématique et automatisé de vérifier la logique et le comportement d'un contrat par rapport à ses caractéristiques attendues. Cela facilite l’identification et la correction des bogues ou vulnérabilités potentiels. Ceci est particulièrement utile pour les problèmes complexes et subtils qui seraient difficiles à détecter par une inspection manuelle.
L'audit manuel implique des experts qui examinent le code, la conception et le déploiement du contrat. Les auditeurs utilisent leur expérience et leur expertise pour identifier les risques de sécurité et évaluer la situation de sécurité globale du contrat. Ils peuvent également confirmer que le processus de vérification formelle est effectué correctement et rechercher tout problème que les outils automatisés pourraient ne pas détecter.
En combinant vérification formelle et audit manuel, nous pouvons procéder à une évaluation complète de la sécurité des contrats intelligents. Cela améliore les chances de trouver et de corriger les vulnérabilités. Ce faisant, nous adoptons une approche de sécurité de défense en profondeur qui combine l’expertise de l’humain et de la machine.
Conclusion
Pour garantir la sécurité des contrats intelligents, la vérification formelle et l’audit manuel doivent être combinés pour garantir une évaluation complète et approfondie de la posture de sécurité des contrats intelligents.
Même si la vérification formelle nécessite plus de ressources, elle constitue un investissement rentable pour les contrats présentant une valeur élevée ou des facteurs de risque élevés. Après tout, en fin de compte, la sécurité est plus importante que toute autre chose. Assurez-vous de donner la priorité à la sécurité et de vous assurer que les contrats intelligents sont exempts de bogues, de vulnérabilités et de comportements inattendus indésirables.
Lectures complémentaires
Qu'est-ce qu'un contrat intelligent ?
Qu’est-ce que l’audit de sécurité des contrats intelligents ?
Avis de non-responsabilité et avertissement de risque : le contenu de cet article est constitué de faits et est uniquement destiné à des fins d'information générale et d'éducation et ne constitue aucune représentation ou garantie. Cet article ne doit pas être interprété comme un conseil financier et ne vous recommande pas d’acheter un produit ou un service spécifique. Les prix des actifs numériques peuvent fluctuer. La valeur de votre investissement peut baisser comme augmenter et vous risquez de ne pas récupérer le capital investi. Vous êtes seul responsable de vos propres décisions d'investissement et Binance Academy n'est pas responsable des pertes que vous pourriez subir. Ce matériel ne constitue pas un conseil financier.
