diff --git a/.changelog/fix-symbolic-memory-dynamic-read-false-negative.md b/.changelog/fix-symbolic-memory-dynamic-read-false-negative.md new file mode 100644 index 0000000000000..696bfa19f4a06 --- /dev/null +++ b/.changelog/fix-symbolic-memory-dynamic-read-false-negative.md @@ -0,0 +1,6 @@ +--- +forge: patch +foundry-evm-symbolic: patch +--- + +Fixed a false negative in symbolic execution's dynamic-offset memory reads: a write recorded past the tracked materialized region (including one dispatched as symbolic despite its offset being constant-evaluable) could silently read back as zero instead of its stored value, which could hide a genuine violation behind an apparent "Safe" result. diff --git a/crates/evm/symbolic/src/runtime/memory.rs b/crates/evm/symbolic/src/runtime/memory.rs index b92994f910de6..ed49adbdd3039 100644 --- a/crates/evm/symbolic/src/runtime/memory.rs +++ b/crates/evm/symbolic/src/runtime/memory.rs @@ -233,25 +233,15 @@ impl SymMemory { } else { let size = Self::size_after_access_word(cx, offset.clone(), 32); self.expand_to(cx, size); - self.load_word_dynamic(cx, &offset) + // Delegate to `read_bytes_offset`'s dynamic-offset path rather than + // maintaining a separate implementation here: it already assembles a + // dynamic read out of `byte_dynamic_with_delta`, which is the single + // place responsible for staying sound with respect to writes whose + // own offset is genuinely symbolic (see that function's doc comment). + Ok(self.read_bytes_offset(cx, offset, 32).word_at(cx, 0)) } } - fn load_word_dynamic( - &self, - cx: &mut SymCx, - offset: &SymExpr, - ) -> Result { - let mut result = SymExpr::zero(cx); - for candidate in (0..self.materialized_size).rev() { - let candidate_expr = SymExpr::constant(cx, U256::from(candidate)); - let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr); - let word = self.load_word(cx, candidate)?; - result = SymExpr::ite(cx, condition, word, result); - } - Ok(result) - } - pub(crate) fn read_concrete( &self, cx: &mut SymCx, @@ -439,18 +429,80 @@ impl SymMemory { result } + /// Resolves the byte at logical position `offset + delta` for a + /// dynamic (non-constant) `offset`. + /// + /// `store_symbolic_bytes` records writes without extending + /// `materialized_size`, including writes whose offsets are + /// constant-evaluable but not literal constants. Therefore, + /// `materialized_size` does not automatically bound every recorded + /// write; a write recorded via `store_symbolic_bytes` can land at a + /// position the candidate enumeration below never reaches, and would + /// silently read back as zero instead of its stored value. + /// + /// When every recorded write's full extent is provably within + /// `materialized_size`, that bound is a correct bound and the + /// enumeration below (unchanged from before) is sound. Only when at + /// least one write falls outside that guarantee do we fall back to + /// folding every write directly + /// against the (symbolic) read target, mirroring `byte()`'s own + /// technique -- which already handles a symbolic write offset soundly, + /// just for a *concrete* read target -- generalized to a symbolic one. + /// This full fold is deliberately not combined with the bounded + /// enumeration: doing so would require re-deriving cross-write + /// insertion-order priority by hand, and get it wrong for two writes + /// that could alias at solve time. + /// + /// The bound check below is deliberately `write.concrete_offset()` + /// (`offset.eval()`, full evaluation) *combined with* a checked + /// `offset + len <= materialized_size` extent check -- not + /// `concrete_offset().is_some()` alone. `materialized_size` is only + /// ever bumped by `store_bytes` (reached when the store dispatch's + /// `offset.as_const()` succeeds) and, separately, by + /// `store_symbolic_sized_bytes` when its own `offset.eval()` succeeds. + /// A write can land in `store_symbolic_bytes` (no bump, ever) because + /// `as_const()` -- a shallow single-node check -- failed on an offset + /// expression that `eval()` -- full recursive evaluation -- can still + /// resolve to a constant. `concrete_offset()` uses `eval()`, so such a + /// write reports as "concrete" here even though `materialized_size` + /// was never extended to cover it. Requiring the full extent to fit + /// inside the current bound (not just the offset to be evaluable) + /// catches exactly that mismatch and routes it to the safe fold-every- + /// write fallback instead of silently reading back zero. pub(crate) fn byte_dynamic_with_delta( &self, cx: &mut SymCx, offset: &SymExpr, delta: usize, ) -> SymExpr { + let materialized_size = self.materialized_size; + let all_writes_bounded = self.symbolic_writes.iter().all(|write| { + write + .concrete_offset() + .and_then(|write_offset| write_offset.checked_add(write.bytes.len())) + .is_some_and(|end| end <= materialized_size) + }); + + if all_writes_bounded { + let mut result = SymExpr::zero(cx); + for candidate in (delta..self.materialized_size).rev() { + let candidate_expr = SymExpr::constant(cx, U256::from(candidate - delta)); + let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr); + let byte = self.byte(cx, candidate); + result = SymExpr::ite(cx, condition, byte, result); + } + return result; + } + + let target = SymExpr::add_const(cx, offset.clone(), U256::from(delta)); let mut result = SymExpr::zero(cx); - for candidate in (delta..self.materialized_size).rev() { - let candidate_expr = SymExpr::constant(cx, U256::from(candidate - delta)); - let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr); - let byte = self.byte(cx, candidate); - result = SymExpr::ite(cx, condition, byte, result); + for write in &self.symbolic_writes { + for idx in 0..write.bytes.len() { + let write_offset = SymExpr::add_const(cx, write.offset.clone(), U256::from(idx)); + let condition = SymBoolExpr::eq(cx, write_offset, target.clone()); + let byte = write.bytes.byte(cx, idx); + result = SymExpr::ite(cx, condition, byte, result); + } } result } diff --git a/crates/evm/symbolic/src/tests.rs b/crates/evm/symbolic/src/tests.rs index 5db874fb7a5c9..5daaf5843dcf5 100644 --- a/crates/evm/symbolic/src/tests.rs +++ b/crates/evm/symbolic/src/tests.rs @@ -1173,6 +1173,256 @@ fn memory_symbolic_write_after_concrete_overwrite_still_applies() { assert_eq!(loaded.eval_model(&later_symbolic_wins).unwrap(), U256::from(0xbb)); } +#[test] +fn memory_dynamic_read_finds_symbolic_write_with_no_concrete_write_at_all() { + // Regression for a false negative: a store at a genuinely symbolic offset + // never extends `materialized_size` (there is no concrete candidate to + // extend it to), so a dynamic read used to enumerate zero candidates and + // silently return zero instead of the write's actual value. + let mut cx = SymCx::new(); + let mut memory = SymMemory::default(); + + let write_offset = SymExpr::var(&mut cx, "write_offset"); + let byte = SymExpr::var(&mut cx, "byte"); + memory.store_byte_offset(&mut cx, write_offset, byte); + + let read_offset = SymExpr::var(&mut cx, "read_offset"); + let loaded = memory.byte_dynamic_with_delta(&mut cx, &read_offset, 0); + + let model = symbolic_model( + &mut cx, + [ + ("write_offset".to_string(), U256::from(500)), + ("read_offset".to_string(), U256::from(500)), + ("byte".to_string(), U256::from(0xcd)), + ], + ); + assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0xcd)); +} + +#[test] +fn memory_dynamic_read_finds_symbolic_write_beyond_concretely_materialized_region() { + // Same defect, shaped like the realistic trigger: some concrete writes + // establish a modest `materialized_size` (e.g. a Solidity free-memory + // pointer write), then a *symbolic*-offset write lands well past that + // region with no further concrete write. A dynamic read at the symbolic + // write's own location must still find it. + let mut cx = SymCx::new(); + let mut memory = SymMemory::default(); + + let concrete = SymExpr::constant(&mut cx, U256::from(0xaa)); + memory.store_byte(&mut cx, 0x20, concrete); // establishes a small materialized_size + + let write_offset = SymExpr::var(&mut cx, "write_offset"); + let byte = SymExpr::var(&mut cx, "byte"); + memory.store_byte_offset(&mut cx, write_offset, byte); // symbolic offset, well past 0x20 + + let read_offset = SymExpr::var(&mut cx, "read_offset"); + let loaded = memory.byte_dynamic_with_delta(&mut cx, &read_offset, 0); + + let model = symbolic_model( + &mut cx, + [ + ("write_offset".to_string(), U256::from(0x200)), + ("read_offset".to_string(), U256::from(0x200)), + ("byte".to_string(), U256::from(0xef)), + ], + ); + assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0xef)); +} + +#[test] +fn memory_load_word_offset_dynamic_finds_symbolic_write_beyond_materialized_region() { + // Same defect via `load_word_offset` (MLOAD's entry point), which used to + // have its own separate, independently-buggy `load_word_dynamic` bounded + // the same way. Now delegates through the fixed read path. + let mut cx = SymCx::new(); + let mut memory = SymMemory::default(); + + let concrete = SymExpr::constant(&mut cx, U256::from(0xaa)); + memory.store_byte(&mut cx, 0x20, concrete); + + let write_offset = SymExpr::var(&mut cx, "write_offset"); + let word = SymExpr::var(&mut cx, "word"); + memory.store_word_offset(&mut cx, write_offset, word); + + let read_offset = SymExpr::var(&mut cx, "read_offset"); + let loaded = memory.load_word_offset(&mut cx, read_offset).unwrap(); + + let model = symbolic_model( + &mut cx, + [ + ("write_offset".to_string(), U256::from(0x200)), + ("read_offset".to_string(), U256::from(0x200)), + ("word".to_string(), U256::from(0x1234)), + ], + ); + assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0x1234)); +} + +#[test] +fn memory_dynamic_read_finds_write_at_const_evaluable_but_undispatched_concrete_offset() { + // Regression for the store-dispatch / `concrete_offset()` mismatch: store + // dispatch (`store_byte_offset` et al.) gates on `offset.as_const()` -- a + // shallow "is this literally a `Const` node" check -- to decide whether a + // write bumps `materialized_size`. `SymbolicMemoryWrite::concrete_offset` + // gates on the strictly broader `offset.eval()` (full recursive + // evaluation). `Keccak(1) & 0xff` evaluates to a concrete, small value via + // `eval()` without ever folding to a literal `Const` at construction time + // (the mask-folding rules in `and_const` have no case for a bare + // `Keccak` operand), so `as_const()` reports `None`, the write is + // dispatched through `store_symbolic_bytes` -- which never bumps + // `materialized_size` -- while `concrete_offset()` still reports it as + // concrete. A naive `concrete_offset().is_some()` fast-path predicate + // would wrongly trust `materialized_size` here and silently return zero. + let mut cx = SymCx::new(); + let mut memory = SymMemory::default(); + + let (write_offset, concrete_write_offset) = undispatched_concrete_offset(&mut cx, 1); + + let write_byte = SymExpr::constant(&mut cx, U256::from(0xef)); + memory.store_byte_offset(&mut cx, write_offset, write_byte); + + let read_offset = SymExpr::var(&mut cx, "read_offset"); + let loaded = memory.byte_dynamic_with_delta(&mut cx, &read_offset, 0); + + let model = symbolic_model(&mut cx, [("read_offset".to_string(), concrete_write_offset)]); + assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0xef)); +} + +#[test] +fn memory_load_word_offset_dynamic_finds_write_at_const_evaluable_but_undispatched_concrete_offset() +{ + // Same defect as above, exercised through `load_word_offset` (MLOAD's + // entry point) with a materialized region already established by an + // ordinary concrete store, matching the realistic trigger: some earlier + // concrete writes give a modest `materialized_size`, then a write whose + // offset only *looks* symbolic to the store dispatch (but is actually + // const-evaluable) lands past that region. + let mut cx = SymCx::new(); + let mut memory = SymMemory::default(); + + let filler = SymExpr::constant(&mut cx, U256::from(0xaa)); + memory.store_byte(&mut cx, 31, filler); // establishes materialized_size = 32 + + let (write_offset, concrete_write_offset) = undispatched_concrete_offset(&mut cx, 2); + + let write_byte = SymExpr::constant(&mut cx, U256::from(0xef)); + memory.store_byte_offset(&mut cx, write_offset, write_byte); + + // Read a full word starting exactly at the write's own (now-known) + // concrete position, so the write's byte lands at the word's most + // significant (first) position. + let read_offset = SymExpr::var(&mut cx, "read_offset"); + let loaded = memory.load_word_offset(&mut cx, read_offset).unwrap(); + + let model = symbolic_model(&mut cx, [("read_offset".to_string(), concrete_write_offset)]); + let mut expected_bytes = [0u8; 32]; + expected_bytes[0] = 0xef; + let expected = U256::from_be_bytes(expected_bytes); + assert_eq!(loaded.eval_model(&model).unwrap(), expected); +} + +/// Builds an offset expression that is const-evaluable (via `Keccak(..) & +/// 0xff`) but not `as_const()`-able, so store dispatch never bumps +/// `materialized_size` for a write using it, while `concrete_offset()` +/// still resolves it to a concrete value. Returns the offset expression and +/// its resolved concrete value (in `0..=0xff`, unpredictable but +/// deterministic per `seed`). +fn undispatched_concrete_offset(cx: &mut SymCx, seed: u64) -> (SymExpr, U256) { + let preimage = SymExpr::constant(cx, U256::from(seed)); + let len = SymExpr::constant(cx, U256::from(1)); + let name = stable_symbol(cx, "test-keccak-offset", &seed.to_be_bytes()); + let keccak = SymExpr::keccak_symbol(cx, name, len, vec![preimage]); + let mask = SymExpr::constant(cx, U256::from(0xff)); + let offset = SymExpr::binop(cx, SymBinOp::And, keccak, mask); + assert!(offset.as_const().is_none(), "must not fold to a literal Const at construction"); + let value = offset.eval().expect("Keccak(const) & 0xff is fully evaluable with no free vars"); + (offset, value) +} + +#[test] +fn memory_dynamic_read_finds_write_straddling_the_materialized_boundary() { + // Coverage gap named by review: the fast-path predicate must reject a + // write whose const-evaluable-but-undispatched offset starts INSIDE the + // current `materialized_size` bound but whose full extent (offset + + // length) ends past it. A predicate that only checked the offset itself + // (not the write's full extent) would wrongly accept this write into + // the bounded fast path, which stops enumerating at `materialized_size` + // and would miss the write's tail bytes. + let mut cx = SymCx::new(); + let mut memory = SymMemory::default(); + + let (write_offset, offset_value) = undispatched_concrete_offset(&mut cx, 3); + let offset_usize = usize::try_from(offset_value).unwrap(); + + // A concrete filler two bytes past the write's own start pins + // `materialized_size` to `offset + 2`: inside the write's real 32-byte + // extent (`store_word_offset` always writes a full EVM word), so it + // starts inside the bound and ends well past it. + let filler = SymExpr::constant(&mut cx, U256::from(0xaa)); + memory.store_byte(&mut cx, offset_usize + 1, filler); + + let write_word = SymExpr::var(&mut cx, "write_word"); + memory.store_word_offset(&mut cx, write_offset, write_word); + + // Read word-local index 3 (a marker byte placed there via the model) -- + // inside the write's real extent but well past `materialized_size`, so + // a predicate that ignored the write's full extent would have wrongly + // trusted the bounded fast path and returned zero here. + let read_offset = SymExpr::var(&mut cx, "read_offset"); + let loaded = memory.byte_dynamic_with_delta(&mut cx, &read_offset, 0); + + let mut write_word_bytes = [0u8; 32]; + write_word_bytes[3] = 0xab; + let model = symbolic_model( + &mut cx, + [ + ("read_offset".to_string(), offset_value + U256::from(3)), + ("write_word".to_string(), U256::from_be_bytes(write_word_bytes)), + ], + ); + assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0xab)); +} + +#[test] +fn memory_load_word_offset_dynamic_word_read_includes_pseudo_concrete_write_past_materialized_size() +{ + // The exact regression named by review, relative to the deleted + // `load_word_dynamic`: a const-evaluable (but undispatched-as-concrete) + // write lands well past `materialized_size`, and a dynamic WORD read + // starts 24 bytes before it -- so the write falls at word-local index + // 24, not at the read's own start. Byte-by-byte enumeration over a + // wrongly-accepted bounded fast path would exclude it entirely. + let mut cx = SymCx::new(); + let mut memory = SymMemory::default(); + + let filler = SymExpr::constant(&mut cx, U256::from(0xaa)); + memory.store_byte(&mut cx, 31, filler); // establishes materialized_size = 32 + + // `| 0x80` guarantees the resolved offset is >= 128, so `offset - 24` + // below never underflows. + let (keccak_masked, _) = undispatched_concrete_offset(&mut cx, 4); + let high_bit = SymExpr::constant(&mut cx, U256::from(0x80)); + let write_offset = SymExpr::binop(&mut cx, SymBinOp::Or, keccak_masked, high_bit); + assert!(write_offset.as_const().is_none(), "must not fold to a literal Const at construction"); + let offset_value = write_offset.eval().expect("offset is fully evaluable with no free vars"); + assert!(offset_value >= U256::from(0x80)); + + let write_byte = SymExpr::constant(&mut cx, U256::from(0xef)); + memory.store_byte_offset(&mut cx, write_offset, write_byte); + + let read_offset = SymExpr::var(&mut cx, "read_offset"); + let loaded = memory.load_word_offset(&mut cx, read_offset).unwrap(); + + let model = + symbolic_model(&mut cx, [("read_offset".to_string(), offset_value - U256::from(24))]); + let mut expected_bytes = [0u8; 32]; + expected_bytes[24] = 0xef; + let expected = U256::from_be_bytes(expected_bytes); + assert_eq!(loaded.eval_model(&model).unwrap(), expected); +} + #[test] fn memory_store_byte_accepts_symbolic_offsets() { let mut cx = SymCx::new();