PaperlayerView exact revision on arXiv

Source-linked AI summary

Lie to Me: Finding Bugs in ZK DSL Toolchains with Adversarial Witness Injection

Sebastian Watzinger, Christoph Hochrainer, Valentin Wüstholz, Maria Christakis

arXiv:2608.30648v1cs.CRcs.SE

TL;DR

ZK DSL toolchains may enforce constraints weaker than source semantics, allowing invalid executions while valid-execution tests still pass. Liezz constructs invalid witnesses by splicing executions with different outputs and tests whether four toolchains reject them. It finds 13 bugs, seven with soundness impact, including six exposed by accepted injected witnesses, while the valid-execution baseline exposes none of those soundness failures under the same budget.

  • Problem

    Valid-execution oracles do not directly test rejection of invalid witnesses, allowing purely underconstrained deterministic computations to remain invisible.

  • Method

    Liezz generates deterministic ZK DSL programs, splices witnesses from two executions with different outputs, and uses parameterized standard-library calls to reach complex functionality.

  • Results

    Across four toolchains, Liezz found 13 bugs, seven with soundness impact, and six were exposed by accepted injected witnesses; CIRCUZZ exposed none of these soundness failures under the same budget.

  • Takeaways & Limitations

    Adversarial witness injection complements valid-execution testing by checking not only what toolchains accept, but also what they must reject.

  • Takeaways & Limitations

    False negatives remain possible because coverage depends on generated programs, sampled inputs, splicing strategies, and target-specific operations supported by the implementation.

Abstract

from arXiv · show

Zero-knowledge domain-specific language (ZK DSL) toolchains compile programs into constraint systems and generate witnesses for cryptographic proofs. Bugs in these toolchains can leave the enforced constraints weaker than the source-program semantics, admitting proofs for invalid executions. Such soundness bugs may remain invisible to valid-execution testing because all valid executions still behave correctly. We present Liezz, a testing framework that generates ZK DSL programs and exposes these bugs through adversarial witness injection. For each generated deterministic program, Liezz executes two public input assignments with different outputs and splices their witnesses, combining the input of one execution with the output of the other. The resulting witness is invalid by construction. A correct toolchain must reject it; acceptance exposes a soundness bug. Controlled divergence and multiple witness-splicing strategies preserve enough consistency to expose missing constraints. Liezz also generates parameterized standard-library calls to reach complex functionality. Liezz supports Circom, Corset, Gnark, and Noir. It finds 13 bugs, including seven with soundness impact. Several are reachable only through generated standard-library calls. Under the same testing budget, a valid-execution baseline does not expose any of the soundness failures revealed by accepted injected witnesses, showing that adversarial witness injection reaches failures missed by valid-execution testing.

1 Introduction

ZK DSL toolchains can accept invalid executions when constraints fail to enforce source semantics, a soundness failure that valid-execution testing may miss. Liezz addresses this gap by injecting adversarial witnesses and finds soundness bugs across four toolchains.

  • Motivation: Soundness bugs can let malicious provers produce proofs for nonexistent computations, enabling unauthorized withdrawals, asset minting, or bypassed policy checks.Completeness bugs instead reject valid transactions or proofs, potentially causing denial of service.
  • Motivation: Existing valid-execution oracles test semantics-preserving behavior but do not directly test whether toolchains reject invalid witnesses.Purely underconstrained deterministic computations may therefore pass because all valid executions remain correct.
  • Approach: Liezz executes deterministic programs on two public inputs with different outputs, then combines one input with the other output and splices intermediate witness values.The constructed witness is invalid by construction, so acceptance exposes a soundness bug.
  • Approach: Liezz generates parameterized standard-library calls to reach complex routines where several bugs occur.Specifications select properties such as array lengths, integer widths, signedness, and element types.
  • Approach: Controlled divergence and multiple witness-splicing strategies preserve expected witness structure while exposing missing constraints involving coordinated intermediate values.Random witness mutation can violate unrelated constraints or produce a still-valid witness.
  • Results: 13 bugs were found across CIRCOM, CORSET, GNARK, and NOIR, including seven with soundness impact; several were reachable only through generated standard-library calls.Under the same budget, the valid-execution baseline exposed none of the soundness failures revealed by accepted injected witnesses.

2 Background

A ZK DSL program is compiled into constraints and executed to produce a witness, which a prover uses to create a proof checked against public inputs and constraints. Liezz reuses CIRCIL-based generation and translations while changing the tested property to rejection of invalid witnesses.

  • Toolchain architecture: A program P is compiled into a constraint system C, and executing P on inputs I produces a witness W used with C to generate a verifier-checked proof.The witness contains execution values associated with the program's inputs and computation.
  • Witnesses: Witness layouts differ across toolchains, so Liezz identifies modifiable inputs, outputs, and intermediate values rather than requiring a flat witness array.Some toolchains use execution traces instead of flat arrays.
  • Program semantics: Determinism ensures that differing outputs identify an invalid splice: combining I1 with O2 cannot represent a valid execution when P(I1) → O1 and O1 ≠ O2.This assumption underlies adversarial witness construction.
  • Bug classes: A soundness bug accepts an invalid execution, whereas a completeness bug rejects a valid execution or proof.Adversarial witness injection primarily targets soundness, but crashes during processing can also expose completeness bugs.
  • Example: Figure 2 illustrates a generated CIRCIL program translated to NOIR that performs fixed-base scalar multiplication and branches on the resulting is_infinite flag.The example corresponds to a NOIR soundness bug found by Liezz.
  • Testing infrastructure: Liezz builds on CIRCuzz's CIRCIL representation and target-language translations but changes the property from valid-execution consistency to rejection of invalid witnesses.CIRCIL supports typed operations, inputs, outputs, and Boolean assertions.

3 Overview

LIEZZ generates ZK DSL programs and constructs lying witnesses by combining valid executions with contradictory inputs, outputs, and intermediate values. Its workflow treats rejection as expected and acceptance as evidence of a soundness bug.

  • 3 Overview: LIEZZ generates programs, translates them to target ZK DSLs, and constructs witnesses that are invalid by construction while retaining valid-witness structure.The workflow combines program generation, translation, input sampling, and witness injection.
  • 3.1 Running Example: In the running example, scalar inputs 0 and 1 produce outputs 123 and 42, respectively, with different point and is_infinite values.Input 0 yields the point at infinity with b = 1; input 1 yields the generator with b = 0.
  • 3.1 Running Example: LIEZZ retains the first execution’s input and point coordinates but takes the second execution’s flag and output to form a lying witness.Both original witnesses are valid, but their adversarial combination claims that input 1 produces both the generator and the point at infinity.
  • 3.1 Running Example: The NOIR bug constrains point coordinates without enforcing their relationship with is_infinite, allowing the invalid witness to be accepted.The developers fixed the reported soundness bug.
  • 3.1 Running Example: Generated CIRCIL function support reaches standard-library routines, while adversarial injection exercises behavior absent from valid executions.Both valid executions behave correctly; only their adversarial combination exposes the bug.
  • 3 Overview: For retained input pairs with different outputs, LIEZZ checks the spliced witness: rejection is expected, acceptance exposes a soundness bug, and crashes expose a completeness bug.The workflow compiles and executes the translated program before processing the injected witness.

4 Adversarial Witness Injection

Adversarial witness injection relies on deterministic source semantics to combine two valid executions into an invalid input-output pairing. Controlled divergence, mutation, and multiple splicing strategies preserve consistency while targeting missing constraints.

  • 4 Adversarial Witness Injection: For deterministic programs, LIEZZ combines input I1 from one execution with output O2 from another where O1 != O2, making the witness invalid regardless of intermediate values.The oracle tests whether the target toolchain enforces the source-level input-output relation.
  • 4 Adversarial Witness Injection: A correct toolchain must reject the injected witness; acceptance reports a soundness bug, while crashes during processing report a completeness bug.The same classification applies across compilation, original witness generation, and injected-witness processing.
  • 4.2 Generating Diverging Executions: Unrelated input pairs often alter many computations simultaneously, causing unrelated constraints to reject the spliced witness and reducing its effectiveness.This can hide a missing constraint when another constraint still detects the inconsistency.
  • 4.2 Generating Diverging Executions: LIEZZ creates controlled divergence by replacing one input occurrence with a fresh fault input f and varying only f between the two assignments.The assignments agree on every ordinary input, localizing witness differences after the selected occurrence.
  • 4.2 Generating Diverging Executions: Mutation strategies include local increments or decrements, sign changes, special field values 0, 1, and p −1, and random offsets; only pairs with different outputs are retained.Equal-output pairs do not provide the required input-output contradiction.
  • 4.3 Witness-Splicing Strategies: LIEZZ uses multiple splicing strategies because standard-library operations may require coordinated combinations of intermediate values to expose missing constraints.The strategies differ in how they select values at and after the divergence point.
  • 4.3 Witness-Splicing Strategies: Divergence-point, shifted, windowed, and suffix splicing explore abrupt, delayed, localized, and gradual transitions between the two executions.Windowed and suffix strategies include uniform and tapered variants.

5 Extending CIRCIL

LIEZZ extends CIRCIL beyond primitive operations so generated programs can exercise parameterized standard-library functionality and richer data types. Generation-time constraints keep instantiated calls valid for target-language requirements without becoming source-level assertions.

  • Function specifications: LIEZZ adds typed function specifications that map target-independent CIRCIL calls to target-specific standard-library routines or language constructs.This enables testing of functionality beyond primitive CIRCIL operations while keeping generation independent of target-language syntax.
  • Parameterized specifications: Parameterized specifications let LIEZZ vary generic types and properties such as array lengths, integer widths, signedness, and element types.Concrete parameters are selected during instantiation subject to generation-time relationships.
  • Standard-library coverage: Standard-library calls expose complex routines, including curve operations, conversions, comparisons, decompositions, hash functions, and scalar-field operations.The fixed-base scalar-multiplication example depends on function specifications to reach standard-library code.
  • Generation-time constraints: Generation-time constraints reject invalid parameter combinations before emission, avoiding type-checking or configuration failures unrelated to the tested behavior.They can impose bounds or relationships among generic values, but do not become assertions in the generated ZK DSL program.
  • Richer data types: LIEZZ extends CIRCIL with bounded-size arrays that can serve as inputs, outputs, function arguments, and return values.The generator supports array literals, whole-array assignment, element access and updates, and element-wise initialization.
  • Richer data types: Arrays and generic specifications support collection-oriented routines such as list operations, hashes, and field-to-bit or field-to-byte conversions.The same specification can range over both element type and array length.
  • Richer expressions: Let expressions add expression-local bindings and intermediate values, with Noir translations choosing variables or inline closures.Inline closures exercise target-language machinery not reached by simpler representations.

6 Evaluation

LIEZZ found 13 bugs across four ZK DSL toolchains, including seven with soundness impact, and exposed most soundness failures through accepted adversarial witnesses. The evaluation shows that underconstrained constraints can preserve valid executions while accepting invalid witnesses, with detection depending on witness-splicing strategy and generated functionality.

  • RQ1: Bugs Found: 13 bugs were found across four toolchains: five soundness bugs, six completeness bugs, and two with both impacts.Six of the seven soundness-impact bugs were exposed when toolchains accepted lying witnesses.
  • RQ1: Bugs Found: Soundness bugs primarily reflect underconstrainedness, allowing invalid witnesses while valid executions still behave correctly.The generated constraints accept more witnesses than the source-program semantics permits, so valid-execution oracles may observe no disagreement.
  • RQ2: Witness-Splicing Behavior: Successful witness-splicing strategies varied with each bug’s required post-divergence consistency and edge-case inputs.Bug 7 used divergence-point splicing with scalar zero, whereas bug 10 required shifted, windowed, or suffix splicing to combine coordinates, flags, and outputs selectively.
  • RQ1: Bugs Found: Standard-library functionality enabled several findings, including elliptic-curve bugs that base CIRCIL generation could not reach.Bugs 7 and 10 require library routines, while additional completeness bugs involve lookup tables, assertions, or elliptic-curve scalar operations.
  • RQ3: Time to Bug: The full configuration rediscovered four of five fixed bugs originally exposed through accepted injected witnesses, while bug 12 was not rediscovered within seven days.Bug 12 required the exact scalar value 2128 and a specific surrounding expression controlling scalar-decomposition representation.
  • RQ3: Time to Bug: Bug 9 was exposed by all splicing strategies and many mutations, while bug 10 appeared in nine of ten seeds with a median time of 3d 01h 23m.Bug 9’s median time to bug was 1h 21m, reflecting its broad strategy-insensitive underconstrainedness.

7 Related Work

Prior work applies compiler-testing, circuit-analysis, and formal-verification techniques to ZK systems, but LIEZZ targets invalid-witness rejection across complete ZK DSL toolchains.

  • Testing ZK systems: CIRCUZZ and MTZK apply metamorphic testing to semantics-preserving executions, which does not directly test rejection of invalid witnesses.This leaves purely underconstrained computations potentially invisible when all valid executions behave correctly.
  • Testing ZK systems: ARGUZZ combines metamorphic testing with fault injection inside zkVM provers, whereas LIEZZ constructs invalid witnesses from valid executions and injects them into ZK DSL toolchains.SNARKProbe instead combines dynamic analysis, fuzzing, and SMT solving for cryptographic libraries and prover implementations.
  • Testing and analyzing ZK circuits: Current automated ZK security tools focus mainly on CIRCOM and nondeterminism, with weaker support for semantic mismatches and newer DSLs.LIEZZ contributes a testing oracle for complete ZK DSL toolchains.
  • Testing and analyzing ZK circuits: Circuit-level analyses use fuzzing, SMT-based analysis, static analysis, value inference, and refinement types to examine circuits or constraint consistency.These approaches are complementary to LIEZZ because they can detect source-circuit or compiled-constraint bugs, while LIEZZ tests complete-toolchain rejection of invalid witnesses.
  • Formal verification of ZK compilers: Formal-verification work applies correctness guarantees to ZK compilation, including verified protocol implementations and bounded SMT verification of CirC's field-blasting pass.These techniques provide formal guarantees, while LIEZZ contributes dynamic testing of generated DSL programs through the complete toolchain.

8 Conclusion

LIEZZ tests whether ZK DSL toolchains reject witnesses that violate source-program semantics by splicing executions with different outputs. Across four toolchains, it found soundness-impacting bugs that valid-execution testing missed.

  • Conclusion: Adversarial witness injection constructs invalid witnesses by splicing executions with different outputs, while controlled divergence and splicing strategies expose missing constraints.Function specifications extend reach into standard-library code.
  • Conclusion: Across four toolchains, LIEZZ found 13 bugs, seven with soundness impact, and six were exposed by accepted injected witnesses.The bugs span compilers, witness generation, constraint lowering, standard libraries, and prover backends.
  • Conclusion: Under the same budget, CIRCUZZ exposed none of the soundness failures but remained effective for completeness bugs.Adversarial witness injection complements valid-execution testing by checking what systems must reject as well as what they accept.
Loading 2608.30648v1…