💻 computer science

zkFuzz: Foundation and Framework for Effective Fuzzing of Zero-Knowledge Circuits

Dit artikel introduceert zkFuzz, een nieuw mutatiegebaseerd fuzzing-kader dat is gebaseerd op de theoretische Trace-Constraint Consistency Test (TCCT), en dat effectief zowel onder- als over-beperkte kwetsbaarheden in zero-knowledge circuits detecteert door de beperkingen van bestaande statische en formele analysehulpmiddelen te overwinnen.

Oorspronkelijke auteurs: Hideaki Takahashi, Jihwan Kim, Suman Jana, Junfeng Yang

Gepubliceerd 2026-05-26

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Hideaki Takahashi, Jihwan Kim, Suman Jana, Junfeng Yang

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 magische kluis bouwt die bewijst dat je een geheim wachtwoord kent, zonder het wachtwoord ooit daadwerkelijk te tonen. Dit is wat "Zero-Knowledge (ZK)-circuits" doen in de digitale wereld. Ze fungeren als de beveiligingswachten voor privacybehoudende technologieën zoals anonieme cryptocurrencies en veilige stemsystemen.

Het bouwen van deze kluizen is echter ontzettend lastig. Als je een klein foutje maakt in de blauwdrukken, kan de kluis het volgende doen:

Iedereen binnenlaten (zelfs als ze het wachtwoord niet kennen).
De echte eigenaar buitensluiten (zelfs als ze het juiste wachtwoord hebben).

Het artikel introduceert een nieuw hulpmiddel genaamd ZKFUZZ om deze fouten te vinden voordat kwaadwillenden dat doen. Hier is hoe het werkt, simpel uitgelegd:

Het Probleem: De "Blauwdruk" versus de "Realiteit"

In deze systemen schrijven ontwikkelaars een programma dat twee dingen tegelijk doet:

De Berekening: De feitelijke wiskunde om het geheim te achterhalen (zoals het berekenen van een route op een kaart).
De Beperkingen: De regels die bewijzen dat de wiskunde correct is uitgevoerd (zoals een checklist om te verifiëren dat de route bestaat).

Het probleem is dat deze twee delen vaak uit sync raken.

Onder-beperkt: De regels zijn te los. Een hacker kan het systeem bedriegen om een nep-route te accepteren.
Over-beperkt: De regels zijn te streng. Het systeem weigert een perfect geldige route vanwege een klein, onnodig regel.

Bestaande tools om deze fouten te vinden, lijken op slechte spellingscontroles. Ze gokken op basis van patronen en schreeuwen "FOUT!" bij dingen die eigenlijk goed zijn (valse alarmen), of ze missen diepe, complexe fouten volledig.

De Oplossing: ZKFUZZ (De "Mutatie Fuzzer")

De auteurs hebben een nieuw raamwerk ontwikkeld genaamd ZKFUZZ. In plaats van alleen de code te lezen, treedt ZKFUZZ op als een kieskeurige testengineer die het systeem opzettelijk probeert te breken.

Hier is de analogie:
Stel je voor dat je een recept hebt (de berekening) en een proeverij (de beperkingen).

Oude Tools: Kijken naar het recept en zeggen: "Dit ziet er verdacht uit omdat het zout gebruikt." (Ze gokken op basis van regels).
ZKFUZZ: Kookt daadwerkelijk het gerecht, maar mutateert vervolgens het recept. Het verwisselt "suiker" met "zout", of verandert de kooktijd. Vervolgens voert het dit gemuteerde gerecht aan de proeverij.
- Als de proeverij zegt: "Lekker!" tegen een gerecht dat slecht had moeten smaken (omdat het recept was veranderd), weet ZKFUZZ dat de regels te los zijn (Onder-beperkt).
- Als de proeverij zegt: "Ew!" tegen een gerecht dat heerlijk had moeten zijn (omdat het originele recept correct was), weet ZKFUZZ dat de regels te streng zijn (Over-beperkt).

Het Geheime Ingrediënt: "Fitness" en "Targeting"

Het vinden van een bug in een ZK-circuit is als het zoeken naar een speld in een hooiberg ter grootte van een planeet. De betrokken getallen zijn zo enorm dat een computer niet zomaar elke mogelijkheid kan proberen.

ZKFUZZ maakt gebruik van een Genetisch Algorithm (zoals evolutie):

Mutatie: Het creëert duizenden lichtelijk gebroken versies van het programma.
Fitness Score: Het beoordeelt deze gebroken versies. Als een gebroken versie dichtbij komt om de test te slagen (zelfs als het faalt), krijgt het een "goede score". Dit vertelt het systeem: "Je wordt warmer!"
Targeting: Het gokt niet zomaar willekeurig. Het weet dat bugs vaak voorkomen bij "edge cases" (zoals wanneer getallen nul zijn, of extreem groot). Het probeert specifiek het systeem deze lastige getallen te voeren om te zien of het breekt.

De Resultaten: Het Vangen van het Onzichtbare

Het team testte ZKFUZZ op 452 real-world circuits die worden gebruikt in echte projecten.

De Score: Het vond 85 bugs.
De Zero-Days: 59 hiervan waren nieuwe, onbekende bugs (Zero-Days) waarvan niemand wist dat ze bestonden.
De Impact: 39 hiervan werden bevestigd door de ontwikkelaars, en 14 zijn al gerepareerd. Dit omvat bugs in grote projecten zoals zkSync (een crypto-platform) en passport-zk-circuits (digitale ID-systemen).
Geen Valse Alarmen: In tegenstelling tot andere tools, markeerde ZKFUZZ niets als een bug dat geen bug was.

Waarom Dit Belangrijk Is

Het artikel betoogt dat eerdere tools een groot stuk van het probleem misten. Ze keken alleen naar "willekeurigheid" in de regels. ZKFUZZ introduceerde een nieuwe theorie genaamd TCCT (Trace-Constraint Consistency Test), die controleert of het daadwerkelijke pad dat de computer neemt overeenkomt met de regels die het zou moeten volgen.

Deze nieuwe theorie ving bugs op die ontstonden wanneer de computer "crashte" of onverwacht stopte, wat eerdere tools volledig negeerden.

In het Kort

ZKFUZZ is een slimme, geautomatiseerde "bugjager" die Zero-Knowledge circuits breekt door hun code te muteren en ze lastige invoer te geven. Het vond tientallen kritieke beveiligingsgaten die andere tools misten, en bewees dat zelfs in de complexe wereld van privacy-wiskunde, een beetje gecontroleerde chaos de beste manier is om de waarheid te vinden.

Technische Samenvatting: ZKFUZZ: Fundament en Kader voor Effectieve Fuzzing van Zero-Knowledge Circuits

1. Probleemstelling

Zero-knowledge (ZK) circuits vormen de basis voor privacybehoudende berekeningen en maken beknopte bewijzen en efficiënte verificatie mogelijk in toepassingen variërend van anonieme cryptocurrencies tot verifieerbare machine learning. Het ontwikkelen van correcte ZK-circuits is echter berucht moeilijk vanwege de misalignatie tussen logica voor algemene doeleinden en polynoombeperkingen in eindige velden.

Er bestaan twee hoofdklassen van kwetsbaarheden:

Onder-beperkte circuits: De beperkingen zijn te los, waardoor kwaadaardige bewijzers geldige bewijzen kunnen genereren voor ongeldige getuigenissen (schending van soundness).
Over-beperkte circuits: De beperkingen zijn te streng, waardoor het systeem geldige getuigenissen van eerlijke bewijzers afwijst (schending van completeness).

Bestaande detectiemethoden ondervinden aanzienlijke beperkingen:

Statische Analyse: Tools zoals Circomspect en ZKAP lijden vaak onder hoge rates van vals-positieven en slagen er niet in diepe semantische problemen te vangen, met name die welke betrekking hebben op tussenberekeningen of abnormale programma-afsluiting.
Formele Methoden: Tools die vertrouwen op SMT-oplossers (bijv. Picus, ConsCS) hebben moeite om te schalen naar circuits van werkelijke grootte en vertrouwen vaak op onvolledige definities van kwetsbaarheden, met de focus uitsluitend op non-determinisme in beperkingen terwijl gevallen worden genegeerd waarin de berekening afbreekt of waarin tussenwaarden niet overeenkomen.
Definitiegaten: Vorige formele definities van ZK-bugs zijn onvolledig. Ze negeren vaak "abnormale afsluiting" (waarbij een berekening crasht maar de beperkingen toch worden voldaan) en houden geen rekening met de volledige set van uitvoeringssporen, inclusief tussenwaarden.

2. Methodologie

2.1 Theoretisch Fundament: Trace-Constraint Consistentietest (TCCT)

De auteurs introduceren TCCT, een taal-onafhankelijk formeel kader dat ZK-kwetsbaarheden definieert als discrepanties tussen twee verzamelingen:

Trace Set $T(P)$ : De verzameling van alle mogelijke uitvoeringssporen (invoer, tussenwaarden, uitvoer) geproduceerd door het getuigenis-berekeningsprogramma $P$ .
Verzameling van Bevrediging van Beperkingen $S(C)$ : De verzameling van alle tuples (invoer, tussenwaarden, uitvoer) die voldoen aan de circuitbeperkingen $C$ .

TCCT definieert een circuit als goed-beperkt dan en slechts dan als:

Geen onder-beperking: De projectie van $S(C)$ op invoer-uitvoerparen is een deelverzameling van de projectie van $T(P)$ . Dit zorgt ervoor dat geen ongeldige sporen worden geaccepteerd.
Geen over-beperking: $T(P)$ is een deelverzameling van $S(C)$ . Dit zorgt ervoor dat alle geldige sporen (inclusief specifieke tussenwaarden) worden geaccepteerd.

Deze formulering vangt kwetsbaarheden op die worden veroorzaakt door afbrekingen van berekeningen (waarbij $P$ faalt maar $C$ de invoer accepteert) en mismatches in tussenwaarden, wat eerdere definities misten. De auteurs bewijzen dat het beslissen over onder- of over-beperking NP-compleet is, en de volledige TCCT co-NP-compleet is.

2.2 Systeemontwerp: ZKFUZZ

ZKFUZZ is een dynamisch analysekader dat TCCT-schendingen detecteert met behulp van een gezamenlijke programma-mutatie en invoergeneratie-aanpak. In tegenstelling tot traditionele fuzzing die alleen invoer muteren, muteren ZKFUZZ zowel de programmalogica als de invoer.

Kernworkflow:

Mutatie: Het systeem genereert mutanten ( $P'$ ) van het oorspronkelijke berekeningsprogramma ( $P$ ). Mutaties omvatten het verwijderen van asserties, het transformeren van toewijzingen (bijv. het vervangen van operatoren of waarden) en het wijzigen van zwakke toewijzingen.
Uitvoering: Zowel het oorspronkelijke programma ( $P$ ) als de mutant ( $P'$ ) worden uitgevoerd op bemonsterde invoer ( $x$ ).
Verificatie:
- Detectie van over-beperking: Als $P(x)$ een geldig spoor produceert dat $C$ faalt, is het circuit over-beperkt.
- Detectie van onder-beperking: Als $P'(x)$ een spoor produceert met een andere uitvoer ( $y' \neq y$ ) dat toch $C$ voldoet, is het circuit onder-beperkt (aangezien de mutantlogica semantisch anders is, zou de uitvoer niet geaccepteerd moeten worden).
Gestuurde zoektocht: Om de enorme zoekruimte van grote priemvelden en oneindige mutatiemogelijkheden te navigeren, hanteert ZKFUZZ een genetisch algoritme:
- Fitnessfunctie: Een nieuwe min-sum fitnessfunctie berekent de som van beperkingsfouten over alle beperkingen voor een gegeven spoor. De mutant wordt gescoord op basis van de som van de minimale fouten over de bemonsterde invoer. Dit verschilt van eerdere alleen-max-methoden en is beter geschikt voor gezamenlijke mutatie.
- Doelselectoren: Het systeem gebruikt statische analyse om mutatie en invoergeneratie te sturen naar hoog-risico patronen, zoals:
  - Delen door nul: Het genereren van invoer waarbij zowel teller als noemer nul zijn.
  - Hash-check: Het forceren van invoer om gelijkheidsbeperkingen voor hashes te voldoen.
  - Scheve verdeling: Het bevoorrechten van invoergeneratie naar randgevallen (0, 1 en waarden dicht bij de veldmodulus $q$ ).
  - Witlijsten: Het overslaan van bekende veilige sjablonen (bijv. IsZero, Num2Bits) om zich te richten op foutgevoelige code.

3. Belangrijkste Bijdragen

TCCT-kader: Een unificerend, taal-onafhankelijk formeel model dat eerdere definities omvat en de volledige ruimte van ZK-bugs vangt, inclusief die welke voortvloeien uit abnormale afsluiting en mismatches in tussenwaarden.
ZKFUZZ-systeem: Een nieuw fuzzing-kader dat programma's en invoer gezamenlijk muteren om TCCT-schendingen te detecteren, gebruikmakend van een min-sum fitnessfunctie en gestuurde zoekheuristieken.
Empirische Validatie: Evaluatie op 452 Circom-circuits uit de echte wereld, waarbij superieure prestaties worden aangetoond ten opzichte van state-of-the-art tools.
Noir-prototype: Een voorlopige implementatie voor Noir, een andere ZK-DSL, die het potentieel van het kader voor taal-onafhankelijkheid demonstreert.

4. Resultaten

De auteurs evalueerden ZKFUZZ op 452 Circom-circuits uit de echte wereld, waarbij ze het vergeleken met vier state-of-the-art tools: Circomspect, ZKAP, Picus en ConsCS.

Bug-detectie: ZKFUZZ identificeerde 85 unieke bugs, waaronder 59 eerder onbekende zero-day kwetsbaarheden. Van deze werden 39 bevestigd door ontwikkelaars en 14 opgelost.
Vergelijking: ZKFUZZ vond 30% tot 300% meer bugs dan bestaande tools over verschillende circuitgroottes.
Precisie: ZKFUZZ behaalde 100% precisie (nul vals-positieven), terwijl statische analyzers zoals Circomspect en ZKAP hoge rates van vals-positieven hadden (precisie variërend van 0,06 tot 0,75).
Snelheid: ZKFUZZ++ (met doelselectoren) identificeerde meer dan 90% van de bugs binnen 100 seconden, wat aanzienlijk beter presteert dan formele methoden en statische analyzers.
Impact: De ontdekte bugs omvatten kritieke onder-beperkte kwetsbaarheden in projecten zoals zk-regex en passport-zk-circuits, die aanvallers in staat zouden kunnen stellen bewijzen te vervalsen of fondsen te extraheren.

5. Betekenis en Claims

Het artikel beweert dat ZKFUZZ een aanzienlijke vooruitgang vertegenwoordigt in de beveiliging van ZK-circuits door de fundamentele onvolledigheid van eerdere kwetsbaarheidsdefinities aan te pakken. Door bugs te formaliseren als trace-constraint inconsistenties (TCCT), leggen de auteurs een grote klasse van kwetsbaarheden bloot (bijna 50% van de bugs uit de echte wereld in hun evaluatie) die eerder ondetecteerbaar waren voor tools die zich uitsluitend richtten op non-determinisme in beperkingen.

Het vermogen van het systeem om bugs te detecteren zonder vals-positieven maakt het een praktisch hulpmiddel voor ontwikkelaars, die vaak waarschuwingen negeren van statische analyzers met hoge rates van vals-positieven. Bovendien suggereert de succesvolle detectie van bugs in Noir-circuits dat het TCCT-kader en de ZKFUZZ-architectuur niet beperkt zijn tot Circom, maar kunnen generaliseren naar andere ZK-talen die compileren naar gestandaardiseerde beperkingsformaten.

De auteurs benadrukken dat hun werk zich richt op kwetsbaarheden die voortvloeien uit de misalignatie van berekening en beperkingen (soundness en completeness), en expliciet bugs uitsluit in de onderliggende bewijssystemen, pure logische fouten (zoals ongebruikte invoer) of zero-knowledge-lekken op protocolniveau.