# PSE & Scroll zkEVM: Missing Overflow Constraint

{% hint style="info" %}
[**Book an audit with Zokyo**](https://www.zokyo.io/)
{% endhint %}

**Summary**

Related Vulnerabilities: 1. [Under-constrained Circuits](../common-vulnerabilities-in-zk-code/under-constrained-circuits), 2. [Nondeterministic Circuits](../common-vulnerabilities-in-zk-code/nondeterministic-circuits), 8.[ Assigned but not Constrained](../common-vulnerabilities-in-zk-code/assigned-but-not-constrained)

Identified By: [PSE Security Team](https://twitter.com/PrivacyScaling)

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](https://github.com/zcash/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:

```
a mod n = r, if n!=0
r = 0,       if n==0
```

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:

```
a * b + c == d (modulo 2**256)
```

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:

```
k * n + r == a (modulo 2**256)
```

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:

```
n = 3
k = 2^255
r = 0
a = 2^255
```

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**

1. [Github Issue](https://github.com/privacy-scaling-explorations/zkevm-circuits/issues/996)
2. [Commit of the Fix](https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/999)
