# IsLtArraySubAir is unsound

IsLtArraySubAir's diff_marker lacked a constraint that the marked position actually differs, letting a malicious prover prove x<y as false in OpenVM's zkVM circuit.

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

**Target:** zkVM circuit AIR (IsLtArraySubAir, used by VolatileBoundaryChip)
**Root cause:** The circuit never constrained that when diff_marker is set at a position, x and y actually differ there; a prover can set the marker at index 0 with diff_val=0 even when x[0]==y[0], forcing out=false for x<y.
**Steps:**
1. Pick x=[0,0], y=[0,1] where x<y.
2. Set witness diff_marker=[1,0], diff_val=0, out=0 instead of the honest [0,1]/1/1.
3. All AIR constraints pass because nothing ties marker position to an actual inequality.
4. Result: circuit accepts out=false for x<y, breaking soundness of the less-than gadget.
**How found:** Code review of IsLtArraySubAir's subrow generator and constraints: noticed diff_marker selection logic only enforced 'first differing element' on the honest generator path, not in the AIR constraints, so a prover could place the marker arbitrarily early.
**Exploitation:** A malicious prover crafts a witness with diff_marker placed at index 0 and diff_val=0, producing a valid proof that x<y is false when it is true; this unsound comparison feeds VolatileBoundaryChip, potentially letting the prover forge boundary/less-than constraints in the zkVM.
**Escalation:** Unsound less-than propagates into VolatileBoundaryChip, potentially allowing forged boundary conditions in OpenVM proofs; exact downstream impact not fully traced by the finder.
**Insight:** In zk circuits, always check that witness-generation logic is mirrored by hard constraints: any 'first difference' selector must be constrained so a set marker implies an actual inequality at that index (e.g. via diff_inv with diff*diff_inv=1).