PSE & Scroll zkEVM: Missing Constraint
PSE & Scroll zkEVM: Missing Constraint
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]))
References
https://github.com/0xPARC/zk-bug-tracker#pse-zkevm-2
Related Vulnerabilities
Under-Constrained Circuits vulnerability