Under-Constrained Signal

Overview

Remediation Guide: How to Fix Under-Constrained Signals

The under-constrained signal detector identifies Circom signals that are assigned using the unconstrained assignment operator (<--) without a corresponding constraint (=== or <==). When a signal lacks constraints, the prover can set it to any value in the finite field, and the verifier has no way to detect the manipulation. This is the most fundamental ZK circuit vulnerability.

Circom provides two assignment operators for a reason. The constraining operator <== simultaneously assigns a value and generates an R1CS constraint. The unconstrained operator <-- assigns a value during witness generation but creates no constraint. Developers use <-- when the computation is not directly expressible as a quadratic constraint (division, modular arithmetic, comparisons), then add a separate === constraint to verify the result. Forgetting the === constraint is the bug this detector catches.

Why This Is an Issue

ZK proof systems separate computation into two phases: witness generation (what the prover computes) and constraint satisfaction (what the verifier checks). The verifier only sees the constraints. A signal assigned via <-- with no constraint is invisible to the verifier — the prover can substitute any field element and the proof will still verify.

This class of bug has caused real-world exploits. The Tornado Cash governance attack and multiple circomlib issues trace back to under-constrained signals. Academic research (Pailoor et al., “Automated Detection of Under-Constrained Circuits,” 2023) identifies this as the most prevalent ZK vulnerability class.

How to Resolve

Replace <-- with <== when the computation can be expressed as an R1CS constraint. When it cannot (e.g., integer division), keep <-- but add an explicit === constraint that binds the result.

// Before: Vulnerable -- no constraint on quotient
signal input a;
signal input b;
signal quotient;
quotient <-- a / b;  // prover can set quotient to anything

// After: Fixed -- constraint verifies the division
signal input a;
signal input b;
signal quotient;
quotient <-- a / b;
quotient * b === a;  // verifier checks quotient * b == a

Examples

Vulnerable Code

template UnsafeDivision() {
    signal input dividend;
    signal input divisor;
    signal output quotient;
    signal output remainder;

    quotient <-- dividend / divisor;   // no constraint!
    remainder <-- dividend % divisor;  // no constraint!
}

Both quotient and remainder are completely unconstrained. The prover can claim 100 / 7 = 999 and the proof will verify.

Fixed Code

template SafeDivision() {
    signal input dividend;
    signal input divisor;
    signal output quotient;
    signal output remainder;

    quotient <-- dividend / divisor;
    remainder <-- dividend % divisor;

    // Constrain: dividend == quotient * divisor + remainder
    dividend === quotient * divisor + remainder;

    // Constrain: remainder < divisor (requires a range check component)
    component lt = LessThan(252);
    lt.in[0] <== remainder;
    lt.in[1] <== divisor;
    lt.out === 1;
}

Sample Sigvex Output

CRITICAL  under-constrained-signal
  Signal `quotient` is assigned via `<--` (unconstrained) at line 6 but does not
  appear in any `===` or `<==` constraint. A malicious prover can set this signal
  to any value, potentially forging invalid proofs.

  Template: UnsafeDivision
  Signal:   quotient
  Line:     6
  Confidence: 0.92

  Recommendation: Either:
    1. Replace `<--` with `<==` to add a constraint, OR
    2. Add an explicit `===` constraint after the `<--` assignment

Detection Methodology

The detector builds two sets per template:

1. Unconstrained signals: all signals on the LHS of <-- assignments.
2. Constrained signals: all signals that appear anywhere in a === or <== expression (either side). This includes signals wired to component inputs or outputs, since the component’s internal constraints bind them.

Any signal in set 1 but not in set 2 is reported. The detector also recognizes component wiring patterns — when a signal is passed to a component input via <==, the component’s internal constraints are considered sufficient.

Signal name extraction uses word-boundary tokenization with filtering for Circom keywords and built-in identifiers to reduce false positives. Array index expressions inside brackets are excluded from signal name extraction.

Limitations

• Does not track transitive constraints through intermediate variables. If signal a is unconstrained but feeds into a constrained computation via a var, the detector may still flag a.
• Cannot verify that a === constraint is sufficient — only that one exists. A constraint like x === x is technically present but provides no security.
• Template-scoped analysis only. Cross-template constraint propagation (e.g., a signal constrained inside a sub-component) requires the signal to be wired via <==.

Related Detectors

• unconstrained-output — output signals with no constraints (distinct: focuses on outputs specifically)
• unconstrained-public-input — public inputs used only in <-- expressions
• prover-controlled-loop-bound — loop bounds depending on unconstrained signals

References

• Circom Documentation: Signals and Constraints
• Pailoor, S. et al. “Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs.” IEEE S&P 2023.
• circomlib GitHub repository
• 0xPARC: Common ZK Circuit Vulnerabilities