Résumé technique : ZKFUZZ, fondement et cadre pour le fuzzing efficace des circuits à connaissance nulle

1. Énoncé du problème

Les circuits à connaissance nulle (ZK) sont fondamentaux pour les calculs préservant la vie privée, permettant des preuves succinctes et une vérification efficace dans des applications allant des cryptomonnaies anonymes à l'apprentissage automatique vérifiable. Cependant, développer des circuits ZK corrects est notoirement difficile en raison du décalage entre la logique de calcul à usage général et les contraintes polynomiales sur les corps finis.

Deux classes principales de vulnérabilités existent :

• Circuits sous-contraints : Les contraintes sont trop lâches, permettant à des prouveurs malveillants de générer des preuves valides pour des témoins invalides (violation de la solidité).
• Circuits sur-contraints : Les contraintes sont trop strictes, amenant le système à rejeter des témoins valides de la part de prouveurs honnêtes (violation de la complétude).

Les méthodes de détection existantes font face à des limitations significatives :

• Analyse statique : Des outils comme Circomspect et ZKAP souffrent souvent de taux élevés de faux positifs et échouent à capturer des problèmes sémantiques profonds, en particulier ceux impliquant des calculs intermédiaires ou des terminaisons anormales de programmes.
• Méthodes formelles : Les outils reposant sur des solveurs SMT (par exemple, Picus, ConsCS) peinent à passer à l'échelle pour des tailles de circuits réels et reposent souvent sur des définitions incomplètes des vulnérabilités, se concentrant uniquement sur le non-déterminisme dans les contraintes tout en ignorant les cas où le calcul s'interrompt ou où des valeurs intermédiaires sont incohérentes.
• Lacunes de définition : Les définitions formelles antérieures des bugs ZK sont incomplètes. Elles ignorent souvent la « terminaison anormale » (où un calcul plante mais où les contraintes sont toujours satisfaites) et ne tiennent pas compte de l'ensemble complet des traces d'exécution, y compris les valeurs intermédiaires.

2. Méthodologie

2.1 Fondement théorique : Test de cohérence trace-contrainte (TCCT)

Les auteurs introduisent le TCCT, un cadre formel indépendant du langage qui définit les vulnérabilités ZK comme des écarts entre deux ensembles :

1. Ensemble de traces $T(P)$ : L'ensemble de toutes les traces d'exécution possibles (entrée, valeurs intermédiaires, sortie) produites par le programme de calcul de témoin $P$.
2. Ensemble de satisfaction des contraintes $S(C)$ : L'ensemble de tous les tuples (entrée, valeurs intermédiaires, sortie) qui satisfont les contraintes du circuit $C$.

Le TCCT définit un circuit comme bien contraint si et seulement si :

• Pas de sous-contrainte : La projection de $S(C)$ sur les paires entrée-sortie est un sous-ensemble de la projection de $T(P)$. Cela garantit qu'aucune trace invalide n'est acceptée.
• Pas de sur-contrainte : $T(P)$ est un sous-ensemble de $S(C)$. Cela garantit que toutes les traces valides (y compris des valeurs intermédiaires spécifiques) sont acceptées.

Cette formulation capture les vulnérabilités causées par des interruptions de calcul (où $P$ échoue mais $C$ accepte l'entrée) et des incohérences dans les valeurs intermédiaires, que les définitions antérieures manquaient. Les auteurs prouvent que la décision de la sous- ou sur-contrainte est NP-complète, et que le TCCT complet est co-NP-complet.

2.2 Conception du système : ZKFUZZ

ZKFUZZ est un cadre d'analyse dynamique qui détecte les violations du TCCT en utilisant une approche de mutation conjointe du programme et de génération d'entrées. Contrairement au fuzzing traditionnel qui ne mutate que les entrées, ZKFUZZ mutate à la fois la logique du programme et les entrées.

Flux de travail principal :

1. Mutation : Le système génère des mutants ($P'$) du programme de calcul original ($P$). Les mutations incluent la suppression d'assertions, la transformation d'affectations (par exemple, remplacement d'opérateurs ou de valeurs) et la modification d'affectations faibles.
2. Exécution : Le programme original ($P$) et le mutant ($P'$) sont exécutés sur des échantillons d'entrées ($x$).
3. Vérification :
   • Détection de sur-contrainte : Si $P(x)$ produit une trace valide qui échoue face à $C$, le circuit est sur-contraint.
   • Détection de sous-contrainte : Si $P'(x)$ produit une trace avec une sortie différente ($y' \neq y$) qui satisfait toujours $C$, le circuit est sous-contraint (puisque la logique du mutant est sémantiquement différente, la sortie ne devrait pas être acceptée).
4. Recherche guidée : Pour naviguer dans l'immense espace de recherche des grands corps premiers et des possibilités infinies de mutation, ZKFUZZ emploie un algorithme génétique :
   • Fonction de fitness : Une nouvelle fonction de fitness min-somme calcule la somme des erreurs de contraintes sur toutes les contraintes pour une trace donnée. Le mutant est noté par la somme minimale d'erreurs sur les entrées échantillonnées. Cela diffère des méthodes antérieures basées uniquement sur le maximum et est mieux adapté à la mutation conjointe.
   • Sélecteurs de cible : Le système utilise l'analyse statique pour guider la mutation et la génération d'entrées vers des modèles à haut risque, tels que :
     • Division par zéro : Génération d'entrées où le numérateur et le dénominateur sont tous deux nuls.
     • Vérification de hachage : Forcer les entrées à satisfaire des contraintes d'égalité de hachage.
     • Distribution biaisée : Biais de la génération d'entrées vers des cas limites (0, 1 et des valeurs proches du module du corps $q$).
     • Liste blanche : Saut des modèles sûrs connus (par exemple, IsZero, Num2Bits) pour se concentrer sur le code sujet aux erreurs.

3. Contributions clés

1. Cadre TCCT : Un modèle formel unifié et indépendant du langage qui englobe les définitions antérieures et capture l'espace complet des bugs ZK, y compris ceux résultant de terminaisons anormales et d'incohérences de valeurs intermédiaires.
2. Système ZKFUZZ : Un nouveau cadre de fuzzing qui mutate conjointement les programmes et les entrées pour détecter les violations du TCCT, utilisant une fonction de fitness min-somme et des heuristiques de recherche guidée.
3. Validation empirique : Évaluation sur 452 circuits Circom réels, démontrant des performances supérieures par rapport aux outils de l'état de l'art.
4. Prototype Noir : Une implémentation préliminaire pour Noir, un autre DSL ZK, démontrant le potentiel d'indépendance linguistique du cadre.

4. Résultats

Les auteurs ont évalué ZKFUZZ sur 452 circuits Circom réels, en le comparant à quatre outils de l'état de l'art : Circomspect, ZKAP, Picus et ConsCS.

• Détection de bugs : ZKFUZZ a identifié 85 bugs uniques, dont 59 vulnérabilités zero-day précédemment inconnues. Parmi ceux-ci, 39 ont été confirmés par les développeurs et 14 ont été corrigés.
• Comparaison : ZKFUZZ a trouvé 30 % à 300 % de bugs en plus que les outils existants pour diverses tailles de circuits.
• Précision : ZKFUZZ a atteint 100 % de précision (zéro faux positif), alors que les analyseurs statiques comme Circomspect et ZKAP avaient des taux de faux positifs élevés (précision allant de 0,06 à 0,75).
• Vitesse : ZKFUZZ++ (avec sélecteurs de cible) a identifié plus de 90 % des bugs en 100 secondes, surpassant nettement les méthodes formelles et les analyseurs statiques.
• Impact : Les bugs découverts comprenaient des vulnérabilités critiques de sous-contrainte dans des projets comme zk-regex et passport-zk-circuits, qui pourraient permettre à des attaquants de forger des preuves ou de soutirer des fonds.

5. Signification et affirmations

L'article affirme que ZKFUZZ représente une avancée significative dans la sécurité des circuits ZK en s'attaquant à l'incomplétude fondamentale des définitions antérieures de vulnérabilités. En formalisant les bugs comme des incohérences trace-contrainte (TCCT), les auteurs exposent une grande classe de vulnérabilités (près de 50 % des bugs réels dans leur évaluation) qui étaient précédemment indétectables par des outils se concentrant uniquement sur le non-déterminisme des contraintes.

La capacité du système à détecter des bugs sans faux positifs en fait un outil pratique pour les développeurs, qui ignorent souvent les alertes des analyseurs statiques à fort taux de faux positifs. De plus, la détection réussie de bugs dans les circuits Noir suggère que le cadre TCCT et l'architecture ZKFUZZ ne sont pas limités à Circom mais peuvent se généraliser à d'autres langages ZK qui se compilent vers des formats de contraintes standardisés.

Les auteurs soulignent que leur travail se concentre sur les vulnérabilités résultant du décalage entre le calcul et les contraintes (solidité et complétude), excluant explicitement les bugs dans les systèmes de preuve sous-jacents, les erreurs de logique pure (comme les entrées inutilisées) ou les fuites de connaissance nulle au niveau du protocole.