🚔PSE & Scroll zkEVM: Missing Overflow Constraint
Summary
Related Vulnerabilities: 1. Under-constrained Circuits, 2. Nondeterministic Circuits, 8. Assigned but not Constrained
Identified By: PSE Security Team
The PSE & Scroll zkEVM modulo circuit was missing a constraint, which would allow a malicious prover to create a valid proof of a false modulo operation. Since the modulo operation is a basic building block for the zkEVM, the prover could convince the verifier of a wrong state update.
Background
The PSE & Scroll zkEVM circuits are programmed using their own fork of Zcash's Halo2. Small components of the large zkEVM circuit can be broken down into what are called gadgets. In this case, the modulo gadget was missing a constraint.
The Modulo gadget is intended to constrain:
The prover must supply a, n, r, and k, where they are all less than 2^256. The Modulo gadget uses the MulAddWords gadget which constrains:
And the prover must supply a, b, c, and d. So the Modulo gadget inputs k, n, r, a for a, b, c, d. This creates the following constraint:
This constraint is intended to prove that r = a mod n. The assignment in the assign function calculates this correctly, but the constraints do not enforce it properly.
The Vulnerability
The vulnerability arises from the fact that the MulAddWords gadget is done modulo 2^256 and that k * n + r can also be greater than 2^256. This is because even though k, n, r are all less than 2^256, their multiplication and sum can be greater than that. Since the prover can manipulate k freely for a given n, r and a, the prover can use k to overflow the sum and get a successful modulo operation.
For example, let:
The statement 0 = 2^255mod3 is false. But this statement will prove successfully in the circuit. This is because this is the actual constraint that is checked (which is true in this case):
3 * 2^255 + 0 = 2^255 (mod 2^256).
Since the prover can prove these false modulo operations, they can convince the verifier of incorrect state updates that rely on these operations. The modulo operation is a basic building block of the zkEVM, so there are many possible incorrect state updates that a prover can make that will successfully be verified.
The Fix
The fix for this issue is to add another constraint forcing k * n + r to be less than 2^256 so that no overflows happen. This is enough to avoid the overflow and accurately prove that r = a mod n for any r, a, and n less than 2^256.
Conclusion The Modulo gadget relies on another gadget named MulAddWords to validate its operations. This MulAddWords gadget checks the equation: a * b + c == d, but under the constraint of modulo 2^256.
The problem arose because this equation, even when all numbers are under the constraint of 2^256, can produce results greater than 2^256. This might seem counterintuitive, but it's due to the fact that multiplying or adding large numbers (even if they're individually below a threshold) can result in a value exceeding that threshold.
As an example, consider this false statement: 0 = 2^255 mod 3. Although this is mathematically untrue, the zkEVM circuit would wrongly verify it as true because of the underlying constraint of modulo 2^256.
References
Last updated