Soundness Bug: Modulo Gadget

[kcharbo3]

The Modulo gadget assigns k to a / n. However, k is not actually constrained to a / n. Any prover can substitute their own values for k as long as it is <256 bits.

zkevm-circuits/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs

Line 72 in 9400c62

let k = if n.is_zero() { Word::zero() } else { a / n };

If the prover can submit their own values for k (< 256 bits), they can prove an inaccurate modulo operation.

Take the following values for example:
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 the MulAddWord gadget is done over the 256 bit field. So this is the constraint that is checked (which is true in this case):
3 * 2^255 + 0 = 2^255 (mod 2^256).

But I don't think this should suffice for proving 0 = 2^255mod3 (as 2^255 is not divisible by 3) So there is a whole set of values that will break this modulo operation if the prover is allowed to choose their own k value. To prevent this, another constraint needs to be added on k (ideally so that k*n < 256 bits).

In slightly more formal terms:
Let k, n, r, a < 256 bits.
The current constraint kn + r = a mod2^256 implies there exists some integer j such that kn + r = a + j2^256.
So this can be rewritten as (kn - j2^256) + r = a. (Note that the MulAddWord gadget allows for products greater than 256 bits)
Since we are trying to prove r=amodn, then there must exist some integer h such that hn + r = a.
Therefore if r=amodn is true, then we must be able to write (kn - j2^256) as an integer multiple of n. So, n must divide j * 2^256. But this requirement is never explicitly constrained in the circuit.
So the prover can manipulate k and j to satisfy (kn - j2^256) + r = a with a j * 2^256 value that is not divisible by n. So in this case, r=amodn is false but the circuit has still "proved" it to be true.

[ChihChengLiang]

I have a quick failure case but it looks like the test case failed for a different reason

diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs
index 2c4979645..800add4bb 100644
--- a/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs
+++ b/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs
@@ -142,6 +142,15 @@ mod tests {
         }
     }
 
+    #[test]
+    fn test_soundness_problem() {
+        try_test!(
+            ModGadgetTestContainer<Fr>,
+            vec![Word::from(2).pow(Word::from(255)), Word::from(3), Word::from(0)],
+            false,
+        );
+    }
+
     #[test]

[hero78119]

I have a quick failure case but it looks like the test case failed for a different reason

diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs
index 2c4979645..800add4bb 100644
--- a/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs
+++ b/zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs
@@ -142,6 +142,15 @@ mod tests {
         }
     }
 
+    #[test]
+    fn test_soundness_problem() {
+        try_test!(
+            ModGadgetTestContainer<Fr>,
+            vec![Word::from(2).pow(Word::from(255)), Word::from(3), Word::from(0)],
+            false,
+        );
+    }
+
     #[test]

Did quick test and the error with different reason from my side is as below

panicked at 'arithmetic operation overflow'

which is happened on this line https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/main/zkevm-circuits/src/evm_circuit/util/math_gadget/mul_add_words.rs#L128

However, tried to change a from Word::from(2).pow(Word::from(255)) to Word::MAX then surprisingly there is NO overflow error. Still trying to figure out the reason.

---

Back to reported question, hi @kcharbo3 may I confirm, seems checking k*n < 256 bits is still insufficient, should it be k*n + r < 256 bits instead ? If this is the case seems can leverage mul.overflow()

[kcharbo3]

Right now the test is failing because k is assigned as a/n. This ends up causing some underflows because a/n rounds down to the nearest integer. So the MulAddWords gadget tries to calculate (2^255/3)*3 + 0 = 2^255 but (2^255/3)*3 does not equal 2^255 because the division operation rounds down.
So in this line:

zkevm-circuits/zkevm-circuits/src/evm_circuit/util/math_gadget/mul_add_words.rs

Line 128 in 3da1888

let carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo - d_hi) >> 128;

d_hi > (t2 + (t3 << 64) + c_hi + carry_lo by 1. In terms of a, k, n, r: a_hi > (k*n)_hi + r_hi where k=a/n.
I think this is fine since this example should be false anyways? I think in any instance where the inputs result in a true statement, we won't run into this underflow issue. I think saturating_sub could be used here if you want to prevent this underflow (this is what MulAddWords512 uses). The test passes if you do this.

On another note, this test doesn't actually test when the prover can manipulate k right?

And yes good catch! k*n + r must be less than 256 bits.

[hero78119]

Yes it's right! thanks for the explanations

Although original case error, however yes k need to be constraint, otherwise it can be manipulate externally.

Tks for catch this issue! I raised a pull request to fix it.

[kcharbo3]

Great! Since this issue is already public and the fix request has been made, can I add this issue to the zk-bug-tracker repo? Totally understand if not or I should wait until the fix has been committed. https://github.com/0xPARC/zk-bug-tracker

[ChihChengLiang]

Hi @kcharbo3, feel free to add the issue to the zk-bug-tracker repo before or after the fix is committed.

[ChihChengLiang]

fixed in #999