# Missing range constraint on remainder check in div opcode implementation

zkSync Era zkEVM div opcode circuit omitted range constraint on subtraction result, letting a malicious validator prove an invalid remainder and manipulate on-chain contract arithmetic.

- Payout: Contest reward
- Severity: high
- Program: zkSync
- Credited: chainlight
- Disclosed: 2024-02-29
- Write-up quality: 9/10
- Original: https://github.com/code-423n4/2023-10-zksync-findings/issues/1133
- Library page: https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-01
- Tags: domain:web3 impact:funds-loss impact:integrity kind:contest platform:code4rena sev:high tech:evm tech:solidity technique:source-review vuln:business-logic vuln:crypto

**Target:** zkEVM main VM mul_div circuit (div opcode remainder check)
**Root cause:** The circuit subtracts divisor from remainder to check remainder < divisor but never range-constrains the subtraction result limbs to 32 bits, so a witness can supply out-of-range limbs that force the borrow flag true.
**Steps:**
1. Read `mul_div.rs` remainder check: `allocate_subtraction_result_unchecked(cs, &remainder_unchecked, src1_view)` then `remainder_is_less_than_divisor.conditionally_enforce_true`.
2. Note `subtraction_result_unchecked` limbs are allocated without `UInt32::from_variable_checked`, so limbs may exceed 2^32.
3. Patch witness generation so when src0==1337 the div returns quotient 0 and remainder 1337, and the subtraction witness sets limb[7]=2^32 and borrow=1.
4. Run `run_hack` test: `div r1, r1, r2, r3` with r1=1337 yields quotient 0, remainder 1337 instead of 1/0.
5. Observe the proof is accepted despite the invalid arithmetic, demonstrating a malicious validator can prove incorrect div results.
**How found:** Code review of the div opcode circuit's remainder-less-than-divisor check; noticed the subtraction result was allocated unchecked and hypothesized out-of-range limbs could force the borrow flag, then built a patched test harness to confirm.
**Exploitation:** A malicious validator generates a witness with out-of-range subtraction limbs for the div remainder check, produces a valid proof for an incorrect div result, and submits it; contracts relying on div (e.g. a DEX price calculation) execute with attacker-chosen arithmetic, enabling theft of DEX assets.
**Escalation:** Any smart contract using div is affected; attacker can target high-value contracts like DEXes to drain funds.
**Insight:** In zk circuits, any intermediate value used in a comparison or borrow check must be range-constrained; unchecked subtraction results can be given non-canonical limbs to flip boolean flags. Audit arithmetic gadget witnesses for missing `from_variable_checked` calls.