[erkancamli]

Summary

The tracer's stack canary check is off by one relative to the memory layout the linker script and the book describe.

src/linker.ld.template sets __stack_bottom = ALIGN(8) after __program_end, puts the 128 byte canary at [__stack_bottom, __stack_bottom + 128), and starts the stack right after it. On the host, MemoryLayout::new sets stack_end = RAM_START_ADDRESS + program_size with program_size = program_end - RAM_START_ADDRESS. So whenever the image ends 8 byte aligned, which is the normal case, stack_end == __stack_bottom and the canary is the half-open range [stack_end, stack_end + 128).

Mmu::assert_effective_address checked (stack_end, stack_end + 128] instead:

ea <= layout.stack_end || ea > layout.stack_end + STACK_CANARY_SIZE,

So a store to the lowest doubleword of the stack (stack_end + 128) panics with "Stack overflow ... Increase stack_size", while a store to the first canary byte (stack_end) is not caught.

Reproduced end to end: a minimal RV64 guest linked with the repo's own linker.ld.template (__stack_bottom = __program_end = 0x80000048) that stores to __stack_bottom + 128 panics in the tracer with Stack overflow: attempted to write to 0x800000C8, which is in the stack canary region. With the fix it traces normally. In practice a guest whose deepest frame uses exactly all of its configured stack cannot be traced.

When the image does not end 8 byte aligned, the linker adds up to 7 bytes of padding before __stack_bottom. The new check then covers that padding plus the first 121 to 127 canary bytes, and still never rejects a store inside the stack proper, so it is never stricter than the linker layout. Making it exact in that case would need the host to round program_size up the same way the linker does; I left that out to keep this change minimal, but I am happy to add it if you prefer.

Changes

• tracer/src/emulator/mmu.rs: use ea < layout.stack_end || ea >= layout.stack_end + STACK_CANARY_SIZE, with a comment stating the range and where it comes from.
• Two regression tests in test_mmu: test_stack_overflow_first_canary_byte (a store to stack_end must panic) and test_lowest_stack_word_is_writable (a doubleword store and load at stack_end + STACK_CANARY_SIZE must succeed).

Testing

• Ran tests for modified crates

• cargo clippy and cargo fmt pass

• Both new tests fail on main and pass with the fix; all 7 test_mmu tests pass, including the existing stack_end + 1 case.

• Mutation checks: reverting only the lower bound to <= fails test_stack_overflow_first_canary_byte, reverting only the upper bound to > fails test_lowest_stack_word_is_writable.

• cargo test -p tracer: 127 passed with the fix vs 125 on main. The same 12 tests fail in both runs, all in build_muldiv_guest, because they need the jolt CLI and a RISC-V guest toolchain that my environment does not have.

• cargo clippy -p tracer --all-targets -- -D warnings and cargo fmt --check are clean.

Security Considerations

No effect on proof soundness or verifier correctness. The check lives only in the reference tracer's MMU and decides whether tracing a guest panics; it does not change what is committed or proven. The change makes the tracer accept one more legal store (the lowest stack word) and reject one it previously let through (the first canary byte).

Breaking Changes

None

[moodlezoup]

thanks!