# Missing constraints in LOADW and STOREW

OpenVM recursion VM's LOADW/STOREW AIRs lacked constraints linking read and written data, letting a malicious prover write arbitrary values and forge proof verification.

- Payout: Contest reward
- Severity: high
- Program: OpenVM
- Credited: georg
- Disclosed: 2025-03-24
- Write-up quality: 8/10
- Original: https://cdn.cantina.xyz/reports/cantina_competition_openvm_january2025.pdf#3.1.16
- Library page: https://bugbountylibrary.com/r/cantina%3Aopenvm_january2025%3A3.1.16
- Tags: domain:oss domain:web3 impact:integrity kind:contest platform:cantina sev:high tech:rust technique:source-review vuln:misconfiguration

**Target:** Recursion VM zkVM AIR constraints (NativeLoadStoreCoreAir / NativeLoadStoreAdapterAir)
**Root cause:** NativeLoadStoreCoreAir::eval constrains only opcode flags, not cols.data_read vs cols.data_write; NativeLoadStoreAdapterAir does not constrain ctx.reads.1 against ctx.writes.
**Steps:**
1. Patch VmOpcode to expose inner usize and prepend a dummy LOADW (opcode 256) instruction reading address 111111 and writing to 111111.
2. In core.rs witness gen, when from_pc==0 return data_write = 12345 instead of data_read.
3. Compile the leaf verifier with the dummy instruction and run the Fibonacci example (input 0xF000000000000000).
4. Observe log: `LOADW (PC 0): Reading [0], Writing [12345]` and proof still generated/verified, demonstrating unconstrained write.
**How found:** Code review of NativeLoadStoreCoreAir::eval and NativeLoadStoreAdapterAir, noticing only opcode flags were constrained and no relation between data_read and data_write existed.
**Exploitation:** A malicious prover crafts a recursive verifier program containing LOADW/STOREW instructions whose witness supplies an arbitrary data_write unrelated to data_read; since no AIR constraint ties them, the proof of the recursive verifier still verifies, allowing false 'verification' of an invalid inner proof.
**Escalation:** Breaks soundness of the recursion VM, enabling forged proof verification for any program.
**Insight:** In zkVM AIR audits, enumerate every column pair that should be equal by semantics (read vs write, adapter ctx.reads vs ctx.writes) and grep the eval for a constraint; missing equality constraints between witness-supplied columns are the classic soundness hole.