Sigvex
ZKcriticalDetector5 min read

Unconstrained Divisor

Detects Circom divisions whose divisor signal appears in no constraint at all, giving a malicious prover full control over the divisor and the result.

cross-runtimecriticalstatic-analysisdetector

Unconstrained Divisor

Overview

This detector finds the most severe form of division hazard in a Circom circuit: an unconstrained (<--) assignment that divides by a signal which never appears in any constraint anywhere in its template. It is a stronger and narrower check than the general division-by-zero risk. Where that detector asks whether a divisor is specifically proven non-zero, this one asks whether the divisor is bound by anything at all — non-zero or otherwise. A divisor that participates in no === and no <== is fully prover-controlled.

The distinction matters for triage. A divisor that has constraints but lacks a non-zero proof is a real but bounded problem. A divisor with zero constraints is a blank cheque: the prover assigns it any field element they like, including zero, and the surrounding circuit has no equation that disagrees. That is why this finding is reported at Critical severity while the general division-by-zero check is graded by context.

Why This Is an Issue

When the divisor is wholly unconstrained, two failure modes open at once. The prover can set the divisor to zero, making the witness-time division undefined in the field and collapsing any downstream relation that assumed a meaningful quotient. Or the prover can set the divisor to any non-zero value of their choosing, steering the quotient — and everything computed from it — to whatever serves the attack. Because no constraint references the divisor, neither choice is detectable by the verifier.

The practical consequence is a circuit that verifies proofs unrelated to its intended computation. A division meant to compute a ratio, a share, or an inverse becomes a free parameter. Property tests miss it because honest provers supply sensible divisors; the on-chain verifier accepts the malicious proof because, as far as the R1CS is concerned, nothing is wrong.

How to Resolve

Make the divisor participate in at least one constraint, and ideally prove it non-zero with the multiplicative-inverse idiom. The inverse pattern both binds the divisor and rules out zero, because zero has no inverse in a finite field.

// Vulnerable: `b` appears in no constraint, prover controls it entirely
template Ratio() {
    signal input a;
    signal input b;
    signal output q;
    q <-- a / b;     // b is unconstrained
}
// Fixed: `b` is bound and proven non-zero before the division
template Ratio() {
    signal input a;
    signal input b;
    signal output q;

    signal b_inv;
    b_inv <-- 1 / b;
    b_inv * b === 1; // impossible if b == 0; also binds b in the R1CS

    q <-- a / b;
    q * b === a;     // binds the quotient to a and b
}

Detection Methodology

For each template the detector first builds the set of signals that appear in any constraining (<==) or constraint-only (===) assignment, on either side of the operator. It then walks the unconstrained (<--) assignments, and for each one that contains a division it extracts every divisor signal, including the trailing operands of chained division such as a / b / c. Any divisor signal that is absent from the constrained set is reported as a fully unconstrained divisor.

Constraining (<==) divisions are deliberately out of scope here; those are handled by the general division-by-zero detector, which reasons about non-zero proofs rather than total absence of constraints. Keeping this detector focused on <-- divisions by entirely unbound signals is what lets it report at Critical with high confidence.

Limitations

  • The check is per template; a divisor constrained in a sub-component but only hint-wired into the parent is treated as unconstrained at the parent level.
  • Only <-- divisions are considered, so a constraining division by an otherwise-unbound signal is left to the division-by-zero detector.
  • Divisor extraction is expression-based; a divisor hidden inside an unusual or function-wrapped expression may not be recognised.

References

Sample Sigvex Output

{
  "detector": "unconstrained-divisor",
  "severity": "critical",
  "confidence": 0.85,
  "title": "Division by fully unconstrained signal `b` in `<--` assignment",
  "template": "Ratio",
  "signal": "b",
  "line": 5,
  "description": "Signal `q` is computed via `<--` with division by `b` at line 5 in template `Ratio`. Signal `b` never appears in any constraint (`===` or `<==`), meaning a malicious prover has full control over its value. This is a critical vulnerability: the prover can set `b` to zero or any value.",
  "recommendation": "Ensure the divisor signal participates in at least one constraint. Add a non-zero proof via multiplicative inverse: `signal inv; inv <-- 1 / divisor; inv * divisor === 1;`"
}