Tests symboliques avec Halmos : Tirer parti des tests existants pour une vérification formelle

La vérification formelle - le processus d'utilisation de méthodes mathématiques pour «inspecter» un programme ou un contrat intelligent sur un nombre quelconque d'entrées - est généralement considérée comme l'alternative la plus concise et la plus complète aux tests traditionnels pour écrire un code de meilleure qualité et plus sécurisé. Mais en réalité, la vérification formelle est un processus ouvert et interactif. Tout comme les tests unitaires, les développeurs doivent définir et superposer dynamiquement des spécifications formelles, en itérant sur leur approche à mesure que leur code et leurs analyses évoluent. De plus, la vérification formelle n'est aussi efficace que ses spécifications, qui peuvent prendre du temps à écrire (et s'accompagnent souvent d'une courbe d'apprentissage abrupte). 

Pour de nombreux développeurs qui trouvent le processus intimidant, les tests unitaires sont souvent la voie la plus rentable et la plus rapide pour déterminer l'exactitude d'un programme. En pratique, la vérification formelle n'est pas une alternative plus complète aux tests unitaires, mais une alternative complémentaire. Ces processus ont des forces et des limites différentes, offrant une assurance encore plus grande lorsqu'ils sont utilisés ensemble. Les développeurs auront toujours besoin d'écrire des tests unitaires - et si nous pouvions utiliser les mêmes propriétés pour la vérification formelle ?

Halmos, notre outil de vérification formelle open source, permet aux développeurs de réutiliser les mêmes propriétés écrites pour les tests unitaires pour les spécifications formelles via des tests symboliques. Plutôt que d'avoir à créer un ensemble robuste de propriétés dès le départ, les développeurs peuvent éviter le travail en double et améliorer leurs tests quelques spécifications à la fois sans repartir de zéro. Nous avons conçu cet outil pour être utilisé, avec d'autres dans le processus de vérification formelle, comme une passerelle vers la vérification formelle ; les développeurs peuvent commencer par quelques analyses avec un minimum d'effort, avant d'en ajouter d'autres plus tard dans le processus.

Dans cet article, nous couvrons les défis de la vérification formelle et la possibilité de combler le fossé entre les tests unitaires et la vérification formelle avec des tests symboliques. Nous parcourons ensuite une démonstration de Halmos en utilisant le code de contrat intelligent existant et jetons un coup d'œil aux autres outils de vérification formels (dont beaucoup sont open source) disponibles pour les développeurs.

Vérification formelle vs tests

Vérification formelle - généralement préféré par les développeurs de blockchain pour sa rigueur et son exhaustivité - est le processus de prouver l'exactitude d'un programme en vérifiant qu'il satisfait certaines propriétés d'exactitude. Les propriétés, qui sont spécifiques au programme, sont généralement fournies en externe et exprimées à l'aide d'un langage formel ou d'une notation pris en charge par l'outil de vérification utilisé. Les développeurs perçoivent souvent la vérification formelle comme une solution à bouton-poussoir pour tester automatiquement les propriétés dans tous les scénarios possibles, mais en réalité, la vérification formelle peut être un processus laborieux et hautement interactif.

Comme la vérification formelle, les tests unitaires impliquent d'évaluer si un programme fonctionne comme prévu ; test, cependant, ne vérifie que le comportement du programme pour quelques entrées, tandis que la vérification formelle peut vérifier TOUTE entrées possibles. Les tests et la vérification formelle nécessitent une description du comportement attendu du programme (avec des cas de test utilisés dans les tests et des spécifications formelles utilisées dans la vérification formelle). Mais, lorsqu'ils sont utilisés ensemble, ils peuvent fournir un examen plus approfondi d'un programme. Les tests, par exemple, sont efficaces pour trouver des bogues et des erreurs simples, mais sont généralement plus rapides et plus faciles à réaliser. La vérification formelle, bien que plus lourde à utiliser, est suffisamment puissante pour prouver l'absence d'erreurs ou révéler des bogues subtils faciles à manquer lors des tests ou des revues de code.

Frais généraux de spécification

L'un des principaux défis de la vérification formelle est la surcharge de rédaction et de maintien des spécifications formelles. Ce processus implique souvent la tâche fastidieuse d'écrire manuellement les spécifications à l'aide d'un langage spécialisé (que de nombreux développeurs devront d'abord apprendre). Le processus est également incrémentiel, en commençant généralement par écrire des propriétés simples et en les vérifiant d'abord, puis en ajoutant progressivement des propriétés plus complexes par dessus. Comme les tests, il s'agit d'un processus ouvert, sans point d'arrêt clair, et on ne peut ajouter qu'autant de propriétés que possible dans le laps de temps disponible. De plus, lorsque les développeurs modifient le code en cours de vérification, ils doivent également mettre à jour leurs spécifications existantes, ce qui entraîne des efforts de maintenance supplémentaires. Ces facteurs peuvent faire de la vérification formelle une tâche ardue pour certains développeurs qui hésitent à s'engager dans des frais généraux supplémentaires.

Et bien que les tests et la vérification formelle puissent améliorer la qualité du code lorsqu'ils sont utilisés ensemble, les deux nécessitent des descriptions (parfois similaires) du comportement attendu d'un programme dans différents langages et formats. La rédaction et la maintenance de ces descriptions demandent beaucoup de travail, et la maintenance de deux formes différentes de la même description peut sembler un effort en double. Cela soulève la question suivante : est-il possible de décrire le comportement attendu d'une manière que les développeurs puissent utiliser à la fois pour les tests et la vérification ?

Combler le fossé entre les tests et la vérification formelle avec les tests symboliques et Halmos

Le test symbolique, la pratique consistant à exécuter des tests avec des entrées symboliques, est une méthode de vérification formelle efficace qui réduit la surcharge de spécification. Cette approche permet d'utiliser les mêmes cas de test pour les tests et la vérification formelle. Contrairement aux tests traditionnels, qui vérifient qu'un programme fonctionne correctement pour un ensemble limité d'entrées, les tests symboliques vérifient le programme pour toutes les entrées possibles, par conséquent, un programme qui réussit les tests symboliques peut être considéré comme formellement vérifié.

Halmos est un outil de vérification formelle conçu pour les tests symboliques. Au lieu d'exiger des spécifications distinctes ou d'apprendre un nouveau langage, Halmos utilise les tests existants comme spécifications formelles. L'exécution de tests via Halmos vérifiera automatiquement qu'ils réussissent pour toutes les entrées possibles ou fournira des contre-exemples. Cela élimine non seulement le besoin d'écrire des spécifications supplémentaires, mais permet également la réutilisation de tests écrits pour les tests unitaires ou le fuzzing, à des fins de vérification formelle.

Les développeurs disposent ainsi d'une plus grande flexibilité pour choisir parmi une gamme d'options d'assurance qualité, y compris les tests unitaires, le fuzzing et la vérification formelle, en fonction de leurs besoins actuels. Par exemple, les tests peuvent identifier rapidement des erreurs simples, éventuellement à l'aide d'un fuzzer qui génère des entrées aléatoires, puis Halmos peut encore augmenter la confiance dans l'exactitude du programme pour toutes les entrées.

Exemple : test de la isPowerOfTwo() fonction

A titre d'exemple, considérons ce qui suit isPowerOfTwo() fonction qui détermine si un nombre donné est une puissance de deux. Cette fonction utilise un algorithme de manipulation de bits pour l'efficacité, mais il peut être difficile de prouver son exactitude, en particulier dans le cas où l'entrée n'est pas une puissance de deux.

Imaginez le test suivant pour le isPowerOfTwo() fonction : elle compare la sortie réelle de la fonction avec la sortie attendue pour une entrée donnée. Il s'agit d'un test paramétré (également appelé test basé sur les propriétés), ce qui signifie que vous pouvez facilement l'exécuter avec différentes valeurs d'entrée, éventuellement avec des outils de fuzz comme Foundry.

Vous pouvez utiliser ce test pour examiner la isPowerOfTwo() fonction via des tests unitaires ou des tests fuzz, en l'exécutant avec une sélection d'entrées. Des tests comme ceux-ci ne peuvent pas prouver formellement l'exactitude de la fonction, car il est irréalisable sur le plan informatique d'exécuter le test pour chaque entrée possible.

Halmos, cependant, permet aux développeurs de réutiliser ces tests préexistants pour une vérification formelle avec seulement un petit effort supplémentaire. L'outil vérifie que les tests réussissent pour toutes les entrées possibles en effectuant une exécution symbolique du test, puis en vérifiant que l'assertion n'est jamais violée (ou, si l'assertion is violé, en donnant un contre-exemple). Cela signifie que si le test réussit Halmos, l'exactitude de la fonction est formellement vérifiée, ce qui signifie que l'algorithme est correctement implémenté et a été traduit avec précision par le compilateur en bytecode.

Limitation : Exécution symbolique bornée

Il n'est généralement pas possible d'effectuer des tests symboliques complets entièrement automatiques, car cela nécessiterait de résoudre le problème d'arrêt, qui est connu pour être indécidable. L'une des raisons en est qu'il est souvent impossible de déterminer automatiquement combien de fois une boucle doit itérer symboliquement. Par conséquent, une vérification formelle entièrement automatique est généralement indécidable.

Compte tenu de ces limites fondamentales, Halmos donne la priorité à l'automatisation plutôt qu'à l'exhaustivité. À cette fin, Halmos est conçu pour effectuer un raisonnement symbolique borné pour des boucles illimitées (où le nombre d'itérations dépend des entrées du programme) ou des tableaux de longueur variable (y compris des chaînes). Cela sacrifie une certaine exhaustivité, mais permet à Halmos d'éviter de demander à l'utilisateur de fournir des annotations supplémentaires telles que des invariants de boucle.

Par exemple, considérons la version itérative suivante du isPowerOfTwo() fonction, qui comporte une boucle while illimitée, où le nombre d'itérations de la boucle est déterminé par le nombre minimum de bits requis pour représenter le nombre d'entrée.

Halmos itère symboliquement cette boucle illimitée uniquement jusqu'à une limite spécifiée. Par exemple, si la limite est définie sur 3, Halmos itérera la boucle au plus 3 fois et ne prendra pas en compte les valeurs d'entrée qui entraîneraient l'itération de la boucle plus de 3 fois (c'est-à-dire toute valeur supérieure ou égale à 2 ^ 3 ). Dans ce cas particulier, fixer la limite à 256 ou plus permettrait à Halmos d'être complet.

Démo : vérification formelle de l'ERC721A avec Halmos

Pour démontrer les capacités de Halmos, nous l'avons utilisé pour tester symboliquement et vérifier formellement ERC721A, une implémentation hautement optimisée pour le gaz de la norme ERC721 qui permet la frappe par lots à presque le même coût que la frappe unique. ERC721A comprend plusieurs innovations optimisations pour atteindre cette efficacité ; par exemple, le gaz peut être économisé en retardant les mises à jour des données de propriété du jeton jusqu'à ce que le jeton soit transféré, et non au moment de la frappe. Cela nécessite l'utilisation de structures de données et d'algorithmes complexes pour récupérer efficacement les informations de propriété à partir de la structure de données paresseuse. Et bien que cette optimisation améliore l'efficacité du gaz, elle augmente également la complexité du code et rend difficile la preuve de l'exactitude de l'implémentation. Cela fait de l'ERC721A un bon candidat pour la vérification formelle, car il peut accroître la confiance dans la mise en œuvre et profiter aux utilisateurs potentiels.

Propriétés des tests symboliques

Étant donné que les tests existants pour ERC721A ont été écrits en JavaScript avec Hardhat (qui n'est actuellement pas pris en charge par Halmos), nous avons écrit de nouveaux tests dans Solidity pour les principales fonctions de point d'entrée : mint(), burn()et la transfer(). Ces tests ont vérifié que chaque fonction met correctement à jour la propriété et l'équilibre des jetons, et n'affecte que les utilisateurs concernés sans modifier l'équilibre ou la propriété des autres utilisateurs. Ce dernier n'est pas trivial à prouver en raison de l'utilisation de l'algorithme de structure de données paresseux dans ERC721A. Par exemple, le test suivant vérifie que le transfer() la fonction met correctement à jour la propriété du jeton spécifié :

Un autre test vérifie que le transfer() fonction ne modifie pas le solde pour les autres adresses, ce qui est difficile à prouver comme mentionné précédemment :

Résultats de la vérification

Nous avons mené une expérience de vérification en utilisant Halmos sur le contrat intelligent ERC721A en écrivant un total de 19 tests. Les tests ont été effectués via Halmos avec une boucle déroulante liée de 3, ce qui a pris 16 minutes. La répartition du temps de vérification peut être consultée dans le tableau ci-dessous. L'expérience a été menée sur un MacBook Pro avec une puce M1 Pro et 16 Go de mémoire.

Teste	Heure (s)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdUnchanged	1.40
testGraverAutreÉquilibrePréservation	5.69
testGraverAutrePropriétéPréservation	189.70
testBurnOwnershipUpdate	3.81
testBurnRequirements	71.95
testMintBalanceMise à jour	0.20
testMintNextTokenIdUpdate	0.18
testMintAutreÉquilibrePréservation	0.26
testMintAutrePropriétéPréservation	5.74
testMintOwnershipUpdate	1.38
testMintExigences	0.09
testTransferBalanceInchangé	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdUnchanged	4.47
testTransferAutreBalancePreservation	19.57
testTransferOtherOwnershipPreservation	430.61
testTransferOwnershipUpdatetestTransferOwnershipUpdate	18.71
testTransferRequirementstestTransferRequirements	149.18

Alors que la plupart des tests ont été effectués en quelques secondes, certains d'entre eux ont pris plusieurs minutes. Ces tests chronophages étaient difficiles à vérifier en raison de la nature complexe des cas à examiner et étaient étroitement liés à l'exactitude de l'algorithme de structure de données paresseux.

Dans l'ensemble, les résultats de cette expérience indiquent que Halmos est en mesure de vérifier efficacement l'exactitude du code de contrat intelligent. Il offre une confiance accrue dans l'intégrité du code, malgré la complexité et les cas marginaux potentiels du contrat intelligent.

Expérimenter avec des bogues injectés

Pour démontrer l'efficacité du raisonnement borné de Halmos, nous l'avons utilisé pour détecter des bogues dans une version précédente du contrat ERC721A. Cette version présentait un problème qui gérait mal le débordement arithmétique et permettait potentiellement la création par lots d'un grand nombre de jetons, ce qui pouvait rompre l'intégrité de la structure de données paresseuse et entraîner la perte de la propriété de certains utilisateurs (un problème résolu dans la version actuelle). Nous avons exécuté le même ensemble de 19 tests pour ERC721A sur la version boguée, et Halmos a pu trouver un contre-exemple pour les propriétés du mint() fonction. Plus précisément, Halmos a fourni des valeurs d'entrée qui ont conduit au scénario d'exploitation décrit ci-dessus. Les résultats de cette expérience indiquent que, malgré son caractère incomplet, le raisonnement borné de Halmos peut être un moyen efficace de détecter et de prévenir les bogues exploitables dans les contrats intelligents.

Travaux connexes

Des outils de vérification formels pour le bytecode du contrat intelligent Ethereum ont été développés par différentes équipes. Ces outils, y compris Halmos, peuvent être utilisés pour aider à garantir la sécurité et l'exactitude des contrats intelligents. La comparaison et la compréhension des différentes fonctionnalités, capacités et limites de ces outils peuvent aider les développeurs à choisir celui qui convient le mieux à leurs besoins uniques.

Bien que Halmos soit un ajout précieux à l'ensemble d'outils disponibles pour la vérification intelligente des contrats, il est destiné à compléter (et non à remplacer) les outils existants. Les développeurs peuvent combiner Halmos avec d'autres outils pour atteindre un niveau d'assurance plus élevé dans leurs contrats. Ci-dessous, nous comparons Halmos avec quelques outils formels sélectionnés prenant en charge le bytecode EVM.

• K est un puissant cadre de vérification formelle qui permet la vérification déductive et la démonstration interactive de théorèmes. Sa théorie sous-jacente et sa mise en œuvre offrent un haut niveau d'expressivité, ce qui le rend adapté à la vérification de programmes et d'algorithmes complexes. Cependant, il convient de noter que K n'est pas conçu avec un accent particulier sur la vérification automatisée et manque de certaines fonctionnalités d'automatisation qui peuvent nécessiter plus d'efforts manuels pendant le processus de vérification. Pour utiliser le framework K, les spécifications formelles sont écrites dans le langage K, qui doit être appris avant utilisation. Sa force est particulièrement utile pour vérifier des systèmes complexes, qui peuvent être difficiles à analyser à l'aide d'un raisonnement automatisé.
• Certora est un outil de vérification formel pour les contrats intelligents qui se concentre sur la vérification automatisée et prend en charge la vérification de modèle limité, similaire à Halmos. Pour utiliser Certora, les développeurs doivent apprendre leur nouveau langage, CVL, afin de rédiger un cahier des charges. Ce langage permet la description concise de nombreuses propriétés critiques par le biais d'invariants de contrat, une fonctionnalité que Halmos ne prend actuellement pas en charge. Bien qu'il s'agisse d'un outil propriétaire à source fermée, Certora fournit un outil de vérification formel robuste, avec un développement continu et un bon support utilisateur.
  
  Halmos, d'autre part, est un outil open source qui est à plus petite échelle et qui manque actuellement de certaines fonctionnalités fournies par Certora, mais il est destiné à servir de bien public et est conçu comme une solution de niche pour vérifier rapidement les contrats intelligents sans la nécessité d'une configuration et d'une maintenance étendues.
• HEVM est un autre outil de vérification formelle similaire à Halmos. Il faisait auparavant partie de DappTools, qui est un précurseur de Foundry. HEVM et Halmos ont la particularité de ne pas nécessiter de spécification distincte et peuvent symboliquement exécuter des tests existants pour identifier les violations d'assertion. Cela permet aux utilisateurs d'utiliser les deux outils de manière interchangeable ou de les exécuter en parallèle pour les mêmes tests, ce qui leur offre plusieurs options pour les tests symboliques.
  
  Il convient de noter que, malgré leurs similitudes, HEVM et Halmos ont été développés indépendamment et diffèrent dans leurs détails de mise en œuvre ; notamment en termes d'optimisations et de stratégies de raisonnement symbolique. De plus, HEVM est écrit en Haskell, tandis que Halmos est écrit en Python, offrant une exposition au riche écosystème Python. La possibilité d'utiliser les deux outils offre aux utilisateurs plus de flexibilité et d'options pour garantir la sécurité et l'exactitude des contrats intelligents.

Halmos est open source, et actuellement en phase bêta. Nous travaillons activement sur de nouveaux Caractéristiques et fonctionnalités, y compris les codes de triche Foundry et plusieurs autres fonctionnalités clés d'utilisation. Nous apprécierions grandement vos réflexions sur les fonctionnalités les plus importantes et nous serions heureux de recevoir vos commentaires, suggestions et contributions pour faire de Halmos un meilleur outil pour tout le monde.

**

Les opinions exprimées ici sont celles du personnel individuel d'AH Capital Management, LLC (« a16z ») cité et ne sont pas les opinions d'a16z ou de ses sociétés affiliées. Certaines informations contenues ici ont été obtenues de sources tierces, y compris de sociétés de portefeuille de fonds gérés par a16z. Bien qu'elles proviennent de sources considérées comme fiables, a16z n'a pas vérifié ces informations de manière indépendante et ne fait aucune déclaration quant à l'exactitude actuelle ou durable des informations ou à leur pertinence dans une situation donnée. De plus, ce contenu peut inclure des publicités de tiers ; a16z n'a pas examiné ces publicités et n'approuve aucun contenu publicitaire qu'elles contiennent.

Ce contenu est fourni à titre informatif uniquement et ne doit pas être considéré comme un conseil juridique, commercial, d'investissement ou fiscal. Vous devriez consulter vos propres conseillers sur ces questions. Les références à des titres ou à des actifs numériques sont uniquement à des fins d'illustration et ne constituent pas une recommandation d'investissement ou une offre de fournir des services de conseil en investissement. En outre, ce contenu n'est ni destiné ni destiné à être utilisé par des investisseurs ou des investisseurs potentiels, et ne peut en aucun cas être invoqué pour prendre une décision d'investir dans un fonds géré par a16z. (Une offre d'investissement dans un fonds a16z ne sera faite que par le mémorandum de placement privé, le contrat de souscription et toute autre documentation pertinente de ce fonds et doit être lu dans son intégralité.) Tous les investissements ou sociétés de portefeuille mentionnés, référencés ou décrits ne sont pas représentatifs de tous les investissements dans des véhicules gérés par a16z, et rien ne garantit que les investissements seront rentables ou que d'autres investissements réalisés à l'avenir auront des caractéristiques ou des résultats similaires. Une liste des investissements effectués par des fonds gérés par Andreessen Horowitz (à l'exclusion des investissements pour lesquels l'émetteur n'a pas autorisé a16z à divulguer publiquement ainsi que des investissements non annoncés dans des actifs numériques cotés en bourse) est disponible sur https://a16z.com/investments /.

Les tableaux et graphiques fournis ici sont uniquement à des fins d'information et ne doivent pas être utilisés pour prendre une décision d'investissement. Les performances passées ne représentent pas les résultats futurs. Le contenu ne parle qu'à la date indiquée. Toutes les projections, estimations, prévisions, objectifs, perspectives et/ou opinions exprimées dans ces documents sont susceptibles d'être modifiées sans préavis et peuvent différer ou être contraires aux opinions exprimées par d'autres. Veuillez consulter https://a16z.com/disclosures pour des informations supplémentaires importantes.