Skip to main content

Compute-Constrain Difference

Detector Type:Compute and Constrain

Summary and Usage​

The Compute-Constrain Difference (CCD) detector flags signals where the witness assignment (i.e., dataflow operations) uses a different set of signals or constants than the set used to constrain that signal. These differences typically arise when witness computation and constraint generation for a signal are performed separately (e.g., <-- and === operations in Circom instead of <==, or NondetRegs in Zirgen). This separation can lead to underconstrained or improperly constrained signals. These discrepancies may allow malicious actors to construct bogus proofs and bypass application-level security checks.

Usage​

info

Coming soon.

Example and Explanation​

The LessThanPower circuit (from the ed25519-circom repo) is designed to determine whether the input signal in is less than or equal to 2base2^{base}. The circuit therefore sets out = 1 if in ≤2base\le 2^{base} and out = 0 otherwise.

We've translated this example into Zirgen below.

compute_constrain_difference_bug.zir
component Po2<n: Val>() {
  if (Isz(n)) {
    1
  } else {
    reduce for i : 0..n { 2 } init 1 with Mul;
  }
}

component LessThanPower<base: Val>(in: Reg) {
  po2 := Val(Po2<base>());
  public out := NondetReg(if (InRange(0, in, po2)) {
    1
  } else {
    0
  });
  out * (out - 1) = 0;
}

However, this code has a bug: out is only constrained to be binary (line 16) and is not constrained by in or the base constant at all. This allows a malicious actor to set out to be any value independent of in as long as out = 0 or out = 1 (to satisfy the constraint on line 16).

For example, the assignment in = 0, out = 0 satisfies the constraints, even though the intended behavior is out = 1 when in = 0.

This example demonstrates that special care must be taken when using NondetRegs to ensure that the signals involved are properly constrained. This illustrates why the CCD detector is useful: it flags discrepancies between separate constraints and assignments that may otherwise go unnoticed.

Usage Example​

info

Coming soon.

Limitations​

The CCD detector only tracks what signals and constants a given signal is constrained by for constraints that directly include the given signal. For example, if in the above example, if out was constrained by intermediate signal foo and foo was constrained by in, the detector would not show that out was constrained by in. This may lead to false positive alerts in some cases, but in practice we find signals missing direct constraints to values used in their dataflow assignments are often unconstrained even if they have a transitive constraint on the values, as the transitive constraints are often not precise enough.

The CCD detector also only tracks the set of signals and constants in constraints and dataflow assignments, but not the operations performed over those values (e.g., addition, multiplication). The detector may therefore generate false negatives for assignments and constraints that contain the same values, but perform different operations (e.g., in + 7, in * 7 are treated as equivalent expressions).

How to Assess Severity​

The severity of a compute-constrain difference depends on whether the involved signals are properly constrained according to the circuit's design.

If the finding is not a false positive (i.e., signals are underconstrained), the consequences can be severe: the verifier may accept proofs with signal assignments outside the intended range, allowing malicious users to prove invalid statements.