fix(symbolic): reject oversized memory offsets

.changelog/reject-oversized-symbolic-memory-offsets.md

@@ -0,0 +1,6 @@
+---
+forge: patch
+foundry-evm-symbolic: patch
+---
+
+Fixed symbolic execution of fixed-width memory operations at oversized offsets.

crates/evm/symbolic/src/executor/calls.rs

@@ -1046,7 +1046,7 @@ impl SymbolicExecutor {
         };
 
         let original_world = state.world.clone();
-        let mut child = state.child(frame);
+        let mut child = state.child(&mut self.cx, frame);
         if let Some((origin, origin_word)) = pranked_origin {
             child.origin = origin;
             child.origin_word = origin_word;

crates/evm/symbolic/src/executor/cheatcodes.rs

@@ -179,7 +179,7 @@ impl SymbolicExecutor {
         );
         frame.address_word = created_word.clone();
         frame.caller_word = state.address_word.clone();
-        let mut child = state.child(frame);
+        let mut child = state.child(&mut self.cx, frame);
         let pending_expected_creates = std::mem::take(&mut child.expected_creates);
         child.world = failure_world.clone();
         child.world.mark_current_transaction_created(created);

crates/evm/symbolic/src/executor/create.rs

@@ -104,7 +104,7 @@ impl SymbolicExecutor {
         );
         frame.address_word = created_word.clone();
         frame.caller_word = state.address_word.clone();
-        let mut child = state.child(frame);
+        let mut child = state.child(&mut self.cx, frame);
         let pending_expected_creates = std::mem::take(&mut child.expected_creates);
         child.world = failure_world.clone();
         child.world.mark_current_transaction_created(created);

crates/evm/symbolic/src/executor/opcodes.rs

@@ -204,7 +204,7 @@ impl SymbolicExecutor {
             false,
             calldata,
         );
-        let child = state.storage_hook_child(frame);
+        let child = state.storage_hook_child(&mut self.cx, frame);
         let outcomes = self.execute_external_call(executor, child, &code, completed_paths)?;
         if outcomes.is_empty() {
             return Ok(StepOutcome::AssumeRejected);
@@ -290,6 +290,95 @@ impl SymbolicExecutor {
         Ok(true)
     }
 
+    fn guard_fixed_memory_access<FEN: FoundryEvmNetwork>(
+        &mut self,
+        executor: &Executor<FEN>,
+        state: &mut PathState,
+        worklist: &mut VecDeque<PathState>,
+        offset: &SymExpr,
+        size: usize,
+    ) -> Result<Option<StepOutcome>, SymbolicError> {
+        let memory_limit = executor.evm_env().cfg_env.memory_limit();
+        let memory_limit_usize = usize::try_from(memory_limit).unwrap_or(usize::MAX);
+        let host_max_offset = (usize::MAX & !31usize).checked_sub(size);
+        let max_offset = |checkpoint: usize| {
+            memory_limit_usize
+                .checked_sub(checkpoint)
+                .map(|remaining| remaining & !31usize)
+                .and_then(|remaining| remaining.checked_sub(size))
+        };
+        let memory_checkpoint = state.memory_checkpoint.clone();
+        let constrained_offset = state.constrained_usize_checked(&mut self.cx, offset);
+        let constrained_checkpoint =
+            state.constrained_usize_checked(&mut self.cx, &memory_checkpoint);
+        if constrained_offset.as_ref().is_some_and(|offset| match offset {
+            Ok(offset) => host_max_offset.is_none_or(|max| *offset > max),
+            Err(_) => true,
+        }) || constrained_checkpoint.as_ref().is_some_and(Result::is_err)
+        {
+            state.return_data = SymReturnData::empty(&mut self.cx);
+            return Ok(Some(StepOutcome::Revert));
+        }
+        if let (Some(Ok(offset)), Some(Ok(checkpoint))) =
+            (&constrained_offset, &constrained_checkpoint)
+        {
+            if max_offset(*checkpoint).is_some_and(|max| *offset <= max) {
+                return Ok(None);
+            }
+            state.return_data = SymReturnData::empty(&mut self.cx);
+            return Ok(Some(StepOutcome::Revert));
+        }
+        let offset_bound = state.upper_bound_usize(&mut self.cx, offset);
+        let checkpoint_bound = state.upper_bound_usize(&mut self.cx, &memory_checkpoint);
+        if let (Some(offset), Some(checkpoint)) = (offset_bound, checkpoint_bound)
+            && max_offset(checkpoint).is_some_and(|max| offset <= max)
+        {
+            return Ok(None);
+        }
+
+        let representable = if let Some(host_max_offset) = host_max_offset {
+            let host_max_offset = SymExpr::constant(&mut self.cx, U256::from(host_max_offset));
+            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, offset.clone(), host_max_offset)
+        } else {
+            SymBoolExpr::constant(&mut self.cx, false)
+        };
+        let local_size = SymMemory::size_after_access_word(&mut self.cx, offset.clone(), size);
+        let total_size = SymExpr::binop(&mut self.cx, SymBinOp::Add, memory_checkpoint, local_size);
+        let memory_limit = SymExpr::constant(&mut self.cx, U256::from(memory_limit));
+        let within_limit = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, total_size, memory_limit);
+        let valid_access = SymBoolExpr::and(&mut self.cx, vec![representable, within_limit]);
+        let (valid_constraints, valid_sat) =
+            self.constraints_with_condition(state, valid_access.clone())?;
+        let invalid = valid_access.clone().not(&mut self.cx);
+        let (invalid_constraints, invalid_sat) = self.constraints_with_condition(state, invalid)?;
+        match (valid_sat, invalid_sat) {
+            (true, true) => {
+                let (valid_seed_models, invalid_seed_models) =
+                    state.split_corpus_seed_models(&valid_access);
+                let mut valid = state.clone();
+                valid.pc = valid.pc.saturating_sub(1);
+                valid.depth = valid.depth.saturating_sub(1);
+                valid.constraints = valid_constraints;
+                valid.set_corpus_seed_models(valid_seed_models);
+                worklist.push_back(valid);
+                state.constraints = invalid_constraints;
+                state.set_corpus_seed_models(invalid_seed_models);
+                state.return_data = SymReturnData::empty(&mut self.cx);
+                Ok(Some(StepOutcome::Revert))
+            }
+            (true, false) => {
+                state.constraints = valid_constraints;
+                Ok(None)
+            }
+            (false, true) => {
+                state.constraints = invalid_constraints;
+                state.return_data = SymReturnData::empty(&mut self.cx);
+                Ok(Some(StepOutcome::Revert))
+            }
+            (false, false) => Ok(Some(StepOutcome::AssumeRejected)),
+        }
+    }
+
     #[expect(clippy::too_many_arguments)]
     pub(super) fn step<FEN: FoundryEvmNetwork>(
         &mut self,
@@ -725,16 +814,34 @@ impl SymbolicExecutor {
                 state.stack.pop()?;
             }
             opcode::MLOAD => {
+                let offset = state.stack.peek(0)?.clone();
+                if let Some(outcome) =
+                    self.guard_fixed_memory_access(executor, state, worklist, &offset, 32)?
+                {
+                    return Ok(outcome);
+                }
                 let offset = state.stack.pop()?;
                 let value = state.memory.load_word_offset(&mut self.cx, offset)?;
                 state.stack.push(value)?;
             }
             opcode::MSTORE => {
+                let offset = state.stack.peek(0)?.clone();
+                if let Some(outcome) =
+                    self.guard_fixed_memory_access(executor, state, worklist, &offset, 32)?
+                {
+                    return Ok(outcome);
+                }
                 let offset = state.stack.pop()?;
                 let value = state.stack.pop()?;
                 state.memory.store_word_offset(&mut self.cx, offset, value);
             }
             opcode::MSTORE8 => {
+                let offset = state.stack.peek(0)?.clone();
+                if let Some(outcome) =
+                    self.guard_fixed_memory_access(executor, state, worklist, &offset, 1)?
+                {
+                    return Ok(outcome);
+                }
                 let offset = state.stack.pop()?;
                 let value = state.stack.pop()?;
                 state.memory.store_byte_offset(&mut self.cx, offset, value);

crates/evm/symbolic/src/lib.rs

@@ -23,7 +23,7 @@ use foundry_evm::{
     executors::Executor,
     revm::{
         bytecode::{Bytecode, JumpTable, opcode},
-        context::{Block, Transaction},
+        context::{Block, Cfg, Transaction},
         database::DatabaseRef,
         precompile::{blake2, bn254, hash, identity, kzg_point_evaluation, modexp, secp256k1},
         primitives::hardfork::SpecId,

crates/evm/symbolic/src/runtime/memory.rs

@@ -44,6 +44,7 @@ pub(crate) enum BoundedCopySize {
 #[derive(Clone, Debug, Default)]
 pub(crate) struct SymMemory {
     symbolic_writes: Vec<SymbolicMemoryWrite>,
+    symbolic_read_sizes: Vec<SymExpr>,
     size: usize,
 }
 
@@ -55,12 +56,7 @@ struct SymbolicMemoryWrite {
 
 impl SymbolicMemoryWrite {
     fn size_after_access(&self, cx: &mut SymCx) -> SymExpr {
-        let len = SymExpr::constant(cx, U256::from(self.bytes.len()));
-        let end = SymExpr::binop(cx, SymBinOp::Add, self.offset.clone(), len);
-        let round = SymExpr::constant(cx, U256::from(31));
-        let rounded = SymExpr::binop(cx, SymBinOp::Add, end, round);
-        let mask = SymExpr::constant(cx, !U256::from(31));
-        SymExpr::binop(cx, SymBinOp::And, rounded, mask)
+        SymMemory::size_after_access_word(cx, self.offset.clone(), self.bytes.len())
     }
 
     fn concrete_offset(&self) -> Option<usize> {
@@ -79,6 +75,15 @@ impl SymbolicMemoryWrite {
 }
 
 impl SymMemory {
+    pub(crate) fn size_after_access_word(cx: &mut SymCx, offset: SymExpr, len: usize) -> SymExpr {
+        let len = SymExpr::constant(cx, U256::from(len));
+        let end = SymExpr::binop(cx, SymBinOp::Add, offset, len);
+        let round = SymExpr::constant(cx, U256::from(31));
+        let rounded = SymExpr::binop(cx, SymBinOp::Add, end, round);
+        let mask = SymExpr::constant(cx, !U256::from(31));
+        SymExpr::binop(cx, SymBinOp::And, rounded, mask)
+    }
+
     fn size_after_access(offset: usize, len: usize) -> usize {
         let Some(end) = offset.checked_add(len) else {
             return usize::MAX & !31usize;
@@ -167,14 +172,17 @@ impl SymMemory {
     }
 
     pub(crate) fn load_word_offset(
-        &self,
+        &mut self,
         cx: &mut SymCx,
         offset: SymExpr,
     ) -> Result<SymExpr, SymbolicError> {
         if let Some(offset) = offset.as_const() {
             let Ok(offset) = usize::try_from(offset) else { return Ok(SymExpr::zero(cx)) };
+            self.size = self.size.max(Self::size_after_access(offset, 32));
             self.load_word(cx, offset)
         } else {
+            let size = Self::size_after_access_word(cx, offset.clone(), 32);
+            self.symbolic_read_sizes.push(size);
             self.load_word_dynamic(cx, &offset)
         }
     }
@@ -406,6 +414,9 @@ impl SymMemory {
             let write_size = write.size_after_access(cx);
             size = Self::max_size_word(cx, size, write_size);
         }
+        for read_size in &self.symbolic_read_sizes {
+            size = Self::max_size_word(cx, size, read_size.clone());
+        }
         size
     }
 

crates/evm/symbolic/src/runtime/state.rs

@@ -203,7 +203,8 @@ impl PathState {
         }
     }
 
-    pub(crate) fn child(&self, frame: CallFrame) -> Self {
+    pub(crate) fn child(&self, cx: &mut SymCx, mut frame: CallFrame) -> Self {
+        frame.memory_checkpoint = self.total_memory_size(cx);
         Self {
             depth: self.depth,
             call_depth: self.call_depth + 1,
@@ -246,8 +247,8 @@ impl PathState {
         }
     }
 
-    pub(crate) fn storage_hook_child(&self, frame: CallFrame) -> Self {
-        let mut child = self.child(frame);
+    pub(crate) fn storage_hook_child(&self, cx: &mut SymCx, frame: CallFrame) -> Self {
+        let mut child = self.child(cx, frame);
         child.storage_hook_active = true;
         child.recorded_logs = None;
         child.access_record = None;
@@ -1442,6 +1443,7 @@ pub(crate) struct CallFrame {
     pub(crate) is_static: bool,
     pub(crate) calldata: SymCalldata,
     pub(crate) stack: SymStack,
+    pub(crate) memory_checkpoint: SymExpr,
     pub(crate) memory: SymMemory,
     pub(crate) return_data: SymReturnData,
 }
@@ -1470,10 +1472,16 @@ impl CallFrame {
             is_static,
             calldata,
             stack: SymStack::default(),
+            memory_checkpoint: SymExpr::zero(cx),
             memory: SymMemory::default(),
             return_data: SymReturnData::empty(cx),
         }
     }
+
+    pub(crate) fn total_memory_size(&self, cx: &mut SymCx) -> SymExpr {
+        let size = self.memory.size_word(cx);
+        SymExpr::binop(cx, SymBinOp::Add, self.memory_checkpoint.clone(), size)
+    }
 }
 
 #[derive(Clone, Debug)]
@@ -2498,7 +2506,7 @@ mod tests {
         state.function_mocks.push(FunctionMock::new(callee, Address::ZERO, data));
         let frame = state.frame.clone();
 
-        let child = state.storage_hook_child(frame);
+        let child = state.storage_hook_child(&mut cx, frame);
 
         assert!(child.storage_hook_active);
         assert!(child.branch_target().is_none());

crates/evm/symbolic/src/tests.rs

@@ -1738,6 +1738,8 @@ fn path_state_child_replaces_frame_and_resets_local_loop_state() {
 
     let parent_stack = SymExpr::constant(&mut cx, U256::from(0xab));
     state.stack.push(parent_stack).unwrap();
+    let parent_memory = SymExpr::constant(&mut cx, U256::from(0xcd));
+    state.memory.store_word(&mut cx, 32, parent_memory);
 
     let constrained = SymExpr::var(&mut cx, "constrained");
     let seven = SymExpr::constant(&mut cx, U256::from(7));
@@ -1762,13 +1764,14 @@ fn path_state_child_replaces_frame_and_resets_local_loop_state() {
         calldata,
     );
 
-    let child = state.child(frame);
+    let child = state.child(&mut cx, frame);
 
     assert_eq!(child.call_depth, 3);
     assert_eq!(child.next_symbol, 7);
     assert_eq!(child.constraints, vec![constraint]);
     assert_eq!(child.world.cached_nonce(cached), Some(9));
     assert_eq!(child.address, child_address);
+    assert_eq!(child.memory_checkpoint.as_const(), Some(U256::from(64)));
     assert!(child.loop_jumps.is_empty());
     assert_eq!(state.loop_jumps.get(&3), Some(&4));
     assert!(child.stack.peek(0).is_err());