From d2fffde159f67c765392e767bc4208455d95b07a Mon Sep 17 00:00:00 2001 From: Michael Starzinger Date: Mon, 8 Mar 2021 13:39:39 +0100 Subject: [PATCH] feat: implement write syscall in engine (#20) (#109) This commit adds support for the `write` syscall to symbolic execution and rarity simulation. It also changes how invalid addresses passed to `read` and `write` are handled by reporting them as bugs now. --- Cargo.toml | 2 +- examples/echo-line.c | 17 +++++ examples/memory-invalid-read.c | 12 +++ examples/memory-invalid-write.c | 12 +++ examples/memory-uninitialized-write.c | 12 +++ src/engine/rarity_simulation.rs | 104 ++++++++++++++++++++++++-- src/engine/symbolic_execution.rs | 100 +++++++++++++++++++++++-- src/lib.rs | 2 +- tests/engine.rs | 10 ++- 9 files changed, 256 insertions(+), 15 deletions(-) create mode 100644 examples/echo-line.c create mode 100644 examples/memory-invalid-read.c create mode 100644 examples/memory-invalid-write.c create mode 100644 examples/memory-uninitialized-write.c diff --git a/Cargo.toml b/Cargo.toml index fe63c8ab..85c7a697 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "monster-rs" description = "Monster is a symbolic execution engine for 64-bit RISC-U code" -authors = ["Alexander Lackner ", "Alexander Linz ", "Christian Mösl ", "Fabian Nedoluha "] +authors = ["Alexander Lackner ", "Alexander Linz ", "Christian Mösl ", "Fabian Nedoluha ", "Michael Starzinger "] documentation = "https://docs.rs/monster" repository = "https://github.com/cksystemsgroup/monster" homepage = "https://cksystemsgroup.github.io/monster" diff --git a/examples/echo-line.c b/examples/echo-line.c new file mode 100644 index 00000000..7e3eb936 --- /dev/null +++ b/examples/echo-line.c @@ -0,0 +1,17 @@ +uint64_t main() { + uint64_t a; + uint64_t* x; + + a = 16; + x = malloc(8); + + *x = 0; + + while (a) { + read(0, x, 8); + write(1, x, 8); + a = a - 1; + } + + return *x == 23; +} diff --git a/examples/memory-invalid-read.c b/examples/memory-invalid-read.c new file mode 100644 index 00000000..5a09bf11 --- /dev/null +++ b/examples/memory-invalid-read.c @@ -0,0 +1,12 @@ +uint64_t main() { + uint64_t* x; + + x = malloc(8); + + // address out of range + x = x + 268435456 + + read(0, x, 1); + + return 0; +} diff --git a/examples/memory-invalid-write.c b/examples/memory-invalid-write.c new file mode 100644 index 00000000..37d2059a --- /dev/null +++ b/examples/memory-invalid-write.c @@ -0,0 +1,12 @@ +uint64_t main() { + uint64_t* x; + + x = malloc(8); + + // address out of range + x = x + 268435456 + + write(1, x, 1); + + return 0; +} diff --git a/examples/memory-uninitialized-write.c b/examples/memory-uninitialized-write.c new file mode 100644 index 00000000..11eff6e4 --- /dev/null +++ b/examples/memory-uninitialized-write.c @@ -0,0 +1,12 @@ +uint64_t main() { + uint64_t* x; + + x = malloc(16); + + *x = 0; + + // accesses uninitialized memory + write(1, x, 12); + + return 0; +} diff --git a/src/engine/rarity_simulation.rs b/src/engine/rarity_simulation.rs index def66291..d116644f 100644 --- a/src/engine/rarity_simulation.rs +++ b/src/engine/rarity_simulation.rs @@ -466,7 +466,7 @@ impl Executor { fn execute(&mut self, instruction: Instruction) -> Result, RaritySimulationError> { match instruction { - Instruction::Ecall(_) => self.execute_ecall(), + Instruction::Ecall(_) => self.execute_ecall(instruction), Instruction::Lui(utype) => self.execute_lui(utype), Instruction::Addi(itype) => self.execute_itype(instruction, itype, u64::wrapping_add), Instruction::Add(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_add), @@ -557,6 +557,34 @@ impl Executor { } } + fn check_for_valid_memory_range( + &mut self, + instruction: &str, + address: u64, + size: u64, + ) -> Option { + if !self.is_in_vaddr_range(address) || !self.is_in_vaddr_range(address + size) { + trace!( + "{}: buffer {:#x} - {:#x} out of virtual address range (0x0 - {:#x}) => computing reachability", + instruction, + address, + address + size, + self.state.memory.len() * 8, + ); + + self.is_running = false; + + Some(Bug::AccessToOutOfRangeAddress { + info: RarityBugInfo { + inputs: self.concrete_inputs.clone(), + pc: self.state.pc, + }, + }) + } else { + None + } + } + #[allow(clippy::unnecessary_wraps)] fn execute_lui(&mut self, utype: UType) -> Result, RaritySimulationError> { let immediate = u64::from(utype.imm()) << 12; @@ -653,7 +681,7 @@ impl Executor { _ => { let bug = self.access_to_uninitialized_memory(instruction, lhs, rhs); - trace!("could not find input assignment => exeting this context"); + trace!("could not find input assignment => exiting this context"); self.is_running = false; @@ -722,8 +750,9 @@ impl Executor { trace!("read: fd={} buffer={:#x} size={}", 0, buffer, size,); - if !self.is_in_vaddr_range(buffer) || !self.is_in_vaddr_range(buffer + size) { - return not_supported("read syscall failed to"); + let bug = self.check_for_valid_memory_range("read", buffer, size); + if bug.is_some() { + return Ok(bug); } let size_of_u64 = size_of::() as u64; @@ -782,6 +811,63 @@ impl Executor { Ok(None) } + fn execute_write( + &mut self, + instruction: Instruction, + ) -> Result, RaritySimulationError> { + if !matches!(self.state.regs[Register::A0 as usize], Value::Concrete(1)) { + return not_supported("can not handle other fd than stdout in write syscall"); + } + + let buffer = if let Value::Concrete(b) = self.state.regs[Register::A1 as usize] { + b + } else { + return not_supported( + "can not handle symbolic or uninitialized buffer address in write syscall", + ); + }; + + let size = if let Value::Concrete(s) = self.state.regs[Register::A2 as usize] { + s + } else { + return not_supported("can not handle symbolic or uinitialized size in write syscall"); + }; + + trace!("write: fd={} buffer={:#x} size={}", 1, buffer, size,); + + let bug = self.check_for_valid_memory_range("write", buffer, size); + if bug.is_some() { + return Ok(bug); + } + + let size_of_u64 = size_of::() as u64; + let start = buffer / size_of_u64; + let bytes_to_read = size + buffer % size_of_u64; + let words_to_read = (bytes_to_read + size_of_u64 - 1) / size_of_u64; + + for word_count in 0..words_to_read { + if self.state.memory[(start + word_count) as usize] == Value::Uninitialized { + trace!( + "write: access to uninitialized memory at {:#x} => computing reachability", + (start + word_count) * size_of_u64, + ); + + return Ok(Some(Bug::AccessToUnitializedMemory { + info: RarityBugInfo { + inputs: self.concrete_inputs.clone(), + pc: self.state.pc, + }, + instruction, + operands: vec![], + })); + } + } + + self.state.regs[Register::A0 as usize] = Value::Concrete(size); + + Ok(None) + } + #[allow(clippy::unnecessary_wraps)] fn execute_beq(&mut self, btype: BType) -> Result, RaritySimulationError> { let lhs = self.state.regs[btype.rs1() as usize]; @@ -811,7 +897,7 @@ impl Executor { let result = self.access_to_uninitialized_memory(Instruction::Beq(btype), v1, v2); - trace!("access to uninitialized memory => exeting this context"); + trace!("access to uninitialized memory => exiting this context"); Ok(Some(result)) } @@ -845,7 +931,10 @@ impl Executor { } } - fn execute_ecall(&mut self) -> Result, RaritySimulationError> { + fn execute_ecall( + &mut self, + instruction: Instruction, + ) -> Result, RaritySimulationError> { trace!("[{:#010x}] ecall", self.state.pc); let result = match self.state.regs[Register::A7 as usize] { @@ -855,6 +944,9 @@ impl Executor { Value::Concrete(syscall_id) if syscall_id == (SyscallId::Read as u64) => { self.execute_read() } + Value::Concrete(syscall_id) if syscall_id == (SyscallId::Write as u64) => { + self.execute_write(instruction) + } Value::Concrete(syscall_id) if syscall_id == (SyscallId::Exit as u64) => { self.execute_exit() } diff --git a/src/engine/symbolic_execution.rs b/src/engine/symbolic_execution.rs index 00b721bd..6addf3fd 100644 --- a/src/engine/symbolic_execution.rs +++ b/src/engine/symbolic_execution.rs @@ -273,6 +273,31 @@ where } } + fn check_for_valid_memory_range( + &mut self, + instruction: &str, + address: u64, + size: u64, + ) -> Result, SymbolicExecutionError> { + if !self.is_in_vaddr_range(address) || !self.is_in_vaddr_range(address + size) { + trace!( + "{}: buffer {:#x} - {:#x} out of virtual address range (0x0 - {:#x}) => computing reachability", + instruction, + address, + address + size, + self.memory.len() * 8, + ); + + self.is_running = false; + + self.execute_query(Query::Reachable, |info| Bug::AccessToOutOfRangeAddress { + info, + }) + } else { + Ok(None) + } + } + #[allow(clippy::unnecessary_wraps)] fn execute_lui(&mut self, utype: UType) -> Result, SymbolicExecutionError> { let immediate = u64::from(utype.imm()) << 12; @@ -389,7 +414,7 @@ where _ => { let bug = self.check_for_uninitialized_memory(instruction, lhs, rhs)?; - trace!("could not find input assignment => exeting this context"); + trace!("could not find input assignment => exiting this context"); self.is_running = false; @@ -511,8 +536,9 @@ where trace!("read: fd={} buffer={:#x} size={}", 0, buffer, size,); - if !self.is_in_vaddr_range(buffer) || !self.is_in_vaddr_range(buffer + size) { - return not_supported("read syscall failed to"); + let bug = self.check_for_valid_memory_range("read", buffer, size)?; + if bug.is_some() { + return Ok(bug); } let size_of_u64 = size_of::() as u64; @@ -567,6 +593,62 @@ where Ok(None) } + fn execute_write( + &mut self, + instruction: Instruction, + ) -> Result, SymbolicExecutionError> { + if !matches!(self.regs[Register::A0 as usize], Value::Concrete(1)) { + return not_supported("can not handle other fd than stdout in write syscall"); + } + + let buffer = if let Value::Concrete(b) = self.regs[Register::A1 as usize] { + b + } else { + return not_supported( + "can not handle symbolic or uninitialized buffer address in write syscall", + ); + }; + + let size = if let Value::Concrete(s) = self.regs[Register::A2 as usize] { + s + } else { + return not_supported("can not handle symbolic or uinitialized size in write syscall"); + }; + + trace!("write: fd={} buffer={:#x} size={}", 1, buffer, size,); + + let bug = self.check_for_valid_memory_range("write", buffer, size)?; + if bug.is_some() { + return Ok(bug); + } + + let size_of_u64 = size_of::() as u64; + let start = buffer / size_of_u64; + let bytes_to_read = size + buffer % size_of_u64; + let words_to_read = (bytes_to_read + size_of_u64 - 1) / size_of_u64; + + for word_count in 0..words_to_read { + if self.memory[(start + word_count) as usize] == Value::Uninitialized { + trace!( + "write: access to uninitialized memory at {:#x} => computing reachability", + (start + word_count) * size_of_u64, + ); + + return self.execute_query(Query::Reachable, |info| { + Bug::AccessToUnitializedMemory { + info, + instruction, + operands: vec![], + } + }); + } + } + + self.regs[Register::A0 as usize] = Value::Concrete(size); + + Ok(None) + } + fn execute_beq_branches( &mut self, true_branch: u64, @@ -697,7 +779,7 @@ where let result = self.check_for_uninitialized_memory(Instruction::Beq(btype), v1, v2); - trace!("access to uninitialized memory => exeting this context"); + trace!("access to uninitialized memory => exiting this context"); result } @@ -733,7 +815,10 @@ where } } - fn execute_ecall(&mut self) -> Result, SymbolicExecutionError> { + fn execute_ecall( + &mut self, + instruction: Instruction, + ) -> Result, SymbolicExecutionError> { trace!("[{:#010x}] ecall", self.pc); let result = match self.regs[Register::A7 as usize] { @@ -743,6 +828,9 @@ where Value::Concrete(syscall_id) if syscall_id == (SyscallId::Read as u64) => { self.execute_read() } + Value::Concrete(syscall_id) if syscall_id == (SyscallId::Write as u64) => { + self.execute_write(instruction) + } Value::Concrete(syscall_id) if syscall_id == (SyscallId::Exit as u64) => { self.execute_exit() } @@ -903,7 +991,7 @@ where fn execute(&mut self, instruction: Instruction) -> Result, SymbolicExecutionError> { match instruction { - Instruction::Ecall(_) => self.execute_ecall(), + Instruction::Ecall(_) => self.execute_ecall(instruction), Instruction::Lui(utype) => self.execute_lui(utype), Instruction::Addi(itype) => self.execute_itype(instruction, itype, u64::wrapping_add), Instruction::Add(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_add), diff --git a/src/lib.rs b/src/lib.rs index 933da3ba..cc2b67a8 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -23,7 +23,7 @@ pub enum MonsterError { #[error("preprocessing failed with error")] Preprocessing(anyhow::Error), - #[error("symbolic execution stopped with error")] + #[error("symbolic execution stopped with error, {0}")] SymbolicExecution(SymbolicExecutionError), #[error("rarity simulation stopped with error")] diff --git a/tests/engine.rs b/tests/engine.rs index 0ca118bb..dfded3e0 100644 --- a/tests/engine.rs +++ b/tests/engine.rs @@ -13,14 +13,18 @@ use std::{ }; use utils::{compile_riscu, init, with_temp_dir}; -const TEST_FILES: [&str; 15] = [ +const TEST_FILES: [&str; 19] = [ "arithmetic.c", + "echo-line.c", "if-else.c", // needs timeout "invalid-memory-access-2-35.c", "division-by-zero-3-35.c", "simple-assignment-1-35.c", "test-sltu.c", //"memory-access-1-35.c", + "memory-invalid-read.c", + "memory-invalid-write.c", + "memory-uninitialized-write.c", "nested-if-else-reverse-1-35", "nested-recursion-1-35.c", "recursive-ackermann-1-35.c", @@ -172,12 +176,16 @@ fn execute_riscu(source: PathBuf, object: PathBuf, solver: &S) { matches!( (file_name, bug.clone()), ("arithmetic.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) | + ("echo-line.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) | ("invalid-memory-access-2-35.c", SymbolicExecutionBug::AccessToOutOfRangeAddress { .. }) | ("if-else.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) | ("division-by-zero-3-35.c", SymbolicExecutionBug::DivisionByZero { .. }) | ("simple-assignment-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) | ("test-sltu.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) | //("memory-access-1-35.c", Bug:: + ("memory-invalid-read.c", SymbolicExecutionBug::AccessToOutOfRangeAddress { .. }) | + ("memory-invalid-write.c", SymbolicExecutionBug::AccessToOutOfRangeAddress { .. }) | + ("memory-uninitialized-write.c", SymbolicExecutionBug::AccessToUnitializedMemory { .. }) | ("nested-if-else-reverse-1-35", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) | ("nested-recursion-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) | ("recursive-ackermann-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |