Non-Deterministic Witness (non-det-wit)
Summary and Usage
The Non-Deterministic Witness (NDW) detector warns the user about non-deterministic witness code (i.e., dataflow operations) in their ZK circuit, which occurs when dataflow is dependent on conditional branches or conditional assignments. Conditional assignments are difficult to properly constrain and likely to lead to unconstrained values, which can lead to significant security risks as unconstrained values could allow for the construction of bogus proofs.
Usage
The NDW detector is invoked by selecting "Non-deterministic dataflow"
(non-det-wit) in the Detector selection during the tool configuration step.
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.
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, it follows thaat the value of -in*inv should be
-1 (mod p) if in is non-zero, and 0 otherwise.
Therefore, the computation and assignment of out <== -in*inv + 1 should be
1 if in is 0, and 0 if in is non zero.
However, this code has a bug: there is no constraint that requires out to be a boolean
value (i.e., 0 or 1).
out being boolean a consequence of inv being the inverse of in, which
is not a constraint in this circuit due to the use of the conditional assignment
used to create inv.
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 are why the NDW detector can be a useful tool in flagging conditional logic for further scrutiny.
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:
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.
Usage Example
Running the above example circuit in ZK Vanguard using the non-det-wit detector yields
the following output text log:
ZK Vanguard Output
----Running Vanguard with non-det-wit detector----
Running detector: non-det-wit
[Critical] Found signal in component that are used in conditional expressions IsZero @ non_det_wit_bug.circom:3
Reported By: vanguard:non-det-wit
Location: IsZero @ non_det_wit_bug.circom:3
Confidence: 0.99
More Info: placeholder
Details:
Found signal in component that are used in conditional expressions IsZero @ non_det_wit_bug.circom:3
* Signal in in expression IsZero @ non_det_wit_bug.circom:9
Line 3 of the above log tells us that the NDW detector has found a signal that is used in a conditional expression.
Lines 9–10 of the above log tell us that the input signal in is being used in a conditional expression on
line 9 of non_det_wit_bug.circom, which is the assignment inv <-- in!=0 ? 1/in : 0.
This finding tells us we need to confirm that inv and in are sufficiently constrained
given the conditional assignment.
Limitations
The NDW 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 NDW detector would still report the same issue for circomlib's IsZero circuit, even
though it is properly constrained.
Assesing Severity
The severity of a non-deterministic witness computation 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.