📌Polygon zkEVM: Missing Remainder Constraint
Summary
Related Vulnerabilities: 1. Under-constrained Circuits, 2. Nondeterministic Circuits
Identified By: Spearbit
The Polygon zkEVM division circuit was missing a constraint, which would allow a malicious prover to create a valid proof of a false division or modulo operation. Since the division and modulo operation are basic building blocks for the zkEVM, the prover could convince the verifier of a faulty state update.
Background
The Polygon zkEVM circuits are programmed using their own zk assembly language known as zkASM. Small components of the large zkEVM circuit can be broken down into different subroutines. In this case, the divARITH subroutine was missing a constraint.
The division subroutine is intended to constrain:
where:
A = divisor
E = dividend
B = quotient
C = remainder
D = set to 0 by subroutine
The inputs B and C are free inputs chosen by the prover. B is supposed to be constrained to E / A and C is supposed to be constrained to C = E % A. This subroutine provides a way to prove the division or modulo operation.
The Vulnerability
The issue with this subroutine is that there is no constraint that the remainder is less than the divisor. So in this case, without the constraint, it's possible for C >= A. A malicious prover could set B = E / A - 1 and C = (E % A) + A. This would still satisfy the equation A * B + C = D*2**256 + E.
A good example (taken from the twitter explanation) is to let:
A (divisor) = 10
E (dividend) = 101
The expected remainder (C) is 1 and the expected quotient (B) is 10. However, a malicious prover could choose B = 9 and C = 11. This would satisfy 10*9 + 11 = 101. The code never constrains C < A or 11 < 10 so the proof is successful.
This kind of forgery allows a malicious prover to tweak division and modulo operations in their favor. Since division and modulo operations are basic building blocks of the EVM, this could result in many different types of hacks favorable to the prover.
The Fix
The original authors had a constraint that C < E but instead needed C < A. So the original code:
was updated to:
Conclusion
Using the example provided: If you're dividing 101 by 10, you'd expect a quotient of 10 and a remainder of 1. But due to the missing constraint, a person could prove that 101 divided by 10 gives a quotient of 9 with a remainder of 11, which, while mathematically incorrect in the real world, still satisfies the equation within the zkEVM circuit.
This means that someone could manipulate the results of division and modulo operations, and since these are fundamental operations in computation, it could lead to numerous unintended consequences or hacks.
References
Last updated