Dans un article précédent, nous avons abordé la vérification formelle avancée des systèmes de preuve à divulgation nulle de connaissance (ZKP) : comment vérifier une instruction ZK. En vérifiant formellement chaque instruction zkWasm, nous pouvons garantir pleinement la sécurité technique et l’exactitude de l’ensemble du circuit zkWasm. Dans cet article, nous nous concentrerons sur la perspective de la découverte des vulnérabilités, en analysant les vulnérabilités spécifiques identifiées lors des processus d’audit et de vérification, et les leçons qui en ont été tirées. Pour une discussion générale sur la vérification formelle avancée des blockchains ZKP, veuillez vous référer à l’article sur la vérification formelle avancée des blockchains ZKP.

Avant d’aborder les vulnérabilités ZK, comprenons d’abord comment CertiK effectue la vérification formelle ZK. Pour les systèmes complexes comme la machine virtuelle ZK (zkVM), la première étape de la vérification formelle (FV) consiste à définir clairement ce qui doit être vérifié et ses propriétés. Cela nécessite un examen complet de la conception, de l’implémentation du code et de la configuration des tests du système ZK. Ce processus chevauche les vérifications régulières, mais diffère en ce sens qu’après l’examen, les objectifs et les propriétés de la vérification doivent être établis. Chez CertiK, nous appelons cela la vérification orientée audit. Les travaux d’audit et de vérification sont généralement intégrés. Pour zkWasm, nous avons effectué simultanément un audit et une vérification formelle.

Qu’est-ce qu’une vulnérabilité ZK ?

La principale caractéristique des systèmes de preuve à divulgation nulle de connaissance (ZKP) est qu’ils permettent le transfert d’une brève preuve cryptée des calculs exécutés hors ligne ou en privé (comme les transactions blockchain) à un vérificateur ZKP. Le vérificateur vérifie et confirme la preuve pour s’assurer que le calcul s’est déroulé comme prévu. Dans ce contexte, une vulnérabilité ZK permettrait à un pirate de soumettre de fausses preuves ZK pour de fausses transactions et de les faire accepter par le vérificateur ZKP.

Pour un prouveur zkVM, le processus de preuve ZK implique l’exécution d’un programme, la génération d’enregistrements d’exécution pour chaque étape et la conversion de ces enregistrements d’exécution en un ensemble de tables numériques (un processus connu sous le nom d'« arithmétisation »). Ces nombres doivent satisfaire un ensemble de contraintes (le « circuit »), qui incluent les relations entre des cellules de table spécifiques, des constantes fixes, des contraintes de recherche de base de données entre les tables et des équations polynomiales (ou « portes ») que chaque paire de lignes de table adjacentes doit satisfaire. La vérification on-chain peut confirmer l’existence d’une table qui répond à toutes les contraintes sans révéler les numéros spécifiques dans la table.

Tableau d’arithmétisation dans zkWasm

La précision de chaque contrainte est cruciale. Toute erreur dans une contrainte, qu’elle soit trop faible ou manquante, pourrait permettre à un pirate de soumettre une preuve trompeuse. Ces tableaux peuvent sembler représenter une exécution valide d’un contrat intelligent, mais ce n’est pas le cas en réalité. Par rapport aux machines virtuelles traditionnelles, l’opacité des transactions zkVM amplifie ces vulnérabilités. Dans les chaînes non-ZK, les détails des calculs de transaction sont enregistrés publiquement sur la blockchain ; Toutefois, les zkVM ne stockent pas ces détails sur la chaîne. Ce manque de transparence rend difficile la détermination des spécificités d’une attaque ou même si une attaque a eu lieu.

Le circuit ZK qui applique les règles d’exécution des instructions zkVM est extrêmement complexe. Pour zkWasm, l’implémentation de son circuit ZK implique plus de 6 000 lignes de code Rust et des centaines de contraintes. Cette complexité signifie souvent qu’il peut y avoir plusieurs vulnérabilités en attente d’être découvertes.

Architecture de circuit zkWasm

En effet, grâce à l’audit et à la vérification formelle de zkWasm, nous avons découvert plusieurs vulnérabilités de ce type. Ci-dessous, nous discuterons de deux exemples représentatifs et examinerons les différences entre eux.

Vulnérabilité du code : attaque par injection de données Load8

La première vulnérabilité concerne l’instruction Load8 dans zkWasm. Dans zkWasm, les lectures de mémoire de tas sont effectuées à l’aide d’un ensemble d’instructions LoadN, où N est la taille des données à charger. Par exemple, Load64 doit lire les données 64 bits à partir d’une adresse mémoire zkWasm. Load8 doit lire les données 8 bits (c’est-à-dire un octet) de la mémoire et les remplir de zéros pour créer une valeur de 64 bits. En interne, zkWasm représente la mémoire comme un tableau d’octets de 64 bits, il doit donc « sélectionner » une partie du tableau de mémoire. Cela se fait à l’aide de quatre variables intermédiaires (u16_cells), qui forment ensemble la valeur de charge complète de 64 bits.

Les contraintes de ces instructions LoadN sont définies comme suit :

Cette contrainte est divisée en trois cas : Charge32, Charge16 et Charge8. Load64 n’a pas de contraintes car les unités de mémoire sont exactement de 64 bits. Dans le cas de Load32, le code garantit que les 4 octets (32 bits) les plus élevés de l’unité de mémoire doivent être nuls.

Dans le cas de Load16, le code garantit que les 6 octets (48 bits) les plus élevés de l’unité de mémoire doivent être nuls.

Dans le cas de Load8, il devrait être nécessaire que les 7 octets (56 bits) les plus élevés de l’unité de mémoire soient nuls. Malheureusement, ce n’est pas le cas dans le code.

Comme vous pouvez le voir, seuls les 9 à 16 bits élevés sont limités à zéro. Les 48 autres bits élevés peuvent être n’importe quelle valeur et passer comme « lecture en mémoire ».

En exploitant cette vulnérabilité, un pirate pourrait altérer la preuve ZK d’une séquence d’exécution légitime, provoquant le chargement de ces octets inattendus par l’instruction Load8, entraînant une corruption des données. De plus, grâce à une disposition minutieuse du code et des données environnantes, il peut déclencher de fausses exécutions et transferts, entraînant le vol de données et d’actifs. Ces transactions falsifiées pourraient passer les contrôles des vérificateurs zkWasm et être reconnues à tort comme des transactions légitimes par la blockchain.

Corriger cette vulnérabilité est en fait assez simple.

Cette vulnérabilité représente une classe de vulnérabilités ZK appelées « vulnérabilités de code » car elles proviennent de l’implémentation du code et peuvent être facilement corrigées par des modifications mineures du code local. Comme vous pouvez en convenir, ces vulnérabilités sont également relativement plus faciles à identifier pour les gens.

Vulnérabilité de conception : Attaque de retour forgée

Jetons un coup d’œil à une autre vulnérabilité, cette fois concernant l’invocation et le retour de zkWasm. L’appel et le retour sont des instructions de machine virtuelle fondamentales qui permettent à un contexte en cours d’exécution (par exemple, une fonction) d’en appeler un autre et de reprendre l’exécution du contexte d’appel une fois que l’appelé a terminé son exécution. Chaque invocation s’attend à un retour plus tard. Les données dynamiques suivies par zkWasm pendant le cycle de vie de l’appel et du retour sont connues sous le nom de « trame d’appel ». Comme zkWasm exécute les instructions de manière séquentielle, toutes les trames d’appel peuvent être ordonnées en fonction de leur occurrence pendant l’exécution. Vous trouverez ci-dessous un exemple de code d’appel/retour exécuté sur zkWasm.

Les utilisateurs peuvent appeler la fonction buy_token() pour acheter des jetons (éventuellement par paiement ou transfert d’autres objets de valeur). L’une de ses principales étapes consiste à augmenter le solde du compte de jetons de 1 en appelant la fonction add_token(). Étant donné que le prouveur ZK lui-même ne prend pas en charge la structure de données de la trame d’appel, la table d’exécution (E-Table) et la table de saut (J-Table) sont nécessaires pour enregistrer et suivre l’historique complet de ces trames d’appel.

La figure ci-dessus illustre le processus de buy_token() appelant add_token() et revenant de add_token() à buy_token(). On peut voir que le solde du compte de jetons augmente de 1. Dans la table d’exécution, chaque étape d’exécution occupe une ligne, y compris le numéro de trame d’appel en cours d’exécution, le nom de la fonction de contexte en cours (à des fins d’illustration uniquement), le numéro de l’instruction en cours d’exécution dans la fonction et l’instruction en cours stockée dans la table (à des fins d’illustration uniquement). Dans la table de saut, chaque trame d’appel occupe une ligne, stockant le numéro de sa trame appelante, le nom du contexte de la fonction appelante (à des fins d’illustration uniquement) et la position d’instruction suivante de la trame appelante (afin que la trame puisse retourner). Dans les deux tables, il y a une colonne « jops » qui suit si l’instruction actuelle est un appel/retour (dans la table d’exécution) et le nombre total d’instructions d’appel/retour pour cette trame (dans la table de saut).

Comme prévu, chaque appel doit avoir un retour correspondant, et chaque trame ne doit avoir qu’un appel et un retour. Comme le montre la figure ci-dessus, la valeur « jops » pour la première image de la table de saut est 2, correspondant aux première et troisième lignes de la table d’exécution, où la valeur « jops » est 1. Tout semble normal pour le moment.

Cependant, il y a un problème ici : alors qu’un appel et un retour augmenteront le nombre de « jops » pour la trame à 2, deux appels ou deux retours entraîneront également un compte de 2. Avoir deux appels ou deux retours par image peut sembler absurde, mais il est important de se rappeler que c’est exactement ce qu’un pirate essaierait de faire en dépassant les attentes.

Vous vous sentez peut-être excité maintenant, mais avons-nous vraiment trouvé le problème ?

Il s’avère que deux appels ne sont pas un problème car les contraintes de la table d’exécution et de la table de saut empêchent deux appels d’être encodés dans la même ligne d’une trame car chaque appel génère un nouveau numéro de trame, c’est-à-dire le numéro de trame d’appel actuel plus 1.

Cependant, la situation n’est pas si chanceuse pour deux retours : puisqu’aucune nouvelle trame n’est créée au retour, un pirate pourrait en effet obtenir la table d’exécution et la table de saut d’une séquence d’exécution légitime et injecter des retours falsifiés (et les trames correspondantes). Par exemple, l’exemple précédent de la table d’exécution et de la table de saut de buy_token() appelant add_token() pourrait être altéré par un pirate dans le scénario suivant :

Le pirate a injecté deux retours falsifiés entre l’appel et le retour d’origine dans la table d’exécution et a ajouté une nouvelle ligne de trame falsifiée dans la table de saut (le retour d’origine et les étapes d’exécution d’instructions ultérieures dans la table d’exécution doivent être incrémentés de 4). Comme le nombre de « jops » pour chaque ligne de la table de saut est de 2, les contraintes sont satisfaites et le vérificateur de preuve zkWasm accepterait la « preuve » de cette séquence d’exécution falsifiée. Comme le montre la figure, le solde du compte de jetons augmente 3 fois au lieu de 1. Par conséquent, le pirate pourrait obtenir 3 jetons pour le prix d'1.

Il existe différentes façons de résoudre ce problème. Une approche évidente consiste à suivre séparément les appels et les retours et à s’assurer que chaque trame a exactement un appel et un retour.

Vous avez peut-être remarqué que jusqu’à présent, nous n’avons pas montré une seule ligne de code pour cette vulnérabilité. La raison principale est qu’il n’y a pas de ligne de code problématique ; L’implémentation du code s’aligne parfaitement sur les conceptions de table et de contrainte. Le problème réside dans la conception elle-même, tout comme la correction.

Vous pourriez penser que cette vulnérabilité devrait être évidente, mais en réalité, ce n’est pas le cas. En effet, il y a un écart entre « deux appels ou deux retours entraîneront également un nombre de « jops » de 2 » et « deux retours sont réellement possibles ». Ce dernier nécessite une analyse détaillée et complète des diverses contraintes dans la table d’exécution et la table de saut, ce qui rend difficile la réalisation d’un raisonnement informel complet.

Comparaison de deux vulnérabilités

La « vulnérabilité d’injection de données Load8 » et la « vulnérabilité de retour de falsification » ont toutes deux le potentiel de permettre aux pirates de manipuler les preuves ZK, de créer de fausses transactions, de tromper les vérificateurs de preuves et de se livrer à des vols ou à des détournements. Cependant, leur nature et la façon dont ils ont été découverts sont très différentes.

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 nous avons dû revoir des centaines de contraintes dans plus de 6 000 lignes de code Rust et des dizaines d’instructions zkWasm. Malgré cela, la vulnérabilité était relativement facile à détecter et à confirmer. Comme cette vulnérabilité a été corrigée avant le début de la vérification formelle, elle n’a pas été rencontrée pendant le processus de vérification. Si cette vulnérabilité n’avait pas été découverte lors de l’audit, on pouvait s’attendre à ce qu’elle soit trouvée lors de la vérification de l’instruction Load8.

La « vulnérabilité de retour de falsification » a été découverte lors d’une vérification formelle après l’audit. L’une des raisons pour lesquelles nous n’avons pas réussi à le découvrir lors de l’audit est que zkWasm a un mécanisme similaire à « jops » appelé « mops », qui suit les instructions d’accès à la mémoire correspondant aux données historiques pour chaque unité de mémoire pendant l’exécution de zkWasm. Les contraintes sur le nombre de vadrouilles sont en effet correctes car il ne suit qu’un seul type d’instruction de mémoire, les écritures en mémoire, et les données historiques de chaque unité de mémoire sont immuables et écrites une seule fois (le nombre de vadrouilles est de 1). Mais même si nous avions remarqué cette vulnérabilité potentielle lors de l’audit, nous n’aurions toujours pas pu confirmer ou infirmer facilement tous les scénarios possibles sans un raisonnement formel rigoureux sur toutes les contraintes pertinentes, car il n’y a en fait aucune ligne de code incorrecte.

En résumé, ces deux vulnérabilités appartiennent respectivement aux catégories « vulnérabilités de code » et « vulnérabilités de conception ». Les vulnérabilités du code sont relativement simples, plus faciles à découvrir (code défectueux) et plus faciles à raisonner et à confirmer. Les vulnérabilités de conception peuvent être très subtiles, plus difficiles à découvrir (pas de code « défectueux ») et plus difficiles à raisonner et à confirmer.

Meilleures pratiques pour découvrir les vulnérabilités ZK

Sur la base de notre expérience en matière d’audit et de vérification formelle de zkVM et d’autres chaînes ZK et non-ZK, voici quelques suggestions sur la meilleure façon de protéger les systèmes ZK :

Vérification du code et de la conception

Comme mentionné précédemment, le code et la conception de ZK peuvent contenir des vulnérabilités. Les deux types de vulnérabilités peuvent potentiellement compromettre l’intégrité du système ZK, elles doivent donc être corrigées avant la mise en service du système. L’un des problèmes des systèmes ZK, par rapport aux systèmes non ZK, est que les attaques sont plus difficiles à détecter et à analyser car leurs détails de calcul ne sont pas accessibles au public ou conservés sur la chaîne. Par conséquent, les gens peuvent être conscients qu’une attaque de pirates informatiques a eu lieu, mais ils peuvent ne pas connaître les détails techniques de la façon dont cela s’est produit. Cela rend le coût de toute vulnérabilité ZK très élevé. Par conséquent, il est également très utile d’assurer à l’avance la sécurité des systèmes ZK.

Effectuer des audits et des vérifications formelles

Les deux vulnérabilités dont nous avons parlé ici ont été découvertes par un audit et une vérification formelle. Certains pourraient supposer que la vérification formelle seule évite la nécessité d’un audit puisque toutes les vulnérabilités seraient détectées par une vérification formelle. Cependant, notre recommandation est d’effectuer les deux. Comme expliqué au début de cet article, un travail de vérification formelle de haute qualité commence par un examen approfondi, une inspection et un raisonnement informel sur le code et la conception, qui recoupent l’audit. De plus, la recherche et la résolution de vulnérabilités plus simples pendant l’audit peuvent simplifier et rationaliser le processus de vérification formel.

Si vous effectuez à la fois un audit et une vérification formelle pour un système ZK, l’approche optimale consiste à effectuer les deux simultanément. Cela permet aux auditeurs et aux ingénieurs de vérification formelle de collaborer efficacement, ce qui peut révéler davantage de vulnérabilités, car des données d’audit de haute qualité sont nécessaires pour la vérification formelle.

Si votre projet ZK a déjà fait l’objet d’audits (kudos) ou de plusieurs audits (big kudos), nous vous suggérons d’effectuer une vérification formelle sur le circuit sur la base des résultats de l’audit précédent. Notre expérience de l’audit et de la vérification formelle dans des projets comme zkVM et d’autres, ZK et non-ZK, a montré à plusieurs reprises que la vérification formelle capture souvent les vulnérabilités manquées lors de l’audit. Compte tenu de la nature de ZKP, alors que les systèmes ZK devraient offrir une meilleure sécurité et une meilleure évolutivité de la blockchain que les solutions non-ZK, la criticité de leur sécurité et de leur exactitude est beaucoup plus élevée que les systèmes traditionnels non-ZK. Par conséquent, la valeur d’une vérification formelle de haute qualité pour les systèmes ZK dépasse de loin celle des systèmes non ZK.

Assurer la sécurité des circuits et des contrats intelligents

Les applications ZK se composent généralement de deux composants : des circuits et des contrats intelligents. Pour les applications basées sur zkVM, il existe des circuits zkVM universels et des applications de contrats intelligents. Pour les applications non basées sur zkVM, il existe des circuits ZK spécifiques à l’application ainsi que des contrats intelligents correspondants déployés sur la chaîne L1 ou à l’autre extrémité d’un pont.

Nos efforts d’audit et de vérification formelle pour zkWasm n’impliquent que le circuit zkWasm. Cependant, du point de vue de la sécurité globale des applications ZK, il est crucial d’auditer et de vérifier formellement leurs contrats intelligents. Après tout, il serait regrettable qu’après avoir investi des efforts importants pour assurer la sécurité des circuits, le laxisme dans l’examen des contrats intelligents conduise à la compromission des applications.

Deux types de contrats intelligents méritent une attention particulière. Le premier type gère directement les épreuves ZK. Bien qu’ils ne soient pas à grande échelle, leur risque est exceptionnellement élevé. Le deuxième type comprend des contrats intelligents à moyenne et grande échelle fonctionnant sur zkVM. Nous savons que ces contrats peuvent parfois être très complexes, et que les plus précieux doivent faire l’objet d’un audit et d’une vérification, d’autant plus 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 pratique et préparée pour les cibles appropriées à forte valeur ajoutée.

Résumons l’impact de la vérification formelle (FV) sur les systèmes ZK et leurs composants avec les points suivants.

Déclaration:

1. Cet article est reproduit à partir de [panewslab], les droits d’auteur appartiennent à l’auteur original [CertiK], si vous avez des objections à la réimpression, veuillez contacter l’équipe de Gate Learn, et l’équipe s’en occupera dès que possible selon les procédures pertinentes.

2. Avis de non-responsabilité : Les points de vue et opinions exprimés dans cet article ne représentent que les points de vue personnels de l’auteur et ne constituent aucun conseil en investissement.

3. Les autres versions linguistiques de l’article sont traduites par l’équipe de Gate Learn et ne sont pas mentionnées dans Gate.io, l’article traduit ne peut être reproduit, distribué ou plagié.