Technical Summary: ZKFUZZ: Foundation and Framework for Effective Fuzzing of Zero-Knowledge Circuits

1. Problem Statement

Zero-knowledge (ZK) circuits are foundational to privacy-preserving computations, enabling succinct proofs and efficient verification in applications ranging from anonymous cryptocurrencies to verifiable machine learning. However, developing correct ZK circuits is notoriously difficult due to the misalignment between general-purpose computation logic and finite-field polynomial constraints.

Two primary classes of vulnerabilities exist:

• Under-constrained circuits: The constraints are too loose, allowing malicious provers to generate valid proofs for invalid witnesses (violating soundness).
• Over-constrained circuits: The constraints are too strict, causing the system to reject valid witnesses from honest provers (violating completeness).

Existing detection methods face significant limitations:

• Static Analysis: Tools like Circomspect and ZKAP often suffer from high false positive rates and fail to capture deep semantic issues, particularly those involving intermediate computations or abnormal program termination.
• Formal Methods: Tools relying on SMT solvers (e.g., Picus, ConsCS) struggle to scale to real-world circuit sizes and often rely on incomplete definitions of vulnerabilities, focusing solely on non-determinism in constraints while ignoring cases where computation aborts or where intermediate values are mismatched.
• Definition Gaps: Prior formal definitions of ZK bugs are incomplete. They often ignore "abnormal termination" (where a computation crashes but constraints are still satisfied) and fail to account for the full set of execution traces, including intermediate values.

2. Methodology

2.1 Theoretical Foundation: Trace-Constraint Consistency Test (TCCT)

The authors introduce TCCT, a language-independent formal framework that defines ZK vulnerabilities as discrepancies between two sets:

1. Trace Set $T(P)$: The set of all possible execution traces (input, intermediate values, output) produced by the witness computation program $P$.
2. Constraint Satisfaction Set $S(C)$: The set of all tuples (input, intermediate values, output) that satisfy the circuit constraints $C$.

TCCT defines a circuit as well-constrained if and only if:

• No Under-constraint: The projection of $S(C)$ onto input-output pairs is a subset of the projection of $T(P)$. This ensures no invalid traces are accepted.
• No Over-constraint: $T(P)$ is a subset of $S(C)$. This ensures all valid traces (including specific intermediate values) are accepted.

This formulation captures vulnerabilities caused by computation aborts (where $P$ fails but $C$ accepts the input) and mismatches in intermediate values, which prior definitions missed. The authors prove that deciding under- or over-constrainedness is NP-complete, and the full TCCT is co-NP-complete.

2.2 System Design: ZKFUZZ

ZKFUZZ is a dynamic analysis framework that detects TCCT violations using a joint program mutation and input generation approach. Unlike traditional fuzzing that only mutates inputs, ZKFUZZ mutates both the program logic and the inputs.

Core Workflow:

1. Mutation: The system generates mutants ($P'$) of the original computation program ($P$). Mutations include removing assertions, transforming assignments (e.g., replacing operators or values), and modifying weak assignments.
2. Execution: Both the original program ($P$) and the mutant ($P'$) are executed on sampled inputs ($x$).
3. Verification:
   • Over-constrained Detection: If $P(x)$ produces a valid trace that fails $C$, the circuit is over-constrained.
   • Under-constrained Detection: If $P'(x)$ produces a trace with a different output ($y' \neq y$) that still satisfies $C$, the circuit is under-constrained (since the mutant logic is semantically different, the output should not be accepted).
4. Guided Search: To navigate the vast search space of large prime fields and infinite mutation possibilities, ZKFUZZ employs a genetic algorithm:
   • Fitness Function: A novel min-sum fitness function calculates the sum of constraint errors across all constraints for a given trace. The mutant is scored by the minimum error sum across sampled inputs. This differs from prior max-only methods and is better suited for joint mutation.
   • Target Selectors: The system uses static analysis to guide mutation and input generation toward high-risk patterns, such as:
     • Zero-Division: Generating inputs where numerator and denominator are both zero.
     • Hash-Check: Forcing inputs to satisfy hash equality constraints.
     • Skewed Distribution: Biasing input generation toward edge cases (0, 1, and values near the field modulus $q$).
     • White-listing: Skipping known safe templates (e.g., IsZero, Num2Bits) to focus on error-prone code.

3. Key Contributions

1. TCCT Framework: A unified, language-agnostic formal model that subsumes prior definitions and captures the full space of ZK bugs, including those arising from abnormal termination and intermediate value mismatches.
2. ZKFUZZ System: A novel fuzzing framework that jointly mutates programs and inputs to detect TCCT violations, utilizing a min-sum fitness function and guided search heuristics.
3. Empirical Validation: Evaluation on 452 real-world Circom circuits, demonstrating superior performance over state-of-the-art tools.
4. Noir Prototype: A preliminary implementation for Noir, a different ZK DSL, demonstrating the framework's potential for language independence.

4. Results

The authors evaluated ZKFUZZ on 452 real-world Circom circuits, comparing it against four state-of-the-art tools: Circomspect, ZKAP, Picus, and ConsCS.

• Bug Detection: ZKFUZZ identified 85 unique bugs, including 59 previously unknown zero-day vulnerabilities. Of these, 39 were confirmed by developers, and 14 were fixed.
• Comparison: ZKFUZZ found 30% to 300% more bugs than existing tools across various circuit sizes.
• Precision: ZKFUZZ achieved 100% precision (zero false positives), whereas static analyzers like Circomspect and ZKAP had high false positive rates (precision ranging from 0.06 to 0.75).
• Speed: ZKFUZZ++ (with target selectors) identified over 90% of bugs within 100 seconds, significantly outperforming formal methods and static analyzers.
• Impact: The discovered bugs included critical under-constrained vulnerabilities in projects like zk-regex and passport-zk-circuits, which could allow attackers to forge proofs or extract funds.

5. Significance and Claims

The paper claims that ZKFUZZ represents a significant advancement in ZK circuit security by addressing the fundamental incompleteness of prior vulnerability definitions. By formalizing bugs as trace-constraint inconsistencies (TCCT), the authors expose a large class of vulnerabilities (nearly 50% of real-world bugs in their evaluation) that were previously undetectable by tools focusing solely on constraint non-determinism.

The system's ability to detect bugs without false positives makes it a practical tool for developers, who often ignore alerts from high-false-positive static analyzers. Furthermore, the successful detection of bugs in Noir circuits suggests that the TCCT framework and ZKFUZZ architecture are not limited to Circom but can generalize to other ZK languages that compile to standardized constraint formats.

The authors emphasize that their work focuses on vulnerabilities arising from the misalignment of computation and constraints (soundness and completeness), explicitly excluding bugs in the underlying proving systems, pure logic errors (like unused inputs), or protocol-level zero-knowledge leaks.