Vérification formelle des zk-SNARKs : méthode de preuve de mémoire

Lors de la vérification formelle des systèmes de zk-SNARKs, le traitement du sous-système mémoire représente un défi clé. Contrairement aux machines virtuelles traditionnelles, le zkVM utilise des tables d'exécution et des tables auxiliaires pour représenter l'état de la mémoire, ce qui nécessite des méthodes de vérification spéciales.

Le système de mémoire de zkWasm est composé d'une table d'exécution et d'une table de mémoire. La table d'exécution enregistre le processus d'exécution des instructions, tandis que la table de mémoire conserve tout l'historique des accès à la mémoire. Pour simplifier le développement, zkWasm fournit une couche d'abstraction, permettant d'opérer sur la mémoire via les deux fonctions alloc_memory_table_lookup_write_cell et alloc_memory_table_lookup_read_cell.

Dans le processus de vérification, nous considérons la table de mémoire comme une structure de données modifiable, construisant une carte d'adresses via la fonction memory_at. Cela permet de prouver que les contraintes générées par la fonction alloc sont équivalentes aux opérations set et get effectuées sur la carte, simplifiant ainsi la validation des instructions sous une forme similaire à celle d'un interpréteur non-ZK.

Pour empêcher les attaquants de manipuler la table de mémoire, zkWasm utilise un mécanisme de comptage pour suivre le nombre d'entrées valides. La table d'exécution et la table de mémoire maintiennent respectivement des compteurs, garantissant la cohérence entre les deux par des contraintes. Cela exige une plus grande précision lors de la vérification, nécessitant de prouver que chaque instruction correspond au bon nombre d'entrées dans la table de mémoire.

Le processus de vérification adopte une approche descendante, comprenant trois étapes :

1. Le nombre d'entrées que la commande estimée doit créer
2. Le nombre d'entrées dans le tableau des preuves ne dépasse pas les attentes.
3. Prouver par induction que cum_mops et instructions_mops sont toujours cohérents dans le tableau.

Cette méthode de validation détaillée aide à découvrir des erreurs potentielles, comme un problème clé dans le mécanisme de comptage des tables de saut.

Pour réaliser la vérification modulaire, nous avons divisé le système en trois parties indépendantes : la vérification du circuit d'instructions, la vérification de la table d'exécution et la mise en œuvre de la table de mémoire. Cette structure permet à plusieurs ingénieurs de travailler en parallèle, améliorant ainsi l'efficacité de la vérification.

Dans l'ensemble, bien que la validation zkVM présente des différences lors du traitement des états dynamiques, elle peut toujours adopter une approche modulaire similaire à celle de la validation des interprètes traditionnels en faisant correspondre les niveaux d'abstraction de l'implémentation. Cette approche minimise l'impact des différences, permettant à chaque instruction d'être validée de manière indépendante via l'interface get-set.