💻 computer science

Formally Verifying Noir Zero Knowledge Programs with NAVe

Dit artikel presenteert NAVe, een open-source formele verifieerder die SMT-LIB en de cvc5-solver gebruikt om de correctheid en de juiste beperkingen van Noir zero-knowledge-programma's formeel te verifiëren door hun ACIR-tussenrepresentatie te vertalen naar polynoomvergelijkingen over eindige velden.

Oorspronkelijke auteurs: Pedro Antonino, Namrata Jain

Gepubliceerd 2026-01-15

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Pedro Antonino, Namrata Jain

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een hoogbeveiligde kluis bouwt. Je wilt aan een bankdirecteur bewijzen dat je de combinatie van de kluis kent, zonder hem de combinatie daadwerkelijk te vertellen. Dit is de magie van Zero-Knowledge (ZK) proofs.

Het bouwen van deze kluizen is echter lastig. De "blauwdrukken" voor deze bewijzen zijn complexe wiskundige puzzels die arithmetic circuits worden genoemd. Als één regel van de blauwdruk fout is, kan de kluis onveilig zijn, of kan het bewijs mislukken.

Dit artikel introduceert een nieuwe tool genaamd NAVe (Noir Acir Verifier), ontworpen om deze blauwdrukken te controleren op fouten voordat ze ooit worden gebruikt. Hier is hoe het werkt, eenvoudig uitgelegd:

1. Het Probleem: Het "Geheime Recept" versus het "Kookboek"

De auteurs richten zich op een programmeertaal genaamd Noir. Denk aan Noir als een hoogwaardig kookboek dat het makkelijk maakt om recepten voor deze kluizen te schrijven.

De Kok (Developer): Schrijft een recept in gemakkelijk leesbare Noir.
De Vertaler (Compiler): Vertaalt dat recept naar een strikte, laag-niveau instructiehandleiding genaamd ACIR. Deze handleiding is een lijst met wiskundige vergelijkingen die de computer moet oplossen om te bewijzen dat de kluis veilig is.
Het Gevaar: Soms maakt de vertaler een fout, of vergeet de kok een cruciale stap toe te voegen. In de wereld van ZK wordt dit "under-constrained" genoemd. Het is alsof je een recept schrijft waarin staat "voeg zout toe", maar vergeet te vermelden hoeveel. Het resultaat is misschien eetbaar, maar het is niet het gerecht dat je bedoelde.

2. De Oplossing: De "Wiskundige Detective" (NAVe)

De auteurs hebben NAVe gecreëerd, een formele verifieerder. Denk aan NAVe als een super slimme wiskundige detective die de laag-niveau instructiehandleiding (ACIR) leest en controleert of de wiskunde daadwerkelijk overeenkomt met wat de kok bedoelde.

NAVe gebruikt een krachtige logische engine (een SMT solver) om vragen te stellen zoals:

"Als ik een geheim getal invoer, resulteert de wiskunde dan altijd in het juiste publieke bewijs?"
"Is er een manier om het systeem te misleiden met een vals getal?"

Als de wiskunde niet klopt, zegt NAVe niet alleen "Error". Het gedraagt zich als een detective die een aanwijzing vindt: het laat de ontwikkelaar precies zien welk getal zij hadden kunnen gebruiken om het systeem te breken. Dit helpt hen om de blauwdruk direct te herstellen.

3. Twee Manieren om de Puzzel Op te Lossen

Het paper beschrijft twee verschillende manieren waarop NAVe de wiskundige puzzels vertaalt om ze op te lossen:

De Integer-manier: Het behandelt de getallen als gewone gehele getallen (1, 2, 3...) en controleert de wiskunde met standaard rekenregels.
De Finite Field-manier: Het behandelt de getallen alsof ze op een cirkelvormige klok staan (waarbij je na een bepaald getal weer terugvalt naar nul). Dit is hoe de werkelijke ZK-bewijzen werken.

De auteurs ontdekten dat geen van beide methoden perfect is voor elke situatie. Soms is de "Integer"-detective sneller; andere keren is de "Finite Field"-detective beter. Ze suggereren om beide detectives tegelijkertief te gebruiken voor het beste resultaat.

4. De "Unconstrained" Valstrik

Een uniek kenmerk van Noir is "unconstrained code". Stel je een deel van het recept voor waar de chef de ingrediënten mag raden zonder dat dit gecontroleerd wordt. Dit is nuttig voor de snelheid, maar gevaarlijk als de chef het fout heeft.

Het Risico: Een ontwikkelaar kan code schrijven die lijkt op een controle van de ingrediënten, maar omdat het in het "unconstrained" gedeelte staat, dwingt de computer de controle niet echt af.
De Taak van NAVe: NAVe zoekt specifiek naar deze "ghost checks". Het verifieert dat zelfs als een ontwikkelaar het "raden"-gedeelte gebruikt, hij een aparte, strikte regel (een assert) heeft toegevoegd om te controleren of de gok daadwerkelijk correct was.

5. Wat Ze Hebben Ontdekt

De auteurs hebben NAVe getest op een verscheidenheid aan bestaande Noir-programma's:

Het Werkt: NAVe heeft succesvol fouten opgevangen in programma's waar de wiskunde niet overeenkwam met de intentie.
De Bottleneck: Ze ontdekten dat het controleren van "range constraints" (controleren of een getal binnen een specifiek aantal bits past, zoals controleren of een getal tussen 0 en 255 ligt) erg moeilijk is voor de wiskundige detective. Het duurt soms lang of loopt vast.
De Toekomst: Ze zijn van plan om betere "shortcuts" (abstracties) te bouwen om de detective te helpen deze lastige range-puzzels sneller op te lossen.

Samenvatting

Kortom, NAVe is een vangnet voor ontwikkelaars die privacy-beschermende applicaties bouwen. Het vertaalt hun code naar een strikte wiskundige taal en gebruikt een krachtige solver om te garanderen dat de code precies doet wat deze beweert te doen, waarbij subtiele bugs worden opgevangen die anders tot beveiligingsproblemen zouden kunnen leiden. Het is alsof er een rigoureuze inspecteur de structurele integriteit van een brug controleert voordat er iemand overheen mag rijden.

Technische Samenvatting: Formele verificatie van Noir Zero-Knowledge programma's met NAVe

Probleemstelling
Zero-Knowledge (ZK) bewijssystemen vertrouwen op rekenkundige circuits—verzamelingen van polynoomvergelijkingen over eindige velden—om te verifiëren dat een private input $W$ een relatie $R(X, W)$ vervult zonder $W$ te onthullen. High-level Domain-Specific Languages (DSLs) zoals Noir vereenvoudigen het maken van deze circuits door code te compileren naar een intermediate representation genaamd ACIR (Abstract Circuit Intermediate Representation). Deze abstractie introduceert echter subtiele kwetsbaarheden. Specifiek ondersteunt Noir "onconstrained code" (via unconstrained functies en unsafe blokken) die ontworpen is om de efficiëntie van het bewijs te verbeteren door complexe berekeningen naar de prover te verplaatsen. Als ontwikkelaars er niet in slagen om handmatig overeenkomstige constraints toe te voegen (bijv. via assert statements) voor de resultaten van unconstrained code, kan de gegenereerde rekenkundige circuit de beoogde relatie mogelijk niet accuraat weergeven. Deze "under-constrained" bug kan leiden tot ernstige beveiligingskwetsbaarheden, zoals het toestaan dat een prover geldige bewijzen genereert voor onjuiste beweringen. Bestaande formele verificatietools richten zich grotendeels op lagere-niveau circuit DSL's (zoals Circom) of vereisen interactief bewijs, en missen geautomatiseerde, schaalbare verificatie voor high-level Noir-programma's en hun specifieke kenmerken zoals geheugenmanipulatie en black-box functies.

Methodologie
De auteurs stellen NAVe (Noir Acir Verifier) voor, een open-source formeel verificatieframework dat opereert op de ACIR intermediate representation in plaats van de high-level Noir broncode. Deze keuze zorgt voor stabiliteit tegen taalevolutie en stelt het hulpmiddel in staat om potentieel andere talen te ondersteunen die ACIR targeten.

Formalisering via SMT-LIB: De kern van NAVe is een formalisering van een subset van ACIR opcodes naar Satisfiability Modulo Theories (SMT) formules. De auteurs implementeren twee verschillende encodings:
- Finite Field Encoding: Maakt gebruik van een niet-standaard theorie van eindige velden van priemorde, geïmplementeerd in de cvc5 solver. Deze aanpak gebruikt specifieke operatoren zoals ff.add, ff.mul en ff.bitsum om veld-arithmetiek direct te modelleren.
- Integer Arithmetic Encoding: Maakt gebruik van de standaard theorie van integers in SMT-LIB. Het vertrouwt op de isomorfie tussen eindige velden van priemorde $p$ en integers modulo $p$ , waarbij veld-operaties worden gecodeerd als modulaire integer-arithmetiek (bijv. (mod (+ ...) p)).
Opcode Semantiek: De formalisering dekt belangrijke ACIR opcodes:
- AssertZero: Gecodeerd als een polynoomvergelijking constraint gelijk aan nul.
- BlackBoxFuncCall: Specifiek geformaliseerd voor de Range check opcode. In de finite-field encoding wordt dit gemodelleerd met een binaire decompositie (bitsum) en constraints die garanderen dat bits 0 of 1 zijn. In de integer encoding wordt dit gemodelleerd met standaard integer ordeningsconstraints ( $x < 2^n$ ).
- MemoryOp en MemoryInit: Geformaliseerd om array-mutaties bij te houden met behulp van een map van indices naar witness-waarden, waarbij zowel read als write operaties sequentieel worden afgehandeld.
- BrilligCall: Representeert unconstrained code; deze worden vertaald als de altijd-voldane constraint true (of genegeerd), aangezien het doel van de verifier is om de constraints buiten de unconstrained blokken te controleren.
Verificatie Workflow:
- Het hulpmiddel integreert met Nargo, de Noir package manager, als een formal-verify command.
- Ontwikkelaars annoteren Noir-programma's met verify_assert(b: bool) statements. In tegenstelling tot standaard assert statements die circuit constraints genereren, creëert verify_assert een bewijslast (proof obligation).
- NAVe compileert het Noir-programma naar ACIR, vertaalt de ACIR opcodes naar SMT-formules, en construeert een verificatieformule $F = \text{ACIR}_{\text{constraints}} \land \neg \text{verify\_assert}_{\text{condition}}$ .
- De cvc5 solver controleert de bevredigbaarheid van $F$ . Als $F$ unsatisfiable is, houdt de verificatievoorwaarde stand (het programma is correct geconstraineerd). Als $F$ satisfiable is, geeft de solver een model (tegenvoorbeeld) terug dat een witness-toewijzing laat zien die de conditie schendt, wat helpt bij het debuggen.

Belangrijkste Bijdragen

Formalisering van ACIR: De eerste formalisering van een subset van de ACIR-taal met behulp van SMT-LIB, die complexe kenmerken zoals geheugenoperaties, range checks en het onderscheid tussen constrained en unconstrained code dekt.
Dual Encoding Strategy: De voorstel van twee complementaire encodings (finite-field theorie en integer arithmetic) om de verschillende mogelijkheden van solvers te benutten.
NAVe Tool: Een open-source, geautomatiseerde formele verifier geïntegreerd in het Noir-ecosysteem (Nargo), ontworpen om toegankelijk te zijn voor ontwikkelaars zonder dat zij interactief bewijs vereisen.
Empirische Evaluatie: Een uitgebreide evaluatie van NAVe op een suite van Noir testprogramma's, waarbij de prestaties over verschillende constraint-typen en solver-configuraties worden geanalyseerd.

Resultaten
De auteurs hebben NAVe geëvalueerd op 4 verschillende sets Noir-programma's (geverifieerde condities, gefalsifieerde condities, met en zonder range checks) met behulp van de cvc5 solver.

Solver Performance: Geen enkele backend (integer encoding, finite-field --ff=gb, of finite-field --ff=split) presteerde consistent beter dan de andere. De resultaten geven aan dat de encodings complementair zijn; sommige programma's worden sneller opgelost door één encoding, terwijl andere tijdslimieten overschrijden op diezelfde encoding maar slagen met een andere.
Impact van Range Checks: Programma's die Range checks bevatten (BlackBoxFuncCall opcodes) verhoogden de verificatietijd aanzienlijk. De --ff=split configuratie, die de finite-field theorie benadert, vertoonde een superieure prestatie op programma's met grote range checks vergeleken met de standaard --ff=gb configuratie, hoewel timeouts nog steeds voorkwamen bij complexe gevallen.
Counterexample Generation: Het hulpmiddel genereerde succesvol tegenvoorbeelden voor gefalsifieerde condities, wat het nut ervan aantoont bij het identificeren van under-constrained logica.

Betekenis en Claims
Het artikel beweert dat NAVe een kritieke kloof in de ZK-ecosysteem aanpakt door een geautomatiseerde, schaalbare methode te bieden voor het verifiëren van high-level ZK-programma's op under-constrained bugs, een klasse van fouten die tot reële kwetsbaarheden heeft geleid. Door ACIR te targeten, blijft het hulpmiddel robuust tegen veranderingen in de high-level Noir syntaxis en is het potentieel toepasbaar op andere talen die dezelfde intermediate representation targeten.

De auteurs kaderen hun werk bescheiden als een stap naar bredere verificatiemogelijkheden. Ze erkennen dat hun huidige formalisering slechts een subset van ACIR dekt (exclusief recursieve Call opcodes en de meeste BlackBoxFuncCalls behalve Range). Ze identificeren de hoge kosten van het verifiëren van range checks als een primaire beperking, en suggereren dat toekomstig werk zich moet richten op het ontwikkelen van abstracties of benaderingen om deze complexe constraints efficiënter te kunnen afhandelen. Het artikel positioneert NAVe niet als een volledige oplossing voor alle ZK-verificatiebehoeften, maar als een praktisch, geïntegreerd hulpmiddel dat de haalbaarheid van geautomatiseerde formele verificatie voor Noir aantoont en een pad uitstippelt voor het verbeteren van de solver-afhandeling van complexe bit-level constraints.