💻 computer science

Formally Verifying Noir Zero Knowledge Programs with NAVe

Ce document présente NAVe, un vérificateur formel open-source qui utilise SMT-LIB et le solveur cvc5 pour vérifier formellement la correction et les contraintes appropriées des programmes zero-knowledge de Noir en traduisant leur représentation intermédiaire ACIR en équations polynomiales de corps finis.

Auteurs originaux : Pedro Antonino, Namrata Jain

Publié 2026-01-15

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Pedro Antonino, Namrata Jain

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous construisez un coffre-fort de haute sécurité. Vous voulez prouver à un directeur de banque que vous connaissez la combinaison du coffre sans pour autant lui révéler la combinaison elle-même. C'est toute la magie des preuves à connaissance nulle (Zero-Knowledge ou ZK).

Cependant, la construction de ces coffres-forts est délicate. Les « plans » de ces preuves sont des puzzles mathématiques complexes appelés circuits arithmétiques. Si une seule ligne du plan est erronée, le coffre pourrait être vulnérable, ou la preuve pourrait échouer.

Ce document présente un nouvel outil appelé NAVe (Noir Acir Verifier) conçu pour vérifier ces plans afin de détecter les erreurs avant même qu'ils ne soient utilisés. Voici comment cela fonctionne, expliqué simplement :

1. Le Problème : La « Recette Secrète » contre le « Livre de Cuisine »

Les auteurs se concentrent sur un langage de programmation appelé Noir. Considérez Noir comme un livre de cuisine de haut niveau qui facilite l'écriture de recettes pour ces coffres-forts.

Le Cuisinier (Développeur) : Écrit une recette en Noir, facile à lire.
Le Traducteur (Compilateur) : Transforme cette recette en un manuel d'instructions de bas niveau très strict appelé ACIR. Ce manuel est une liste d'équations mathématiques que l'ordinateur doit résoudre pour prouver que le coffre est sécurisé.
Le Danger : Parfois, le traducteur commet une erreur, ou le cuisinier oublie d'inclure une étape cruciale. Dans le monde de la ZK, on appelle cela être « sous-contraint » (under-constrained). C'est comme écrire une recette qui dit « ajoutez du sel » mais en oubliant de préciser combien. Le résultat sera peut-être comestible, mais ce n'est pas le plat que vous aviez prévu.

2. La Solution : Le « Détective Mathématique » (NAVe)

Les auteurs ont créé NAVe, un vérificateur formel. Considérez NAVe comme un détective mathématique super intelligent qui lit le manuel d'instructions de bas niveau (ACIR) et vérifie si les mathématiques correspondent réellement à ce que le cuisinier avait prévu.

NAVe utilise un puissant moteur logique (appelé solveur SMT) pour poser des questions telles que :

« Si je saisis un nombre secret, est-ce que les mathématiques aboutissent toujours à la preuve publique correcte ? »
« Existe-t-il un moyen de tromper le système avec un faux nombre ? »

Si les mathématiques sont défaillantes, NAVe ne se contente pas de dire « Erreur ». Il agit comme un détective trouvant un indice : il montre au développeur exactement quel nombre aurait pu être utilisé pour briser le système. Cela l'aide à corriger le plan immédiatement.

3. Deux Façons de Résoudre l'Énigme

Le document décrit deux manières différentes dont NAVe traduit les puzzles mathématiques pour les résoudre :

La Voie des Entiers : Il traite les nombres comme des nombres entiers ordinaires (1, 2, 3...) et vérifie les calculs selon les règles arithmétiques standards.
La Voie du Corps Fini (Finite Field) : Il traite les nombres comme s'ils étaient sur une horloge circulaire (où, après un certain nombre, on revient à zéro). C'est ainsi que fonctionnent les véritables preuves ZK.

Les auteurs ont découvert qu'aucune des deux méthodes n'est parfaite pour toutes les situations. Parfois, le détective des « Entiers » est plus rapide ; d'autres fois, le détective du « Corps Fini » est meilleur. Ils suggèrent d'utiliser les deux détectives en même temps pour obtenir les meilleurs résultats.

4. Le Piège de l'« Implicite » (Unconstrained)

Une caractéristique unique de Noir est le code « non contraint » (unconstrained). Imaginez une partie de la recette où le chef est autorisé à deviner les ingrédients sans être contrôlé. Cela est utile pour la vitesse, mais dangereux si le chef se trompe dans ses suppositions.

Le Risque : Un développeur pourrait écrire un code qui semble vérifier les ingrédients, mais parce qu'il se trouve dans la section « non contrainte », l'ordinateur ne force pas réellement la vérification.
Le Rôle de NAVe : NAVe recherche spécifiquement ces « vérifications fantômes ». Il vérifie que même si un développeur utilise la section de « supposition », il a ajouté une règle stricte distincte (un assert) pour s'assurer que la supposition était bien correcte.

5. Ce Qu'Ils Ont Découvert

Les auteurs ont testé NAVe sur une variété de programmes Noir existants :

Cela fonctionne : NAVe a réussi à détecter des erreurs dans des programmes où les mathématiques ne correspondaient pas à l'intention initiale.
Le Goulot d'Étranglement : Ils ont découvert que vérifier les « contraintes de plage » (s'assurer qu'un nombre respecte un certain nombre de bits, comme vérifier si un nombre est compris entre 0 et 255) est très difficile pour le détective mathématique. Cela prend parfois beaucoup de temps ou bloque le processus.
L'Avenir : Ils prévoient de construire de meilleurs « raccourcis » (abstractions) pour aider le détective à résoudre ces puzzles de plage complexes plus rapidement.

Résumé

En bref, NAVe est un filet de sécurité pour les développeurs construisant des applications préservant la confidentialité. Il traduit leur code en un langage mathématique strict et utilise un solveur puissant pour s'assurer que le code fait exactement ce qu'il prétend faire, capturant des bugs subtils qui pourraient autrement conduire à des failles de sécurité. C'est comme avoir un inspecteur rigoureux qui vérifie l'intégrité structurelle d'un pont avant que quiconque ne soit autorisé à rouler dessus.

Résumé Technique : Vérification Formelle des Programmes Zero-Knowledge Noir avec NAVe

Énoncé du Problème
Les systèmes de preuve à divulgation nulle de connaissance (Zero-Knowledge ou ZK) reposent sur des circuits arithmétiques — des ensembles d'équations polynomiales sur des corps finis — pour vérifier qu'une entrée privée $W$ satisfait une relation $R(X, W)$ sans révéler $W$ . Les langages de domaine spécifique (DSL) de haut niveau comme Noir simplifient la création de ces circuits en compilant le code en une représentation intermédiaire appelée ACIR (Abstract Circuit Intermediate Representation). Cependant, cette abstraction introduit des vulnérabilités subtiles. Plus précisément, Noir prend en charge le « code non contraint » (via les fonctions unconstrained et les blocs unsafe) conçu pour améliorer l'efficacité de la preuve en déchargeant les calculs complexes sur le prouveur. Si les développeurs omettent d'ajouter manuellement les contraintes correspondantes (par exemple, via des instructions assert) pour les résultats du code non contraint, le circuit arithmétique généré peut ne pas capturer fidèlement la relation voulue. Ce bug de « sous-contrainte » (under-constrained) peut mener à de graves vulnérabilités de sécurité, permettant par exemple à un prouveur de générer des preuves valides pour des énoncés faux. Les outils de vérification formelle existants ciblent largement des DSL de circuits de plus bas niveau (comme Circom) ou nécessitent une preuve de théorème interactive, manquant ainsi d'une vérification automatisée et évolutive pour les programmes Noir de haut niveau et leurs fonctionnalités spécifiques telles que la manipulation de la mémoire et les fonctions boîte noire.

Méthodologie
Les auteurs proposent NAVe (Noir Acir Verifier), un cadre de vérification formelle open-source qui opère sur la représentation intermédiaire ACIR plutôt que sur le code source de haut niveau Noir. Ce choix garantit une stabilité face à l'évolution du langage et permet à l'outil de potentiellement supporter d'autres langages ciblant l'ACIR.

Formalisation via SMT-LIB : Le cœur de NAVe est une formalisation d'un sous-ensemble d'opcodes ACIR en formules SMT (Satisfiability Modulo Theories). Les auteurs implémentent deux encodages distincts :
- Encodage de Corps Fini : Utilise une théorie non standard des corps finis d'ordre premier implémentée dans le solveur cvc5. Cette approche utilise des opérateurs spécifiques comme ff.add, ff.mul, et ff.bitsum pour modéliser directement l'arithmétique de corps.
- Encodage d'Arithmétique Entière : Exploite la théorie standard des entiers dans SMT-LIB. Il repose sur l'isomorphisme entre les corps finis d'ordre premier $p$ et les entiers modulo $p$ , en encodant les opérations de corps comme une arithmétique entière modulaire (par exemple, (mod (+ ...) p)).
Sémantique des Opcodes : La formalisation couvre les opcodes ACIR clés :
- AssertZero : Encodé comme une contrainte d'équation polynomiale égale à zéro.
- BlackBoxFuncCall : Spécifiquement formalisé pour l'opcode de vérification de plage (Range). Dans l'encodage en corps fini, cela est modélisé par une décomposition binaire (bitsum) et des contraintes garantissant que les bits sont de 0 ou 1. Dans l'encodage entier, cela est modélisé par des contraintes d'ordre entier standard ( $x < 2^n$ ).
- MemoryOp et MemoryInit : Formalisés pour suivre les mutations de tableaux en utilisant une application (map) d'indices vers des valeurs de témoin (witness), gérant les opérations de lecture et d'écriture de manière séquentielle.
- BrilligCall : Représentant le code non contraint, ceux-ci sont traduits comme la contrainte toujours satisfaite true (ou ignorés), car le but du vérificateur est de vérifier les contraintes en dehors des blocs non contraints.
Flux de Travail de Vérification :
- L'outil s'intègre à Nargo, le gestionnaire de paquets de Noir, en tant que commande formal-verify.
- Les développeurs annotent les programmes Noir avec des instructions verify_assert(b: bool). Contrairement aux instructions assert standards qui génèrent des contraintes de circuit, verify_assert crée une obligation de preuve.
- NAVe compile le programme Noir en ACIR, traduit les opcodes ACIR en formules SMT, et construit une formule de vérification $F = \text{ACIR}_{\text{contraintes}} \land \neg \text{verify\_assert}_{\text{condition}}$ .
- Le solveur cvc5 vérifie la satisfaisabilité de $F$ . Si $F$ est insatisfaisable, la condition de vérification est respectée (le programme est correctement contraint). Si $F$ est satisfaisable, le solveur retourne un modèle (contre-exemple) montrant une assignation de témoin qui viole la condition, aidant ainsi au débogage.

Contributions Clés

Formalisation de l'ACIR : La première formalisation d'un sous-ensemble du langage ACIR utilisant SMT-LIB, couvrant des fonctionnalités complexes comme les opérations de mémoire, les vérifications de plage et la distinction entre code contraint et non contraint.
Stratégie de Double Encodage : La proposition de deux encodages complémentaires (théorie du corps fini et arithmétique entière) pour exploiter les capacités différentes des solveurs.
Outil NAVe : Un vérificateur formel automatisé et open-source intégré à l'écosystème Noir (Nargo), conçu pour être accessible aux développeurs sans nécessiter de preuve de théorème interactive.
Évaluation Empirique : Une évaluation complète de NAVe sur une suite de programmes de test Noir, analysant les performances à travers différents types de contraintes et configurations de solveurs.

Résultats
Les auteurs ont évalué NAVe sur 4 ensembles distincts de programmes Noir (conditions vérifiées, conditions falsifiées, avec et sans vérifications de plage) en utilisant le solveur cvc5.

Performance du Solveur : Aucun backend (encodage entier, corps fini --ff=gb, ou corps fini --ff=split) n'a été systématiquement plus performant que les autres. Les résultats indiquent que les encodages sont complémentaires ; certains programmes sont résolus plus rapidement par un encodage, tandis que d'autres expirent (timeout) sur cet encodage mais réussissent sur un autre.
Impact des Vérifications de Plage : Les programmes contenant des vérifications de plage (opcodes BlackBoxFuncCall) augmentent considérablement le temps de vérification. La configuration --ff=split, qui approxime la théorie du corps fini, a montré une performance supérieure sur les programmes avec de grandes vérifications de plage par rapport à la configuration par défaut --ff=gb, bien que des expirations se produisent encore pour les cas complexes.
Génération de Contre-exemples : L'outil a réussi à générer des contre-exemples pour les conditions falsifiées, démontrant son utilité pour identifier la logique sous-contrainte.

Signification et Revendications
L'article affirme que NAVe comble une lacune critique dans l'écosystème ZK en fournissant une méthode automatisée et évolutive pour vérifier les programmes ZK de haut niveau contre les bugs de sous-contrainte, une classe d'erreurs ayant conduit à des vulnérabilités réelles. En ciblant l'ACIR, l'outil reste robuste face aux changements de la syntaxe de haut niveau de Noir et est potentiellement applicable à d'autres langages ciblant la même représentation intermédiaire.

Les auteurs présentent modestement leur travail comme une étape vers des capacités de vérification plus larges. Ils reconnaissent que leur formalisation actuelle ne couvre qu'un sous-ensemble de l'ACIR (excluant les appels Call récursifs et la plupart des BlackBoxFuncCalls sauf Range). Ils identifient le coût élevé de la vérification des plages comme une limitation primaire, suggérant que les travaux futurs devront se concentrer sur le développement d'abstractions ou d'approximations pour gérer efficacement ces contraintes complexes. Le papier positionne NAVe non pas comme une solution complète pour tous les besoins de vérification ZK, mais comme un outil pratique et intégré qui démontre la faisabilité d'une vérification formelle automatisée pour Noir et trace une voie pour améliorer la gestion par les solveurs des contraintes complexes de niveau bit.