➡️PSE & Scroll zkEVM: Missing Constraint

Book an audit with Zokyo

Summary

Related Vulnerabilities: 1. Under-constrained Circuits, 2. Nondeterministic Circuits, 8. Assigned but not Constrained

Identified By: PSE Security Team

The PSE & Scroll zkEVM SHL/SHR opcode circuit was missing a constraint, which would allow a malicious prover to create a valid proof of a false shift operation. Since the SHL/SHR opcode is a basic building block for the zkEVM, the prover could convince the verifier of a wrong state update.

Background

The SHL/SHR opcode (bit shift left and bit shift right) takes in two inputs from the stack: x and shift. For SHL it should output x << shift and for SHR it should output x >> shift. Since x and shift are on the stack, they each can be any 256 bit value. The calculation of a shift operation involves calculating 2^shift. Since shift can be a very large number, this calculation in a circuit could become very expensive. A to avoid this is recognizing that whenever shift > 255, the output to the stack should be 0 both for SHL or SHR. Then make the circuit compute 2^shift only when shift <= 255. This is what the zkEVM SHL/SHR opcode circuit does. Also note that this circuit is shared between both opcodes.

The Vulnerability

The opcode circuits take in shf0 and shift as two separate variables, where shf0 is meant to be the first byte of the shift variable. Then, if shift <= 255, the circuit calculates 2^shf0. The assign_exec_step function properly assigns these two variables:

let shf0 = pop1.to_le_bytes()[0];
...
self.shift.assign(region, offset, Some(pop1.to_le_bytes()))?;
self.shf0.assign(region, offset, Value::known(u64::from(shf0).into()))?;

However, the configure function, where constraints are created for this opcode, does not properly constrain shf0 to be the first byte of shift. This allows a malicious prover to fork this code and change the assign_exec_step function to assign whatever they want to shf0. This would allow them to successfully prove 2 << 1 outputs 8 if they assign shf0 = 2 when it should actually be constrained to output 4.

The Fix

The fix was to add the constraint forcing shf0 to be the first byte of shift. This was done with the following code addition:

instruction.constrain_zero(shf0 - FQ(shift.le_bytes[0]))

Conclusion: The circuit that handles these shift operations uses two distinct variables: shf0 and shift. While shift represents the complete shift value, shf0 is designed to capture the first byte (or 8 bits) of shift.

Though the assign_exec_step function correctly assigns values to these two variables, the constraints set in the configure function missed out on enforcing the relation between shf0 and the first byte of shift.

This oversight allows a bad actor to manipulate the shf0 value in their favor. As an example, let's look at the operation 2 << 1 (meaning, shifting the bits of number 2 to the left by one place). Mathematically, the result should be 4. However, a malicious actor can change shf0 and potentially trick the system into proving a false result, like 8, by manipulating the shift value.

References

1. Github Issue

2. The Fix