Zero-knowledge circuit soundness: the under-constrained circuit

A zero-knowledge proof convinces a verifier that a statement is true without revealing why. In most deployed systems the statement is “I know values that satisfy this circuit”, and the circuit is a set of arithmetic constraints written by a developer. If the constraints say less than the developer intended, the proof proves less than the application assumes, and a dishonest prover can produce valid proofs of false statements.

That failure is called an under-constrained circuit. It is among the vulnerability classes catalogued in the systematisation of 141 SNARK vulnerabilities by Chaliasos et al., and in public collections such as 0xPARC’s ZK Bug Tracker. This primer explains how it arises, with Circom examples, and how to look for it.

Witness, constraints, proof

A circuit has inputs, some public and some private, and intermediate values called signals. Proving happens in two steps. First, a witness generator computes a value for every signal from the inputs. Second, the prover produces a proof that the witness satisfies every constraint of the circuit, which for Circom is a rank-1 constraint system (R1CS): a list of equations of the form A × B = C over a large prime field.

The verifier checks only the proof against the public inputs. It never sees the witness generator, and it does not care how the witness was produced. Any assignment of signals that satisfies the constraints yields a valid proof. Soundness, the property that false statements cannot be proved, therefore depends entirely on the constraints.

Assignment is not constraint

Circom has three operators that look similar and mean different things. <-- assigns a value to a signal in the witness generator and adds no constraint. === adds a constraint and assigns nothing. <== does both. The Circom documentation is explicit that <-- is needed for expressions that cannot be written as quadratic constraints, such as division or comparisons, and that the developer must then constrain the result separately.

A signal assigned with <-- and never constrained is a free variable. An honest prover computes it as the code says, but a dishonest prover can set it to anything, and the proof will still verify.

A worked example: IsZero

The IsZero template from circomlib outputs 1 if its input is zero and 0 otherwise. It cannot compute an inverse with a quadratic constraint, so it supplies the inverse as a hint and constrains the result in two equations.

1// IsZero as written in circomlib (comparators.circom).2template IsZero() {3    signal input in;4    signal output out;5    signal inv;6 7    inv <-- in != 0 ? 1 / in : 0;   // witness hint: computed, not constrained8    out <== -in * inv + 1;          // constrained: out = 1 - in * inv9    in * out === 0;                 // constrained: if in != 0 then out must be 010}

With input 5, an honest witness sets inv to the field inverse of 5 and out to 0, which satisfies both constraints. Now suppose the last line were missing. A dishonest prover sets inv = 0, so the first constraint gives out = 1. That satisfies every remaining constraint, and the proof claims that 5 is zero. The second constraint is what forbids this: 5 × 1 ≠ 0.

1 template IsZero() {2     signal input in;3     signal output out;4     signal inv;5 6     inv <-- in != 0 ? 1 / in : 0;7     out <== -in * inv + 1;8-    // second constraint missing: nothing forces out = 0 when in != 09+    in * out === 0;10 }

The example generalises. For every signal computed with a hint, the question is whether the constraints admit exactly one value of that signal for each valid input, or, where several are acceptable, whether every admitted value is acceptable to the application.

Ranges, bits and field arithmetic

Circuits compute in a prime field, not in integers. Values wrap around the field modulus, and “negative” numbers are large field elements. Two consequences cause many bugs.

Missing range checks. Comparison templates such as circomlib’s LessThan(n) assume their inputs fit in n bits. If the circuit does not enforce that, for example by decomposing the inputs into bits, a prover can supply a field element outside the range for which the comparison gives the wrong answer.

Bit decomposition aliasing. Decomposing a value into as many bits as the field has allows two different bit strings to represent the same field element, since a value and that value plus the modulus are both representable. circomlib provides strict variants with an alias check for this case.

Components and wiring

Circuits are built from components, and a component constrains only the signals it is connected to. A component whose output is computed but never used to constrain anything has no effect on soundness. A component whose input is assigned with <-- rather than <== receives an unconstrained value. And a public input that the circuit never uses in a constraint, such as a recipient address in a withdrawal proof, can be changed by anyone who copies the proof, because the proof does not depend on it. Binding such values usually requires a dummy constraint such as squaring the signal.

Soundness outside the circuit

A sound circuit can still be deployed unsoundly. On-chain verifiers receive public inputs as 256-bit integers, while the proof treats them as field elements. If the verifier contract does not require each input to be less than the scalar field modulus, two different integers, x and x + p, verify with the same proof. An application that uses a public input as a key, for instance a nullifier recorded to prevent double spending, then accepts the same proof twice under different keys. Other issues outside the circuit include the trusted setup for proving systems that need one, and the integrity of the verification key deployed with the contract.

Finding under-constrained circuits

Under-constrained signals are invisible to ordinary testing, because tests use the honest witness generator, which always produces the intended values. Finding them requires a different approach.

• Static analysis. circomspect includes analysis passes for signal assignments made with <--, under-constrained signals, non-strict binary conversion and unconstrained less-than comparisons, among others.
• Adversarial witnesses. For each hinted signal, construct an alternative witness by hand that keeps the public inputs fixed and changes the signal, and check whether it still satisfies the constraints.
• Formal tools. Solver-based approaches ask whether two different witnesses can exist for the same public inputs, which is the definition of an under-constrained output.
• Review. For every template, write down the relation the constraints define and compare it with the relation the application needs.

A catalogue of soundness bugs

Conclusions

A zero-knowledge proof proves that a witness satisfies the constraints, and nothing about how the witness was computed. Under-constrained circuits arise wherever the developer’s intent lives in witness-generation code rather than in constraints: hints that are never checked, ranges that are assumed, components that are not wired, public inputs that are not bound.

Because honest tests cannot reveal them, finding these bugs requires reasoning from the prover’s side: for each signal, could a dishonest prover choose a different value and still produce a valid proof?

Recommendations