fix(symbolic): reject oversized memory offsets - #16183
Conversation
✅ Changelog foundThe deterministic check will validate the changed entry. |
figtracer
left a comment
figtracer
left a comment
There was a problem hiding this comment.
found two concrete/symbolic parity blockers and two hot-path representation costs on the current head. the full symbolic crate suite and the focused cli tests pass, but one added regression currently codifies a false proof.
mablr
left a comment
mablr
left a comment
There was a problem hiding this comment.
I don't see other blockers, sgtm
…-memory Amp-Thread-ID: https://ampcode.com/threads/T-01a01a8e-87d2-70ec-be7e-fed27bfe3644 Co-authored-by: Amp <amp@ampcode.com> # Conflicts: # crates/evm/symbolic/src/runtime/memory.rs
| } | ||
| } | ||
|
|
||
| pub(super) fn guard_memory_range<FEN: FoundryEvmNetwork>( |
There was a problem hiding this comment.
guard_memory_range only validates that the access fits the memory limit; it never grows logical_size. Read-only ops that route through it (KECCAK256, LOGn, MCOPY's src) leave memory size stale, so a later MSIZE won't reflect the expansion a real EVM would have performed for these reads.
| Ok(true) | ||
| } | ||
|
|
||
| fn guard_fixed_memory_access<FEN: FoundryEvmNetwork>( |
There was a problem hiding this comment.
This and guard_memory_range below duplicate ~25 lines of near-identical fork/clone/split-corpus-seed/push-to-worklist logic on the same (valid_sat, invalid_sat) match. Worth factoring into a shared helper so a future fix to the split idiom doesn't need to be applied twice.
| (false, false) => Ok(Some(StepOutcome::AssumeRejected)), | ||
| } | ||
| } | ||
|
|
There was a problem hiding this comment.
Unlike guard_fixed_memory_access's local_size.as_const() fast path, this always issues two constraints_with_condition solver calls, even for fully concrete offset/size that are trivially in-bounds. Once size_word() becomes non-constant (any earlier symbolic-length write in the path), every guarded opcode here pays two SMT queries unconditionally.
4 participants
Rejects unrepresentable offsets for symbolic
MLOAD,MSTORE, andMSTORE8, matching concrete EVM failure behavior and preventing false passes.