Vérification formelle avancée des preuves à divulgation nulle : analyse approfondie de deux vulnérabilités ZK
TechFlow SélectionTechFlow Sélection
Vérification formelle avancée des preuves à divulgation nulle : analyse approfondie de deux vulnérabilités ZK
Dans cet article, nous allons nous concentrer sur le point de vue de la découverte de vulnérabilités, analyser les failles spécifiques identifiées lors des processus d'audit et de vérification, ainsi que les enseignements et retours d'expérience qui en découlent.
Dédié à des analyses Web3 approfondiesPar : CertiK
Dans un article précédent, nous avons discuté de la vérification formelle avancée des preuves à divulgation nulle (ZKP) : comment vérifier une instruction ZK. En vérifiant formellement chaque instruction zkWasm, nous pouvons entièrement garantir la sécurité technique et la correction du circuit zkWasm dans son ensemble. Dans cet article, nous adoptons une perspective axée sur la découverte de vulnérabilités : analyser les failles concrètes détectées lors d'audits et de processus de vérification, ainsi que les enseignements tirés. Pour une discussion générale sur la vérification formelle avancée des blockchains ZKP, veuillez consulter notre article intitulé « Vérification formelle avancée des blockchains à preuve à divulgation nulle ».
Avant d’aborder les vulnérabilités ZK, examinons comment CertiK procède à la vérification formelle ZK. Pour des systèmes complexes comme une machine virtuelle à divulgation nulle (zkVM), la première étape de la vérification formelle (FV) consiste à définir clairement ce qui doit être vérifié et selon quelles propriétés. Cela nécessite un examen approfondi de la conception du système ZK, de l'implémentation du code et des configurations de test. Ce processus chevauche partiellement un audit classique, mais s’en distingue par l’établissement, après examen, des objectifs et propriétés à vérifier. Chez CertiK, nous appelons cela un « audit orienté vérification ». L’audit et la vérification sont généralement menés conjointement. Pour zkWasm, nous avons effectué simultanément un audit et une vérification formelle.
Qu'est-ce qu'une vulnérabilité ZK ?
La caractéristique fondamentale des systèmes de preuve à divulgation nulle (ZKP) réside dans leur capacité à transmettre aux validateurs ZK une preuve cryptographique concise d’un calcul exécuté hors ligne ou en privé (par exemple, une transaction blockchain), afin qu’il puisse la vérifier et confirmer avec certitude que le calcul a bien eu lieu comme annoncé. Dans ce contexte, une vulnérabilité ZK permettrait à un pirate de soumettre une fausse preuve ZK prouvant une transaction invalide, que le vérificateur ZK accepterait néanmoins.
Pour le prouveur d’une zkVM, le processus de preuve ZK implique d’exécuter un programme, d’enregistrer chaque étape d’exécution, puis de convertir ces données d’exécution en un ensemble de tableaux numériques (processus appelé « arithmétisation »). Ces tableaux doivent respecter un ensemble de contraintes (le « circuit »), incluant des équations reliant des cellules spécifiques, des constantes fixes, des contraintes de recherche entre tables, ainsi que des équations polynomiales entre chaque paire de lignes consécutives (appelées « portes »). La validation on-chain peut alors confirmer qu’un tableau satisfaisant toutes les contraintes existe bien, sans pour autant révéler les valeurs numériques contenues dans ce tableau.
Tableaux d’arithmétisation zkWasm
La précision de chaque contrainte est cruciale. Une erreur dans une contrainte — qu’elle soit trop faible ou manquante — pourrait permettre à un pirate de soumettre une preuve trompeuse, où les tableaux semblent représenter une exécution valide d’un contrat intelligent, alors qu’il n’en est rien. Comparée aux machines virtuelles traditionnelles, l’opacité des transactions zkVM amplifie ces vulnérabilités. Sur les blockchains non-ZK, les détails des calculs sont enregistrés publiquement dans les blocs ; tandis que dans une zkVM, ces détails ne sont pas stockés sur la chaîne. Cette absence de transparence rend difficile non seulement la détermination de la nature d’une attaque, mais aussi la simple détection de sa survenue.
Les circuits ZK régissant l’exécution des instructions zkVM sont extrêmement complexes. Pour zkWasm, l’implémentation du circuit ZK comprend plus de 6 000 lignes de code Rust et des centaines de contraintes. Cette complexité signifie souvent qu’un grand nombre de vulnérabilités peuvent rester cachées.
Architecture du circuit zkWasm
En effet, grâce à nos audits et vérifications formelles de zkWasm, nous avons découvert plusieurs de ces vulnérabilités. Nous allons maintenant examiner deux exemples représentatifs et discuter de leurs différences.
Vulnérabilité de code : Attaque par injection de données Load8
La première vulnérabilité concerne l’instruction Load8 de zkWasm. Dans zkWasm, la lecture de la mémoire tas s’effectue via un ensemble d’instructions LoadN, où N désigne la taille des données à charger. Par exemple, Load64 doit lire 64 bits à partir d’une adresse mémoire zkWasm. Load8 doit lire 8 bits (un octet) depuis la mémoire, puis compléter avec des zéros au début pour former une valeur de 64 bits. À l’intérieur de zkWasm, la mémoire est représentée sous forme de tableau de mots de 64 bits, donc il faut « extraire » une partie de ce tableau. Pour cela, quatre variables intermédiaires (u16_cells) sont utilisées, combinées pour former la valeur complète de 64 bits chargée.
Les contraintes définissant ces instructions LoadN sont les suivantes :
Cette contrainte distingue trois cas : Load32, Load16 et Load8. Load64 n’a aucune contrainte, car les unités mémoire correspondent exactement à 64 bits. Dans le cas de Load32, le code garantit que les 4 octets supérieurs (32 bits) de l’unité mémoire doivent être nuls.
Pour Load16, les 6 octets supérieurs (48 bits) de l’unité mémoire doivent être nuls.
Pour Load8, il devrait être exigé que les 7 octets supérieurs (56 bits) de l’unité mémoire soient nuls. Malheureusement, ce n’est pas le cas dans le code.
Comme vous pouvez le constater, seuls les bits 9 à 16 supérieurs sont contraints à zéro. Les 48 autres bits supérieurs peuvent prendre n’importe quelle valeur tout en passant pour des données « lues depuis la mémoire ».
En exploitant cette vulnérabilité, un pirate peut altérer la preuve ZK d’une séquence d’exécution légitime, faisant en sorte que l’instruction Load8 charge ces octets inattendus, provoquant ainsi une corruption de données. En organisant soigneusement le code et les données environnants, il pourrait déclencher des exécutions et transferts fictifs, permettant de voler des données et des actifs. Cette transaction falsifiée passerait le contrôle du vérificateur zkWasm et serait incorrectement considérée comme valide par la blockchain.
La correction de cette vulnérabilité est en réalité assez simple.
Cette vulnérabilité représente une catégorie appelée « vulnérabilité de code », car elle découle directement d’une erreur dans l’écriture du code et peut être corrigée par une modification locale mineure. Comme vous l’admettrez probablement, ces vulnérabilités sont également relativement faciles à repérer.
Vulnérabilité de conception : Attaque par faux retour
Examinons maintenant une autre vulnérabilité, cette fois liée aux instructions d’appel et de retour dans zkWasm. Appel et retour sont des instructions fondamentales de toute machine virtuelle, permettant à un contexte d’exécution (comme une fonction) d’appeler un autre, puis de reprendre son exécution après la fin du contexte appelé. Chaque appel doit idéalement être suivi d’un retour. Les données dynamiques suivies par zkWasm pendant le cycle de vie des appels/retours sont appelées « cadres d’appel (call frames) ». Étant donné que zkWasm exécute les instructions séquentiellement, tous les cadres d’appel peuvent être ordonnés selon leur moment d’apparition. Voici un exemple de code d’appel/retour exécuté sur zkWasm.
Un utilisateur peut appeler la fonction buy_token() pour acheter un jeton (probablement en payant ou en transférant quelque chose de valeur). L’une des étapes clés consiste à appeler la fonction add_token(), qui incrémente réellement le solde du compte de jetons de 1. Puisque le prouveur ZK lui-même ne prend pas en charge la structure de données des cadres d’appel, il faut utiliser une table d’exécution (E-Table) et une table de sauts (J-Table) pour enregistrer et suivre l’historique complet de ces cadres.
L’image ci-dessus illustre le processus d’appel de add_token() par buy_token(), puis le retour de add_token() à buy_token(). On observe que le solde du compte de jetons augmente de 1. Dans la table d’exécution, chaque étape occupe une ligne, contenant notamment le numéro du cadre d’appel en cours, le nom de la fonction (à titre explicatif ici), le numéro de l’instruction en cours dans cette fonction, et l’instruction courante (à titre explicatif). Dans la table de sauts, chaque cadre d’appel occupe une ligne, contenant le numéro du cadre appelant, le nom du contexte fonctionnel appelant (à titre explicatif), et la position de la prochaine instruction du cadre appelant (pour permettre le retour). Dans les deux tables, une colonne jops indique si l’instruction actuelle est un appel/retour (dans la E-Table) ou le nombre total d’appels/retours pour ce cadre (dans la J-Table).
Comme attendu, chaque appel devrait avoir un retour correspondant, et chaque cadre ne devrait comporter qu’un seul appel et un seul retour. Sur l’image, le jops du cadre 1 vaut 2, correspondant aux lignes 1 et 3 de la table d’exécution où jops vaut 1. Tout semble normal.
Mais en réalité, un problème existe : bien qu’un appel et un retour donnent un jops de 2, deux appels ou deux retours donneraient aussi un jops de 2. Deux appels ou deux retours par cadre paraissent absurdes, mais rappelez-vous que c’est précisément ce genre de comportement inattendu que les pirates cherchent à exploiter.
Vous êtes peut-être excité maintenant, mais avons-nous vraiment trouvé le problème ?
Il s’avère que deux appels ne posent pas de problème, car les contraintes de la table d’exécution et de la table de sauts empêchent deux appels d’être codés dans la même ligne de cadre : chaque appel crée un nouveau numéro de cadre, égal au numéro actuel + 1.
Malheureusement, deux retours sont possibles : comme aucun nouveau cadre n’est créé lors d’un retour, un pirate peut effectivement prendre une séquence d’exécution légitime et injecter des retours falsifiés (ainsi qu’un cadre correspondant). Par exemple, l’exemple précédent d’appel de add_token() par buy_token() peut être altéré comme suit :
Le pirate insère deux faux retours entre l’appel initial et le retour dans la table d’exécution, ajoute une nouvelle ligne de cadre falsifiée dans la table de sauts (et décale les numéros d’étapes ultérieures de 4 dans la table d’exécution). Puisque chaque ligne de la table de sauts a un jops égal à 2, toutes les contraintes sont satisfaites, et le vérificateur zkWasm acceptera cette preuve falsifiée. Comme visible sur l’image, le solde du compte de jetons augmente 3 fois au lieu de 1. Le pirate obtient ainsi 3 jetons en n’en payant qu’un.
Plusieurs solutions existent pour corriger ce problème. Une solution évidente consiste à comptabiliser séparément les appels et les retours, et à imposer exactement un appel et un retour par cadre.
Vous avez peut-être remarqué que nous n’avons montré aucune ligne de code pour cette vulnérabilité. La raison principale est qu’aucune ligne de code n’est erronée : l’implémentation correspond parfaitement à la conception des tables et des contraintes. Le problème réside dans la conception elle-même, et c’est là aussi que se situe la correction.
Vous pourriez penser que cette vulnérabilité aurait dû être évidente, mais ce n’est pas le cas. Il existe un fossé entre « deux appels ou deux retours donnent un jops de 2 » et « deux retours sont effectivement possibles ». Ce dernier point nécessite une analyse détaillée et complète de toutes les contraintes associées dans les tables d’exécution et de sauts, difficile à réaliser sans raisonnement formel rigoureux.
Comparaison des deux vulnérabilités
Les vulnérabilités « d’injection de données Load8 » et « de faux retour » peuvent toutes deux permettre à un pirate de manipuler la preuve ZK, créer des transactions falsifiées, tromper le vérificateur et voler des actifs. Mais leurs natures et leurs modes de découverte sont très différents.
La vulnérabilité « d’injection de données Load8 » a été découverte lors de l’audit de zkWasm. Ce n’était pas une tâche facile, car il fallait passer en revue plus de 6 000 lignes de code Rust et des centaines de contraintes pour des dizaines d’instructions zkWasm. Néanmoins, cette vulnérabilité était relativement facile à repérer et à confirmer. Elle ayant été corrigée avant le début de la vérification formelle, nous ne l’avons pas rencontrée durant ce processus. Si elle n’avait pas été trouvée lors de l’audit, nous l’aurions très probablement découverte lors de la vérification de l’instruction Load8.
La vulnérabilité « de faux retour » a été découverte lors de la vérification formelle, après l’audit. Une raison pour laquelle nous ne l’avons pas trouvée lors de l’audit est qu’il existe dans zkWasm un mécanisme similaire appelé « mops », qui trace, pendant l’exécution, les accès mémoire pour chaque unité mémoire. La contrainte de comptage mops est correcte, car elle ne suit qu’un type d’instruction mémoire (l’écriture), et chaque unité mémoire n’est écrite qu’une seule fois (mops = 1). Même si nous avions soupçonné un problème similaire pendant l’audit, sans un raisonnement formel strict sur toutes les contraintes concernées, nous n’aurions pu facilement confirmer ou exclure toutes les possibilités, car aucune ligne de code n’était incorrecte.
En résumé, ces deux vulnérabilités relèvent respectivement des catégories « vulnérabilité de code » et « vulnérabilité de conception ». Les premières sont relativement superficielles, plus faciles à découvrir (code erroné), et plus simples à raisonner ; les secondes peuvent être très subtiles, difficiles à détecter (aucun « code erroné »), et encore plus complexes à analyser et confirmer.
Bonnes pratiques pour détecter les vulnérabilités ZK
D’après notre expérience d’audit et de vérification formelle de zkVM et d’autres blockchains ZK ou non-ZK, voici quelques recommandations pour mieux protéger les systèmes ZK.
Vérifier le code et la conception
Comme mentionné précédemment, les vulnérabilités peuvent résider tant dans le code que dans la conception d’un système ZK. Ces deux types peuvent compromettre le système, et doivent donc être éliminés avant son déploiement. Contrairement aux systèmes non-ZK, toute attaque contre un système ZK est plus difficile à révéler ou analyser, car les détails de calcul ne sont ni publics ni conservés sur la chaîne. On peut savoir qu’un piratage a eu lieu, sans comprendre techniquement comment. Cela rend le coût de toute vulnérabilité ZK particulièrement élevé. Par conséquent, la valeur d’une sécurisation préalable rigoureuse est immense.
Effectuer à la fois audit et vérification formelle
Les deux vulnérabilités présentées ont été découvertes respectivement par audit et par vérification formelle. On pourrait croire qu’avec une vérification formelle, l’audit devient inutile, car toutes les vulnérabilités seraient détectées. Notre recommandation reste cependant de faire les deux. Comme expliqué en début d’article, une vérification formelle de qualité commence par un examen approfondi du code et de la conception, incluant vérifications et raisonnements informels — ce qui recoupe largement l’audit. De plus, éliminer les vulnérabilités simples durant l’audit rend la vérification formelle plus simple et efficace.
Si vous devez auditer et vérifier formellement un système ZK, le meilleur moment est de le faire simultanément, afin que les auditeurs et ingénieurs de vérification collaborent efficacement (ce qui peut permettre de trouver davantage de vulnérabilités, car la vérification formelle dépend fortement de la qualité des entrées fournies par l’audit).
Si votre projet ZK a déjà fait l’objet d’un audit (bravo) ou de plusieurs audits (très bien), nous vous conseillons fortement d’effectuer ensuite une vérification formelle du circuit à partir des résultats d’audit. Notre expérience répétée sur zkVM et d'autres projets ZK et non-ZK montre que la vérification formelle parvient souvent à détecter des vulnérabilités passées inaperçues lors des audits. En raison des caractéristiques des ZKP, bien qu’un système ZK doive offrir une meilleure sécurité et évolutivité que les solutions non-ZK, la garantie de sa propre sécurité et correction est bien plus critique que pour un système traditionnel. Ainsi, la valeur d’une vérification formelle de haute qualité pour un système ZK est bien supérieure à celle pour un système non-ZK.
Assurer la sécurité du circuit et des contrats intelligents
Les applications ZK comprennent généralement deux composants : le circuit et les contrats intelligents. Pour les applications basées sur zkVM, il y a un circuit zkVM générique et une application de contrat intelligent. Pour celles qui ne le sont pas, il y a un circuit ZK spécifique à l’application, accompagné d’un contrat intelligent déployé sur une blockchain L1 ou de l’autre côté d’un pont. Basé sur zkVM Non basé sur zkVM
Notre audit et vérification formelle de zkWasm n’ont concerné que le circuit zkWasm. Du point de vue de la sécurité globale d’une application ZK, auditer et vérifier formellement ses contrats intelligents est également crucial. Après avoir investi tant d’efforts pour sécuriser le circuit, il serait regrettable que l’application soit compromise par une négligence au niveau du contrat intelligent.
Deux types de contrats intelligents méritent une attention particulière. Premièrement, ceux qui traitent directement les preuves ZK. Bien que souvent petits, ils présentent un risque très élevé. Deuxièmement, les contrats intelligents moyens ou grands exécutés sur zkVM. Nous savons qu’ils peuvent être très complexes, et les plus précieux doivent faire l’objet d’un audit et d’une vérification, surtout parce que leurs détails d’exécution ne sont pas visibles sur la chaîne. Heureusement, après des années de développement, la vérification formelle des contrats intelligents est désormais applicable en pratique et prête pour des cibles à forte valeur.
Résumons l’impact de la vérification formelle (FV) sur les systèmes ZK et leurs composants :
-
Circuit FV + Contrat intelligent non-FV = Preuve à divulgation nulle non-FV
-
Circuit non-FV + Contrat intelligent FV = Preuve à divulgation nulle non-FV
-
Circuit FV + Contrat intelligent FV = Preuve à divulgation nulle FV
Bienvenue dans la communauté officielle TechFlow
Groupe Telegram :https://t.me/TechFlowDaily
Compte Twitter officiel :https://x.com/TechFlowPost
Compte Twitter anglais :https://x.com/BlockFlow_News
CertiK
