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 contrats intelligents Web3.
Les opinions exprimées dans cet article sont celles du contributeur/auteur et ne reflètent pas nécessairement celles de Binance Academy.
TL;DR
La vérification formelle des contrats intelligents 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 contrat intelligent 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 d'une vérification formelle et d'un audit manuel fournit une évaluation complète de la sécurité d'un contrat intelligent.
Introduction
Les contrats intelligents sont des programmes informatiques déployés sur une blockchain qui s'exécutent automatiquement lorsque certaines conditions sont remplies. Ils peuvent être simples ou extrêmement complexes et détenir des actifs valant des millions, voire des milliards de dollars.
Les failles de sécurité dans le code des contrats intelligents peuvent avoir des conséquences dévastatrices, notamment le vol de tous les actifs détenus par un contrat intelligent. En 2021, le teneur de marché automatisé (AMM) Uranium Finance s'est vu voler 50 millions de dollars en raison d'une seule faute de frappe dans un contrat intelligent.
Également en 2021, Compound Finance a distribué 80 millions de dollars de récompenses non gagnées en raison d'une erreur de personnage. En 2022, 320 millions de dollars ont été volés au Wormhole Bridge en raison d'un bug dans l'un de ses contrats intelligents.
Il est important de réussir le programme de contrats intelligents du premier coup. Les contrats intelligents sont open source, ce qui signifie que le code est accessible au public une fois le contrat déployé. Si un pirate découvre un bug, il peut en profiter immédiatement. De plus, corriger les vulnérabilités de sécurité au fil du temps n’est pas une option, car le code d’un contrat intelligent ne peut généralement pas être modifié après le déploiement.
Comment fonctionne la vérification des contrats intelligents ?
La vérification formelle des contrats intelligents fonctionne en présentant la logique et le comportement souhaité des contrats intelligents 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 les spécifications et les propriétés souhaitées d'un contrat en langage formel.
Traduire le code du contrat en une représentation formelle, telle que des modèles mathématiques ou logiques.
Utiliser des prouveurs 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.
Répéter le processus de vérification pour rechercher et corriger les erreurs ou les écarts par rapport aux propriétés souhaitées.
Pourquoi la vérification des contrats intelligents est importante
L’utilisation d’un raisonnement mathématique permet de garantir que les contrats intelligents 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.
Vous trouverez ci-dessous quelques exemples de la manière dont la vérification intelligente des contrats a contribué à éviter des pertes financières importantes et d’autres conséquences désastreuses.
Uniswap
Uniswap est un AMM bien connu. Lorsque le contrat intelligent Uniswap V1 a été développé, il a été formellement vérifié. Avant sa publication, cette vérification formelle a détecté et corrigé des erreurs d'arrondi qui auraient pu conduire à une perte de fonds d'Uniswap V1.
Balancier
Balancer V2 est également un AMM qui a été formellement vérifié. Une vérification formelle a révélé et corrigé un calcul de frais incorrect impliquant la fonctionnalité de prêt flash dans le contrat intelligent, ce qui aurait pu rendre l'échange vulnérable au vol.
Lune sûre
SafeMoon V1 contenait un bug 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 puis de le racheter à nouveau, si certaines opérations étaient effectuées avant de renoncer à la propriété.
Ce bug a été manqué dans la plupart des audits manuels des forks SafeMoon V1 car sa découverte nécessitait d'analyser des combinaisons spécifiques de valeurs de variables du programme. C’est quelque chose qui est facile à manquer pour les humains et facile à détecter pour une machine.
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 propriétés souhaitées. Cela facilite l’identification et la correction des erreurs ou bugs potentiels. Il est particulièrement utile pour détecter 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 la situation de sécurité globale du contrat. Ils peuvent également confirmer que le processus de vérification formelle a été effectué correctement et rechercher tout problème qui pourrait ne pas être détectable par les outils automatisés.
La combinaison de la vérification formelle et de l'audit manuel permet une évaluation complète et approfondie de la sécurité d'un contrat intelligent. Cela augmente les chances de trouver et de corriger les vulnérabilités. Le résultat est une approche de défense en profondeur de la sécurité qui exploite les capacités uniques des humains et des machines.
Pensées finales
Pour garantir la sécurité des contrats intelligents, il est essentiel de recourir à la fois à une vérification formelle et à un audit manuel pour garantir une évaluation complète et approfondie de la posture de sécurité d'un contrat intelligent.
Même si la vérification formelle peut nécessiter beaucoup de ressources, elle constitue un investissement rentable pour les contrats présentant une valeur élevée ou des facteurs de risque élevés. En fin de compte, il est essentiel de donner la priorité à la sécurité et de garantir que les contrats intelligents sont exempts de bogues, de vulnérabilités et de comportements involontaires.
Lectures complémentaires
Que sont les contrats intelligents ?
Qu’est-ce qu’un audit de sécurité des contrats intelligents ?
Avis de non-responsabilité et avertissement de risque : ce contenu vous est présenté « tel quel » à des fins d'information générale et éducatives uniquement, sans représentation ni garantie d'aucune sorte. Il ne doit pas être interprété comme un conseil financier, juridique ou autre conseil professionnel, et il n’est pas non plus destiné à recommander l’achat d’un produit ou d’un service spécifique. Vous devriez demander votre propre avis auprès de conseillers professionnels appropriés. Lorsque l'article est rédigé par un contributeur tiers, veuillez noter que les opinions exprimées appartiennent au contributeur tiers et ne reflètent pas nécessairement celles de Binance Academy. Veuillez lire notre clause de non-responsabilité complète ici pour plus de détails. Les prix des actifs numériques peuvent être volatils. La valeur de votre investissement peut augmenter ou diminuer et vous ne récupérerez peut-être pas le montant investi. Vous êtes seul responsable de vos décisions d'investissement et Binance Academy n'est pas responsable des pertes que vous pourriez subir. Ce matériel ne doit pas être interprété comme un conseil financier, juridique ou autre conseil professionnel. Pour plus d’informations, consultez nos conditions d’utilisation et nos avertissements de risque.
