💻 computer science

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

Dieser Beitrag stellt zkFuzz vor, ein neuartiges mutationsbasiertes Fuzzing-Framework, das auf dem theoretischen Trace-Constraint Consistency Test (TCCT) basiert und durch die Überwindung der Grenzen bestehender statischer und formaler Analysewerkzeuge sowohl unter- als auch überbeschränkte Schwachstellen in Zero-Knowledge-Schaltungen effektiv aufdeckt.

Ursprüngliche Autoren: Hideaki Takahashi, Jihwan Kim, Suman Jana, Junfeng Yang

Veröffentlicht 2026-05-26

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Hideaki Takahashi, Jihwan Kim, Suman Jana, Junfeng Yang

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie bauen einen magischen Tresor, der beweist, dass Sie ein geheimes Passwort kennen, ohne das Passwort jemals tatsächlich preiszugeben. Genau das tun „Zero-Knowledge (ZK)-Schaltungen" in der digitalen Welt. Sie sind die Sicherheitswächter für datenschutzfreundliche Technologien wie anonyme Kryptowährungen und sichere Wahlsysteme.

Der Bau dieser Tresore ist jedoch unglaublich schwierig. Wenn Sie einen winzigen Fehler in den Bauplänen machen, könnte der Tresor entweder:

Jeden hereinlassen (selbst wenn er das Passwort nicht kennt).
Den echten Eigentümer aussperren (selbst wenn er das korrekte Passwort hat).

Die Arbeit stellt ein neues Werkzeug namens ZKFUZZ vor, um diese Fehler zu finden, bevor böswillige Akteure dies tun. So funktioniert es, einfach erklärt:

Das Problem: Der „Bauplan" vs. die „Realität"

In diesen Systemen schreiben Entwickler ein Programm, das zwei Dinge gleichzeitig tut:

Die Berechnung: Die eigentliche Mathematik, um das Geheimnis zu ermitteln (wie das Berechnen einer Route auf einer Karte).
Die Einschränkungen: Die Regeln, die beweisen, dass die Mathematik korrekt durchgeführt wurde (wie eine Checkliste, um zu verifizieren, dass die Route existiert).

Das Problem ist, dass diese beiden Teile oft aus dem Takt geraten.

Unterbeschränkt: Die Regeln sind zu locker. Ein Hacker kann das System dazu bringen, eine gefälschte Route zu akzeptieren.
Überbeschränkt: Die Regeln sind zu streng. Das System lehnt eine völlig gültige Route wegen einer winzigen, unnötigen Regel ab.

Bestehende Werkzeuge zur Fehlerfindung sind wie schlechte Rechtschreibprüfungen. Sie raten basierend auf Mustern und schreien „FEHLER!" bei Dingen, die eigentlich in Ordnung sind (falsche Alarme), oder sie übersehen tiefe, komplexe Fehler ganz.

Die Lösung: ZKFUZZ (Der „Mutations-Fuzzer")

Die Autoren haben ein neues Framework namens ZKFUZZ entwickelt. Anstatt den Code nur zu lesen, agiert ZKFUZZ wie ein schelmischer Testingenieur, der versucht, das System absichtlich zu brechen.

Hier ist die Analogie:
Stellen Sie sich vor, Sie haben ein Rezept (die Berechnung) und einen Geschmackstest (die Einschränkungen).

Alte Werkzeuge: Schauen sich das Rezept an und sagen: „Das sieht verdächtig aus, weil es Salz enthält." (Sie raten basierend auf Regeln).
ZKFUZZ: Kocht tatsächlich das Gericht, mutiert dann aber das Rezept. Es tauscht „Zucker" gegen „Salz" aus oder ändert die Garzeit. Dann füttert es dieses mutierte Gericht dem Geschmackstest.
- Wenn der Geschmackstest zu einem Gericht, das schrecklich schmecken sollte (weil das Rezept geändert wurde), „Lecker!" sagt, weiß ZKFUZZ, dass die Regeln zu locker sind (Unterbeschränkt).
- Wenn der Geschmackstest zu einem Gericht, das köstlich sein sollte (weil das ursprüngliche Rezept korrekt war), „Ekelhaft!" sagt, weiß ZKFUZZ, dass die Regeln zu streng sind (Überbeschränkt).

Das Geheimnis: „Fitness" und „Zielgerichtetheit"

Einen Fehler in einer ZK-Schaltung zu finden, ist wie eine Nadel im Heuhaufen von der Größe eines Planeten zu suchen. Die beteiligten Zahlen sind so riesig, dass ein Computer nicht einfach jede Möglichkeit durchprobieren kann.

ZKFUZZ verwendet einen Genetischen Algorithmus (wie Evolution):

Mutation: Es erstellt Tausende leicht defekter Versionen des Programms.
Fitness-Score: Es bewertet diese defekten Versionen. Wenn eine defekte Version es fast schafft, den Test zu bestehen (auch wenn sie scheitert), erhält sie einen „guten Score". Das sagt dem System: „Sie werden wärmer!"
Zielgerichtetheit: Es rät nicht einfach zufällig. Es weiß, dass Fehler oft bei „Randfällen" auftreten (wie wenn Zahlen null oder extrem groß sind). Es versucht gezielt, dem System diese kniffligen Zahlen zu geben, um zu sehen, ob es zusammenbricht.

Die Ergebnisse: Das Unsichtbare fangen

Das Team testete ZKFUZZ an 452 realen Schaltungen, die in echten Projekten verwendet werden.

Die Punktzahl: Es fand 85 Fehler.
Die Zero-Days: 59 davon waren brandneue, unbekannte Fehler (Zero-Days), von denen niemand wusste, dass sie existieren.
Die Auswirkungen: 39 davon wurden von den Entwicklern bestätigt, und 14 wurden bereits behoben. Dazu gehören Fehler in großen Projekten wie zkSync (eine Krypto-Plattform) und passport-zk-circuits (digitale ID-Systeme).
Keine falschen Alarme: Im Gegensatz zu anderen Werkzeugen markierte ZKFUZZ nichts als Fehler, was tatsächlich kein Fehler war.

Warum das wichtig ist

Die Arbeit argumentiert, dass frühere Werkzeuge einen riesigen Teil des Problems übersehen haben. Sie suchten nur nach „Zufälligkeit" in den Regeln. ZKFUZZ führte eine neue Theorie namens TCCT (Trace-Constraint Consistency Test) ein, die prüft, ob der tatsächliche Pfad, den der Computer nimmt, mit den Regeln übereinstimmt, die er befolgen soll.

Diese neue Theorie fing Fehler auf, die auftraten, wenn der Computer „abstürzte" oder unerwartet aufhörte, was frühere Werkzeuge völlig ignorierten.

In Kürze

ZKFUZZ ist ein intelligenter, automatisierter „Fehlerjäger", der Zero-Knowledge-Schaltungen bricht, indem er ihren Code mutiert und sie mit kniffligen Eingaben füttert. Es fand Dutzende kritischer Sicherheitslücken, die andere Werkzeuge übersehen hatten, und bewies, dass selbst in der komplexen Welt der Datenschutzmathematik ein wenig kontrolliertes Chaos der beste Weg ist, die Wahrheit zu finden.

Technische Zusammenfassung: ZKFUZZ: Grundlage und Framework für effektives Fuzzing von Zero-Knowledge-Schaltungen

1. Problemstellung

Zero-Knowledge (ZK)-Schaltungen sind grundlegend für datenschutzkonforme Berechnungen und ermöglichen prägnante Beweise sowie eine effiziente Verifizierung in Anwendungen, die von anonymen Kryptowährungen bis hin zu überprüfbarer maschineller Lernverarbeitung reichen. Die Entwicklung korrekter ZK-Schaltungen ist jedoch berüchtigt schwierig, da eine Diskrepanz zwischen der Logik allgemeiner Berechnungen und den Polynom-Bedingungen über endlichen Körpern besteht.

Es existieren zwei Hauptklassen von Schwachstellen:

Unterbeschränkte Schaltungen: Die Bedingungen sind zu locker, was böswilligen Beweisführern ermöglicht, gültige Beweise für ungültige Zeugen zu generieren (Verletzung der Soundness).
Überbeschränkte Schaltungen: Die Bedingungen sind zu streng, wodurch das System gültige Zeugen von ehrlichen Beweisführern ablehnt (Verletzung der Completeness).

Bestehende Erkennungsmethoden weisen erhebliche Einschränkungen auf:

Statische Analyse: Tools wie Circomspect und ZKAP leiden häufig unter hohen Raten falsch-positiver Meldungen und erfassen keine tiefgreifenden semantischen Probleme, insbesondere solche, die Zwischenberechnungen oder abnormalen Programmabbruch betreffen.
Formale Methoden: Tools, die auf SMT-Lösern basieren (z. B. Picus, ConsCS), haben Schwierigkeiten, auf reale Schaltungsgrößen zu skalieren, und verlassen sich oft auf unvollständige Definitionen von Schwachstellen. Sie konzentrieren sich ausschließlich auf Nicht-Determinismus in den Bedingungen, ignorieren jedoch Fälle, in denen die Berechnung abbricht oder in denen Zwischenwerte nicht übereinstimmen.
Definitionslücken: Bisherige formale Definitionen von ZK-Fehlern sind unvollständig. Sie ignorieren häufig „abnormalen Abbruch" (bei dem eine Berechnung abstürzt, die Bedingungen jedoch dennoch erfüllt sind) und berücksichtigen nicht die vollständige Menge der Ausführungsprotokolle, einschließlich Zwischenwerte.

2. Methodik

2.1 Theoretische Grundlage: Konsistenztest von Protokoll und Bedingungen (TCCT)

Die Autoren führen TCCT ein, ein sprachunabhängiges formales Framework, das ZK-Schwachstellen als Diskrepanzen zwischen zwei Mengen definiert:

Protokollmenge $T(P)$ : Die Menge aller möglichen Ausführungsprotokolle (Eingabe, Zwischenwerte, Ausgabe), die vom Zeugenberechnungsprogramm $P$ erzeugt werden.
Menge der Bedingungserfüllung $S(C)$ : Die Menge aller Tupel (Eingabe, Zwischenwerte, Ausgabe), die die Schaltungsbedingungen $C$ erfüllen.

TCCT definiert eine Schaltung genau dann als gut beschränkt, wenn:

Keine Unterbeschränkung: Die Projektion von $S(C)$ auf Eingabe-Ausgabe-Paare eine Teilmenge der Projektion von $T(P)$ ist. Dies stellt sicher, dass keine ungültigen Protokolle akzeptiert werden.
Keine Überbeschränkung: $T(P)$ ist eine Teilmenge von $S(C)$ . Dies stellt sicher, dass alle gültigen Protokolle (einschließlich spezifischer Zwischenwerte) akzeptiert werden.

Diese Formulierung erfasst Schwachstellen, die durch Berechnungsabbrüche (wobei $P$ fehlschlägt, $C$ die Eingabe jedoch akzeptiert) und Nicht-Übereinstimmungen in Zwischenwerten verursacht werden, die von früheren Definitionen übersehen wurden. Die Autoren beweisen, dass die Entscheidung über Unter- oder Überbeschränktheit NP-vollständig ist und der vollständige TCCT co-NP-vollständig ist.

2.2 Systemdesign: ZKFUZZ

ZKFUZZ ist ein Framework zur dynamischen Analyse, das TCCT-Verletzungen mithilfe eines Ansatzes der kombinierten Programmmutation und Eingabegenerierung erkennt. Im Gegensatz zum herkömmlichen Fuzzing, das nur Eingaben mutiert, mutiert ZKFUZZ sowohl die Programmlastik als auch die Eingaben.

Kernarbeitsablauf:

Mutation: Das System generiert Mutanten ( $P'$ ) des ursprünglichen Berechnungsprogramms ( $P$ ). Mutationen umfassen das Entfernen von Assertions, das Transformieren von Zuweisungen (z. B. Ersetzen von Operatoren oder Werten) und das Modifizieren schwacher Zuweisungen.
Ausführung: Sowohl das ursprüngliche Programm ( $P$ ) als auch die Mutante ( $P'$ ) werden auf Stichprobeneingaben ( $x$ ) ausgeführt.
Verifizierung:
- Erkennung von Überbeschränkung: Wenn $P(x)$ ein gültiges Protokoll erzeugt, das $C$ nicht erfüllt, ist die Schaltung überbeschränkt.
- Erkennung von Unterbeschränkung: Wenn $P'(x)$ ein Protokoll mit einer anderen Ausgabe ( $y' \neq y$ ) erzeugt, das dennoch $C$ erfüllt, ist die Schaltung unterbeschränkt (da die Mutantenlogik semantisch unterschiedlich ist, sollte die Ausgabe nicht akzeptiert werden).
Gesteuerte Suche: Um den riesigen Suchraum großer Primfeldzahlen und unendlicher Mutationsmöglichkeiten zu navigieren, setzt ZKFUZZ einen genetischen Algorithmus ein:
- Fitnessfunktion: Eine neuartige Min-Sum-Fitnessfunktion berechnet die Summe der Bedingungsfehler über alle Bedingungen hinweg für ein gegebenes Protokoll. Die Mutante wird anhand der minimalen Fehlersumme über die Stichprobeneingaben bewertet. Dies unterscheidet sich von früheren Methoden, die nur das Maximum betrachteten, und ist besser für die kombinierte Mutation geeignet.
- Zielauswähler: Das System nutzt statische Analyse, um Mutation und Eingabegenerierung auf risikoreiche Muster zu lenken, wie zum Beispiel:
  - Null-Division: Generierung von Eingaben, bei denen sowohl Zähler als auch Nenner null sind.
  - Hash-Prüfung: Erzwingung von Eingaben, die Hash-Gleichheitsbedingungen erfüllen.
  - Verzerrte Verteilung: Verzerrung der Eingabegenerierung hin zu Randfällen (0, 1 und Werte in der Nähe des Feldmoduls $q$ ).
  - Whitelisting: Überspringen bekannter sicherer Vorlagen (z. B. IsZero, Num2Bits), um sich auf fehleranfälligen Code zu konzentrieren.

3. Hauptbeiträge

TCCT-Framework: Ein einheitliches, sprachagnostisches formales Modell, das frühere Definitionen umfasst und den vollständigen Raum von ZK-Fehlern erfasst, einschließlich solcher, die durch abnormalen Abbruch und Nicht-Übereinstimmungen von Zwischenwerten entstehen.
ZKFUZZ-System: Ein neuartiges Fuzzing-Framework, das Programme und Eingaben gemeinsam mutiert, um TCCT-Verletzungen zu erkennen, wobei eine Min-Sum-Fitnessfunktion und gesteuerte Suchheuristiken verwendet werden.
Empirische Validierung: Evaluierung an 452 realen Circom-Schaltungen, die eine überlegene Leistung gegenüber State-of-the-Art-Tools demonstriert.
Noir-Prototyp: Eine vorläufige Implementierung für Noir, eine andere ZK-DSL, die das Potenzial des Frameworks für sprachunabhängige Anwendungen demonstriert.

4. Ergebnisse

Die Autoren bewerteten ZKFUZZ an 452 realen Circom-Schaltungen und verglichen es mit vier State-of-the-Art-Tools: Circomspect, ZKAP, Picus und ConsCS.

Fehlererkennung: ZKFUZZ identifizierte 85 eindeutige Fehler, darunter 59 bisher unbekannte Zero-Day-Schwachstellen. Davon wurden 39 von Entwicklern bestätigt und 14 behoben.
Vergleich: ZKFUZZ fand 30 % bis 300 % mehr Fehler als bestehende Tools über verschiedene Schaltungsgrößen hinweg.
Präzision: ZKFUZZ erreichte 100 % Präzision (keine falsch-positiven Meldungen), wohingegen statische Analytiker wie Circomspect und ZKAP hohe Raten falsch-positiver Meldungen aufwiesen (Präzision zwischen 0,06 und 0,75).
Geschwindigkeit: ZKFUZZ++ (mit Zielauswählern) identifizierte über 90 % der Fehler innerhalb von 100 Sekunden und übertraf damit formale Methoden und statische Analytiker erheblich.
Auswirkung: Die entdeckten Fehler umfassten kritische unterbeschränkte Schwachstellen in Projekten wie zk-regex und passport-zk-circuits, die Angreifern ermöglichen könnten, Beweise zu fälschen oder Mittel zu extrahieren.

5. Bedeutung und Behauptungen

Die Arbeit behauptet, dass ZKFUZZ einen bedeutenden Fortschritt in der Sicherheit von ZK-Schaltungen darstellt, indem es die grundlegende Unvollständigkeit früherer Schwachstellendefinitionen adressiert. Durch die Formalisierung von Fehlern als Inkonsistenzen zwischen Protokoll und Bedingungen (TCCT) legen die Autoren eine große Klasse von Schwachstellen offen (nahezu 50 % der realen Fehler in ihrer Evaluierung), die zuvor von Tools, die sich ausschließlich auf Nicht-Determinismus in Bedingungen konzentrierten, nicht erkannt werden konnten.

Die Fähigkeit des Systems, Fehler ohne falsch-positive Meldungen zu erkennen, macht es zu einem praktischen Werkzeug für Entwickler, die Warnungen von statischen Analytikern mit hoher Rate falsch-positiver Meldungen oft ignorieren. Darüber hinaus deutet die erfolgreiche Erkennung von Fehlern in Noir-Schaltungen darauf hin, dass das TCCT-Framework und die ZKFUZZ-Architektur nicht auf Circom beschränkt sind, sondern auf andere ZK-Sprachen verallgemeinert werden können, die in standardisierte Bedingungsformate kompiliert werden.

Die Autoren betonen, dass sich ihre Arbeit auf Schwachstellen konzentriert, die aus der Diskrepanz zwischen Berechnung und Bedingungen (Soundness und Completeness) entstehen, und explizit Fehler in den zugrunde liegenden Beweissystemen, reine Logikfehler (wie ungenutzte Eingaben) oder Protokoll-Level-Zero-Knowledge-Lecks ausschließt.