Dans cette série de blogs sur la vérification formelle avancée des preuves de connaissance nulle, nous avons expliqué comment vérifier les instructions ZK et une analyse approfondie de deux vulnérabilités ZK. Comme le montrent les rapports publics et les bases de code, en vérifiant formellement chaque instruction zkWasm, nous avons trouvé et corrigé chaque vulnérabilité, nous permettant ainsi de vérifier pleinement la sécurité technique et l'exactitude de l'ensemble du circuit zkWasm.
Bien que nous ayons montré le processus de vérification d'une instruction zkWasm et présenté les concepts préliminaires du projet associé, les lecteurs familiers avec la vérification formelle pourraient être plus intéressés par la compréhension de la vérification de zkVM avec d'autres systèmes ZK plus petits ou d'autres types de VM de bytecode. sur. Dans cet article, nous aborderons en profondeur certains des points techniques rencontrés lors de la validation du sous-système mémoire zkWasm. La mémoire est la partie la plus unique de zkVM, et sa gestion est essentielle pour toutes les autres vérifications de zkVM.
Vérification formelle : machine virtuelle (VM) versus machine virtuelle ZK (zkVM)
Notre objectif ultime est de vérifier l'exactitude de zkWasm, qui est similaire au théorème d'exactitude des interpréteurs de bytecode ordinaires (VM, tels que l'interpréteur EVM utilisé par les nœuds Ethereum). C'est-à-dire qu'à chaque étape d'exécution de l'interpréteur correspond une étape juridique basée sur la sémantique opérationnelle du langage. Comme le montre la figure ci-dessous, si l'état actuel de la structure de données de l'interpréteur de bytecode est SL et que cet état est marqué comme état SH dans la spécification de haut niveau de la machine Wasm, alors lorsque l'interpréteur passe à l'état SL', il y a doit être un état légal de haut niveau correspondant SH', et la spécification Wasm stipule que SH doit passer à SH'.
De même, zkVM a un théorème d'exactitude similaire : chaque nouvelle ligne dans la table d'exécution de zkWasm correspond à une étape légale basée sur la sémantique opérationnelle du langage. Comme le montre la figure ci-dessous, si l'état actuel d'une ligne de structure de données dans la table d'exécution est SR et que cet état est exprimé comme état SH dans la spécification de haut niveau de la machine Wasm, alors l'état de la ligne suivante de la table d'exécution SR' doit correspondre à un état de haut niveau SH' , et la spécification Wasm stipule que SH doit passer à SH'.
On peut voir que la spécification des états de haut niveau et des étapes Wasm est cohérente que ce soit dans VM ou zkVM, elle peut donc s'appuyer sur l'expérience de vérification antérieure des interprètes ou des compilateurs de langage de programmation. La particularité de la vérification zkVM réside dans le type de structure de données qui constitue l'état de bas niveau du système.
Premièrement, comme nous l'avons indiqué dans un article de blog précédent, le prouveur zk est essentiellement une opération entière modulo de grands nombres premiers, alors que la spécification Wasm et l'interpréteur normal traitent des entiers de 32 ou 64 bits. La majeure partie de l'implémentation de zkVM implique cela, par conséquent, le traitement correspondant doit également être effectué lors de la vérification. Cependant, il s'agit d'un problème « local » : chaque ligne de code devient plus complexe en raison des opérations arithmétiques qu'elle doit gérer, mais la structure globale du code et de la preuve ne change pas.
Une autre différence majeure réside dans la manière dont les structures de données de taille dynamique sont gérées. Dans un interpréteur de bytecode standard, la mémoire, la pile de données et la pile d'appels sont toutes implémentées en tant que structures de données mutables. De même, la spécification Wasm représente la mémoire comme un type de données avec des méthodes get/set. Par exemple, l'interpréteur EVM de Geth a un type de données « Memory », qui est implémenté sous la forme d'un tableau d'octets représentant la mémoire physique et est écrit et lu via les méthodes « Set 32 » et « GetPtr ». Afin d'implémenter une instruction de stockage en mémoire, Geth appelle le « Set 32 » pour modifier la mémoire physique.
func opMstore(pc *uint 64, interpréteur *EVMInterpreter, scope *ScopeContext) ([]octet, erreur) {
// valeur pop de la pile
mStart, val := scope.Stack.pop(), scope.Stack.pop()
scope.Memory.Set 32(mStart.Uint 64(), val)
retour nul, nul
}
Dans la preuve d'exactitude de l'interpréteur ci-dessus, nous avons prouvé que son état de haut niveau et son état de bas niveau se correspondent après avoir attribué des valeurs à la mémoire concrète dans l'interpréteur et à la mémoire abstraite dans la spécification. C'est relativement simple.
Cependant, avec zkVM, la situation devient plus compliquée.
Table mémoire et couche d'abstraction mémoire de zkWasm
Dans zkVM, il existe des colonnes sur la table d'exécution pour les données de taille fixe (similaires aux registres du CPU), mais elle ne peut pas être utilisée pour gérer des structures de données de taille dynamique, qui sont implémentées en recherchant des tables auxiliaires. La table d'exécution de zkWasm a une colonne EID, dont les valeurs sont 1, 2, 3..., et possède deux tables auxiliaires, une table mémoire et une table de sauts, qui sont utilisées respectivement pour représenter les données mémoire et la pile d'appels.
Voici un exemple de la façon de mettre en œuvre un programme de retrait :
solde int, montant ;
vide principal () {
solde = 100 ;
montant = 10 ;
solde -= montant ; // retirer
}
Le contenu et la structure de la table d'exécution sont assez simples. Elle comporte 6 étapes d'exécution (EID 1 à 6), chaque étape possède une ligne listant son opcode (opcode) et, si l'instruction est une lecture ou une écriture mémoire, son adresse et ses données :
Chaque ligne de la table mémoire contient l'adresse, les données, l'EID de début et l'EID de fin. L'EID de début est l'EID de l'étape d'exécution qui écrit ces données à cette adresse, et l'EID de fin est l'EID de la prochaine étape d'exécution qui écrira cette adresse. (Il contient également un décompte, dont nous discuterons en détail plus tard.) Pour le circuit d'instruction de lecture de mémoire Wasm, il utilise une contrainte de recherche pour garantir qu'il existe une entrée appropriée dans la table de telle sorte que l'EID de l'instruction de lecture soit dans le s'étend du début à la fin à l'intérieur. (De même, chaque ligne de la table de sauts correspond à une trame de la pile d'appels, et chaque ligne est étiquetée avec l'EID de l'étape d'instruction d'appel qui l'a créée.)
Ce système de mémoire est très différent d'un interpréteur VM classique : la table mémoire n'est pas une mémoire mutable qui est progressivement mise à jour, mais contient un historique de tous les accès mémoire tout au long de la trace d'exécution. Afin de simplifier le travail des programmeurs, zkWasm fournit une couche d'abstraction, implémentée via deux fonctions d'entrée pratiques. Ils sont:
alloc_memory_table_lookup_write_cell
et
Alloc_memory_table_lookup_read_cell
Ses paramètres sont les suivants :
Par exemple, le code qui implémente les instructions de stockage en mémoire dans zkWasm contient un appel à la fonction « write alloc » :
laissez memory_table_lookup_heap_write1 = allocateur
.alloc_memory_table_lookup_write_cell_with_value(
"stocker la résolution d'écriture 1",
contrainte_builder,
l'Aïd,
bouger |____| constant_from !(LocationType::Heap as u 64),
déplacer |méta| load_block_index.expr(meta), // adresse
bouger |____| constant_from!( 0), // est 32 bits
bouger |____| constant_from!( 1), // (toujours) activé
);
laissez store_value_in_heap1 = memory_table_lookup_heap_write1.value_cell;
La fonction `alloc` est responsable de la gestion des contraintes de recherche entre les tables et des contraintes arithmétiques reliant l'`eid` actuel aux entrées de la table mémoire. À partir de là, les programmeurs peuvent traiter ces tables comme une mémoire ordinaire, et la valeur de `store_value_in_heap1` a été attribuée à l'adresse `load_block_index` après l'exécution du code.
De même, les instructions de lecture de mémoire sont implémentées à l'aide de la fonction `read_alloc`. Dans l'exemple de séquence d'exécution ci-dessus, il existe une contrainte de lecture pour chaque instruction de chargement et une contrainte d'écriture pour chaque instruction de stockage, et chaque contrainte est satisfaite par une entrée dans la table mémoire.
mtable_lookup_write(ligne 1.eid, ligne 1.store_addr, ligne 1.store_value)
⇐ (ligne 1.eid= 1 ∧ ligne 1.store_addr=balance ∧ ligne 1.store_value= 100 ∧ ...)
mtable_lookup_write(ligne 2.eid, ligne 2.store_addr, ligne 2.store_value)
⇐ (ligne 2.eid= 2 ∧ ligne 2.store_addr=montant ∧ ligne 2.store_value= 10 ∧ ...)
mtable_lookup_read(ligne 3.eid, ligne 3.load_addr, ligne 3.load_value)
⇐ ( 2
mtable_lookup_read(ligne 4.eid, ligne 4.load_addr, ligne 4.load_value)
⇐ ( 1
mtable_lookup_write(ligne 6.eid, ligne 6.store_addr, ligne 6.store_value)
⇐ (ligne 6.eid= 6 ∧ ligne 6.store_addr=balance ∧ ligne 6.store_value= 90 ∧ ...)
La structure de la vérification formelle doit correspondre aux abstractions utilisées dans le logiciel vérifié, afin que la preuve puisse suivre la même logique que le code. Pour zkWasm, cela signifie que nous devons vérifier le circuit de la table mémoire et les fonctions « allouer la cellule de lecture/écriture » en tant que module, qui s'interface comme une mémoire variable. Compte tenu d'une telle interface, la vérification de chaque circuit d'instruction peut être effectuée d'une manière similaire à un interpréteur classique, tandis que la complexité ZK supplémentaire est encapsulée dans le module du sous-système de mémoire.
Lors de la vérification, nous avons mis en œuvre l'idée selon laquelle « la table mémoire peut en fait être considérée comme une structure de données mutable ». Autrement dit, écrivez la fonction `memory_at type`, qui analyse complètement la table mémoire et construit le mappage de données d'adresse correspondant. (La plage de valeurs de la variable « type » comprend ici trois types différents de données de mémoire Wasm : tas, pile de données et variables globales.) Ensuite, nous prouvons que les contraintes de mémoire générées par la fonction alloc sont équivalentes à l'utilisation de set et get fonctions. Modifications de données apportées par le mappage de données d’adresse correspondant. Nous pouvons prouver :
Pour chaque eid, si les contraintes suivantes sont vérifiées
valeur de décalage de type eid memory_table_lookup_read_cell
mais
get (memory_at eid type) offset = Une valeur
Et, si les contraintes suivantes sont vérifiées
valeur de décalage de type eid memory_table_lookup_write_cell
mais
type memory_at (eid+ 1) = définir la valeur de décalage (type memory_at eid)
Après cela, la vérification de chaque instruction peut être basée sur des opérations d'obtention et de définition sur la carte de données d'adresse, similaires aux interpréteurs de bytecode non ZK.
Le mécanisme de comptage des écritures mémoire de zkWasm
Cependant, la description simplifiée ci-dessus ne révèle pas tout le contenu de la table mémoire et de la table de sauts. Dans le cadre de zkVM, ces tables peuvent être manipulées par des attaquants, qui peuvent facilement manipuler les instructions de chargement mémoire et renvoyer des valeurs arbitraires en insérant une ligne de données.
En prenant le programme de retrait comme exemple, l'attaquant a la possibilité d'injecter de fausses données dans le solde du compte en falsifiant une opération d'écriture en mémoire de 110 $ avant l'opération de retrait. Ce processus peut être réalisé en ajoutant une ligne de données à la table mémoire et en modifiant les valeurs des cellules existantes dans la table mémoire et la table d'exécution. Cela entraînera des retraits « gratuits » puisque le solde du compte restera toujours à 100 $ après l'opération.
Pour garantir que la table mémoire (et la table de sauts) ne contient que des entrées valides générées par les instructions d'écriture mémoire (et d'appel et de retour) réellement exécutées, zkWasm utilise un mécanisme de comptage spécial pour surveiller le nombre d'entrées. Plus précisément, la table mémoire comporte une colonne dédiée qui assure le suivi du nombre total d'entrées écrites en mémoire. Parallèlement, la table d'exécution contient également un compteur pour compter le nombre d'opérations d'écriture en mémoire attendues pour chaque instruction. Assurez-vous que les deux décomptes sont cohérents en définissant une contrainte d'égalité. La logique de cette méthode est très intuitive : chaque fois qu'une opération d'écriture est effectuée dans la mémoire, elle sera comptée une fois et il devrait y avoir un enregistrement correspondant dans la table mémoire. Par conséquent, l’attaquant ne peut insérer aucune entrée supplémentaire dans la table mémoire.
L'énoncé logique ci-dessus est un peu vague et, dans le processus de preuve mécanisée, il doit être rendu plus précis. Tout d’abord, nous devons réviser l’énoncé du lemme d’écriture en mémoire mentionné ci-dessus. Nous définissons la fonction `mops_at eid type` pour compter les entrées de la table mémoire avec un `eid` et un `type` donnés (la plupart des instructions créeront 0 ou 1 entrées à un eid). L'énoncé complet du théorème a une condition préalable supplémentaire indiquant qu'il n'y a pas d'entrées parasites dans la table mémoire :
Si les contraintes suivantes sont vérifiées
(valeur de décalage de type eid memory_table_lookup_write_cell)
Et les nouvelles contraintes suivantes sont établies
(type mops_at eid) = 1
mais
(memory_at(eid+ 1) type) = définir la valeur de décalage (memory_at eid type)
Cela nécessite que notre vérification soit plus précise que le cas précédent. Le simple fait de dériver de la contrainte d'égalité selon laquelle le nombre total d'entrées de la table mémoire est égal au nombre total d'écritures en mémoire lors de l'exécution n'est pas suffisant pour terminer la vérification. Afin de prouver l’exactitude d’une instruction, nous devons savoir que chaque instruction correspond au nombre correct d’entrées dans la table mémoire. Par exemple, nous devons exclure qu’un attaquant puisse omettre une entrée de table mémoire pour une instruction dans la séquence d’exécution et créer une nouvelle entrée de table mémoire malveillante pour une autre instruction sans rapport.
Pour le prouver, nous utilisons une approche descendante pour limiter le nombre d’entrées de table mémoire correspondant à une instruction donnée, ce qui implique trois étapes. Tout d’abord, nous estimons le nombre d’entrées qui doivent être créées pour les instructions dans la séquence d’exécution en fonction du type d’instruction. Nous appelons le nombre attendu d'écritures depuis la ième étape jusqu'à la fin de l'exécution `instructions_mops i`, et le nombre correspondant d'entrées dans la table mémoire depuis la ième instruction jusqu'à la fin de l'exécution `cum_mops (eid i) `. En analysant les contraintes de recherche de chaque instruction, nous pouvons prouver qu'elle ne crée pas moins d'entrées que prévu, ce qui conduit à la conclusion que chaque segment de [i... numRows] suivi ne crée pas moins d'entrées que prévu :
Lemme cum_mops_bound' : pour tout n i,
0 ≤ je ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≥ instructions_mops' i n.
Deuxièmement, si vous pouvez montrer que la table ne contient pas plus d’entrées que prévu, alors elle contient exactement le bon nombre d’entrées, ce qui est évident.
Lemme cum_mops_equal' : forall n i,
0 ≤ je ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≤ instructions_mops' i n ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) = instructions_mops' i n.
Passez maintenant à la troisième étape. Notre théorème d'exactitude stipule que pour tout n, cum_mops et instructions_mops sont toujours cohérents de la ligne n jusqu'à la fin du tableau :
Lemme cum_mops_equal : forall n,
0 <= Z.of_nat n < etable_numRow ->
MTable.cum_mops (etable_values eid_cell (Z.of_nat n)) (max_eid+ 1) = instructions_mops (Z.of_nat n)
La vérification est complétée par la synthèse de n. La première ligne du tableau est la contrainte d'égalité de zkWasm, indiquant que le nombre total d'entrées dans la table mémoire est correct, c'est-à-dire cum_mops 0 = instructions_mops 0 . Pour les lignes suivantes, l’hypothèse inductive nous dit :
cum_mops n = instructions_mops n
et nous espérons prouver
cum_mops (n+ 1) = instructions_mops (n+ 1)
Faites attention ici
cum_mops n = mop_at n + cum_mops (n+ 1)
et
instructions_mops n = instruction_mops n + instructions_mops (n+ 1)
On peut donc obtenir
mops_at n + cum_mops (n+ 1) = instruction_mops n + instructions_mops (n+ 1)
Précédemment, nous avons montré que chaque instruction ne créera pas moins que le nombre attendu d'entrées, par ex.
mops_at n ≥ instruction_mops n.
On peut donc conclure
cum_mops (n+ 1) ≤ instructions_mops (n+ 1)
Ici, nous devons appliquer le deuxième lemme ci-dessus.
(En utilisant un lemme similaire pour vérifier la table de sauts, il peut être prouvé que chaque instruction d'appel peut produire avec précision une entrée de table de sauts, donc cette technique de preuve est généralement applicable. Cependant, nous avons encore besoin d'un travail de vérification supplémentaire pour prouver que le retour de l'exactitude de l'instruction. L'eid renvoyé est différent de l'eid de l'instruction appelante qui a créé la trame d'appel, nous avons donc également besoin d'une propriété invariante supplémentaire pour déclarer que la valeur eid est incrémentée dans une direction pendant la séquence d'exécution.)
Décrire le processus de preuve avec autant de détails est typique de la vérification formelle et c'est la raison pour laquelle la vérification d'un morceau de code spécifique prend souvent plus de temps que son écriture. Mais est-ce que ça en vaut la peine? Cela en valait la peine dans ce cas car nous avons trouvé un bug critique dans le mécanisme de comptage des tables de sauts lors de la preuve. Ce bug a été décrit en détail dans un article précédent - en résumé, les anciennes versions du code représentaient à la fois les instructions d'appel et de retour, et un attaquant pourrait créer un faux saut en ajoutant des instructions de retour supplémentaires à la séquence d'exécution. . Bien qu’un mécanisme de comptage incorrect puisse satisfaire l’intuition selon laquelle chaque instruction d’appel et de retour compte, des problèmes surviennent lorsque nous essayons d’affiner cette intuition en un énoncé de théorème plus précis.
Rendre le processus de preuve modulaire
D’après la discussion ci-dessus, nous pouvons voir qu’il existe une dépendance circulaire entre la preuve sur le circuit de chaque instruction et la preuve sur la colonne de comptage de la table d’exécution. Pour prouver l'exactitude du circuit d'instructions, nous devons raisonner sur les écritures en mémoire ; c'est-à-dire que nous devons connaître le nombre d'entrées de la table mémoire à un EID spécifique, et nous devons prouver que les opérations d'écriture en mémoire comptent dans la table d'exécution est correcte ; et il faut également prouver que chaque instruction effectue au moins un nombre minimum d'écritures mémoire.
De plus, il y a un autre facteur à prendre en compte. Le projet zkWasm est assez volumineux, le travail de vérification doit donc être modularisé afin que plusieurs ingénieurs de vérification puissent diviser le travail. Par conséquent, une attention particulière doit être portée à sa complexité lors de la déconstruction de la preuve du mécanisme de comptage. Par exemple, pour l'instruction LocalGet, deux théorèmes sont les suivants :
Théorème opcode_mops_correct_local_get : pour tout i,
0 <= i ->
etable_values eid_cell i > 0 ->
opcode_mops_correct LocalGet i.
Théorème LocalGetOp_correct : pour tous i st y xs,
0 <= i ->
etable_values enabled_cell i = 1 ->
mops_at_correct i ->
etable_values (ops_cell LocalGet) i = 1 ->
state_rel i st ->
wasm_stack st = xs ->
(etable_values offset_cell i) > 1 ->
nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = Certains y ->
state_rel (i+ 1) (update_stack (incr_iid st) (y :: xs)).
Le premier énoncé du théorème
opcode_mops_correct LocalGet i
Une fois développée, cela signifie que l'instruction crée au moins une entrée de table mémoire sur la ligne i (le numéro 1 est spécifié dans la spécification de l'opcode LocalGet de zkWasm).
Le deuxième théorème est le théorème d’exactitude complète de l’instruction, qui cite
vadrouilles_at_correct je
En hypothèse, cela signifie que l'instruction crée exactement une entrée de table mémoire.
Un ingénieur vérificateur peut prouver ces deux théorèmes indépendamment, puis les combiner avec une preuve sur la table d'exécution pour prouver l'exactitude de l'ensemble du système. Il est à noter que toutes les preuves d'instructions individuelles peuvent être effectuées au niveau des contraintes de lecture/écriture sans connaître l'implémentation spécifique de la table mémoire. Le projet est donc divisé en trois parties pouvant être traitées indépendamment.
Résumer
La vérification ligne par ligne des circuits de zkVM n'est pas fondamentalement différente de la vérification des applications ZK dans d'autres domaines, car elles nécessitent toutes deux un raisonnement similaire sur les contraintes arithmétiques. D'un point de vue de haut niveau, la vérification de zkVM nécessite bon nombre des mêmes méthodes de vérification formelle que celles utilisées dans les interpréteurs et les compilateurs de langage de programmation. La principale différence ici réside dans l’état de la machine virtuelle dimensionné dynamiquement. Cependant, l'impact de ces différences peut être minimisé en structurant soigneusement la structure de vérification pour qu'elle corresponde à la couche d'abstraction utilisée dans l'implémentation, permettant à chaque instruction d'être implémentée en tant que module indépendant basé sur l'interface get-set comme pour un interpréteur chimique classique. vérification.
