Skip to main content

Signal-Dependent Control Flow

Detector Type:Compute Only

Summary and Usage​

The Signal-Dependent Control Flow (SDCF) detector flags cases where signal-derived values are used to control conditional statements in a ZK circuit. Conditional assignments are difficult to constrain correctly and may lead to unconstrained values. This poses a significant security risk, since unconstrained values could enable the construction of bogus proofs.

Usage​

Select "Signal-Dependent Control Flow" in the "Required Detector Selection" section of the ZK Vanguard Task Wizard.

info

This detector will report an error if run on an LLZK file where the witness generation functions are empty, as this detector analyzes witness generation code only.

Example and Explanation​

The following circuit is designed to determine whether the input in is 0 or not. If in = 0, then out = 1. For any other value of in where in != 0, then out = 0.

signal_dependent_control_flow_bug.circom
pragma circom 2.0.0;

template IsZero() {
  signal input in;
  signal output out;

  signal inv;

  inv <-- in!=0 ? 1/in : 0; // conditional expression in inv assignment

  out <== -in*inv +1;
}

component main = IsZero();

To implement this functionality, the circuit first computes the inverse inv of the input in, but uses a conditional assignment such that inv will be 0 if in is 0, with inv = 1/in otherwise (line 9). With this conditional assignment, the value of -in*inv should be -1 (mod p) if in is non-zero, and 0 otherwise. Therefore, out <== -in*inv + 1 should evaluate to 1 if in is 0, and 0 otherwise.

However, this code has a bug: there is no constraint that requires out to be a boolean value (i.e., 0 or 1). The expectation that out is boolean depends on inv being the inverse of in, but that relationship is not actually enforced in this circuit because of the conditional assignment. This allows a malicious actor to set inv to be any value independent of in as long as the out <== -in*inv +1 constraint is satisfied. The witness assignment of in = 1, inv = -1 (mod p), and out = 2 would therefore satisfy the circuit's constraints, but violates the intended output of the circuit, which is that if in = 1, out should be 0.

This example demonstrates that conditional assignments often require additional and more nuanced constraints than normal unconditional assignments may require. These challenges highlight why the SDCF detector is useful: it flags conditional logic that requires additional scrutiny.

note

This example is adapted from the IsZero circuit provided by circomlib. However, unlike our above example, the version in circomlib (found in comparators.circom) is properly constrained:

IsZero circuit from circomlib. The constraint missing from our example above is highlighted.
template IsZero() {
  signal input in;
  signal output out;


  signal inv;


  inv <-- in!=0 ? 1/in : 0;


  out <== -in*inv +1;
  in*out === 0;
}

The addition of the in*out === 0 constraint on line 13 fixes the issue pointed out in our example, as it forces one of in and out to be 0.

Limitations​

The SDCF detector flags conditional expressions and the signals used in those conditional expressions, but is unable to determine if the conditional expressions are properly constrained or not, as this requires knowledge of what the design goal of the circuit is. For example, the SDCF detector would still report the same issue for circomlib's IsZero circuit, even though it is properly constrained.

How to Assess Severity​

The severity of signal-dependent control flow depends heavily on whether or not the involved signals have been properly constrained according to the design of the circuit. Assuming that the finding is not a false positive, then the consequences can be severe, as the verifier may accept a proof with signal assignments outside of what is intended, allowing malicious users to prove invalid statements.