Skip to content

Commit

Permalink
feat: implement write syscall in engine (#20) (#109)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
mstarzinger authored Mar 8, 2021
1 parent 6e73284 commit d2fffde
Show file tree
Hide file tree
Showing 9 changed files with 256 additions and 15 deletions.
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
[package]
name = "monster-rs"
description = "Monster is a symbolic execution engine for 64-bit RISC-U code"
authors = ["Alexander Lackner <[email protected]>", "Alexander Linz <[email protected]>", "Christian Mösl <[email protected]>", "Fabian Nedoluha <[email protected]>"]
authors = ["Alexander Lackner <[email protected]>", "Alexander Linz <[email protected]>", "Christian Mösl <[email protected]>", "Fabian Nedoluha <[email protected]>", "Michael Starzinger <[email protected]>"]
documentation = "https://docs.rs/monster"
repository = "https://github.com/cksystemsgroup/monster"
homepage = "https://cksystemsgroup.github.io/monster"
Expand Down
17 changes: 17 additions & 0 deletions examples/echo-line.c
Original file line number Diff line number Diff line change
@@ -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;
}
12 changes: 12 additions & 0 deletions examples/memory-invalid-read.c
Original file line number Diff line number Diff line change
@@ -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;
}
12 changes: 12 additions & 0 deletions examples/memory-invalid-write.c
Original file line number Diff line number Diff line change
@@ -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;
}
12 changes: 12 additions & 0 deletions examples/memory-uninitialized-write.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
uint64_t main() {
uint64_t* x;

x = malloc(16);

*x = 0;

// accesses uninitialized memory
write(1, x, 12);

return 0;
}
104 changes: 98 additions & 6 deletions src/engine/rarity_simulation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -466,7 +466,7 @@ impl Executor {

fn execute(&mut self, instruction: Instruction) -> Result<Option<Bug>, 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),
Expand Down Expand Up @@ -557,6 +557,34 @@ impl Executor {
}
}

fn check_for_valid_memory_range(
&mut self,
instruction: &str,
address: u64,
size: u64,
) -> Option<Bug> {
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<Option<Bug>, RaritySimulationError> {
let immediate = u64::from(utype.imm()) << 12;
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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::<u64>() as u64;
Expand Down Expand Up @@ -782,6 +811,63 @@ impl Executor {
Ok(None)
}

fn execute_write(
&mut self,
instruction: Instruction,
) -> Result<Option<Bug>, 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::<u64>() 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<Option<Bug>, RaritySimulationError> {
let lhs = self.state.regs[btype.rs1() as usize];
Expand Down Expand Up @@ -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))
}
Expand Down Expand Up @@ -845,7 +931,10 @@ impl Executor {
}
}

fn execute_ecall(&mut self) -> Result<Option<Bug>, RaritySimulationError> {
fn execute_ecall(
&mut self,
instruction: Instruction,
) -> Result<Option<Bug>, RaritySimulationError> {
trace!("[{:#010x}] ecall", self.state.pc);

let result = match self.state.regs[Register::A7 as usize] {
Expand All @@ -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()
}
Expand Down
100 changes: 94 additions & 6 deletions src/engine/symbolic_execution.rs
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,31 @@ where
}
}

fn check_for_valid_memory_range(
&mut self,
instruction: &str,
address: u64,
size: u64,
) -> Result<Option<Bug>, 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<Option<Bug>, SymbolicExecutionError> {
let immediate = u64::from(utype.imm()) << 12;
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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::<u64>() as u64;
Expand Down Expand Up @@ -567,6 +593,62 @@ where
Ok(None)
}

fn execute_write(
&mut self,
instruction: Instruction,
) -> Result<Option<Bug>, 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::<u64>() 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,
Expand Down Expand Up @@ -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
}
Expand Down Expand Up @@ -733,7 +815,10 @@ where
}
}

fn execute_ecall(&mut self) -> Result<Option<Bug>, SymbolicExecutionError> {
fn execute_ecall(
&mut self,
instruction: Instruction,
) -> Result<Option<Bug>, SymbolicExecutionError> {
trace!("[{:#010x}] ecall", self.pc);

let result = match self.regs[Register::A7 as usize] {
Expand All @@ -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()
}
Expand Down Expand Up @@ -903,7 +991,7 @@ where

fn execute(&mut self, instruction: Instruction) -> Result<Option<Bug>, 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),
Expand Down
2 changes: 1 addition & 1 deletion src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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")]
Expand Down
Loading

0 comments on commit d2fffde

Please sign in to comment.