From 506fd0b8d9a1c9859890d74421246b19cc4b920a Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 5 Aug 2026 13:17:59 -0300 Subject: [PATCH 1/2] poc: ECSM operand-address AIR/executor divergence (7-value window) Demonstrates that the ECSM AIR accepts operand low limbs the executor rejects with EcsmAddressOverflow. The charged mechanism (unconstrained address limbs => forgeable) is NOT the finding and was refuted: a non-canonical limb is self-defeating on the Memory bus. What survives is an off-by-N: the executor guards +31, the AIR only needs +24, because MEMW carries the last dword's trailing bytes correctly. a0 low limb executor proof verifies 0xFFFF_FFE0 accepts yes (positive control) 0xFFFF_FFE1 EcsmAddressOverflow yes <- GAP 0xFFFF_FFE7 EcsmAddressOverflow yes <- GAP 0xFFFF_FFE8 EcsmAddressOverflow NO (LogUp imbalance) The off=24 / off=25 discrimination is the +-1 the mechanism predicts, so the harness is not rubber-stamping. Only the executor's guard is bypassed (env var); trace builder, AIRs and verifier are untouched. Gain is halt-vs-continue on an attacker-authored ELF: nothing is forged, and the bytes land at arithmetically correct 64-bit addresses. Adjudged LOW. Fix direction: the AIR moves (add the range check), NOT the executor -- the two guards accept incomparable sets, so relaxing the executor to +24 would accept H=0xFFFF_FFFF cases the AIR cannot prove, turning a soundness gap into a liveness bug. --- executor/programs/asm/test_ecsm_limb_24.s | 31 +++++ executor/programs/asm/test_ecsm_limb_25.s | 31 +++++ executor/programs/asm/test_ecsm_limb_31.s | 31 +++++ executor/programs/asm/test_ecsm_limb_32.s | 30 +++++ executor/programs/asm/test_limb_cross_sd.s | 14 +++ executor/src/vm/instruction/execution.rs | 10 +- prover/src/tests/prove_elfs_tests.rs | 126 +++++++++++++++++++++ 7 files changed, 270 insertions(+), 3 deletions(-) create mode 100644 executor/programs/asm/test_ecsm_limb_24.s create mode 100644 executor/programs/asm/test_ecsm_limb_25.s create mode 100644 executor/programs/asm/test_ecsm_limb_31.s create mode 100644 executor/programs/asm/test_ecsm_limb_32.s create mode 100644 executor/programs/asm/test_limb_cross_sd.s diff --git a/executor/programs/asm/test_ecsm_limb_24.s b/executor/programs/asm/test_ecsm_limb_24.s new file mode 100644 index 000000000..44f89b34a --- /dev/null +++ b/executor/programs/asm/test_ecsm_limb_24.s @@ -0,0 +1,31 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + addi sp, sp, -64 + li t0, 0x59F2815B16F81798 + sd t0, 0(sp) + li t0, 0x029BFCDB2DCE28D9 + sd t0, 8(sp) + li t0, 0x55A06295CE870B07 + sd t0, 16(sp) + li t0, 0x79BE667EF9DCBBAC + sd t0, 24(sp) + li t0, 5 + sd t0, 32(sp) + sd zero, 40(sp) + sd zero, 48(sp) + sd zero, 56(sp) + # a0 = 2^32 - 24 (low limb of the xR output address, high limb 0) + li t1, 1 + slli t1, t1, 32 + addi a0, t1, -24 + addi a1, sp, 0 + addi a2, sp, 32 + li a7, -11 + ecall + addi sp, sp, 64 + li a0, 0 + li a7, 93 + ecall +.Lfunc_end1: + .size main, .Lfunc_end1-main diff --git a/executor/programs/asm/test_ecsm_limb_25.s b/executor/programs/asm/test_ecsm_limb_25.s new file mode 100644 index 000000000..db4328565 --- /dev/null +++ b/executor/programs/asm/test_ecsm_limb_25.s @@ -0,0 +1,31 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + addi sp, sp, -64 + li t0, 0x59F2815B16F81798 + sd t0, 0(sp) + li t0, 0x029BFCDB2DCE28D9 + sd t0, 8(sp) + li t0, 0x55A06295CE870B07 + sd t0, 16(sp) + li t0, 0x79BE667EF9DCBBAC + sd t0, 24(sp) + li t0, 5 + sd t0, 32(sp) + sd zero, 40(sp) + sd zero, 48(sp) + sd zero, 56(sp) + # a0 = 2^32 - 25 (low limb of the xR output address, high limb 0) + li t1, 1 + slli t1, t1, 32 + addi a0, t1, -25 + addi a1, sp, 0 + addi a2, sp, 32 + li a7, -11 + ecall + addi sp, sp, 64 + li a0, 0 + li a7, 93 + ecall +.Lfunc_end1: + .size main, .Lfunc_end1-main diff --git a/executor/programs/asm/test_ecsm_limb_31.s b/executor/programs/asm/test_ecsm_limb_31.s new file mode 100644 index 000000000..64aa319db --- /dev/null +++ b/executor/programs/asm/test_ecsm_limb_31.s @@ -0,0 +1,31 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + addi sp, sp, -64 + li t0, 0x59F2815B16F81798 + sd t0, 0(sp) + li t0, 0x029BFCDB2DCE28D9 + sd t0, 8(sp) + li t0, 0x55A06295CE870B07 + sd t0, 16(sp) + li t0, 0x79BE667EF9DCBBAC + sd t0, 24(sp) + li t0, 5 + sd t0, 32(sp) + sd zero, 40(sp) + sd zero, 48(sp) + sd zero, 56(sp) + # a0 = 2^32 - 31 (low limb of the xR output address, high limb 0) + li t1, 1 + slli t1, t1, 32 + addi a0, t1, -31 + addi a1, sp, 0 + addi a2, sp, 32 + li a7, -11 + ecall + addi sp, sp, 64 + li a0, 0 + li a7, 93 + ecall +.Lfunc_end1: + .size main, .Lfunc_end1-main diff --git a/executor/programs/asm/test_ecsm_limb_32.s b/executor/programs/asm/test_ecsm_limb_32.s new file mode 100644 index 000000000..821865d65 --- /dev/null +++ b/executor/programs/asm/test_ecsm_limb_32.s @@ -0,0 +1,30 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + addi sp, sp, -64 + li t0, 0x59F2815B16F81798 + sd t0, 0(sp) + li t0, 0x029BFCDB2DCE28D9 + sd t0, 8(sp) + li t0, 0x55A06295CE870B07 + sd t0, 16(sp) + li t0, 0x79BE667EF9DCBBAC + sd t0, 24(sp) + li t0, 5 + sd t0, 32(sp) + sd zero, 40(sp) + sd zero, 48(sp) + sd zero, 56(sp) + li t1, 1 + slli t1, t1, 32 + addi a0, t1, -32 + addi a1, sp, 0 + addi a2, sp, 32 + li a7, -11 + ecall + addi sp, sp, 64 + li a0, 0 + li a7, 93 + ecall +.Lfunc_end1: + .size main, .Lfunc_end1-main diff --git a/executor/programs/asm/test_limb_cross_sd.s b/executor/programs/asm/test_limb_cross_sd.s new file mode 100644 index 000000000..42dd1a530 --- /dev/null +++ b/executor/programs/asm/test_limb_cross_sd.s @@ -0,0 +1,14 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + li t1, 1 + slli t1, t1, 32 + addi t2, t1, -4 # 0xFFFFFFFC: an 8-byte store here spans into hi=1 + li t0, 0x0123456789ABCDEF + sd t0, 0(t2) + ld t3, 0(t2) + li a0, 0 + li a7, 93 + ecall +.Lfunc_end1: + .size main, .Lfunc_end1-main diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index c92c0ab88..6d1d7fde8 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -429,9 +429,13 @@ impl Instruction { let addr_xr = registers.read(10)?; let addr_xg = registers.read(11)?; let addr_k = registers.read(12)?; - if !ecsm_addr_ok(addr_xg, 31) - || !ecsm_addr_ok(addr_xr, 31) - || !ecsm_addr_ok(addr_k, 31) + // PoC ONLY (adversarial adjudication): the env var lets a test + // run the reference semantics WITHOUT this guard, to see whether + // the resulting trace still satisfies the AIR. + if std::env::var_os("ECSM_NO_LIMB_GUARD").is_none() + && (!ecsm_addr_ok(addr_xg, 31) + || !ecsm_addr_ok(addr_xr, 31) + || !ecsm_addr_ok(addr_k, 31)) { return Err(ExecutionError::EcsmAddressOverflow); } diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index ffe9071b2..a689ff4b9 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -3526,3 +3526,129 @@ fn test_epoch_memory_bus_with_l2g_bookend() { "epoch Memory bus must balance with L2G bookend + PAGE excluding touched cells" ); } + +// ============================================================================= +// PoC (adversarial adjudication): ECSM low-limb window +// ============================================================================= + +/// Shared body: `name` is an asm ELF whose ECSM output address (`a0`) has low +/// limb `2^32 - off`. Returns `(executor_rejects_unpatched, prove_verify_ok)`. +fn ecsm_limb_poc(name: &str) -> (bool, bool) { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = crate::test_utils::asm_elf_bytes(name); + let elf = Elf::load(&elf_bytes).expect("Failed to load ELF"); + + // (1) Reference semantics: the unpatched executor must reject. + unsafe { std::env::remove_var("ECSM_NO_LIMB_GUARD") }; + let ex = Executor::new(&elf, vec![]).expect("Failed to create executor"); + let rejects = match ex.run() { + Err(e) => { + println!("[poc {name}] reference executor: {e:?}"); + format!("{e:?}").contains("EcsmAddressOverflow") + } + Ok(_) => { + println!("[poc {name}] reference executor: COMPLETED (no guard hit)"); + false + } + }; + + // (2) Same program, guard bypassed: does the resulting proof verify? + unsafe { std::env::set_var("ECSM_NO_LIMB_GUARD", "1") }; + let opts = ProofOptions::default_test_options(); + let ok = match crate::prove_with_options(&elf_bytes, &opts, &MaxRowsConfig::default()) { + Ok(proof) => match crate::verify_with_options(&proof, &elf_bytes, &opts, None, None) { + Ok(v) => { + println!("[poc {name}] prove OK, verify = {v}"); + v + } + Err(e) => { + println!("[poc {name}] verify ERROR: {e:?}"); + false + } + }, + Err(e) => { + println!("[poc {name}] prove ERROR: {e:?}"); + false + } + }; + unsafe { std::env::remove_var("ECSM_NO_LIMB_GUARD") }; + (rejects, ok) +} + +#[test] +fn poc_ecsm_limb_gap_31() { + // addr_xr low limb = 2^32 - 31 = 0xFFFF_FFE1. Executor: reject. AIR: ? + let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_31"); + println!("RESULT off=31 executor_rejects={rejects} proof_verifies={ok}"); + assert!(rejects, "executor should reject 0xFFFF_FFE1"); + assert!(ok, "SOUNDNESS GAP: proof verified for an execution the executor halts on"); +} + +#[test] +fn poc_ecsm_limb_gap_25() { + // addr_xr low limb = 2^32 - 25 = 0xFFFF_FFE7 — the last value in the window. + let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_25"); + println!("RESULT off=25 executor_rejects={rejects} proof_verifies={ok}"); + assert!(rejects); + assert!(ok); +} + +#[test] +fn poc_ecsm_limb_gap_24_negative_control() { + // addr_xr low limb = 2^32 - 24 = 0xFFFF_FFE8: dword base +24 leaves the limb, + // so the AIR's byte-0 token is non-canonical. Expect prove/verify to FAIL. + let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_24"); + println!("RESULT off=24 executor_rejects={rejects} proof_verifies={ok}"); + assert!(rejects); + assert!(!ok, "negative control: 0xFFFF_FFE8 should NOT be provable"); +} + +#[test] +fn poc_ecsm_limb_gap_32_positive_control() { + // addr_xr low limb = 2^32 - 32 = 0xFFFF_FFE0: the largest value the EXECUTOR + // allows. Executor accepts AND the proof verifies — so the only thing that + // differs between this and off=31 is the guard, not the harness. + let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_32"); + println!("RESULT off=32 executor_rejects={rejects} proof_verifies={ok}"); + assert!(!rejects, "executor should ACCEPT 0xFFFF_FFE0"); + assert!(ok); +} + +#[test] +fn poc_plain_sd_across_limb_boundary() { + // A plain 8-byte store at 0xFFFF_FFFC (spanning into high limb 1) is accepted + // by the executor AND provable: the VM's general MEMW path carries correctly + // across the 2^32 limb boundary. Only the ECSM ecall refuses it. + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = crate::test_utils::asm_elf_bytes("test_limb_cross_sd"); + let elf = Elf::load(&elf_bytes).expect("Failed to load ELF"); + let ex = Executor::new(&elf, vec![]).expect("Failed to create executor"); + let res = ex.run(); + println!("[poc plain-sd] executor: {:?}", res.as_ref().err()); + assert!(res.is_ok(), "plain limb-crossing sd must execute"); + let opts = ProofOptions::default_test_options(); + let proof = crate::prove_with_options(&elf_bytes, &opts, &MaxRowsConfig::default()) + .expect("prove failed"); + let ok = crate::verify_with_options(&proof, &elf_bytes, &opts, None, None).expect("verify err"); + println!("RESULT plain-sd-across-limb proof_verifies={ok}"); + assert!(ok, "limb-crossing plain store should be provable"); +} + +#[test] +fn poc_ecsm_limb_gap_31_shows_pages_above_2p32() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = crate::test_utils::asm_elf_bytes("test_ecsm_limb_31"); + unsafe { std::env::set_var("ECSM_NO_LIMB_GUARD", "1") }; + let opts = ProofOptions::default_test_options(); + let proof = crate::prove_with_options(&elf_bytes, &opts, &MaxRowsConfig::default()).unwrap(); + unsafe { std::env::remove_var("ECSM_NO_LIMB_GUARD") }; + for r in &proof.runtime_page_ranges { + println!("RUNTIME PAGE base=0x{:016X} count={}", r.base, r.count); + } + let above = proof + .runtime_page_ranges + .iter() + .any(|r| (0..r.count).any(|i| r.base + i * (1u64 << 18) >= (1u64 << 32))); + println!("RESULT has_page_at_or_above_2^32={above}"); + assert!(above, "the xR write must have spilled past the 2^32 limb boundary"); +} From fd4a7e65b4648bfe5cf6a9a2d2840c6892a0709b Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 5 Aug 2026 17:24:05 -0300 Subject: [PATCH 2/2] style: rustfmt the ECSM limb-gap PoC MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `cargo fmt --check` failed CI on two `assert!` calls whose message argument pushed them over the line limit. Formatting only — no assertion, no test, and in particular no part of the `ecsm_addr_ok` env-var gate is touched. That gate is deliberate: it is what lets the PoC run at all, and this branch is a demonstration, not a merge candidate. --- prover/src/tests/prove_elfs_tests.rs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index a689ff4b9..d921a1e4e 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -3581,7 +3581,10 @@ fn poc_ecsm_limb_gap_31() { let (rejects, ok) = ecsm_limb_poc("test_ecsm_limb_31"); println!("RESULT off=31 executor_rejects={rejects} proof_verifies={ok}"); assert!(rejects, "executor should reject 0xFFFF_FFE1"); - assert!(ok, "SOUNDNESS GAP: proof verified for an execution the executor halts on"); + assert!( + ok, + "SOUNDNESS GAP: proof verified for an execution the executor halts on" + ); } #[test] @@ -3650,5 +3653,8 @@ fn poc_ecsm_limb_gap_31_shows_pages_above_2p32() { .iter() .any(|r| (0..r.count).any(|i| r.base + i * (1u64 << 18) >= (1u64 << 32))); println!("RESULT has_page_at_or_above_2^32={above}"); - assert!(above, "the xR write must have spilled past the 2^32 limb boundary"); + assert!( + above, + "the xR write must have spilled past the 2^32 limb boundary" + ); }