# Missing range checks in AUIPC

AUIPC circuit loop skipped range-constraining pc_limbs[1] and [2], letting a malicious prover forge destination register values and redirect execution via JALR.

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

**Target:** zkVM AUIPC instruction circuit (rv32im extension)
**Root cause:** The range-constraint loop iterates one iteration too few, leaving pc_limbs[1] and pc_limbs[2] unconstrained to bytes, so they can exceed BabyBear's modulus.
**Steps:**
1. Read core.rs#L106 loop range-constraining imm_limbs and pc_limbs; note it ends before the last two pc_limbs.
2. Patch witness generation to set pc_limbs = [51,32,240] and rd_data = [194,51,32,240] when from_pc==2110400 and imm==0.
3. Run patched code on Fibonacci example with input 0x1000000000000000; constraints pass though challenge phase errors.
4. Use SMT solver (z3 script) to find malicious limb values satisfying carry constraints without range bounds.
**How found:** Code review of the range-constraint loop in the AUIPC circuit, noticing the loop bound was one iteration short of covering all pc_limbs.
**Exploitation:** A malicious prover supplies unconstrained pc_limbs exceeding the field modulus, manipulating the AUIPC destination register value; combined with JALR this redirects execution to arbitrary program paths.
**Escalation:** Chains with the separate missing PC limb range check in AUIPC to make exploitation easier, since no byte-only witness is needed.
**Insight:** In zkVM circuits, audit loop bounds that range-constrain limb arrays: an off-by-one leaves limbs unconstrained, and SMT solvers can prove nondeterminism by checking whether two distinct witnesses satisfy the same constraints.