diff --git a/.changelog/reject-oversized-symbolic-memory-offsets.md b/.changelog/reject-oversized-symbolic-memory-offsets.md new file mode 100644 index 0000000000000..c251c7ba9fa9f --- /dev/null +++ b/.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. diff --git a/crates/evm/symbolic/src/executor/calls.rs b/crates/evm/symbolic/src/executor/calls.rs index 84ed95fc922d6..6b3077f4b3e58 100644 --- a/crates/evm/symbolic/src/executor/calls.rs +++ b/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() => {} diff --git a/crates/evm/symbolic/src/executor/create.rs b/crates/evm/symbolic/src/executor/create.rs index 6189c0310b625..20e95ca64bee1 100644 --- a/crates/evm/symbolic/src/executor/create.rs +++ b/crates/evm/symbolic/src/executor/create.rs @@ -14,6 +14,12 @@ 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()?; @@ -21,8 +27,7 @@ impl SymbolicExecutor { 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) { diff --git a/crates/evm/symbolic/src/executor/opcodes.rs b/crates/evm/symbolic/src/executor/opcodes.rs index 0c7a245fc2873..f8f4734301d9f 100644 --- a/crates/evm/symbolic/src/executor/opcodes.rs +++ b/crates/evm/symbolic/src/executor/opcodes.rs @@ -291,6 +291,158 @@ impl SymbolicExecutor { Ok(true) } + fn guard_fixed_memory_access( + &mut self, + executor: &Executor, + state: &mut PathState, + worklist: &mut VecDeque, + offset: &SymExpr, + size: usize, + ) -> Result, 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 expanded_size_bound = state + .upper_bound_usize(&mut self.cx, offset) + .and_then(|offset| offset.checked_add(size)) + .and_then(|end| end.checked_add(31)) + .and_then(|end| u64::try_from(end & !31usize).ok()); + if expanded_size_bound.is_some_and(|size| size <= memory_limit) { + 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 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]); + self.apply_memory_access_guard(state, worklist, valid_access) + } + + fn apply_memory_access_guard( + &mut self, + state: &mut PathState, + worklist: &mut VecDeque, + valid_access: SymBoolExpr, + ) -> Result, SymbolicError> { + 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( + &mut self, + executor: &Executor, + state: &mut PathState, + worklist: &mut VecDeque, + offset: &SymExpr, + size: &SymExpr, + ) -> Result, SymbolicError> { + let memory_limit = executor.evm_env().cfg_env.memory_limit(); + if let (Some(offset_value), Some(size_value)) = (offset.as_const(), size.as_const()) { + let valid = size_value.is_zero() + || usize::try_from(offset_value) + .ok() + .zip(usize::try_from(size_value).ok()) + .and_then(|(offset, size)| offset.checked_add(size)) + .and_then(|end| end.checked_add(31)) + .and_then(|end| u64::try_from(end & !31usize).ok()) + .is_some_and(|end| end <= memory_limit); + if !valid { + state.return_data = SymReturnData::empty(&mut self.cx); + return Ok(Some(StepOutcome::Revert)); + } + state.memory.expand_range(&mut self.cx, offset.clone(), size.clone()); + return Ok(None); + } + + let offset_bound = state.upper_bound_usize(&mut self.cx, offset); + let size_bound = state.upper_bound_usize(&mut self.cx, size); + if offset_bound + .zip(size_bound) + .and_then(|(offset, size)| offset.checked_add(size)) + .and_then(|end| end.checked_add(31)) + .and_then(|end| u64::try_from(end & !31usize).ok()) + .is_some_and(|end| end <= memory_limit) + { + state.memory.expand_range(&mut self.cx, offset.clone(), size.clone()); + return Ok(None); + } + + 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(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 outcome = self.apply_memory_access_guard(state, worklist, valid_access)?; + if outcome.is_none() { + state.memory.expand_range(&mut self.cx, offset.clone(), size.clone()); + } + Ok(outcome) + } + #[expect(clippy::too_many_arguments)] pub(super) fn step( &mut self, @@ -430,6 +582,13 @@ impl SymbolicExecutor { state.shift_word(&mut self.cx, ShiftKind::Sar)?; } opcode::KECCAK256 => { + let offset = state.stack.peek(0)?.clone(); + let size = state.stack.peek(1)?.clone(); + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &offset, &size)? + { + return Ok(outcome); + } let offset = state.stack.pop()?; let size = state.stack.pop()?; match state.constrained_usize_checked(&mut self.cx, &size) { @@ -532,6 +691,13 @@ impl SymbolicExecutor { state.stack.push(hash)?; } opcode::EXTCODECOPY => { + let dest = state.stack.peek(1)?.clone(); + let size = state.stack.peek(3)?.clone(); + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &dest, &size)? + { + return Ok(outcome); + } let target = state.stack.pop()?; let dest = state.stack.pop()?; let offset = state.stack.pop()?; @@ -587,6 +753,13 @@ impl SymbolicExecutor { state.stack.push(size)?; } opcode::CALLDATACOPY => { + let dest = state.stack.peek(0)?.clone(); + let size = state.stack.peek(2)?.clone(); + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &dest, &size)? + { + return Ok(outcome); + } let dest = state.stack.pop()?; let offset = state.stack.pop()?; let size = state.stack.pop()?; @@ -630,6 +803,13 @@ impl SymbolicExecutor { state.stack.push(value)?; } opcode::CODECOPY => { + let dest = state.stack.peek(0)?.clone(); + let size = state.stack.peek(2)?.clone(); + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &dest, &size)? + { + return Ok(outcome); + } let dest = state.stack.pop()?; let offset = state.stack.pop()?; let size = state.stack.pop()?; @@ -667,6 +847,13 @@ impl SymbolicExecutor { state.stack.push(size)?; } opcode::RETURNDATACOPY => { + let dest = state.stack.peek(0)?.clone(); + let size = state.stack.peek(2)?.clone(); + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &dest, &size)? + { + return Ok(outcome); + } let dest = state.stack.pop()?; let offset = state.stack.pop()?; let size = state.stack.pop()?; @@ -726,16 +913,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); @@ -974,6 +1179,19 @@ impl SymbolicExecutor { } opcode::JUMPDEST => {} opcode::MCOPY => { + let dest = state.stack.peek(0)?.clone(); + let src = state.stack.peek(1)?.clone(); + let size = state.stack.peek(2)?.clone(); + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &dest, &size)? + { + return Ok(outcome); + } + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &src, &size)? + { + return Ok(outcome); + } let dest = state.stack.pop()?; let src = state.stack.pop()?; let size = state.stack.pop()?; @@ -1010,8 +1228,16 @@ impl SymbolicExecutor { } } } - opcode::RETURN => return self.return_or_revert(state, false), - opcode::REVERT => return self.return_or_revert(state, true), + opcode::RETURN | opcode::REVERT => { + let offset = state.stack.peek(0)?.clone(); + let size = state.stack.peek(1)?.clone(); + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &offset, &size)? + { + return Ok(outcome); + } + return self.return_or_revert(state, op == opcode::REVERT); + } opcode::INVALID => return Ok(StepOutcome::Failure), opcode::CALL => { return self.call(executor, state, worklist, completed_paths, CallKind::Call); @@ -1130,6 +1356,13 @@ impl SymbolicExecutor { return Ok(StepOutcome::Revert); } let topics = (op - opcode::LOG0) as usize; + let offset = state.stack.peek(0)?.clone(); + let size = state.stack.peek(1)?.clone(); + if let Some(outcome) = + self.guard_memory_range(executor, state, worklist, &offset, &size)? + { + return Ok(outcome); + } let offset = state.stack.pop()?; if offset.contains_gasleft() { return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); diff --git a/crates/evm/symbolic/src/lib.rs b/crates/evm/symbolic/src/lib.rs index 11e4881fd8416..b0e951dd81df3 100644 --- a/crates/evm/symbolic/src/lib.rs +++ b/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, diff --git a/crates/evm/symbolic/src/runtime/calldata.rs b/crates/evm/symbolic/src/runtime/calldata.rs index a1a7b63ff051c..288b0e584fe92 100644 --- a/crates/evm/symbolic/src/runtime/calldata.rs +++ b/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, diff --git a/crates/evm/symbolic/src/runtime/memory.rs b/crates/evm/symbolic/src/runtime/memory.rs index 198084ba1b4d4..b92994f910de6 100644 --- a/crates/evm/symbolic/src/runtime/memory.rs +++ b/crates/evm/symbolic/src/runtime/memory.rs @@ -44,37 +44,17 @@ pub(crate) enum BoundedCopySize { #[derive(Clone, Debug, Default)] pub(crate) struct SymMemory { symbolic_writes: Vec, - concrete_size: usize, materialized_size: usize, + logical_size: Option, } #[derive(Clone, Debug)] struct SymbolicMemoryWrite { offset: SymExpr, bytes: SymBytes, - access_size: Option, } impl SymbolicMemoryWrite { - fn size_after_access(&self, cx: &mut SymCx) -> SymExpr { - let len = self - .access_size - .clone() - .unwrap_or_else(|| 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)); - let rounded = SymExpr::binop(cx, SymBinOp::And, rounded, mask); - if let Some(access_size) = &self.access_size { - let is_empty = SymBoolExpr::eq_word_const(cx, access_size, U256::ZERO); - let zero = SymExpr::zero(cx); - SymExpr::ite(cx, is_empty, zero, rounded) - } else { - rounded - } - } - fn concrete_offset(&self) -> Option { self.offset.eval().and_then(|offset| usize::try_from(offset).ok()) } @@ -91,6 +71,29 @@ impl SymbolicMemoryWrite { } impl SymMemory { + fn saturating_add_word(cx: &mut SymCx, left: SymExpr, right: SymExpr) -> SymExpr { + let sum = SymExpr::binop(cx, SymBinOp::Add, left.clone(), right); + let overflow = SymBoolExpr::cmp(cx, SymCmpOp::Ult, sum.clone(), left); + let max = SymExpr::constant(cx, U256::MAX); + SymExpr::ite(cx, overflow, max, sum) + } + + pub(crate) fn size_after_access_word(cx: &mut SymCx, offset: SymExpr, len: usize) -> SymExpr { + let size = SymExpr::constant(cx, U256::from(len)); + Self::size_after_range_word(cx, offset, size) + } + + fn size_after_range_word(cx: &mut SymCx, offset: SymExpr, size: SymExpr) -> SymExpr { + let end = Self::saturating_add_word(cx, offset, size.clone()); + let round = SymExpr::constant(cx, U256::from(31)); + let rounded = Self::saturating_add_word(cx, end, round); + let mask = SymExpr::constant(cx, !U256::from(31)); + let rounded = SymExpr::binop(cx, SymBinOp::And, rounded, mask); + let is_empty = SymBoolExpr::eq_word_const(cx, &size, U256::ZERO); + let zero = SymExpr::zero(cx); + SymExpr::ite(cx, is_empty, zero, rounded) + } + fn size_after_access(offset: usize, len: usize) -> usize { let Some(end) = offset.checked_add(len) else { return usize::MAX & !31usize; @@ -110,6 +113,13 @@ impl SymMemory { } } + fn expand_to(&mut self, cx: &mut SymCx, size: SymExpr) { + self.logical_size = Some(match self.logical_size.take() { + Some(current) => Self::max_size_word(cx, current, size), + None => size, + }); + } + pub(crate) fn store_word(&mut self, cx: &mut SymCx, offset: usize, value: SymExpr) { let bytes = value.into_bytes(cx); self.store_bytes(cx, offset, bytes); @@ -121,7 +131,8 @@ impl SymMemory { self.store_word(cx, offset, value); } } else { - self.store_symbolic_bytes(offset, value.into_bytes(cx)); + let bytes = value.into_bytes(cx); + self.store_symbolic_bytes(cx, offset, bytes); } } @@ -139,7 +150,7 @@ impl SymMemory { } else { let byte = value.low_byte(cx); let bytes = SymBytes::exprs(cx, vec![byte]); - self.store_symbolic_bytes(offset, bytes); + self.store_symbolic_bytes(cx, offset, bytes); } } @@ -148,21 +159,30 @@ impl SymMemory { return; } let size = Self::size_after_access(offset, bytes.len()); - self.concrete_size = self.concrete_size.max(size); self.materialized_size = self.materialized_size.max(size); + let size = SymExpr::constant(cx, U256::from(size)); + self.expand_to(cx, size); let offset = SymExpr::constant(cx, U256::from(offset)); - self.store_symbolic_bytes(offset, bytes); + self.symbolic_writes.push(SymbolicMemoryWrite { offset, bytes }); } - pub(crate) fn store_symbolic_bytes(&mut self, offset: SymExpr, bytes: SymBytes) { + pub(crate) fn store_symbolic_bytes( + &mut self, + cx: &mut SymCx, + offset: SymExpr, + bytes: SymBytes, + ) { if bytes.is_empty() { return; } - self.symbolic_writes.push(SymbolicMemoryWrite { offset, bytes, access_size: None }); + let size = Self::size_after_access_word(cx, offset.clone(), bytes.len()); + self.expand_to(cx, size); + self.symbolic_writes.push(SymbolicMemoryWrite { offset, bytes }); } fn store_symbolic_sized_bytes( &mut self, + cx: &mut SymCx, offset: SymExpr, bytes: SymBytes, access_size: SymExpr, @@ -173,11 +193,11 @@ impl SymMemory { let size = Self::size_after_access(offset, bytes.len()); self.materialized_size = self.materialized_size.max(size); } - self.symbolic_writes.push(SymbolicMemoryWrite { - offset, - bytes, - access_size: Some(access_size), - }); + if !bytes.is_empty() { + self.symbolic_writes.push(SymbolicMemoryWrite { offset: offset.clone(), bytes }); + } + let size = Self::size_after_range_word(cx, offset, access_size); + self.expand_to(cx, size); } pub(crate) fn store_bytes_offset(&mut self, cx: &mut SymCx, offset: SymExpr, bytes: SymBytes) { @@ -186,7 +206,7 @@ impl SymMemory { self.store_bytes(cx, offset, bytes); } } else { - self.store_symbolic_bytes(offset, bytes); + self.store_symbolic_bytes(cx, offset, bytes); } } @@ -200,14 +220,19 @@ impl SymMemory { } pub(crate) fn load_word_offset( - &self, + &mut self, cx: &mut SymCx, offset: SymExpr, ) -> Result { if let Some(offset) = offset.as_const() { let Ok(offset) = usize::try_from(offset) else { return Ok(SymExpr::zero(cx)) }; + let size = Self::size_after_access(offset, 32); + let size = SymExpr::constant(cx, U256::from(size)); + self.expand_to(cx, size); self.load_word(cx, offset) } else { + let size = Self::size_after_access_word(cx, offset.clone(), 32); + self.expand_to(cx, size); self.load_word_dynamic(cx, &offset) } } @@ -431,15 +456,33 @@ impl SymMemory { } pub(crate) fn size_word(&self, cx: &mut SymCx) -> SymExpr { - let mut size = SymExpr::constant(cx, U256::from(self.concrete_size)); - for write in &self.symbolic_writes { - if write.concrete_offset().is_some() && write.access_size.is_none() { - continue; + self.logical_size.clone().unwrap_or_else(|| SymExpr::zero(cx)) + } + + pub(crate) fn size_after_range_expansion_word( + &self, + cx: &mut SymCx, + offset: SymExpr, + size: SymExpr, + ) -> SymExpr { + let current = self.size_word(cx); + let expanded = Self::size_after_range_word(cx, offset, size); + Self::max_size_word(cx, current, expanded) + } + + pub(crate) fn expand_range(&mut self, cx: &mut SymCx, offset: SymExpr, size: SymExpr) { + if let (Some(offset), Some(size)) = (offset.as_const(), size.as_const()) + && let (Ok(offset), Ok(size)) = (usize::try_from(offset), usize::try_from(size)) + { + if size != 0 { + let size = Self::size_after_access(offset, size); + let size = SymExpr::constant(cx, U256::from(size)); + self.expand_to(cx, size); } - let write_size = write.size_after_access(cx); - size = Self::max_size_word(cx, size, write_size); + return; } - size + let size = Self::size_after_range_word(cx, offset, size); + self.expand_to(cx, size); } pub(crate) fn copy_bytes_offset(&mut self, cx: &mut SymCx, dest: SymExpr, src: SymBytes) { @@ -475,7 +518,7 @@ impl SymMemory { .collect::>(); let bytes = SymBytes::exprs(cx, bytes); let dest = SymExpr::constant(cx, U256::from(dest)); - self.store_symbolic_sized_bytes(dest, bytes, size); + self.store_symbolic_sized_bytes(cx, dest, bytes, size); } } else { let bytes = (0..src.len()) @@ -486,7 +529,7 @@ impl SymMemory { }) .collect(); let bytes = SymBytes::exprs(cx, bytes); - self.store_symbolic_sized_bytes(dest, bytes, size); + self.store_symbolic_sized_bytes(cx, dest, bytes, size); } Ok(()) } @@ -628,7 +671,7 @@ impl SymMemory { return_data.read_bytes_offset(cx, offset, copy_size) }; let size = SymExpr::constant(cx, U256::from(*size)); - self.store_symbolic_sized_bytes(dest, bytes, size); + self.store_symbolic_sized_bytes(cx, dest, bytes, size); } } BoundedCopySize::Symbolic { size, max_size } => { @@ -641,7 +684,7 @@ impl SymMemory { }) .collect::>(); let bytes = SymBytes::exprs(cx, bytes); - self.store_symbolic_sized_bytes(dest, bytes, output_size); + self.store_symbolic_sized_bytes(cx, dest, bytes, output_size); } } } diff --git a/crates/evm/symbolic/src/tests.rs b/crates/evm/symbolic/src/tests.rs index 22121f0b26534..e09d71b1763a9 100644 --- a/crates/evm/symbolic/src/tests.rs +++ b/crates/evm/symbolic/src/tests.rs @@ -1075,6 +1075,23 @@ fn memory_size_tracks_concrete_and_symbolic_extents() { assert_eq!(size.eval_model(&above_concrete).unwrap(), U256::from(128)); } +#[test] +fn memory_size_tracks_symbolic_copy_extent_not_materialized_bound() { + let mut cx = SymCx::new(); + let mut memory = SymMemory::default(); + let size = SymExpr::var(&mut cx, "size"); + let bytes = SymBytes::concrete(&mut cx, vec![1, 2, 3, 4]); + let dest = SymExpr::constant(&mut cx, U256::from(64)); + memory.copy_bytes_size_offset(&mut cx, dest, size, bytes).unwrap(); + let logical_size = memory.size_word(&mut cx); + + let empty = symbolic_model(&mut cx, [("size".to_string(), U256::ZERO)]); + assert_eq!(logical_size.eval_model(&empty).unwrap(), U256::ZERO); + + let nonempty = symbolic_model(&mut cx, [("size".to_string(), U256::from(1))]); + assert_eq!(logical_size.eval_model(&nonempty).unwrap(), U256::from(96)); +} + #[test] fn memory_concrete_write_overrides_older_symbolic_write() { let mut cx = SymCx::new(); @@ -1800,7 +1817,6 @@ 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 constrained = SymExpr::var(&mut cx, "constrained"); let seven = SymExpr::constant(&mut cx, U256::from(7)); let constraint = SymBoolExpr::eq(&mut cx, constrained, seven); diff --git a/crates/forge/tests/cli/test_cmd/symbolic_memory.rs b/crates/forge/tests/cli/test_cmd/symbolic_memory.rs index 2107aa464a4fa..2497c51f2f1f6 100644 --- a/crates/forge/tests/cli/test_cmd/symbolic_memory.rs +++ b/crates/forge/tests/cli/test_cmd/symbolic_memory.rs @@ -50,6 +50,367 @@ contract SymbolicMload { assert!(!stdout.contains("symbolic MLOAD offset"), "{stdout}"); }); +forgetest_init!(symbolic_fixed_memory_access_rejects_oversized_offset, |prj, cmd| { + if !z3_available() { + let _ = sh_eprintln!( + "skipping symbolic_fixed_memory_access_rejects_oversized_offset because z3 is not available" + ); + return; + } + + prj.add_test( + "SymbolicOversizedMemoryOffset.t.sol", + r#" +import "forge-std/Test.sol"; + +contract SymbolicOversizedMemoryOffset is Test { + function load(uint256 offset) external pure { + assembly { + pop(mload(offset)) + } + } + + function store(uint256 offset) external pure { + assembly { + mstore(offset, 1) + } + } + + function store8(uint256 offset) external pure { + assembly { + mstore8(offset, 1) + } + } + + function checkOversizedFixedMemoryAccesses() public { + uint256 offset = type(uint256).max; + (bool loadOk,) = address(this).call(abi.encodeCall(this.load, (offset))); + (bool storeOk,) = address(this).call(abi.encodeCall(this.store, (offset))); + (bool store8Ok,) = address(this).call(abi.encodeCall(this.store8, (offset))); + assertFalse(loadOk); + assertFalse(storeOk); + assertFalse(store8Ok); + } + + function checkConstrainedOversizedMemoryAccess(uint256 offset) public { + vm.assume(offset == type(uint256).max); + (bool ok,) = address(this).call(abi.encodeCall(this.store, (offset))); + assertFalse(ok); + } + + function checkMixedMemoryOffsetExploresValidSibling(uint256 offset) public { + bool endpoint; + assembly { + endpoint := or(iszero(offset), eq(offset, not(0))) + } + vm.assume(endpoint); + (bool ok,) = address(this).call(abi.encodeCall(this.store, (offset))); + assertFalse(ok); + } + + function createWithOversizedSize() external { + assembly { + pop(create(0, 0, not(0))) + } + } + + function create2WithOversizedSize() external { + assembly { + pop(create2(0, 0, not(0), 0)) + } + } + + function checkOversizedCreateRanges() public { + (bool createOk,) = address(this).call(abi.encodeCall(this.createWithOversizedSize, ())); + (bool create2Ok,) = address(this).call(abi.encodeCall(this.create2WithOversizedSize, ())); + assertFalse(createOk); + assertFalse(create2Ok); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "check.*Oversized"]) + .assert_success() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +[PASS] checkOversizedFixedMemoryAccesses() +[PASS] checkConstrainedOversizedMemoryAccess(uint256) +[PASS] checkOversizedCreateRanges() +"#]], + ); + + cmd.forge_fuse(); + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkMixedMemoryOffsetExploresValidSibling"]) + .assert_failure() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +[FAIL: +"#]], + ); + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +checkMixedMemoryOffsetExploresValidSibling(uint256) +"#]], + ); + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +args=[0] +"#]], + ); + assert!(!stdout.contains("counterexample did not replay"), "{stdout}"); +}); + +forgetest_init!(symbolic_variable_memory_access_rejects_oversized_ranges, |prj, cmd| { + if !z3_available() { + let _ = sh_eprintln!( + "skipping symbolic_variable_memory_access_rejects_oversized_ranges because z3 is not available" + ); + return; + } + + prj.add_test( + "SymbolicOversizedMemoryRange.t.sol", + r#" +contract SymbolicOversizedMemoryRange { + function calldataCopy() external pure { + assembly { + calldatacopy(not(0), 0, 1) + } + } + + function codeCopy() external pure { + assembly { + codecopy(not(0), 0, 1) + } + } + + function extcodeCopy() external view { + assembly { + extcodecopy(address(), not(0), 0, 1) + } + } + + function returndataCopy() external view { + assembly { + pop(staticcall(gas(), 4, 0, 1, 0, 1)) + returndatacopy(not(0), 0, 1) + } + } + + function memoryCopyDest() external pure { + assembly { + mcopy(not(0), 0, 1) + } + } + + function memoryCopySource() external pure { + assembly { + mcopy(0, not(0), 1) + } + } + + function hash() external pure { + assembly { + pop(keccak256(not(0), 1)) + } + } + + function log() external { + assembly { + log0(not(0), 1) + } + } + + function ret() external pure { + assembly { + return(not(0), 1) + } + } + + function rev() external pure { + assembly { + revert(not(0), 1) + } + } + + function testOversizedVariableMemoryRanges() public { + verifyOversizedVariableMemoryRanges(); + } + + function checkOversizedVariableMemoryRanges() public { + verifyOversizedVariableMemoryRanges(); + } + + function verifyOversizedVariableMemoryRanges() internal { + assertFails(this.calldataCopy.selector); + assertFails(this.codeCopy.selector); + assertFails(this.extcodeCopy.selector); + assertFails(this.returndataCopy.selector); + assertFails(this.memoryCopyDest.selector); + assertFails(this.memoryCopySource.selector); + assertFails(this.hash.selector); + assertFails(this.log.selector); + assertFails(this.ret.selector); + assertFails(this.rev.selector); + } + + function assertFails(bytes4 selector) internal { + (bool ok, bytes memory data) = + address(this).call{gas: 100_000}(abi.encodeWithSelector(selector)); + assert(!ok); + assert(data.length == 0); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--match-test", "testOversizedVariableMemoryRanges"]) + .assert_success() + .get_output() + .stdout_lossy(); + assert_relevant_lines( + &stdout, + str![[r#" +[PASS] testOversizedVariableMemoryRanges() +"#]], + ); + + cmd.forge_fuse(); + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkOversizedVariableMemoryRanges"]) + .assert_success() + .get_output() + .stdout_lossy(); + assert_relevant_lines( + &stdout, + str![[r#" +[PASS] checkOversizedVariableMemoryRanges() +"#]], + ); +}); + +forgetest_init!(symbolic_fixed_memory_access_respects_memory_limit, |prj, cmd| { + if !z3_available() { + let _ = sh_eprintln!( + "skipping symbolic_fixed_memory_access_respects_memory_limit because z3 is not available" + ); + return; + } + + prj.wipe_contracts(); + prj.update_config(|config| config.memory_limit = 4096); + prj.add_test( + "SymbolicMemoryLimit.t.sol", + r#" +contract SymbolicMemoryLimit { + fallback() external payable { + assembly { + switch callvalue() + case 0 { mstore(4065, 1) } + case 1 { mstore8(4096, 1) } + case 2 { mstore(2048, 1) } + default { mstore8(0, 1) } + } + } + + function checkMemoryLimitExactBoundaries() public pure { + assembly { + mstore(4064, 1) + mstore8(4095, 1) + } + } + + function checkMemoryLimitFirstInvalidBoundaries() public { + bool wordOk; + bool byteOk; + assembly { + wordOk := call(gas(), address(), 0, 0, 0, 0, 0) + byteOk := call(gas(), address(), 1, 0, 0, 0, 0) + } + assert(!wordOk && !byteOk); + } + + function checkMemoryLimitNestedCall() public { + bool ok; + assembly { + mstore(2048, 1) + ok := call(gas(), address(), 2, 0, 0, 0, 0) + } + assert(ok); + } + + function checkMemoryLimitCallInputExpansion() public { + bool ok; + assembly { + ok := call(gas(), address(), 3, 2048, 2048, 0, 0) + } + assert(ok); + } + + function checkMemoryLimitSymbolicCallSize(bool expand) public { + bool ok; + assembly { + let size := mul(expand, 2048) + ok := call(gas(), address(), 3, 2048, size, 0, 0) + } + assert(ok); + } + + function wrappingCallRange() external { + assembly { + pop(call(gas(), address(), 0, not(0), 1, 0, 0)) + } + } + + function nestedWrappingCallRange() external { + this.wrappingCallRange(); + } + + function checkMemoryLimitRejectsWrappingCallRanges() public { + (bool directOk,) = address(this).call(abi.encodeCall(this.wrappingCallRange, ())); + (bool nestedOk,) = address(this).call(abi.encodeCall(this.nestedWrappingCallRange, ())); + assert(!directOk && !nestedOk); + } +} +"#, + ); + + cmd.args(["test", "--match-test", "checkMemoryLimitNestedCall"]).assert_success(); + + cmd.forge_fuse(); + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkMemoryLimit"]) + .assert_success() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + str![[r#" +[PASS] checkMemoryLimitExactBoundaries() +[PASS] checkMemoryLimitFirstInvalidBoundaries() +[PASS] checkMemoryLimitNestedCall() +[PASS] checkMemoryLimitCallInputExpansion() +[PASS] checkMemoryLimitSymbolicCallSize(bool) +[PASS] checkMemoryLimitRejectsWrappingCallRanges() +"#]], + ); +}); + forgetest_init!(symbolic_mstore_accepts_constrained_symbolic_offset, |prj, cmd| { if !z3_available() { let _ = sh_eprintln!( @@ -214,6 +575,62 @@ contract SymbolicMsizeAfterWrite { assert!(!stdout.contains("symbolic MSIZE after symbolic memory write"), "{stdout}"); }); +forgetest_init!(symbolic_msize_tracks_read_only_memory_expansion, |prj, cmd| { + skip_unless_z3!("symbolic_msize_tracks_read_only_memory_expansion"); + + prj.add_test( + "SymbolicMsizeAfterRead.t.sol", + r#" +contract SymbolicMsizeAfterRead { + function checkReadOnlyExpansion() public { + uint256 afterHash; + uint256 afterLog; + uint256 afterCopy; + assembly { + pop(keccak256(0x200, 1)) + afterHash := msize() + log0(0x400, 1) + afterLog := msize() + mcopy(0, 0x600, 1) + afterCopy := msize() + } + + assert(afterHash == 0x220); + assert(afterLog == 0x420); + assert(afterCopy == 0x620); + } + + function checkSymbolicReadOnlyExpansion(uint16 offset) public pure { + uint256 afterHash; + assembly { + pop(keccak256(offset, 1)) + afterHash := msize() + } + + assert(afterHash > offset); + } +} +"#, + ); + + cmd.args(["test", "--match-test", "check.*ReadOnlyExpansion"]).assert_success(); + + cmd.forge_fuse(); + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "check.*ReadOnlyExpansion"]) + .assert_success() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +[PASS] checkReadOnlyExpansion() +[PASS] checkSymbolicReadOnlyExpansion(uint16) +"#]], + ); +}); + forgetest_init!(symbolic_msize_respects_zero_symbolic_copy_size, |prj, cmd| { skip_unless_z3!("symbolic_msize_respects_zero_symbolic_copy_size");