Riepilogo Tecnico: ZKFUZZ: Fondamenti e Framework per il Fuzzing Efficace dei Circuiti a Conoscenza Zero

1. Enunciato del Problema

I circuiti a conoscenza zero (ZK) sono fondamentali per i calcoli che preservano la privacy, abilitando prove concise e verifiche efficienti in applicazioni che spaziano dalle criptovalute anonime al machine learning verificabile. Tuttavia, lo sviluppo di circuiti ZK corretti è notoriamente difficile a causa della disallineamento tra la logica di calcolo generico e i vincoli polinomiali su campi finiti.

Esistono due classi principali di vulnerabilità:

• Circuiti sottovincolati: I vincoli sono troppo laschi, permettendo a provatori malintenzionati di generare prove valide per testimoni non validi (violando la soundness).
• Circuiti sovraincolati: I vincoli sono troppo rigidi, causando il rifiuto di testimoni validi da parte di provatori onesti (violando la completezza).

I metodi di rilevamento esistenti presentano limitazioni significative:

• Analisi Statica: Strumenti come Circomspect e ZKAP soffrono spesso di alti tassi di falsi positivi e non riescono a cogliere problemi semantici profondi, in particolare quelli che coinvolgono calcoli intermedi o terminazioni anomale del programma.
• Metodi Formali: Gli strumenti che si basano su solver SMT (ad esempio Picus, ConsCS) faticano a scalare fino alle dimensioni dei circuiti reali e spesso si affidano a definizioni incomplete delle vulnerabilità, concentrandosi esclusivamente sulla non-deterministicità nei vincoli e ignorando i casi in cui il calcolo abortisce o in cui i valori intermedi non corrispondono.
• Lacune nelle Definizioni: Le definizioni formali precedenti dei bug ZK sono incomplete. Spesso ignorano la "terminazione anomala" (dove un calcolo crasha ma i vincoli sono comunque soddisfatti) e non tengono conto dell'insieme completo delle tracce di esecuzione, inclusi i valori intermedi.

2. Metodologia

2.1 Fondamento Teorico: Test di Coerenza Traccia-Vincolo (TCCT)

Gli autori introducono TCCT, un framework formale indipendente dal linguaggio che definisce le vulnerabilità ZK come discrepanze tra due insiemi:

1. Insieme delle Tracce $T(P)$: L'insieme di tutte le possibili tracce di esecuzione (input, valori intermedi, output) prodotte dal programma di calcolo del testimone $P$.
2. Insieme di Soddisfacimento dei Vincoli $S(C)$: L'insieme di tutte le tuple (input, valori intermedi, output) che soddisfano i vincoli del circuito $C$.

TCCT definisce un circuito come ben vincolato se e solo se:

• Nessun sottovincolo: La proiezione di $S(C)$ sulle coppie input-output è un sottoinsieme della proiezione di $T(P)$. Questo assicura che non vengano accettate tracce non valide.
• Nessun sovraincolamento: $T(P)$ è un sottoinsieme di $S(C)$. Questo assicura che tutte le tracce valide (inclusi specifici valori intermedi) vengano accettate.

Questa formulazione cattura le vulnerabilità causate da aborti di calcolo (dove $P$ fallisce ma $C$ accetta l'input) e da disallineamenti nei valori intermedi, che le definizioni precedenti non coglievano. Gli autori dimostrano che decidere se un circuito è sottovincolato o sovraincolato è NP-completo, e il TCCT completo è co-NP-completo.

2.2 Progettazione del Sistema: ZKFUZZ

ZKFUZZ è un framework di analisi dinamica che rileva le violazioni TCCT utilizzando un approccio di mutazione congiunta del programma e generazione degli input. A differenza del fuzzing tradizionale che muta solo gli input, ZKFUZZ muta sia la logica del programma che gli input.

Flusso di Lavoro Principale:

1. Mutazione: Il sistema genera mutanti ($P'$) del programma di calcolo originale ($P$). Le mutazioni includono la rimozione di asserzioni, la trasformazione di assegnazioni (ad esempio, sostituzione di operatori o valori) e la modifica di assegnazioni deboli.
2. Esecuzione: Sia il programma originale ($P$) che il mutante ($P'$) vengono eseguiti su input campionati ($x$).
3. Verifica:
   • Rilevamento del Sovraincolamento: Se $P(x)$ produce una traccia valida che fallisce $C$, il circuito è sovraincolato.
   • Rilevamento del Sottovincolo: Se $P'(x)$ produce una traccia con un output diverso ($y' \neq y$) che soddisfa comunque $C$, il circuito è sottovincolato (poiché la logica del mutante è semanticamente diversa, l'output non dovrebbe essere accettato).
4. Ricerca Guidata: Per navigare nello spazio di ricerca vasto dei grandi campi primi e delle infinite possibilità di mutazione, ZKFUZZ impiega un algoritmo genetico:
   • Funzione di Fitness: Una nuova funzione di fitness min-sum calcola la somma degli errori di vincolo su tutti i vincoli per una data traccia. Il mutante viene valutato in base alla somma minima degli errori su input campionati. Questo differisce dai precedenti metodi basati solo sul massimo ed è più adatto alla mutazione congiunta.
   • Selettori di Target: Il sistema utilizza l'analisi statica per guidare la mutazione e la generazione degli input verso pattern ad alto rischio, come:
     • Divisione per Zero: Generazione di input dove numeratore e denominatore sono entrambi zero.
     • Controllo Hash: Forzare input a soddisfare vincoli di uguaglianza hash.
     • Distribuzione Distorta: Biasing della generazione degli input verso casi limite (0, 1 e valori vicini al modulo del campo $q$).
     • Whitelisting: Saltare template noti come sicuri (ad esempio, IsZero, Num2Bits) per concentrarsi sul codice soggetto a errori.

3. Contributi Chiave

1. Framework TCCT: Un modello formale unificato e indipendente dal linguaggio che ingloba le definizioni precedenti e cattura l'intero spazio dei bug ZK, inclusi quelli derivanti da terminazioni anomale e disallineamenti di valori intermedi.
2. Sistema ZKFUZZ: Un nuovo framework di fuzzing che muta congiuntamente programmi e input per rilevare violazioni TCCT, utilizzando una funzione di fitness min-sum ed euristiche di ricerca guidata.
3. Validazione Empirica: Valutazione su 452 circuiti Circom reali, che dimostra prestazioni superiori rispetto agli strumenti all'avanguardia.
4. Prototipo Noir: Un'implementazione preliminare per Noir, un diverso DSL ZK, che dimostra il potenziale del framework per l'indipendenza linguistica.

4. Risultati

Gli autori hanno valutato ZKFUZZ su 452 circuiti Circom reali, confrontandolo con quattro strumenti all'avanguardia: Circomspect, ZKAP, Picus e ConsCS.

• Rilevamento di Bug: ZKFUZZ ha identificato 85 bug unici, inclusi 59 vulnerabilità zero-day precedentemente sconosciute. Di questi, 39 sono stati confermati dagli sviluppatori e 14 sono stati risolti.
• Confronto: ZKFUZZ ha trovato dal 30% al 300% in più di bug rispetto agli strumenti esistenti su varie dimensioni di circuiti.
• Precisione: ZKFUZZ ha raggiunto il 100% di precisione (zero falsi positivi), mentre gli analizzatori statici come Circomspect e ZKAP presentavano alti tassi di falsi positivi (precisione compresa tra 0,06 e 0,75).
• Velocità: ZKFUZZ++ (con selettori di target) ha identificato oltre il 90% dei bug entro 100 secondi, superando significativamente i metodi formali e gli analizzatori statici.
• Impatto: I bug scoperti includevano vulnerabilità critiche di sottovincolo in progetti come zk-regex e passport-zk-circuits, che avrebbero potuto permettere agli attaccanti di falsificare prove o sottrarre fondi.

5. Significato e Affermazioni

Il paper afferma che ZKFUZZ rappresenta un avanzamento significativo nella sicurezza dei circuiti ZK affrontando l'incompletezza fondamentale delle definizioni precedenti delle vulnerabilità. Formalizzando i bug come incoerenze traccia-vincolo (TCCT), gli autori espongono una vasta classe di vulnerabilità (quasi il 50% dei bug reali nella loro valutazione) che erano precedentemente non rilevabili da strumenti focalizzati esclusivamente sulla non-deterministicità dei vincoli.

La capacità del sistema di rilevare bug senza falsi positivi lo rende uno strumento pratico per gli sviluppatori, che spesso ignorano gli avvisi provenienti da analizzatori statici ad alto tasso di falsi positivi. Inoltre, il rilevamento riuscito di bug nei circuiti Noir suggerisce che il framework TCCT e l'architettura di ZKFUZZ non sono limitati a Circom, ma possono generalizzarsi ad altri linguaggi ZK che compilano in formati di vincoli standardizzati.

Gli autori sottolineano che il loro lavoro si concentra sulle vulnerabilità derivanti dal disallineamento tra calcolo e vincoli (soundness e completezza), escludendo esplicitamente i bug nei sistemi di prova sottostanti, errori di logica pura (come input non utilizzati) o fughe di conoscenza zero a livello di protocollo.