Polygon zkEVM: Missing Remainder Constraint
Polygon zkEVM: Missing Remainder Constraint
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:
A * B + C = D + E
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:
C => A ; remainder E => B ; divisor
was updated to:
A => B ; divisor C => A ; remainder
References
Spearbit Twitter Explanation Thread
https://github.com/0xPARC/zk-bug-tracker#polygon-zkevm-1