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

@@ -15,6 +15,24 @@ impl SymbolicExecutor {
             || (state.is_static && matches!(kind, CallKind::Call)))
         .then(|| state.clone());
         let call_pc = state.pc.saturating_sub(1);
+
+        let has_value = matches!(kind, CallKind::Call | CallKind::CallCode);
+        let in_offset_idx = if has_value { 3 } else { 2 };
+        let in_offset = state.stack.peek(in_offset_idx)?.clone();
+        let in_size = state.stack.peek(in_offset_idx + 1)?.clone();
+        let out_offset = state.stack.peek(in_offset_idx + 2)?.clone();
+        let out_size = state.stack.peek(in_offset_idx + 3)?.clone();
+        if let Some(outcome) =
+            self.guard_memory_range(executor, state, worklist, &in_offset, &in_size)?
+        {
+            return Ok(outcome);
+        }
+        if let Some(outcome) =
+            self.guard_memory_range(executor, state, worklist, &out_offset, &out_size)?
+        {
+            return Ok(outcome);
+        }
+
         let gas = state.stack.pop()?;
         if gas.contains_gasleft() && !gas.is_raw_gasleft() {
             return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
@@ -87,6 +105,9 @@ impl SymbolicExecutor {
             }
         };
 
+        in_size.expand_memory(&mut self.cx, &mut state.memory, in_offset.clone());
+        out_size.expand_memory(&mut self.cx, &mut state.memory, out_offset.clone());
+
         if state.is_static && matches!(kind, CallKind::Call) {
             match state.constrained_word(&mut self.cx, &value) {
                 Some(value) if value.is_zero() => {}

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

@@ -14,15 +14,20 @@ impl SymbolicExecutor {
             return Ok(StepOutcome::Revert);
         }
 
+        let offset = state.stack.peek(1)?.clone();
+        let size = state.stack.peek(2)?.clone();
+        if let Some(outcome) = self.guard_memory_range(executor, state, worklist, &offset, &size)? {
+            return Ok(outcome);
+        }
+
         let value = state.stack.pop()?;
         let offset = state.stack.pop()?;
         let size = state.stack.pop()?;
         let size = match state.constrained_usize_checked(&mut self.cx, &size) {
             Some(Ok(size)) => BoundedCopySize::Concrete(size),
             Some(Err(_)) => {
                 state.return_data = SymReturnData::empty(&mut self.cx);
-                state.stack.push(SymExpr::zero(&mut self.cx))?;
-                return Ok(StepOutcome::Continue);
+                return Ok(StepOutcome::Revert);
             }
             None => {
                 let max_limit = self.config.max_calldata_bytes as usize;
@@ -44,6 +49,8 @@ impl SymbolicExecutor {
         let salt =
             if matches!(kind, CreateKind::Create2) { Some(state.stack.pop()?) } else { None };
 
+        size.expand_memory(&mut self.cx, &mut state.memory, offset.clone());
+
         let initcode = match &size {
             BoundedCopySize::Concrete(size) => {
                 if let Some(offset) = state.constrained_usize(&mut self.cx, &offset) {

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

@@ -290,6 +290,135 @@ 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 host_max_offset = (usize::MAX & !31usize).checked_sub(size);
+        let constrained_offset = state.constrained_usize_checked(&mut self.cx, offset);
+        if constrained_offset.as_ref().is_some_and(|offset| match offset {
+            Ok(offset) => host_max_offset.is_none_or(|max| *offset > max),
+            Err(_) => true,
+        }) {
+            state.return_data = SymReturnData::empty(&mut self.cx);
+            return Ok(Some(StepOutcome::Revert));
+        }
+
+        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 size = SymExpr::constant(&mut self.cx, U256::from(size));
+        let local_size =
+            state.memory.size_after_range_expansion_word(&mut self.cx, offset.clone(), size);
+        if let Some(local_size) = local_size.as_const() {
+            if local_size <= U256::from(memory_limit) {
+                return Ok(None);
+            }
+            state.return_data = SymReturnData::empty(&mut self.cx);
+            return Ok(Some(StepOutcome::Revert));
+        }
+        let memory_limit = SymExpr::constant(&mut self.cx, U256::from(memory_limit));
+        let within_limit = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, local_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)),
+        }
+    }
+
+    pub(super) fn guard_memory_range<FEN: FoundryEvmNetwork>(
+        &mut self,
+        executor: &Executor<FEN>,
+        state: &mut PathState,
+        worklist: &mut VecDeque<PathState>,
+        offset: &SymExpr,
+        size: &SymExpr,
+    ) -> Result<Option<StepOutcome>, SymbolicError> {
+        let zero_size = SymBoolExpr::eq_word_const(&mut self.cx, size, U256::ZERO);
+        let host_max = SymExpr::constant(&mut self.cx, U256::from(usize::MAX & !31usize));
+        let size_fits =
+            SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, size.clone(), host_max.clone());
+        let max_offset = SymExpr::binop(&mut self.cx, SymBinOp::Sub, host_max, size.clone());
+        let offset_fits = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, offset.clone(), max_offset);
+
+        let local_size = state.memory.size_after_range_expansion_word(
+            &mut self.cx,
+            offset.clone(),
+            size.clone(),
+        );
+        let memory_limit =
+            SymExpr::constant(&mut self.cx, U256::from(executor.evm_env().cfg_env.memory_limit()));
+        let local_fits = SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, local_size, memory_limit);
+        let nonzero_valid =
+            SymBoolExpr::and(&mut self.cx, vec![size_fits, offset_fits, local_fits]);
+        let valid_access = SymBoolExpr::or(&mut self.cx, vec![zero_size, nonzero_valid]);
+
+        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 +854,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/calldata.rs

@@ -66,6 +66,11 @@ impl SymCalldata {
 }
 
 impl BoundedCopySize {
+    pub(crate) fn expand_memory(&self, cx: &mut SymCx, memory: &mut SymMemory, offset: SymExpr) {
+        let size = self.size_word(cx);
+        memory.expand_range(cx, offset, size);
+    }
+
     pub(crate) fn read_from_memory(
         &self,
         cx: &mut SymCx,