Unused Subcomponents (unused-subcmps)

Summary and Usage

The Unused Subcomponent (USC) detector detects if any elements in an array of subcomponents are declared, but never assigned any input or output signals by the containing component. This may indicate some computation or safety checks are being erroneously omitted, which a malicious actor may be able to exploit.

Usage

The USC detector is invoked by selecting "Unused subcomponents" (unused-subcmps) in the Detector selection during the tool configuration step.

Example and Explanation

In the following example, similar the two examples in the unconstrained subcomponent inputs and unconstrained subcomponent outputs detectors, the developer is computing the positive difference between inputs. However, unlike the previous two examples, the MultiDiff circuit is computing the pairwise difference between elements in the inp_large and inp_small array, with the differences being output in the outp array. Since the circuit is designed to output a positive difference, each pair of elements in the input is constrained such that:

$$\forall_{i \in [0, n)}\, \text{inp\_large[i]} > \text{inp\_small[i]}$$

Circom Example

unused_subcmps_bug.circom

pragma circom 2.1.8;

// Inlined from circomlib/circuits/bitify.circom
template Num2Bits(n) {
  signal input in;
  signal output out[n];
  var lc1=0;

  var e2=1;
  for (var i = 0; i<n; i++) {
    out[i] <-- (in >> i) & 1;
    out[i] * (out[i] -1 ) === 0;
    lc1 += out[i] * e2;
    e2 = e2+e2;
  }

  lc1 === in;
}

// Inlined from circomlib/circuits/comparators.circom
template LessThan(n) {
  assert(n <= 252);
  signal input in[2];
  signal output out;

  component n2b = Num2Bits(n+1);

  n2b.in <== in[0]+ (1<<n) - in[1];
  for (var i = 0; i < n; i++) {
    n2b.out[i] * (n2b.out[i] - 1) === 0;
  }

  out <== 1-n2b.out[n];
}

template MultiDiff(N) {
  signal input inp_small[N];
  signal input inp_large[N];
  signal output outp[N];

  component lt[N];
  // Bug: should be `var i = 0`!
  for (var i = 1; i < N; i++) {
    lt[i] = LessThan(252);
    lt[i].in[0] <== inp_small[i];
    lt[i].in[1] <== inp_large[i];
    lt[i].out === 1;
  }

  for (var i = 0; i < N; i++) {
    outp[i] <== inp_large[i] - inp_small[i];
  }
}

component main = MultiDiff(3);

To enforce this property, the developer means to use an array of LessThan subcomponent to test if inp_small[i] is less than inp_large[i] for all i in range $[0,n)$, but never initializes the subcomponent lt[0] and therefore never checks the condition for i = 0. A value assignment of inp_small[0] = 100, inp_large[0] = 1, outp[0] = 21888242871839275222246405745257275088548364400416034343698204186575808495518 will therefore satisfy the circuit’s constraints, yet provides an output value outside the range that the developer intended (as if inp_small[0] < inp_large[0], the developer can expect outp[0] < inp_small[0] and outp[0] < inp_large[0]).

Usage Example

Running the USC detector yields the following text output log:

ZK Vanguard Output

----Running Vanguard with unused-subcmps detector----
Running detector: unused-subcmps
[Warning] Unused subcomponent in component MultiDiff @ unused_subcmps_bug.circom:36
Reported By: vanguard:unused-subcmps
Location: MultiDiff @ unused_subcmps_bug.circom:36
Confidence: 1
More Info: placeholder
Details:
In template MultiDiff @ unused_subcmps_bug.circom:36
  * Subcomponent lt[0] (type: LessThan @ unused_subcmps_bug.circom:21 )

Line 3 of the above log tells us that there is an unused subcomponent within the MultiDiff component (which is defined on line 36 of unused_subcmps_bug.circom). Lines 9–10 of the log tell us that the unused subcomponent is the first element of the lt array (lt[0]), which is an unused subcomponent of type LessThan.

Limitations

The USC detector only emits a warning because many correct circuits may leave subcomponents unused for correct circuits. Consider the following example circuit, which is designed to compute the sum of all n inputs:

sum.circom

pragma circom 2.1.8;

template Add() {
  signal input a;
  signal input b;
  signal output o;

  o <== a + b;
}

template Sum(n) {
  signal input inp[n];
  signal output outp;

  component adds[n];
  var last = inp[0];
  for (var i = 1; i < n; i++) {
    // adds[0] will not be initialized in this loop
    adds[i] = Add();
    adds[i].a <== last;
    adds[i].b <== inp[i];
    last = adds[i].o;
  }

  outp <== last;
}

component main = Sum(3);

Even though adds[0] is unused, the sum is still computed correctly (as for n numbers, only n-1 additions must be performed). The USC detector will still output a warning for this case, however, which is a false positive.

Assessing Severity

Unused subcomponents, if unintentional, are indicative of severe computational errors or constraint generation errors that may allow malicious actors to create valid proofs for bogus statements. Manual analysis should be performed to determine if the subcomponent is correctly left unused.