Division by Zero Risk

Overview

The division-by-zero detector finds / and % operators inside <-- assignments whose divisor has no constraint forcing it to be non-zero. In a finite field there is no hardware trap for dividing by zero; the witness generator computes whatever the compiler’s evaluation rules happen to produce (often zero, sometimes a compiler-dependent value, occasionally an error), and the proof proceeds. If no constraint downstream binds the quotient, the prover keeps full freedom over it. If constraints exist but were written assuming the divisor is non-zero (for example q * b === a), a zero divisor makes those constraints trivially satisfied by q = 0 regardless of a, which is just as bad.

The detector’s job is to tell these cases apart from safe usages. Safe usages pair the division with a non-zero witness for the divisor: inv <-- 1/b; inv * b === 1. This pattern rules out b = 0 because 0 * inv cannot equal 1 in any field. The detector recognises the pattern, along with a few equivalents (such as calling the NonZero or IsZero helpers from circomlib and asserting their outputs), and suppresses the finding.

Why This Is an Issue

Zero divisors are attractive to an attacker because they often collapse the surrounding constraint system into a trivial state. A division meant to compute a / b and check q * b === a becomes 0 * 0 === 0 when the attacker sets b = 0 and q = 0, satisfying the constraint regardless of a. Any downstream logic that trusted q to equal a / b then operates on an attacker-controlled zero.

The symptom is almost always the same: the circuit works on random test inputs, the malicious case is never discovered by property tests because honest provers never submit zero divisors, and the proof is silently accepted on-chain.

How to Resolve

Add an explicit non-zero witness for the divisor and assert that its product with the divisor equals one. This both rules out the zero case and documents the author’s intent.

// Vulnerable: no non-zero witness for `b`
template Divide() {
    signal input a;
    signal input b;
    signal output q;
    q <-- a / b;
    q * b === a;   // trivially satisfied when a = b = q = 0
}

// Fixed: `b` is forced to be non-zero before the division
template Divide() {
    signal input a;
    signal input b;
    signal output q;

    signal b_inv;
    b_inv <-- 1 / b;
    b_inv * b === 1;   // impossible if b == 0

    q <-- a / b;
    q * b === a;       // now meaningful
}

Examples

Sample Sigvex Output

{
  "detector": "division-by-zero-risk",
  "severity": "critical",
  "confidence": 0.88,
  "title": "Division by unconstrained divisor `b`",
  "template": "Divide",
  "signal": "b",
  "line": 5,
  "description": "Expression `a / b` appears in a `<--` assignment but `b` has no non-zero binding. No constraint of the form `inv * b === 1` exists in `Divide`, and `b` is not wired to a component that enforces non-zeroness.",
  "recommendation": "Introduce `signal b_inv; b_inv <-- 1 / b; b_inv * b === 1;` before the division."
}

Detection Methodology

The detector scans every <-- assignment for / and % operators and extracts the divisor sub-expression. If the divisor is a literal non-zero constant the finding is skipped. Otherwise, the detector reduces the divisor to a set of signal names (unwrapping simple arithmetic such as b + 0 or 1 * b) and searches the enclosing template for a constraint of the shape x * divisor === 1, a known non-zero helper component (IsZero, NonZero) whose output is asserted, or an explicit bit decomposition that forces the lowest bit to one.

Signals that appear only inside unconstrained branches are treated conservatively as unprotected. Divisions whose divisor is itself derived from another nondeterministic computation are reported with reduced confidence, since the protection may exist one level up.

Limitations

• Non-zero properties established in sub-components are only linked to the division site when the sub-component’s output is read with <==.
• Arithmetic laundering such as q <-- a / (b + 0) is simplified only for additive identities; more complex equivalent forms are not detected.
• Divisions written through function calls (for example a user-defined div(a, b)) are analysed only when the function is inlined.

Related Detectors

• Nondeterministic Witness — other nondeterministic operators in <--
• Under-Constrained Signal — signals missing any binding
• Field Overflow — arithmetic that wraps the field prime

References

• Circom Documentation: Basic Operators
• iden3/circomlib: comparators.circom (IsZero)
• Pailoor, S., Wang, Y., Wang, X., Dillig, I. “Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs.” IACR ePrint 2023/512.