The Prover Accepts a Trace That Never Terminates with Halt/Exit
Summary
This issue was reproduced against the official nexus-zkvm 0.3.6 release source on the default Machine::<BaseComponent>::prove / verify path in prover/.
The upgraded replay uses a real guest compiled through the official runtime entry. The guest first writes exit code 0, then writes public output 7, later overwrites the output with 9, and finally panics with exit code 1. A malicious prover can stop after the first output write, enter padding, and still get the standard proving path to accept the execution prefix with exit code 0 and output 7.
Root Cause Analysis
The padding boundary is introduced by iter_program_steps, which pads the trace with None rows after the supplied execution steps. In the CPU chip, a None row is turned into IsPadding = 1 and returns immediately in cpu.rs.
The constraints enforce padding monotonicity, but they do not require a terminal halt/exit before the transition into padding. The same file also disables the PcNext linkage when the next row is padding. In practice this means:
- entering padding is allowed as long as the trace never comes back out;
- the last active row does not need to be a halt/exit row;
- once the next row is padding, the normal PC continuity check is switched off.
The upgraded replay test in machine.rs uses the honest ELF trace to show the real program ends with output 9 and panic exit code 1, then truncates that same trace after the first output write, builds a prefix view with exit code 0 and output 7, and still gets a valid proof on the standard prover/verifier path through the public prove / verify API. See attachments/evidence.md and attachments/r02.log.
The standalone PoC patch is attached as attachments/r02.patch.
Reproduce Steps
From the extracted source tree:
cd nexus-zkvm-src
cargo test -p nexus-vm-prover accepted_execution_prefix_with_real_early_success_exit_code -- --nocapture
Expected result: the test passes. The honest execution really overwrites the output to 9 and then panics, but the truncated prefix still proves and verifies with the earlier output 7 and an explicit success exit code 0.
Impact
This is a concrete soundness issue in the execution statement. The verifier accepts a proof for a partial execution trace even though the real guest later changes the output and fails. In the reproduced case, the accepted proof says the guest exited successfully with output 7, while the real program continues to output 9 and then exits with panic code 1.
Attachments
attachments.zip
The Prover Accepts a Trace That Never Terminates with Halt/Exit
Summary
This issue was reproduced against the official
nexus-zkvm0.3.6release source on the defaultMachine::<BaseComponent>::prove/verifypath inprover/.The upgraded replay uses a real guest compiled through the official runtime entry. The guest first writes exit code
0, then writes public output7, later overwrites the output with9, and finally panics with exit code1. A malicious prover can stop after the first output write, enter padding, and still get the standard proving path to accept the execution prefix with exit code0and output7.Root Cause Analysis
The padding boundary is introduced by
iter_program_steps, which pads the trace withNonerows after the supplied execution steps. In the CPU chip, aNonerow is turned intoIsPadding = 1and returns immediately incpu.rs.The constraints enforce padding monotonicity, but they do not require a terminal halt/exit before the transition into padding. The same file also disables the
PcNextlinkage when the next row is padding. In practice this means:The upgraded replay test in
machine.rsuses the honest ELF trace to show the real program ends with output9and panic exit code1, then truncates that same trace after the first output write, builds a prefix view with exit code0and output7, and still gets a valid proof on the standard prover/verifier path through the publicprove/verifyAPI. See attachments/evidence.md and attachments/r02.log.The standalone PoC patch is attached as attachments/r02.patch.
Reproduce Steps
From the extracted source tree:
Expected result: the test passes. The honest execution really overwrites the output to
9and then panics, but the truncated prefix still proves and verifies with the earlier output7and an explicit success exit code0.Impact
This is a concrete soundness issue in the execution statement. The verifier accepts a proof for a partial execution trace even though the real guest later changes the output and fails. In the reproduced case, the accepted proof says the guest exited successfully with output
7, while the real program continues to output9and then exits with panic code1.Attachments
attachments.zip