Load/Store AIR Does Not Enforce VM Alignment Rules
Summary
This issue was reproduced against the official nexus-zkvm 0.3.6 release source on the prover/ STWO implementation.
The VM memory model rejects unaligned halfword and word accesses, but the load/store AIR does not enforce the same rule. A forged trace can therefore describe an unaligned memory access that the VM would reject, yet still produce a proof that verifies.
Root Cause Analysis
The runtime side treats alignment as part of the VM semantics. The memory layer documents and implements alignment checks for halfword and word accesses under vm/README.md and the VM memory code.
The proving side only constrains effective-address arithmetic and the byte-level RAM tuples in load_store.rs. There is no constraint on the low address bits for LH/LHU/SH or LW/SW. The relation code even contains an explicit assumption that adding byte offsets without carry is safe because of memory alignment.
The replay PoC starts from an honest aligned SH, changes the instruction immediate from 0 to 1, moves the store record to an odd address, and updates the program word in the view to match. The same test separately confirms that the VM memory model rejects the forged unaligned halfword write, then shows that the proving and verification path still accepts it. The key checkpoints are listed in attachments/evidence.md, and the test output is in attachments/r06.log.
The standalone PoC patch is attached as attachments/r06.patch.
Reproduce Steps
From the extracted source tree:
cd nexus-zkvm-src
cargo test -p nexus-vm-prover test_unaligned_halfword_store_is_still_provable -- --nocapture
Expected result: the test passes. Inside the test, the VM-side write to the forged odd address fails, but the prover and verifier still accept the forged execution trace.
Impact
This creates a semantic mismatch between the VM and the proof system. The verifier can accept a proof for memory behavior that is invalid under the VM's own execution rules. That is a real soundness problem, not just a runtime bug, because the proof no longer enforces the machine semantics it is supposed to certify.
Attachments
attachments.zip
Load/Store AIR Does Not Enforce VM Alignment Rules
Summary
This issue was reproduced against the official
nexus-zkvm0.3.6release source on theprover/STWO implementation.The VM memory model rejects unaligned halfword and word accesses, but the load/store AIR does not enforce the same rule. A forged trace can therefore describe an unaligned memory access that the VM would reject, yet still produce a proof that verifies.
Root Cause Analysis
The runtime side treats alignment as part of the VM semantics. The memory layer documents and implements alignment checks for halfword and word accesses under
vm/README.mdand the VM memory code.The proving side only constrains effective-address arithmetic and the byte-level RAM tuples in
load_store.rs. There is no constraint on the low address bits forLH/LHU/SHorLW/SW. The relation code even contains an explicit assumption that adding byte offsets without carry is safe because of memory alignment.The replay PoC starts from an honest aligned
SH, changes the instruction immediate from0to1, moves the store record to an odd address, and updates the program word in the view to match. The same test separately confirms that the VM memory model rejects the forged unaligned halfword write, then shows that the proving and verification path still accepts it. The key checkpoints are listed in attachments/evidence.md, and the test output is in attachments/r06.log.The standalone PoC patch is attached as attachments/r06.patch.
Reproduce Steps
From the extracted source tree:
Expected result: the test passes. Inside the test, the VM-side write to the forged odd address fails, but the prover and verifier still accept the forged execution trace.
Impact
This creates a semantic mismatch between the VM and the proof system. The verifier can accept a proof for memory behavior that is invalid under the VM's own execution rules. That is a real soundness problem, not just a runtime bug, because the proof no longer enforces the machine semantics it is supposed to certify.
Attachments
attachments.zip