VÉRIFICATION FORMELLE DES CONTRATS INTELLIGENTS
Contrats intelligentspermettent de créer des applications décentralisées, sans confiance et robustes qui introduisent de nouveaux cas d'utilisation et débloquent de la valeur pour les utilisateurs. Comme les contrats intelligents gèrent de grandes quantités de valeur, la sécurité est une considération cruciale pour les développeurs.
La vérification formelle est l'une des techniques recommandées pour améliorer sécurité des contrats intelligentsLa vérification formelle, qui utiliseméthodes formelles
pour spécifier, concevoir et vérifier des programmes, est utilisé depuis des années pour garantir la correction des systèmes matériels et logiciels critiques.
Lorsqu'il est mis en œuvre dans des contrats intelligents, la vérification formelle peut prouver que la logique commerciale d'un contrat répond à une spécification prédéfinie. Comparé à d'autres méthodes d'évaluation de la correction du code de contrat, telles que les tests, la vérification formelle offre des garanties plus solides qu'un contrat intelligent est fonctionnellement correct.
QU'EST-CE QUE LA VÉRIFICATION FORMELLE?
La vérification formelle fait référence au processus d'évaluation de la correction d'un système par rapport à une spécification formelle. En termes plus simples, la vérification formelle nous permet de vérifier si le comportement d'un système satisfait certaines exigences (c'est-à-dire, il fait ce que nous voulons).
Les comportements attendus du système (un smart contract dans ce cas) sont décrits à l'aide d'une modélisation formelle, tandis que les langages de spécification permettent la création de propriétés formelles. Les techniques de vérification formelle peuvent ensuite vérifier que l'implémentation d'un contrat est conforme à sa spécification et dériver une preuve mathématique de la correction de ce dernier. Lorsqu'un contrat satisfait sa spécification, on le décrit comme "fonctionnellement correct", "correct par conception" ou "correct par construction".
Qu'est-ce qu'un modèle formel ?
En informatique, un modèle formel
est une description mathématique d'un processus informatique. Les programmes sont abstraits en fonctions mathématiques (équations), le modèle décrivant comment les sorties des fonctions sont calculées en fonction d'une entrée.
Les modèles formels fournissent un niveau d'abstraction sur lequel l'analyse du comportement d'un programme peut être évaluée. L'existence de modèles formels permet la création d'une spécification formelle, qui décrit les propriétés souhaitées du modèle en question.
Différentes techniques sont utilisées pour modéliser des contrats intelligents en vue d'une vérification formelle. Par exemple, certains modèles sont utilisés pour raisonner sur le comportement de haut niveau d'un contrat intelligent. Ces techniques de modélisation appliquent une vue en boîte noire aux contrats intelligents, les considérant comme des systèmes qui acceptent des entrées et exécutent des calculs en fonction de ces entrées.
Les modèles de haut niveau se concentrent sur la relation entre les contrats intelligents et les agents externes, tels que les comptes détenus de manière externe (EOA), les comptes de contrat et l'environnement blockchain. De tels modèles sont utiles pour définir des propriétés qui spécifient comment un contrat doit se comporter en réponse à certaines interactions utilisateur.
Inversement, d'autres modèles formels se concentrent sur le comportement de bas niveau d'un smart contract. Alors que les modèles de haut niveau peuvent aider à raisonner sur la fonctionnalité d'un contrat, ils peuvent échouer à capturer les détails sur le fonctionnement interne de l'implémentation. Les modèles de bas niveau appliquent une vue en boîte blanche à l'analyse de programme et s'appuient sur des représentations de bas niveau des applications de smart contract, telles que les traces de programme et graphes de flux de contrôle
, pour raisonner sur les propriétés pertinentes à l'exécution d'un contrat.
Les modèles de bas niveau sont considérés comme idéaux car ils représentent l'exécution réelle d'un smart contract dans l'environnement d'exécution d'Ethereum (c.-à-d.EVM). Les techniques de modélisation de bas niveau sont particulièrement utiles pour établir les propriétés de sécurité critiques dans les contrats intelligents et détecter les vulnérabilités potentielles.
Qu'est-ce qu'une spécification formelle ?
Une spécification est simplement une exigence technique que doit satisfaire un système particulier. En programmation, les spécifications représentent des idées générales sur l'exécution d'un programme (c'est-à-dire ce que le programme devrait faire).
Dans le contexte des contrats intelligents, les spécifications formelles font référence à des propriétés, c'est-à-dire des descriptions formelles des exigences qu'un contrat doit satisfaire. Ces propriétés sont décrites comme des "invariants" et représentent des assertions logiques concernant l'exécution d'un contrat qui doivent rester vraies dans toutes les circonstances possibles, sans aucune exception.
Ainsi, nous pouvons considérer une spécification formelle comme un ensemble d'énoncés écrits dans un langage formel qui décrivent l'exécution prévue d'un contrat intelligent. Les spécifications portent sur les propriétés d'un contrat et définissent comment le contrat doit se comporter dans différentes circonstances. Le but de la vérification formelle est de déterminer si un contrat intelligent possède ces propriétés (invariants) et que ces propriétés ne sont pas violées lors de l'exécution.
Les spécifications formelles sont essentielles dans le développement de mises en œuvre sécurisées de contrats intelligents. Les contrats qui échouent à mettre en œuvre des invariants ou dont les propriétés sont violées lors de l'exécution sont sujets à des vulnérabilités qui peuvent nuire à la fonctionnalité ou causer des exploits malveillants.
TYPES DE SPÉCIFICATIONS FORMELLES POUR LES CONTRATS INTELLIGENTS
Les spécifications formelles permettent un raisonnement mathématique sur la correction de l'exécution du programme. Tout comme les modèles formels, les spécifications formelles peuvent capturer des propriétés de haut niveau ou le comportement de bas niveau d'une implémentation de contrat.
Les spécifications formelles sont dérivées en utilisant des éléments de logique de programme
, qui permettent un raisonnement formel sur les propriétés d'un programme. Une logique de programme a des règles formelles qui expriment (dans un langage mathématique) le comportement attendu d'un programme. Diverses logiques de programme sont utilisées dans la création de spécifications formelles, notamment logique de portée
(s'ouvre dans un nouvel onglet)
Les spécifications formelles des contrats intelligents peuvent être classées de manière générale comme des spécifications de haut niveau ou de bas niveau. Peu importe la catégorie à laquelle appartient une spécification, elle doit décrire de manière adéquate et non ambiguë la propriété du système en cours d'analyse.
Spécifications de haut niveau
Comme son nom l'indique, une spécification de haut niveau (également appelée "spécification orientée modèle") décrit le comportement de haut niveau d'un programme. Les spécifications de haut niveau modélisent un smart contract comme un machine à états finis
(FSM), qui peut passer d'un état à un autre en effectuant des opérations, la logique temporelle étant utilisée pour définir les propriétés formelles du modèle FSM.
sont des «règles de raisonnement sur des propositions qualifiées en termes de temps (par exemple, «J'ai toujours faim» ou «Je finirai par avoir faim»).» Lorsqu'ils sont appliqués à la vérification formelle, les logiques temporelles sont utilisées pour énoncer des assertions sur le comportement correct des systèmes modélisés sous forme de machines à états. Plus précisément, une logique temporelle décrit les états futurs dans lesquels un smart contract peut se trouver et comment il passe d'un état à un autre.
Les spécifications de haut niveau capturent généralement deux propriétés temporelles critiques pour les contrats intelligents : la sûreté et la vivacité. Les propriétés de sûreté représentent l'idée que « rien de mal ne se produit jamais » et expriment généralement l'invariance. Une propriété de sûreté peut définir des exigences générales en matière de logiciels, telles que la liberté de impasse
, ou exprimer les propriétés spécifiques au domaine pour les contrats (par exemple, les invariants sur le contrôle d'accès pour les fonctions, les valeurs admissibles des variables d'état, ou les conditions pour les transferts de jetons).
Prenons par exemple cette exigence de sécurité qui couvre les conditions d'utilisation des fonctions transfer() ou transferFrom() dans les contrats de jetons ERC-20 : "Le solde de l'expéditeur n'est jamais inférieur au montant demandé de jetons à envoyer.". Cette description en langage naturel d'une invariance de contrat peut être traduite en une spécification formelle (mathématique), qui peut ensuite être vérifiée rigoureusement pour sa validité.
Les propriétés de vivacité affirment que « quelque chose de bien finira par se produire » et concernent la capacité d'un contrat à progresser à travers différents états. Un exemple de propriété de vivacité est la « liquidité », qui fait référence à la capacité d'un contrat de transférer ses soldes aux utilisateurs sur demande. Si cette propriété est violée, les utilisateurs seraient incapables de retirer les actifs stockés dans le contrat, comme ce qui s'est passé avec le Incident de portefeuille de parité
.
Spécifications de bas niveau
Les spécifications de haut niveau prennent comme point de départ un modèle à états finis d'un contrat et définissent les propriétés souhaitées de ce modèle. En revanche, les spécifications de bas niveau (également appelées "spécifications orientées propriété") modélisent souvent des programmes (contrats intelligents) en tant que systèmes comprenant une collection de fonctions mathématiques et décrivent le comportement correct de ces systèmes.
En termes plus simples, les spécifications de bas niveau analysent les traces de programme et tentent de définir les propriétés d'un smart contrat sur ces traces. Les traces font référence à des séquences d'exécutions de fonctions qui modifient l'état d'un smart contrat; par conséquent, les spécifications de bas niveau aident à spécifier les exigences pour l'exécution interne d'un contrat.
Les spécifications formelles de bas niveau peuvent être données soit sous forme de propriétés de style Hoare, soit sous forme d'invariants sur les chemins d'exécution.
propriétés de style Hoare
fournit un ensemble de règles formelles pour raisonner sur la correction des programmes, y compris les contrats intelligents. Une propriété de style Hoare est représentée par un triple de Hoare {P}c{Q}, où c est un programme et P et Q sont des prédicats sur l'état de c (c'est-à-dire, le programme), formellement décrits comme des préconditions et des postconditions, respectivement.
Une condition préalable est un prédicat décrivant les conditions requises pour l'exécution correcte d'une fonction ; les utilisateurs appelant le contrat doivent satisfaire cette exigence. Une postcondition est un prédicat décrivant la condition qu'une fonction établit si elle est correctement exécutée ; les utilisateurs peuvent s'attendre à ce que cette condition soit vraie après avoir appelé la fonction. Une invariante dans la logique de Hoare est un prédicat préservé par l'exécution d'une fonction (c'est-à-dire qu'il ne change pas).
Les spécifications de style Hoare peuvent garantir soit une correction partielle soit une correction totale. L'implémentation d'une fonction de contrat est "partiellement correcte" si la précondition est vraie avant l'exécution de la fonction, et si l'exécution se termine, la postcondition est également vraie. La preuve de la correction totale est obtenue si une précondition est vraie avant l'exécution de la fonction, l'exécution est garantie de se terminer et lorsque c'est le cas, la postcondition est vraie.
Obtenir la preuve de la correction totale est difficile car certaines exécutions peuvent prendre du retard avant de se terminer, ou ne jamais se terminer du tout. Cela dit, la question de savoir si l'exécution se termine est sans doute un point discutable puisque le mécanisme de gaz d'Ethereum empêche les boucles de programmes infinies (l'exécution se termine soit avec succès, soit à cause d'une erreur de 'hors-gaz').
Les spécifications des contrats intelligents créés à l'aide de la logique de Hoare auront des préconditions, des postconditions et des invariants définis pour l'exécution des fonctions et des boucles dans un contrat. Les préconditions incluent souvent la possibilité d'entrées erronées dans une fonction, les postconditions décrivent la réponse attendue à de telles entrées (par exemple, en lançant une exception spécifique). De cette manière, les propriétés de style Hoare sont efficaces pour garantir la correction des implémentations de contrats.
De nombreux cadres de vérification formelle utilisent des spécifications de style Hoare pour prouver la correction sémantique des fonctions. Il est également possible d'ajouter des propriétés de style Hoare (sous forme d'assertions) directement au code du contrat en utilisant les déclarations require et assert en Solidity.
Les instructions require expriment une précondition ou un invariant et sont souvent utilisées pour valider les saisies de l'utilisateur, tandis que assert capture une postcondition nécessaire à la sécurité. Par exemple, un contrôle d'accès approprié pour les fonctions (un exemple d'une propriété de sécurité) peut être réalisé en utilisant require comme vérification de précondition sur l'identité du compte appelant. De même, un invariant sur les valeurs admissibles des variables d'état dans un contrat (par exemple, le nombre total de jetons en circulation) peut être protégé contre les violations en utilisant assert pour confirmer l'état du contrat après l'exécution de la fonction.
Propriétés de niveau de trace
Les spécifications basées sur les traces décrivent les opérations qui font passer un contrat entre différents états et les relations entre ces opérations. Comme expliqué précédemment, les traces sont des séquences d'opérations qui modifient l'état d'un contrat d'une manière particulière.
Cette approche repose sur un modèle de contrats intelligents en tant que systèmes de transition d'états avec certains états prédéfinis (décrits par des variables d'état) ainsi qu'un ensemble de transitions prédéfinies (décrites par des fonctions de contrat). De plus, un graphe de flux de contrôle
(s'ouvre dans un nouvel onglet)
(CFG), qui est une représentation graphique du flux d'exécution d'un programme, est souvent utilisé pour décrire la sémantique opérationnelle d'un contrat. Ici, chaque trace est représentée comme un chemin sur le graphe de flux de contrôle.
Principalement, les spécifications de niveau de trace sont utilisées pour raisonner sur les schémas d'exécution interne dans les contrats intelligents. En créant des spécifications de niveau de trace, nous affirmons les chemins d'exécution admissibles (c'est-à-dire, les transitions d'état) pour un contrat intelligent. En utilisant des techniques, telles que l'exécution symbolique, nous pouvons vérifier formellement que l'exécution ne suit jamais un chemin non défini dans le modèle formel.
Utilisons un exemple de DAOcontrat qui comporte certaines fonctions accessibles au public pour décrire les propriétés de niveau de trace. Ici, nous supposons que le contrat DAO permet aux utilisateurs d'effectuer les opérations suivantes :
- Déposer des fonds
- Vote sur une proposition après avoir déposé des fonds
- Demander un remboursement s'ils ne votent pas sur une proposition
Les propriétés de niveau de trace d'exemple pourraient être « les utilisateurs qui ne déposent pas de fonds ne peuvent pas voter sur une proposition » ou « les utilisateurs qui ne votent pas sur une proposition devraient toujours pouvoir réclamer un remboursement ». Ces propriétés affirment des séquences d'exécution préférées (le vote ne peut pas avoir lieu avant le dépôt de fonds et la réclamation d'un remboursement ne peut pas avoir lieu après un vote sur une proposition).
TECHNIQUES POUR LA VÉRIFICATION FORMELLE DES CONTRATS INTELLIGENTS
Vérification de modèle
La vérification de modèle est une technique de vérification formelle dans laquelle un algorithme vérifie un modèle formel d'un contrat intelligent par rapport à sa spécification. Dans la vérification de modèle, les contrats intelligents sont souvent représentés comme des systèmes de transition d'états, tandis que les propriétés sur les états de contrat autorisés sont définies en utilisant la logique temporelle.
La vérification de modèle nécessite la création d'une représentation mathématique abstraite d'un système (c'est-à-dire, un contrat) et l'expression de propriétés de ce système en utilisant des formules enracinées danslogique propositionnelle
(s'ouvre dans un nouvel onglet)
. Cela simplifie la tâche de l'algorithme de vérification du modèle, à savoir prouver qu'un modèle mathématique satisfait une formule logique donnée.
La vérification de modèle dans la vérification formelle est principalement utilisée pour évaluer les propriétés temporelles qui décrivent le comportement d'un contrat dans le temps. Les propriétés temporelles des contrats intelligents comprennent la sécurité et la vivacité, que nous avons expliquées plus tôt.
Par exemple, une propriété de sécurité liée au contrôle d'accès (par exemple, Seul le propriétaire du contrat peut appeler selfdestruct) peut être écrite en logique formelle. Ensuite, l'algorithme de vérification de modèle peut vérifier si le contrat satisfait cette spécification formelle.
La vérification de modèle utilise l'exploration de l'espace d'états, ce qui implique la construction de tous les états possibles d'un contrat intelligent et la tentative de trouver des états atteignables entraînant des violations de propriété. Cependant, cela peut conduire à un nombre infini d'états (connu sous le nom de "problème d'explosion d'états"), d'où la dépendance des vérificateurs de modèle sur des techniques d'abstraction pour rendre possible l'analyse efficace des contrats intelligents.
Démonstration de théorème
La preuve de théorème est une méthode de raisonnement mathématique sur la correction des programmes, y compris les contrats intelligents. Elle implique de transformer le modèle du système d'un contrat et ses spécifications en formules mathématiques (énoncés logiques).
L’objectif de la démonstration de théorèmes est de vérifier l’équivalence logique entre ces énoncés. L'« équivalence logique » (également appelée « bi-implication logique ») est un type de relation entre deux énoncés tels que le premier énoncé est vrai si et seulement si le second énoncé est vrai.
La relation requise (équivalence logique) entre les déclarations sur le modèle d'un contrat et sa propriété est formulée comme une déclaration prouvable (appelée théorème). En utilisant un système formel d'inférence, le prouveur de théorème automatisé peut vérifier la validité du théorème. En d'autres termes, un prouveur de théorème peut prouver de manière concluante que le modèle d'un contrat intelligent correspond précisément à ses spécifications.
Alors que la vérification de modèles modélise les contrats en tant que systèmes de transition avec des états finis, la démonstration de théorèmes peut traiter l'analyse des systèmes à états infinis. Cependant, cela signifie qu'un prouveur de théorème automatisé ne peut pas toujours savoir si un problème logique est “ décidable ” ou non.
Par conséquent, une assistance humaine est souvent nécessaire pour guider le prouveur de théorèmes dans la dérivation des preuves de correction. L'utilisation de l'effort humain dans la démonstration de théorèmes le rend plus coûteux à utiliser que la vérification de modèle, qui est entièrement automatisée.
Exécution symbolique
L’exécution symbolique est une méthode d’analyse d’un contrat intelligent en exécutant des fonctions à l’aide de valeurs symboliques (par exemple, x > 5) au lieu de valeurs concrètes (par exemple, x == 5). En tant que technique de vérification formelle, l’exécution symbolique est utilisée pour raisonner formellement sur les propriétés au niveau de la trace dans le code d’un contrat.
L'exécution symbolique représente une trace d'exécution sous forme d'une formule mathématique sur des valeurs d'entrée symboliques, autrement appelée prédicat de chemin. Un Solveur SMT
est utilisé pour vérifier si un prédicat de chemin est "satisfaisable" (c'est-à-dire, s'il existe une valeur qui peut satisfaire la formule). Si un chemin vulnérable est satisfaisable, le solveur SMT générera une valeur concrète qui déclenchera l'exécution vers ce chemin.
Supposons qu'une fonction de contrat intelligent prend en entrée une valeur uint (x) et revient en arrière lorsque x est supérieur à 5 et également inférieur à 10. Trouver une valeur pour x qui déclenche l'erreur en utilisant une procédure de test normale nécessiterait de passer par des dizaines de cas de test (ou plus) sans l'assurance de trouver effectivement une entrée déclenchant l'erreur.
Inversement, un outil d'exécution symbolique exécuterait la fonction avec la valeur symbolique : X > 5 ∧ X < 10 (c'est-à-dire, x est supérieur à 5 ET x est inférieur à 10). Le prédicat de chemin associé x = X > 5 ∧ X < 10 serait ensuite donné à un solveur SMT pour résoudre. Si une valeur particulière satisfait la formule x = X > 5 ∧ X < 10, le solveur SMT la calculera, par exemple, le solveur pourrait produire 7 comme valeur pour x.
Parce que l'exécution symbolique repose sur les entrées d'un programme, et que l'ensemble des entrées à explorer pour atteindre tous les états accessibles est potentiellement infini, il s'agit toujours d'une forme de test. Cependant, comme le montre l'exemple, l'exécution symbolique est plus efficace que les tests réguliers pour trouver les entrées qui déclenchent des violations de propriété.
De plus, l'exécution symbolique produit moins de faux positifs que d'autres techniques basées sur les propriétés (par exemple, le fuzzing) qui génèrent aléatoirement des entrées pour une fonction. Si un état d'erreur est déclenché lors de l'exécution symbolique, il est alors possible de générer une valeur concrète qui déclenche l'erreur et de reproduire le problème.
L'exécution symbolique peut également fournir un certain degré de preuve mathématique de la correction. Considérez l'exemple suivant d'une fonction de contrat avec protection contre les débordements :
Une trace d'exécution qui entraîne un débordement d'entier devrait satisfaire la formule : z = x + y ET (z ≥ x) ET (z>y) ET (z < x OU z < y) Une telle formule est peu probable à résoudre, ce qui prouve mathématiquement que la fonction safe_add ne déborde jamais.
Pourquoi utiliser la vérification formelle pour les contrats intelligents ?
Besoin de fiabilité
La vérification formelle est utilisée pour évaluer la justesse des systèmes critiques pour la sécurité dont la défaillance peut avoir des conséquences dévastatrices, telles que la mort, les blessures ou la ruine financière. Les contrats intelligents sont des applications de grande valeur contrôlant d'énormes quantités de valeur, et des erreurs simples de conception peuvent conduire à pertes irrécupérables pour les utilisateurs
(s’ouvre dans un nouvel onglet)
. Cependant, la vérification formelle d’un contrat avant son déploiement peut augmenter les garanties qu’il fonctionnera comme prévu une fois exécuté sur la blockchain.
La fiabilité est une qualité très recherchée dans tout contrat intelligent, surtout parce que le code déployé dans la machine virtuelle Ethereum (EVM) est généralement immuable. Avec les mises à jour post-lancement pas facilement accessibles, la nécessité de garantir la fiabilité des contrats rend la vérification formelle nécessaire. La vérification formelle est capable de détecter des problèmes délicats, tels que les débordements et les débordements d'entiers, la ré-entrance et les mauvaises optimisations de gaz, qui peuvent échapper aux auditeurs et testeurs.
Prouver la justesse fonctionnelle
Le test de programme est la méthode la plus courante pour prouver qu'un contrat intelligent satisfait certaines exigences. Cela implique d'exécuter un contrat avec un échantillon des données qu'il est censé gérer et d'analyser son comportement. Si le contrat renvoie les résultats attendus pour les données d'échantillonnage, alors les développeurs ont la preuve objective de sa correction.
Cependant, cette approche ne peut pas prouver l'exécution correcte pour les valeurs d'entrée qui ne font pas partie de l'échantillon. Par conséquent, tester un contrat peut aider à détecter des bugs (c'est-à-dire si certains chemins de code ne parviennent pas à renvoyer les résultats souhaités lors de l'exécution), mais cela ne peut pas prouver de manière concluante l'absence de bugs.
Inversement, la vérification formelle peut prouver formellement qu'un contrat intelligent satisfait les exigences pour une gamme infinie d'exécutions sans exécuter le contrat du tout. Cela nécessite la création d'une spécification formelle décrivant précisément les comportements corrects du contrat et le développement d'un modèle formel (mathématique) du système du contrat. Ensuite, nous pouvons suivre une procédure de preuve formelle pour vérifier la cohérence entre le modèle du contrat et sa spécification.
Avec la vérification formelle, la question de vérifier si la logique commerciale d'un contrat satisfait aux exigences est une proposition mathématique qui peut être prouvée ou réfutée. En prouvant formellement une proposition, nous pouvons vérifier un nombre infini de cas de test avec un nombre fini d'étapes. De cette manière, la vérification formelle a de meilleures perspectives de prouver qu'un contrat est fonctionnellement correct par rapport à une spécification.
Cibles de vérification idéales
Une cible de vérification décrit le système à vérifier de manière formelle. La vérification formelle est mieux utilisée dans les "systèmes embarqués" (petits morceaux de logiciel simples faisant partie d'un système plus large). Ils sont également idéaux pour les domaines spécialisés qui ont peu de règles, car cela rend plus facile la modification d'outils pour vérifier les propriétés spécifiques au domaine.
Les contrats intelligents - du moins, dans une certaine mesure - satisfont aux deux exigences. Par exemple, la petite taille des contrats Ethereum les rend propices à la vérification formelle. De même, l'EVM suit des règles simples, ce qui facilite la spécification et la vérification des propriétés sémantiques des programmes s'exécutant dans l'EVM.
Cycle de développement plus rapide
Les techniques de vérification formelle, telles que la vérification de modèle et l'exécution symbolique, sont généralement plus efficaces que l'analyse régulière du code de contrat intelligent (effectuée lors des tests ou de l'audit). Cela est dû au fait que la vérification formelle repose sur des valeurs symboliques pour tester les assertions ("et si un utilisateur essaie de retirer n éther ?") contrairement aux tests qui utilisent des valeurs concrètes ("et si un utilisateur essaie de retirer 5 éther ?").
Les variables d'entrée symboliques peuvent couvrir plusieurs classes de valeurs concrètes, de sorte que les approches de vérification formelle promettent une couverture de code plus importante dans un laps de temps plus court. Lorsqu'il est utilisé efficacement, la vérification formelle peut accélérer le cycle de développement pour les développeurs.
La vérification formelle améliore également le processus de création d'applications décentralisées (dapps) en réduisant les erreurs coûteuses de conception. La mise à niveau des contrats (lorsque c'est possible) pour corriger les vulnérabilités nécessite une refonte approfondie des bases de code et davantage d'efforts de développement. La vérification formelle peut détecter de nombreuses erreurs dans les implémentations de contrats qui pourraient échapper aux testeurs et aux auditeurs, et offre une opportunité suffisante pour corriger ces problèmes avant le déploiement d'un contrat.
INCONVÉNIENTS DE LA VÉRIFICATION FORMELLE
Coût de la main-d'œuvre manuelle
La vérification formelle, en particulier la vérification semi-automatisée dans laquelle un humain guide le prouveur pour dériver des preuves de correction, nécessite beaucoup de travail manuel. De plus, la création d'une spécification formelle est une activité complexe qui exige un haut niveau de compétence.
Ces facteurs (effort et compétence) rendent la vérification formelle plus exigeante et coûteuse par rapport aux méthodes habituelles d'évaluation de la justesse des contrats, telles que les tests et les audits. Néanmoins, payer le coût d'un audit de vérification complet est pratique, étant donné le coût des erreurs dans les implémentations de contrats intelligents.
Faux négatifs
La vérification formelle ne peut vérifier que si l'exécution du contrat intelligent correspond à la spécification formelle. Il est donc important de s'assurer que la spécification décrit correctement les comportements attendus d'un contrat intelligent.
Si les spécifications sont mal rédigées, les violations des propriétés — qui indiquent des exécutions vulnérables — ne peuvent pas être détectées par l'audit de vérification formelle. Dans ce cas, un développeur pourrait supposer à tort que le contrat est exempt de bugs.
Problèmes de performance
La vérification formelle se heurte à un certain nombre de problèmes de performance. Par exemple, les problèmes d'explosion d'états et de chemins rencontrés lors de la vérification de modèle et de la vérification symbolique, respectivement, peuvent affecter les procédures de vérification. De plus, les outils de vérification formelle utilisent souvent des solveurs SMT et d'autres solveurs de contraintes dans leur couche sous-jacente, et ces solveurs reposent sur des procédures intensives en calcul.
De plus, il n'est pas toujours possible pour les vérificateurs de programme de déterminer si une propriété (décrite comme une formule logique) peut être satisfaite ou non (laproblème de décidabilité
“) parce qu'un programme pourrait ne jamais se terminer. En tant que tel, il peut être impossible de prouver certaines propriétés pour un contrat même s'il est bien spécifié.
OUTILS DE VÉRIFICATION FORMELLE POUR LES CONTRATS INTELLIGENTS ETHEREUM
Langages de spécification pour la création de spécifications formelles
Act : Act permet la spécification des mises à jour de stockage, des conditions pré/postérieures et des invariants de contrat. Sa suite d'outils dispose également de backends de preuve capables de prouver de nombreuses propriétés via Coq, des solveurs SMT ou hevm.
Scribble - Scribble transforme les annotations de code dans le langage de spécification Scribble en assertions concrètes qui vérifient la spécification.
Dafny - Dafny est un langage de programmation prêt à la vérification qui repose sur des annotations de haut niveau pour raisonner et prouver la correction du code.
Vérificateurs de programme pour vérifier la correction
Certora Prover - Certora Prover est un outil de vérification formelle automatique pour vérifier la correction du code dans les contrats intelligents. Les spécifications sont écrites en CVL (Certora Verification Language), les violations de propriété étant détectées à l'aide d'une combinaison d'analyse statique et de résolution de contraintes.
SMTChecker Solidity - Le SMTChecker de Solidity est un vérificateur de modèles intégré basé sur SMT (Satisfiability Modulo Theories) et la résolution de Horn. Il confirme si le code source d'un contrat correspond aux spécifications lors de la compilation et vérifie statiquement les violations des propriétés de sécurité.
solc-verify - solc-verify est une version étendue du compilateur Solidity qui peut effectuer une vérification formelle automatisée du code Solidity à l'aide d'annotations et d'une vérification de programme modulaire.
KEVM - KEVM est une sémantique formelle de la machine virtuelle Ethereum (EVM) écrite dans le cadre K. KEVM est exécutable et peut prouver certaines assertions liées aux propriétés en utilisant la logique de la portée.
Cadres logiques pour la démonstration de théorèmes
Isabelle - Isabelle/HOL est un assistant de preuve qui permet d'exprimer des formules mathématiques dans un langage formel et fournit des outils pour prouver ces formules. L'application principale est la formalisation des preuves mathématiques et en particulier la vérification formelle, qui inclut la vérification de la correction du matériel ou du logiciel informatique et la vérification des propriétés des langages et des protocoles informatiques.
Coq - Coq est un prouveur de théorèmes interactif qui vous permet de définir des programmes à l'aide de théorèmes et de générer de manière interactive des preuves de correction vérifiées par machine.
Outils basés sur l'exécution symbolique pour détecter des schémas vulnérables dans les contrats intelligents
Manticore - Un outil d'analyse de bytecode EVM basé sur l'exécution symbolique.
hevm - hevm est un moteur d'exécution symbolique et un vérificateur d'équivalence pour le bytecode EVM.
Mythril - Un outil d'exécution symbolique pour détecter les vulnérabilités dans les contrats intelligents Ethereum
Démenti:
- Cet article est repris de [ ]. Tous les droits d'auteur appartiennent à l'auteur original [**]. Si des objections sont soulevées concernant cette réimpression, veuillez contacter le Porte Apprendreéquipe, et ils s'en occuperont rapidement.
- Clause de non-responsabilité: Les vues et opinions exprimées dans cet article sont uniquement celles de l'auteur et ne constituent aucun conseil en investissement.
- Les traductions de l'article dans d'autres langues sont réalisées par l'équipe Gate Learn. Sauf mention contraire, la copie, la distribution ou le plagiat des articles traduits est interdit.
関連記事
Les meilleures plateformes de loterie en crypto-monnaie pour 2024
Guide sur la façon de changer de réseau dans MetaMask
Qu'est-ce que MetaMask ?
VÉRIFICATION FORMELLE DES CONTRATS INTELLIGENTS
QU'EST-CE QUE LA VÉRIFICATION FORMELLE ?
TYPES DE SPÉCIFICATIONS FORMELLES POUR LES CONTRATS INTELLIGENTS
TECHNIQUES POUR LA VÉRIFICATION FORMELLE DES CONTRATS INTELLIGENTS
INCONVÉNIENTS DE LA VÉRIFICATION FORMELLE
OUTILS DE VÉRIFICATION FORMELLE POUR LES CONTRATS INTELLIGENTS ETHEREUM
Contrats intelligentspermettent de créer des applications décentralisées, sans confiance et robustes qui introduisent de nouveaux cas d'utilisation et débloquent de la valeur pour les utilisateurs. Comme les contrats intelligents gèrent de grandes quantités de valeur, la sécurité est une considération cruciale pour les développeurs.
La vérification formelle est l'une des techniques recommandées pour améliorer sécurité des contrats intelligentsLa vérification formelle, qui utiliseméthodes formelles
pour spécifier, concevoir et vérifier des programmes, est utilisé depuis des années pour garantir la correction des systèmes matériels et logiciels critiques.
Lorsqu'il est mis en œuvre dans des contrats intelligents, la vérification formelle peut prouver que la logique commerciale d'un contrat répond à une spécification prédéfinie. Comparé à d'autres méthodes d'évaluation de la correction du code de contrat, telles que les tests, la vérification formelle offre des garanties plus solides qu'un contrat intelligent est fonctionnellement correct.
QU'EST-CE QUE LA VÉRIFICATION FORMELLE?
La vérification formelle fait référence au processus d'évaluation de la correction d'un système par rapport à une spécification formelle. En termes plus simples, la vérification formelle nous permet de vérifier si le comportement d'un système satisfait certaines exigences (c'est-à-dire, il fait ce que nous voulons).
Les comportements attendus du système (un smart contract dans ce cas) sont décrits à l'aide d'une modélisation formelle, tandis que les langages de spécification permettent la création de propriétés formelles. Les techniques de vérification formelle peuvent ensuite vérifier que l'implémentation d'un contrat est conforme à sa spécification et dériver une preuve mathématique de la correction de ce dernier. Lorsqu'un contrat satisfait sa spécification, on le décrit comme "fonctionnellement correct", "correct par conception" ou "correct par construction".
Qu'est-ce qu'un modèle formel ?
En informatique, un modèle formel
est une description mathématique d'un processus informatique. Les programmes sont abstraits en fonctions mathématiques (équations), le modèle décrivant comment les sorties des fonctions sont calculées en fonction d'une entrée.
Les modèles formels fournissent un niveau d'abstraction sur lequel l'analyse du comportement d'un programme peut être évaluée. L'existence de modèles formels permet la création d'une spécification formelle, qui décrit les propriétés souhaitées du modèle en question.
Différentes techniques sont utilisées pour modéliser des contrats intelligents en vue d'une vérification formelle. Par exemple, certains modèles sont utilisés pour raisonner sur le comportement de haut niveau d'un contrat intelligent. Ces techniques de modélisation appliquent une vue en boîte noire aux contrats intelligents, les considérant comme des systèmes qui acceptent des entrées et exécutent des calculs en fonction de ces entrées.
Les modèles de haut niveau se concentrent sur la relation entre les contrats intelligents et les agents externes, tels que les comptes détenus de manière externe (EOA), les comptes de contrat et l'environnement blockchain. De tels modèles sont utiles pour définir des propriétés qui spécifient comment un contrat doit se comporter en réponse à certaines interactions utilisateur.
Inversement, d'autres modèles formels se concentrent sur le comportement de bas niveau d'un smart contract. Alors que les modèles de haut niveau peuvent aider à raisonner sur la fonctionnalité d'un contrat, ils peuvent échouer à capturer les détails sur le fonctionnement interne de l'implémentation. Les modèles de bas niveau appliquent une vue en boîte blanche à l'analyse de programme et s'appuient sur des représentations de bas niveau des applications de smart contract, telles que les traces de programme et graphes de flux de contrôle
, pour raisonner sur les propriétés pertinentes à l'exécution d'un contrat.
Les modèles de bas niveau sont considérés comme idéaux car ils représentent l'exécution réelle d'un smart contract dans l'environnement d'exécution d'Ethereum (c.-à-d.EVM). Les techniques de modélisation de bas niveau sont particulièrement utiles pour établir les propriétés de sécurité critiques dans les contrats intelligents et détecter les vulnérabilités potentielles.
Qu'est-ce qu'une spécification formelle ?
Une spécification est simplement une exigence technique que doit satisfaire un système particulier. En programmation, les spécifications représentent des idées générales sur l'exécution d'un programme (c'est-à-dire ce que le programme devrait faire).
Dans le contexte des contrats intelligents, les spécifications formelles font référence à des propriétés, c'est-à-dire des descriptions formelles des exigences qu'un contrat doit satisfaire. Ces propriétés sont décrites comme des "invariants" et représentent des assertions logiques concernant l'exécution d'un contrat qui doivent rester vraies dans toutes les circonstances possibles, sans aucune exception.
Ainsi, nous pouvons considérer une spécification formelle comme un ensemble d'énoncés écrits dans un langage formel qui décrivent l'exécution prévue d'un contrat intelligent. Les spécifications portent sur les propriétés d'un contrat et définissent comment le contrat doit se comporter dans différentes circonstances. Le but de la vérification formelle est de déterminer si un contrat intelligent possède ces propriétés (invariants) et que ces propriétés ne sont pas violées lors de l'exécution.
Les spécifications formelles sont essentielles dans le développement de mises en œuvre sécurisées de contrats intelligents. Les contrats qui échouent à mettre en œuvre des invariants ou dont les propriétés sont violées lors de l'exécution sont sujets à des vulnérabilités qui peuvent nuire à la fonctionnalité ou causer des exploits malveillants.
TYPES DE SPÉCIFICATIONS FORMELLES POUR LES CONTRATS INTELLIGENTS
Les spécifications formelles permettent un raisonnement mathématique sur la correction de l'exécution du programme. Tout comme les modèles formels, les spécifications formelles peuvent capturer des propriétés de haut niveau ou le comportement de bas niveau d'une implémentation de contrat.
Les spécifications formelles sont dérivées en utilisant des éléments de logique de programme
, qui permettent un raisonnement formel sur les propriétés d'un programme. Une logique de programme a des règles formelles qui expriment (dans un langage mathématique) le comportement attendu d'un programme. Diverses logiques de programme sont utilisées dans la création de spécifications formelles, notamment logique de portée
(s'ouvre dans un nouvel onglet)
Les spécifications formelles des contrats intelligents peuvent être classées de manière générale comme des spécifications de haut niveau ou de bas niveau. Peu importe la catégorie à laquelle appartient une spécification, elle doit décrire de manière adéquate et non ambiguë la propriété du système en cours d'analyse.
Spécifications de haut niveau
Comme son nom l'indique, une spécification de haut niveau (également appelée "spécification orientée modèle") décrit le comportement de haut niveau d'un programme. Les spécifications de haut niveau modélisent un smart contract comme un machine à états finis
(FSM), qui peut passer d'un état à un autre en effectuant des opérations, la logique temporelle étant utilisée pour définir les propriétés formelles du modèle FSM.
sont des «règles de raisonnement sur des propositions qualifiées en termes de temps (par exemple, «J'ai toujours faim» ou «Je finirai par avoir faim»).» Lorsqu'ils sont appliqués à la vérification formelle, les logiques temporelles sont utilisées pour énoncer des assertions sur le comportement correct des systèmes modélisés sous forme de machines à états. Plus précisément, une logique temporelle décrit les états futurs dans lesquels un smart contract peut se trouver et comment il passe d'un état à un autre.
Les spécifications de haut niveau capturent généralement deux propriétés temporelles critiques pour les contrats intelligents : la sûreté et la vivacité. Les propriétés de sûreté représentent l'idée que « rien de mal ne se produit jamais » et expriment généralement l'invariance. Une propriété de sûreté peut définir des exigences générales en matière de logiciels, telles que la liberté de impasse
, ou exprimer les propriétés spécifiques au domaine pour les contrats (par exemple, les invariants sur le contrôle d'accès pour les fonctions, les valeurs admissibles des variables d'état, ou les conditions pour les transferts de jetons).
Prenons par exemple cette exigence de sécurité qui couvre les conditions d'utilisation des fonctions transfer() ou transferFrom() dans les contrats de jetons ERC-20 : "Le solde de l'expéditeur n'est jamais inférieur au montant demandé de jetons à envoyer.". Cette description en langage naturel d'une invariance de contrat peut être traduite en une spécification formelle (mathématique), qui peut ensuite être vérifiée rigoureusement pour sa validité.
Les propriétés de vivacité affirment que « quelque chose de bien finira par se produire » et concernent la capacité d'un contrat à progresser à travers différents états. Un exemple de propriété de vivacité est la « liquidité », qui fait référence à la capacité d'un contrat de transférer ses soldes aux utilisateurs sur demande. Si cette propriété est violée, les utilisateurs seraient incapables de retirer les actifs stockés dans le contrat, comme ce qui s'est passé avec le Incident de portefeuille de parité
.
Spécifications de bas niveau
Les spécifications de haut niveau prennent comme point de départ un modèle à états finis d'un contrat et définissent les propriétés souhaitées de ce modèle. En revanche, les spécifications de bas niveau (également appelées "spécifications orientées propriété") modélisent souvent des programmes (contrats intelligents) en tant que systèmes comprenant une collection de fonctions mathématiques et décrivent le comportement correct de ces systèmes.
En termes plus simples, les spécifications de bas niveau analysent les traces de programme et tentent de définir les propriétés d'un smart contrat sur ces traces. Les traces font référence à des séquences d'exécutions de fonctions qui modifient l'état d'un smart contrat; par conséquent, les spécifications de bas niveau aident à spécifier les exigences pour l'exécution interne d'un contrat.
Les spécifications formelles de bas niveau peuvent être données soit sous forme de propriétés de style Hoare, soit sous forme d'invariants sur les chemins d'exécution.
propriétés de style Hoare
fournit un ensemble de règles formelles pour raisonner sur la correction des programmes, y compris les contrats intelligents. Une propriété de style Hoare est représentée par un triple de Hoare {P}c{Q}, où c est un programme et P et Q sont des prédicats sur l'état de c (c'est-à-dire, le programme), formellement décrits comme des préconditions et des postconditions, respectivement.
Une condition préalable est un prédicat décrivant les conditions requises pour l'exécution correcte d'une fonction ; les utilisateurs appelant le contrat doivent satisfaire cette exigence. Une postcondition est un prédicat décrivant la condition qu'une fonction établit si elle est correctement exécutée ; les utilisateurs peuvent s'attendre à ce que cette condition soit vraie après avoir appelé la fonction. Une invariante dans la logique de Hoare est un prédicat préservé par l'exécution d'une fonction (c'est-à-dire qu'il ne change pas).
Les spécifications de style Hoare peuvent garantir soit une correction partielle soit une correction totale. L'implémentation d'une fonction de contrat est "partiellement correcte" si la précondition est vraie avant l'exécution de la fonction, et si l'exécution se termine, la postcondition est également vraie. La preuve de la correction totale est obtenue si une précondition est vraie avant l'exécution de la fonction, l'exécution est garantie de se terminer et lorsque c'est le cas, la postcondition est vraie.
Obtenir la preuve de la correction totale est difficile car certaines exécutions peuvent prendre du retard avant de se terminer, ou ne jamais se terminer du tout. Cela dit, la question de savoir si l'exécution se termine est sans doute un point discutable puisque le mécanisme de gaz d'Ethereum empêche les boucles de programmes infinies (l'exécution se termine soit avec succès, soit à cause d'une erreur de 'hors-gaz').
Les spécifications des contrats intelligents créés à l'aide de la logique de Hoare auront des préconditions, des postconditions et des invariants définis pour l'exécution des fonctions et des boucles dans un contrat. Les préconditions incluent souvent la possibilité d'entrées erronées dans une fonction, les postconditions décrivent la réponse attendue à de telles entrées (par exemple, en lançant une exception spécifique). De cette manière, les propriétés de style Hoare sont efficaces pour garantir la correction des implémentations de contrats.
De nombreux cadres de vérification formelle utilisent des spécifications de style Hoare pour prouver la correction sémantique des fonctions. Il est également possible d'ajouter des propriétés de style Hoare (sous forme d'assertions) directement au code du contrat en utilisant les déclarations require et assert en Solidity.
Les instructions require expriment une précondition ou un invariant et sont souvent utilisées pour valider les saisies de l'utilisateur, tandis que assert capture une postcondition nécessaire à la sécurité. Par exemple, un contrôle d'accès approprié pour les fonctions (un exemple d'une propriété de sécurité) peut être réalisé en utilisant require comme vérification de précondition sur l'identité du compte appelant. De même, un invariant sur les valeurs admissibles des variables d'état dans un contrat (par exemple, le nombre total de jetons en circulation) peut être protégé contre les violations en utilisant assert pour confirmer l'état du contrat après l'exécution de la fonction.
Propriétés de niveau de trace
Les spécifications basées sur les traces décrivent les opérations qui font passer un contrat entre différents états et les relations entre ces opérations. Comme expliqué précédemment, les traces sont des séquences d'opérations qui modifient l'état d'un contrat d'une manière particulière.
Cette approche repose sur un modèle de contrats intelligents en tant que systèmes de transition d'états avec certains états prédéfinis (décrits par des variables d'état) ainsi qu'un ensemble de transitions prédéfinies (décrites par des fonctions de contrat). De plus, un graphe de flux de contrôle
(s'ouvre dans un nouvel onglet)
(CFG), qui est une représentation graphique du flux d'exécution d'un programme, est souvent utilisé pour décrire la sémantique opérationnelle d'un contrat. Ici, chaque trace est représentée comme un chemin sur le graphe de flux de contrôle.
Principalement, les spécifications de niveau de trace sont utilisées pour raisonner sur les schémas d'exécution interne dans les contrats intelligents. En créant des spécifications de niveau de trace, nous affirmons les chemins d'exécution admissibles (c'est-à-dire, les transitions d'état) pour un contrat intelligent. En utilisant des techniques, telles que l'exécution symbolique, nous pouvons vérifier formellement que l'exécution ne suit jamais un chemin non défini dans le modèle formel.
Utilisons un exemple de DAOcontrat qui comporte certaines fonctions accessibles au public pour décrire les propriétés de niveau de trace. Ici, nous supposons que le contrat DAO permet aux utilisateurs d'effectuer les opérations suivantes :
- Déposer des fonds
- Vote sur une proposition après avoir déposé des fonds
- Demander un remboursement s'ils ne votent pas sur une proposition
Les propriétés de niveau de trace d'exemple pourraient être « les utilisateurs qui ne déposent pas de fonds ne peuvent pas voter sur une proposition » ou « les utilisateurs qui ne votent pas sur une proposition devraient toujours pouvoir réclamer un remboursement ». Ces propriétés affirment des séquences d'exécution préférées (le vote ne peut pas avoir lieu avant le dépôt de fonds et la réclamation d'un remboursement ne peut pas avoir lieu après un vote sur une proposition).
TECHNIQUES POUR LA VÉRIFICATION FORMELLE DES CONTRATS INTELLIGENTS
Vérification de modèle
La vérification de modèle est une technique de vérification formelle dans laquelle un algorithme vérifie un modèle formel d'un contrat intelligent par rapport à sa spécification. Dans la vérification de modèle, les contrats intelligents sont souvent représentés comme des systèmes de transition d'états, tandis que les propriétés sur les états de contrat autorisés sont définies en utilisant la logique temporelle.
La vérification de modèle nécessite la création d'une représentation mathématique abstraite d'un système (c'est-à-dire, un contrat) et l'expression de propriétés de ce système en utilisant des formules enracinées danslogique propositionnelle
(s'ouvre dans un nouvel onglet)
. Cela simplifie la tâche de l'algorithme de vérification du modèle, à savoir prouver qu'un modèle mathématique satisfait une formule logique donnée.
La vérification de modèle dans la vérification formelle est principalement utilisée pour évaluer les propriétés temporelles qui décrivent le comportement d'un contrat dans le temps. Les propriétés temporelles des contrats intelligents comprennent la sécurité et la vivacité, que nous avons expliquées plus tôt.
Par exemple, une propriété de sécurité liée au contrôle d'accès (par exemple, Seul le propriétaire du contrat peut appeler selfdestruct) peut être écrite en logique formelle. Ensuite, l'algorithme de vérification de modèle peut vérifier si le contrat satisfait cette spécification formelle.
La vérification de modèle utilise l'exploration de l'espace d'états, ce qui implique la construction de tous les états possibles d'un contrat intelligent et la tentative de trouver des états atteignables entraînant des violations de propriété. Cependant, cela peut conduire à un nombre infini d'états (connu sous le nom de "problème d'explosion d'états"), d'où la dépendance des vérificateurs de modèle sur des techniques d'abstraction pour rendre possible l'analyse efficace des contrats intelligents.
Démonstration de théorème
La preuve de théorème est une méthode de raisonnement mathématique sur la correction des programmes, y compris les contrats intelligents. Elle implique de transformer le modèle du système d'un contrat et ses spécifications en formules mathématiques (énoncés logiques).
L’objectif de la démonstration de théorèmes est de vérifier l’équivalence logique entre ces énoncés. L'« équivalence logique » (également appelée « bi-implication logique ») est un type de relation entre deux énoncés tels que le premier énoncé est vrai si et seulement si le second énoncé est vrai.
La relation requise (équivalence logique) entre les déclarations sur le modèle d'un contrat et sa propriété est formulée comme une déclaration prouvable (appelée théorème). En utilisant un système formel d'inférence, le prouveur de théorème automatisé peut vérifier la validité du théorème. En d'autres termes, un prouveur de théorème peut prouver de manière concluante que le modèle d'un contrat intelligent correspond précisément à ses spécifications.
Alors que la vérification de modèles modélise les contrats en tant que systèmes de transition avec des états finis, la démonstration de théorèmes peut traiter l'analyse des systèmes à états infinis. Cependant, cela signifie qu'un prouveur de théorème automatisé ne peut pas toujours savoir si un problème logique est “ décidable ” ou non.
Par conséquent, une assistance humaine est souvent nécessaire pour guider le prouveur de théorèmes dans la dérivation des preuves de correction. L'utilisation de l'effort humain dans la démonstration de théorèmes le rend plus coûteux à utiliser que la vérification de modèle, qui est entièrement automatisée.
Exécution symbolique
L’exécution symbolique est une méthode d’analyse d’un contrat intelligent en exécutant des fonctions à l’aide de valeurs symboliques (par exemple, x > 5) au lieu de valeurs concrètes (par exemple, x == 5). En tant que technique de vérification formelle, l’exécution symbolique est utilisée pour raisonner formellement sur les propriétés au niveau de la trace dans le code d’un contrat.
L'exécution symbolique représente une trace d'exécution sous forme d'une formule mathématique sur des valeurs d'entrée symboliques, autrement appelée prédicat de chemin. Un Solveur SMT
est utilisé pour vérifier si un prédicat de chemin est "satisfaisable" (c'est-à-dire, s'il existe une valeur qui peut satisfaire la formule). Si un chemin vulnérable est satisfaisable, le solveur SMT générera une valeur concrète qui déclenchera l'exécution vers ce chemin.
Supposons qu'une fonction de contrat intelligent prend en entrée une valeur uint (x) et revient en arrière lorsque x est supérieur à 5 et également inférieur à 10. Trouver une valeur pour x qui déclenche l'erreur en utilisant une procédure de test normale nécessiterait de passer par des dizaines de cas de test (ou plus) sans l'assurance de trouver effectivement une entrée déclenchant l'erreur.
Inversement, un outil d'exécution symbolique exécuterait la fonction avec la valeur symbolique : X > 5 ∧ X < 10 (c'est-à-dire, x est supérieur à 5 ET x est inférieur à 10). Le prédicat de chemin associé x = X > 5 ∧ X < 10 serait ensuite donné à un solveur SMT pour résoudre. Si une valeur particulière satisfait la formule x = X > 5 ∧ X < 10, le solveur SMT la calculera, par exemple, le solveur pourrait produire 7 comme valeur pour x.
Parce que l'exécution symbolique repose sur les entrées d'un programme, et que l'ensemble des entrées à explorer pour atteindre tous les états accessibles est potentiellement infini, il s'agit toujours d'une forme de test. Cependant, comme le montre l'exemple, l'exécution symbolique est plus efficace que les tests réguliers pour trouver les entrées qui déclenchent des violations de propriété.
De plus, l'exécution symbolique produit moins de faux positifs que d'autres techniques basées sur les propriétés (par exemple, le fuzzing) qui génèrent aléatoirement des entrées pour une fonction. Si un état d'erreur est déclenché lors de l'exécution symbolique, il est alors possible de générer une valeur concrète qui déclenche l'erreur et de reproduire le problème.
L'exécution symbolique peut également fournir un certain degré de preuve mathématique de la correction. Considérez l'exemple suivant d'une fonction de contrat avec protection contre les débordements :
Une trace d'exécution qui entraîne un débordement d'entier devrait satisfaire la formule : z = x + y ET (z ≥ x) ET (z>y) ET (z < x OU z < y) Une telle formule est peu probable à résoudre, ce qui prouve mathématiquement que la fonction safe_add ne déborde jamais.
Pourquoi utiliser la vérification formelle pour les contrats intelligents ?
Besoin de fiabilité
La vérification formelle est utilisée pour évaluer la justesse des systèmes critiques pour la sécurité dont la défaillance peut avoir des conséquences dévastatrices, telles que la mort, les blessures ou la ruine financière. Les contrats intelligents sont des applications de grande valeur contrôlant d'énormes quantités de valeur, et des erreurs simples de conception peuvent conduire à pertes irrécupérables pour les utilisateurs
(s’ouvre dans un nouvel onglet)
. Cependant, la vérification formelle d’un contrat avant son déploiement peut augmenter les garanties qu’il fonctionnera comme prévu une fois exécuté sur la blockchain.
La fiabilité est une qualité très recherchée dans tout contrat intelligent, surtout parce que le code déployé dans la machine virtuelle Ethereum (EVM) est généralement immuable. Avec les mises à jour post-lancement pas facilement accessibles, la nécessité de garantir la fiabilité des contrats rend la vérification formelle nécessaire. La vérification formelle est capable de détecter des problèmes délicats, tels que les débordements et les débordements d'entiers, la ré-entrance et les mauvaises optimisations de gaz, qui peuvent échapper aux auditeurs et testeurs.
Prouver la justesse fonctionnelle
Le test de programme est la méthode la plus courante pour prouver qu'un contrat intelligent satisfait certaines exigences. Cela implique d'exécuter un contrat avec un échantillon des données qu'il est censé gérer et d'analyser son comportement. Si le contrat renvoie les résultats attendus pour les données d'échantillonnage, alors les développeurs ont la preuve objective de sa correction.
Cependant, cette approche ne peut pas prouver l'exécution correcte pour les valeurs d'entrée qui ne font pas partie de l'échantillon. Par conséquent, tester un contrat peut aider à détecter des bugs (c'est-à-dire si certains chemins de code ne parviennent pas à renvoyer les résultats souhaités lors de l'exécution), mais cela ne peut pas prouver de manière concluante l'absence de bugs.
Inversement, la vérification formelle peut prouver formellement qu'un contrat intelligent satisfait les exigences pour une gamme infinie d'exécutions sans exécuter le contrat du tout. Cela nécessite la création d'une spécification formelle décrivant précisément les comportements corrects du contrat et le développement d'un modèle formel (mathématique) du système du contrat. Ensuite, nous pouvons suivre une procédure de preuve formelle pour vérifier la cohérence entre le modèle du contrat et sa spécification.
Avec la vérification formelle, la question de vérifier si la logique commerciale d'un contrat satisfait aux exigences est une proposition mathématique qui peut être prouvée ou réfutée. En prouvant formellement une proposition, nous pouvons vérifier un nombre infini de cas de test avec un nombre fini d'étapes. De cette manière, la vérification formelle a de meilleures perspectives de prouver qu'un contrat est fonctionnellement correct par rapport à une spécification.
Cibles de vérification idéales
Une cible de vérification décrit le système à vérifier de manière formelle. La vérification formelle est mieux utilisée dans les "systèmes embarqués" (petits morceaux de logiciel simples faisant partie d'un système plus large). Ils sont également idéaux pour les domaines spécialisés qui ont peu de règles, car cela rend plus facile la modification d'outils pour vérifier les propriétés spécifiques au domaine.
Les contrats intelligents - du moins, dans une certaine mesure - satisfont aux deux exigences. Par exemple, la petite taille des contrats Ethereum les rend propices à la vérification formelle. De même, l'EVM suit des règles simples, ce qui facilite la spécification et la vérification des propriétés sémantiques des programmes s'exécutant dans l'EVM.
Cycle de développement plus rapide
Les techniques de vérification formelle, telles que la vérification de modèle et l'exécution symbolique, sont généralement plus efficaces que l'analyse régulière du code de contrat intelligent (effectuée lors des tests ou de l'audit). Cela est dû au fait que la vérification formelle repose sur des valeurs symboliques pour tester les assertions ("et si un utilisateur essaie de retirer n éther ?") contrairement aux tests qui utilisent des valeurs concrètes ("et si un utilisateur essaie de retirer 5 éther ?").
Les variables d'entrée symboliques peuvent couvrir plusieurs classes de valeurs concrètes, de sorte que les approches de vérification formelle promettent une couverture de code plus importante dans un laps de temps plus court. Lorsqu'il est utilisé efficacement, la vérification formelle peut accélérer le cycle de développement pour les développeurs.
La vérification formelle améliore également le processus de création d'applications décentralisées (dapps) en réduisant les erreurs coûteuses de conception. La mise à niveau des contrats (lorsque c'est possible) pour corriger les vulnérabilités nécessite une refonte approfondie des bases de code et davantage d'efforts de développement. La vérification formelle peut détecter de nombreuses erreurs dans les implémentations de contrats qui pourraient échapper aux testeurs et aux auditeurs, et offre une opportunité suffisante pour corriger ces problèmes avant le déploiement d'un contrat.
INCONVÉNIENTS DE LA VÉRIFICATION FORMELLE
Coût de la main-d'œuvre manuelle
La vérification formelle, en particulier la vérification semi-automatisée dans laquelle un humain guide le prouveur pour dériver des preuves de correction, nécessite beaucoup de travail manuel. De plus, la création d'une spécification formelle est une activité complexe qui exige un haut niveau de compétence.
Ces facteurs (effort et compétence) rendent la vérification formelle plus exigeante et coûteuse par rapport aux méthodes habituelles d'évaluation de la justesse des contrats, telles que les tests et les audits. Néanmoins, payer le coût d'un audit de vérification complet est pratique, étant donné le coût des erreurs dans les implémentations de contrats intelligents.
Faux négatifs
La vérification formelle ne peut vérifier que si l'exécution du contrat intelligent correspond à la spécification formelle. Il est donc important de s'assurer que la spécification décrit correctement les comportements attendus d'un contrat intelligent.
Si les spécifications sont mal rédigées, les violations des propriétés — qui indiquent des exécutions vulnérables — ne peuvent pas être détectées par l'audit de vérification formelle. Dans ce cas, un développeur pourrait supposer à tort que le contrat est exempt de bugs.
Problèmes de performance
La vérification formelle se heurte à un certain nombre de problèmes de performance. Par exemple, les problèmes d'explosion d'états et de chemins rencontrés lors de la vérification de modèle et de la vérification symbolique, respectivement, peuvent affecter les procédures de vérification. De plus, les outils de vérification formelle utilisent souvent des solveurs SMT et d'autres solveurs de contraintes dans leur couche sous-jacente, et ces solveurs reposent sur des procédures intensives en calcul.
De plus, il n'est pas toujours possible pour les vérificateurs de programme de déterminer si une propriété (décrite comme une formule logique) peut être satisfaite ou non (laproblème de décidabilité
“) parce qu'un programme pourrait ne jamais se terminer. En tant que tel, il peut être impossible de prouver certaines propriétés pour un contrat même s'il est bien spécifié.
OUTILS DE VÉRIFICATION FORMELLE POUR LES CONTRATS INTELLIGENTS ETHEREUM
Langages de spécification pour la création de spécifications formelles
Act : Act permet la spécification des mises à jour de stockage, des conditions pré/postérieures et des invariants de contrat. Sa suite d'outils dispose également de backends de preuve capables de prouver de nombreuses propriétés via Coq, des solveurs SMT ou hevm.
Scribble - Scribble transforme les annotations de code dans le langage de spécification Scribble en assertions concrètes qui vérifient la spécification.
Dafny - Dafny est un langage de programmation prêt à la vérification qui repose sur des annotations de haut niveau pour raisonner et prouver la correction du code.
Vérificateurs de programme pour vérifier la correction
Certora Prover - Certora Prover est un outil de vérification formelle automatique pour vérifier la correction du code dans les contrats intelligents. Les spécifications sont écrites en CVL (Certora Verification Language), les violations de propriété étant détectées à l'aide d'une combinaison d'analyse statique et de résolution de contraintes.
SMTChecker Solidity - Le SMTChecker de Solidity est un vérificateur de modèles intégré basé sur SMT (Satisfiability Modulo Theories) et la résolution de Horn. Il confirme si le code source d'un contrat correspond aux spécifications lors de la compilation et vérifie statiquement les violations des propriétés de sécurité.
solc-verify - solc-verify est une version étendue du compilateur Solidity qui peut effectuer une vérification formelle automatisée du code Solidity à l'aide d'annotations et d'une vérification de programme modulaire.
KEVM - KEVM est une sémantique formelle de la machine virtuelle Ethereum (EVM) écrite dans le cadre K. KEVM est exécutable et peut prouver certaines assertions liées aux propriétés en utilisant la logique de la portée.
Cadres logiques pour la démonstration de théorèmes
Isabelle - Isabelle/HOL est un assistant de preuve qui permet d'exprimer des formules mathématiques dans un langage formel et fournit des outils pour prouver ces formules. L'application principale est la formalisation des preuves mathématiques et en particulier la vérification formelle, qui inclut la vérification de la correction du matériel ou du logiciel informatique et la vérification des propriétés des langages et des protocoles informatiques.
Coq - Coq est un prouveur de théorèmes interactif qui vous permet de définir des programmes à l'aide de théorèmes et de générer de manière interactive des preuves de correction vérifiées par machine.
Outils basés sur l'exécution symbolique pour détecter des schémas vulnérables dans les contrats intelligents
Manticore - Un outil d'analyse de bytecode EVM basé sur l'exécution symbolique.
hevm - hevm est un moteur d'exécution symbolique et un vérificateur d'équivalence pour le bytecode EVM.
Mythril - Un outil d'exécution symbolique pour détecter les vulnérabilités dans les contrats intelligents Ethereum
Démenti:
- Cet article est repris de [ ]. Tous les droits d'auteur appartiennent à l'auteur original [**]. Si des objections sont soulevées concernant cette réimpression, veuillez contacter le Porte Apprendreéquipe, et ils s'en occuperont rapidement.
- Clause de non-responsabilité: Les vues et opinions exprimées dans cet article sont uniquement celles de l'auteur et ne constituent aucun conseil en investissement.
- Les traductions de l'article dans d'autres langues sont réalisées par l'équipe Gate Learn. Sauf mention contraire, la copie, la distribution ou le plagiat des articles traduits est interdit.
関連記事
Les meilleures plateformes de loterie en crypto-monnaie pour 2024
Guide sur la façon de changer de réseau dans MetaMask