💻 computer science

Formally Verifying Noir Zero Knowledge Programs with NAVe

Questo articolo presenta NAVe, un verificatore formale open-source che utilizza SMT-LIB e il solver cvc5 per verificare formalmente la correttezza e i vincoli appropriati dei programmi zero-knowledge di Noir, traducendo la loro rappresentazione intermedia ACIR in equazioni polinomiali a campo finito.

Autori originali: Pedro Antonino, Namrata Jain

Pubblicato 2026-01-15

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Pedro Antonino, Namrata Jain

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di voler costruire una cassaforte ad alta sicurezza. Vuoi dimostrare a un direttore di banca che conosci la combinazione della cassaforte senza però rivelargli effettivamente qual è la combinazione. Questo è il potere magico delle prove a conoscenza zero (Zero-Knowledge o ZK proofs).

Tuttavia, costruire queste casseforti è complicato. I "progetti" per queste prove sono puzzle matematici complessi chiamati circuiti aritmetici. Se anche una singola riga del progetto è errata, la cassaforte potrebbe essere insicura o la prova potrebbe fallire.

Questo articolo presenta uno strumento nuovo chiamato NAVe (Noir Acir Verifier), progettato per controllare questi progetti alla ricerca di errori prima che vengano effettivamente utilizzati. Ecco come funziona, spiegato in modo semplice:

1. Il Problema: La "Ricetta Segreta" contro il "Libro di Cucina"

Gli autori si concentrano su un linguaggio di programmazione chiamato Noir. Pensa a Noir come a un libro di cucina ad alto livello che rende facile scrivere ricette per queste casseforti.

Il Cuoco (Sviluppatore): Scrive una ricetta in un Noir facile da leggere.
Il Traduttore (Compilatore): Trasforma quella ricetta in un manuale di istruzioni a basso livello chiamato ACIR. Questo manuale è un elenco di equazioni matematiche che il computer deve risolvere per dimostrare che la cassaforte è sicura.
Il Pericolo: A volte il traduttore commette un errore, o il cuoco dimentica di includere un passaggio cruciale. Nel mondo della ZK, questo è chiamato essere "sotto-vincolato" (under-constrained). È come scrivere una ricetta che dice "aggiungi sale" ma dimenticare di dire quanto. Il risultato potrebbe essere commestibile, ma non è il piatto che intendevi preparare.

2. La Soluzione: Il "Detective Matematico" (NAVe)

Gli autori hanno creato NAVe, un verificatore formale. Pensa a NAVe come a un super-intelligente detective matematico che legge il manuale di istruzioni a basso livello (ACIR) e controlla se la matematica corrisponde effettivamente a ciò che il cuoco intendeva.

NAVe utilizza un potente motore logico (chiamato SMT solver) per porre domande come:

"Se inserisco un numero segreto, la matematica porterà sempre alla prova pubblica corretta?"
"Esiste un modo per ingannare il sistema con un numero falso?"

Se la matematica è guasta, NAVe non si limita a dire "Errore". Agisce come un detective che trova un indizio: mostra allo sviluppatore esattamente quale numero avrebbe potuto usare per rompere il sistema. Questo li aiuta a correggere il progetto immediatamente.

3. Due modi per risolvere il puzzle

L'articolo descrive due modi diversi in cui NAVe traduce i puzzle matematici per risolverli:

Il Metodo degli Interi: Tratta i numeri come normali numeri interi (1, 2, 3...) e controlla la matematica usando le regole aritmetiche standard.
Il Metodo del Campo Finito (Finite Field): Tratta i numeri come se fossero su un orologio circolare (dove dopo un certo numero si torna a zero). È così che funzionano le vere prove ZK.

Gli autori hanno scoperto che nessuno dei due metodi è perfetto per ogni situazione. A volte il detective degli "Interi" è più veloce; altre volte, il detective del "Campo Finito" è migliore. Suggeriscono di usare entrambi i detective contemporaneamente per ottenere il miglior risultato.

4. La Trappola dell' "Inosservanza dei Vincoli" (Unconstrained)

Una caratteristica unica di Noir è il "codice non vincolato" (unconstrained code). Immagina una parte della ricetta in cui lo chef è autorizzato a indovinare gli ingredienti senza essere controllato. Questo è utile per la velocità, ma pericoloso se lo chef indovina male.

Il Rischio: Uno sviluppatore potrebbe scrivere del codice che sembra controllare gli ingredienti, ma poiché si trova nella sezione "non vincolata", il computer non impone effettivamente il controllo.
Il Lavoro di NAVe: NAVe cerca specificamente questi "controlli fantasma". Verifica che anche se uno sviluppatore utilizza la sezione delle "ipotesi", abbia aggiunto una regola separata e rigorosa (un assert) per assicurarsi che l'ipotesi sia stata effettivamente corretta.

5. Cosa hanno scoperto

Gli autori hanno testato NAVe su una varietà di programmi Noir esistenti:

Funziona: NAVe è riuscito a individuare errori in programmi in cui la matematica non corrispondeva all'intento.
Il Collo di Bottiglia: Hanno scoperto che controllare i "vincoli di intervallo" (assicurarsi che un numero rientri entro un certo numero di bit, come controllare se un numero è compreso tra 0 e 255) è molto difficile per il detective matematico. A volte richiede molto tempo o si blocca.
Il Futuro: Prevedono di costruire migliori "scorciatoie" (astrazioni) per aiutare il detective a risolvere questi complicati puzzle di intervallo più velocemente.

Riassunto

In breve, NAVe è una rete di sicurezza per gli sviluppatori che costruiscono applicazioni che preservano la privacy. Traduce il loro codice in un linguaggio matematico rigoroso e utilizza un potente risolutore per garantire che il codice faccia esattamente ciò che dichiara di fare, intercettando bug sottili che potrebbero altrimenti portare a fallimenti della sicurezza. È come avere un ispettore rigoroso che controlla l'integrità strutturale di un ponte prima che a chiunque sia permesso attraversarlo.

Sintesi Tecnica: Verifica Formale di Programmi Zero-Knowledge in Noir con NAVe

Problematica
I sistemi di prova Zero-Knowledge (ZK) si basano su circuiti aritmetici — insiemi di equazioni polinomiali su campi finiti — per verificare che un input privato $W$ soddisfi una relazione $R(X, W)$ senza rivelare $W$ . I linguaggi di alto livello Domain-Specific (DSL) come Noir semplificano la creazione di questi circuiti compilando il codice in una rappresentazione intermedia chiamata ACIR (Abstract Circuit Intermediate Representation). Tuttavia, questa astrazione introduce vulnerabilità sottili. Nello specifico, Noir supporta il "codice non vincolato" (tramite funzioni unconstrained e blocchi unsafe) progettato per migliorare l'efficienza della prova delegando computazioni complesse al prover. Se gli sviluppatori non aggiungono manualmente i corrispondenti vincoli (ad esempio, tramite istruzioni assert) per i risultati del codice non vincolato, il circuito aritmetico generato potrebbe non catturare accuratamente la relazione intesa. Questo bug di "sotto-vincolo" (under-constrained) può portare a gravi vulnerabilità di sicurezza, come consentire a un prover di generare prove valide per affermazioni false. Gli strumenti di verifica formale esistenti prendono in bersaglio principalmente DSL di circuiti a basso livello (come Circom) o richiedono la dimostrazione dei teoremi interattiva, mancando di una verifica automatizzata e scalabile per programmi Noir di alto livello e le loro specifiche funzionalità, come la manipolazione della memoria e le funzioni black-box.

Metodologia
Gli autori propongono NAVe (Noir Acir Verifier), un framework di verifica formale open-source che opera sulla rappresentazione intermedia ACIR piuttosto che sul codice sorgente Noir di alto livello. Questa scelta garantisce stabilità rispetto all'evoluzione del linguaggio e consente allo strumento di supportare potenzialmente altri linguaggi che mirano ad ACIR.

Formalizzazione tramite SMT-LIB: Il cuore di NAVe è una formalizzazione di un sottoinsieme di opcode ACIR in formule Satisfiability Modulo Theories (SMT). Gli autori implementano due codifiche distinte:
- Codifica di Campo Finito (Finite Field Encoding): Utilizza una teoria non standard di campi finiti di ordine primo implementata nel solver cvc5. Questo approccio utilizza operatori specifici come ff.add, ff.mul e ff.bitsum per modellare direttamente l'aritmetica di campo.
- Codifica di Aritmetica Intera (Integer Arithmetic Encoding): Sfrutta la teoria standard degli interi in SMT-LIB. Si basa sull'isomorfismo tra campi finiti di ordine primo $p$ e interi modulo $p$ , codificando le operazioni di campo come aritmetica modulare degli interi (ad esempio, (mod (+ ...) p)).
Semantica degli Opcode: La formalizzazione copre i principali opcode ACIR:
- AssertZero: Codificato come un vincolo di equazione polinomiale uguale a zero.
- BlackBoxFuncCall: Specificamente formalizzato per l'opcode di controllo del range (Range). Nella codifica di campo finito, questo è modellato tramite una decomposizione binaria (bitsum) e vincoli che assicurano che i bit siano 0 o 1. Nella codifica intera, è modellato utilizzando l'ordinamento standard degli interi ( $x < 2^n$ ).
- MemoryOp e MemoryInit: Formalizzati per tracciare le mutazioni degli array utilizzando una mappa di indici associati a valori di testimone (witness), gestendo sia le operazioni di lettura che di scrittura sequenzialmente.
- BrilligCall: Rappresentando il codice non vincolato, questi sono tradotti come il vincolo sempre soddisfatto true (o ignorati), poiché l'obiettivo del verificatore è controllare i vincoli al di fuori dei blocchi non vincolati.
Workflow di Verifica:
- Lo strumento si integra con Nargo, il gestore di pacchetti di Noir, come comando formal-verify.
- Gli sviluppatori annotano i programmi Noir con istruzioni verify_assert(b: bool). A differenza delle normali istruzioni assert che generano vincoli di circuito, verify_assert crea un'obbligazione di prova (proof obligation).
- NAVe compila il programma Noir in ACIR, traduce gli opcode ACIR in formule SMT e costruisce la formula di verifica $F = \text{ACIR}_{\text{constraints}} \land \neg \text{verify\_assert}_{\text{condition}}$ .
- Il solver cvc5 controlla la soddisfacibilità di $F$ . Se $F$ è insoddisfacibile (unsatisfiable), la condizione di verifica è soddisfatta (il programma è correttamente vincolato). Se $F$ è soddisfacibile (satisfiable), il solver restituisce un modello (controesempio) che mostra un'assegnazione di testimone che viola la condizione, aiutando nel debugging.

Contributi Chiave

Formalizzazione di ACIR: La prima formalizzazione di un sottoinsieme del linguaggio ACIR utilizzando SMT-LIB, che copre funzionalità complesse come le operazioni di memoria, i controlli del range e la distinzione tra codice vincolato e non vincolato.
Strategia di Doppia Codifica: La proposta di due codifiche complementari (teoria del campo finito e aritmetica intera) per sfruttare le diverse capacità dei solver.
Strumento NAVe: Un verificatore formale automatizzato e open-source integrato nell'ecosistema Noir, progettato per essere accessibile agli sviluppatori senza richiedere la dimostrazione interattiva dei teoremi.
Valutazione Empirica: Una valutazione completa di NAVe su una suite di programmi di test in Noir, analizzando le prestazioni attraverso diversi tipi di vincoli e configurazioni di solver.

Risultati
Gli autori hanno valutato NAVe su 4 set distinti di programmi Noir (condizioni verificate, condizioni falsificate, con e senza controlli del range) utilizzando il solver cvc5.

Prestazioni del Solver: Nessun backend (codifica intera, --ff=gb di campo finito o --ff=split di campo finito) ha superato costantemente gli altri. I risultati indicano che le codifiche sono complementari; alcuni programmi sono risolti più velocemente da una codifica, mentre altri vanno in timeout con quella stessa codifica ma hanno successo con un'altra.
Impatto dei Controlli del Range: I programmi contenenti controlli Range (opcode BlackBoxFuncCall) hanno aumentato significativamente il tempo di verifica. La configurazione --ff=split, che approssima la teoria del campo finito, ha mostrato prestazioni superiori sui programmi con ampi controlli del range rispetto alla configurazione predefinita --ff=gb, sebbene si siano verificati comunque timeout per i casi complessi.
Generazione di Controesempi: Lo strumento ha generato con successo controesempi per le condizioni falsificate, dimostrando la sua utilità nell'identificare la logica sotto-vincolata.

Significatività e Rivendicazioni
L'articolo sostiene che NAVe affronti una lacuna critica nell'ecosistema ZK fornendo un metodo automatizzato e scalabile per verificare programmi ZK di alto livello per bug di sotto-vincolo, una classe di errori che ha portato a vulnerabilità reali. Mirando ad ACIR, lo strumento rimane robusto rispetto ai cambiamenti nella sintassi di alto livello di Noir ed è potenzialmente applicabile ad altri linguaggi che puntano alla stessa rappresentazione intermedia.

Gli autori inquadrano modestamente il loro lavoro come un passo verso capacità di verifica più ampie. Riconoscono che la loro formalizzazione attuale copre solo un sottoinsieme di ACIR (escludendo le chiamate Call ricorsive e la maggior parte delle BlackBoxFuncCall eccetto Range). Identificano l'alto costo della verifica dei controlli del range come una limitazione primaria, suggerendo che il lavoro futuro debba concentrarsi sullo sviluppo di astrazioni o approssimazioni per gestire in modo efficiente questi vincoli complessi. L'articolo posiziona NAVe non come una soluzione completa per tutte le esigenze di verifica ZK, ma come uno strumento pratico e integrato che dimostra la fattibilità della verifica formale automatizzata per Noir e traccia un percorso per migliorare la gestione dei vincoli a livello di bit da parte dei solver.