⛔Assigned but not Constrained

Book an audit with Zokyo

A very common bug and misunderstanding is the difference between assignments and constraints. For zk circuits, constraints are the mathematical equations that must be satisfied by any given inputs for a proof to be valid. If any of the inputs result in one of the constraint equations to be incorrect, a valid proof is not possible (well, extremely unlikely).

Assignments, on the other hand, simply assign a value to a variable during proof generation. Assignments do not have to be followed for a valid proof to be created. Often times, an assignment can be used, in combination with other constraints, to reduce the total number of constraints used.

Constraints actually add equations to the R1CS file whereas assignments do not.

Circom Case and Example

A great example that highlights the difference between assignment and constraint is the IsZero circom circuit:

pragma circom 2.0.0;

template IsZero() {
    signal input in;
    signal output out;
    signal inv;
    inv <-- in!=0 ? 1/in : 0;
    out <== -in*inv +1;
    in*out === 0;
}

component main {public [in]}= IsZero();

In circom, the <--, --> and = operators are assignments, whereas the <==, ==>, and === operators are constraints. So, inv is assigned 1/in if in is not 0 and is assigned 0 otherwise. This is not a constraint - a prover can assign whatever they want to inv as long as it satisfies the constraints. We will see, however, that even if the prover inputs values other than the expected assignment for inv, IsZero will still be constrained to output 1 if in == 0 and 0 otherwise.

There are 2 cases to consider, in is zero and in is nonzero. If in is zero, then the first constraint out <== -in*inv + 1 forces out == 1, and the second constraint in*out === 0 is satisfied. So the circuit acts as expected, no matter what the prover inputs for inv. For the case that in != 0, then by the second constraint, out must be 0. Therefore the first constraint must force that -in*inv + 1 == 0, and so in*inv == 1. This effectively constrains inv to equal the inverse of in as expected. Even though inv is assigned at will by the prover, the added constraints force it to actually be the inverse of in when in != 0. The circuit acts as expected for both cases of in == 0 and when in != 0.

A good question is why don't we remove the first constraint and simplify the code to the following:

template IsZero() {
    signal in;
    signal out;
    signal temp;
    temp <-- in!= 0 ? 0 : 1;
    out === temp;
}

The problem here is that temp is assigned to in != 0 ? 0 : 1 and not actually constrained. So a trustworthy prover will always run this code and generate successful proofs, but a malicious prover can alter the code to assign anything to temp. A malicious prover could copy this circuit and change the temp assignment to temp <-- 1; so that the circuit always outputs 1. Their proofs generated from their slightly changed code would successfully pass a verifier built from this example circuit. We need the out <== -in*temp +1; constraint to ensure that temp is actually the inverse of in.

Another good question is why don't we constrain instead of assign: inv <== in!=0 ? 1/in : 0;. This is because circom does not support the automatic constraint of a ternary operator. It adds more than one constraint behind the scenes which affects performance. For example, the Mux1 circuit is often used in place of the ternary operator, but it adds more than one constraint. So the authors of the IsZero circuit have found a creative way to reduce the constraint count.

Halo2 Case

This type of bug can easily happen with Halo2 circuits as well - maybe even more likely because assigning is done separately from constraints. In Halo2, often times the constraints are created in a configure function, while the assignments are done in an assign function. It is easy for developers to see that the circuit is satisfied because the assign function correctly gives the desired inputs. However, if the configure function is missing a constraint, a malicious prover can fork the code and change the assign function to target the missing constraint.

A good example of this bug is from the SHL and SHR opcode circuit for the PSE zkEVM. The opcode circuit takes as input a shift variable and a shf0 variable:

let shift = cb.query_word_rlc();
let shf0 = cb.query_cell();

Shf0 is assumed to be the first byte of the shift variable. There are later constraints added on shf0 instead of shift because it is cheaper constraint-wise to only consider the first byte. However, there was a missing constraint forcing shf0 to be the first byte of shift. It is easy to miss this because shf0 and shift are properly assigned in the assign function:

let shf0 = pop1.to_le_bytes()[0];
self.shift.assign(region, offset, Some(pop1.to_le_bytes()))?;

The fix was to add a constraint forcing shf0 to equal the first byte of shift.

Preventative Techniques

To prevent these types of bugs, it is important to understand the ins and outs of whatever coding language was used to create the circuits. That way one can quickly identify what's constrained and what's assigned. Additionally, it is extremely important to go over each constraint in detail to ensure that the system is constrained to the exact expected behavior. Do not consider assignments when doing this, only the constraints. A great way to ensure your constraints are sufficient is through formal verification. Some tools are currently in the process that will help enable quick formal verification for circom and halo2 circuits.

References

This repo was inspired by a few other github repos that also document common vulnerabilities (but for solidity) -

PreviousTrusted Setup Leak NextBugs In The Wild

Last updated 1 year ago