Skip to content

Commit

Permalink
feat(symbolic): add support for openat system call (#20)
Browse files Browse the repository at this point in the history 
also implement BugFinder interface for symbolic execution engine

closes #20
  • Loading branch information
@ChristianMoesl
ChristianMoesl committed Jun 10, 2021
1 parent ea421d5 commit 424a3f7
Show file tree
Hide file tree
Showing 3 changed files with 174 additions and 61 deletions.
136 changes: 103 additions & 33 deletions src/engine/symbolic_execution.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ use super::{
use crate::{
path_exploration::ExplorationStrategy,
solver::{BVOperator, Solver, SolverError},
BugFinder,
};
use byteorder::{ByteOrder, LittleEndian};
use bytesize::ByteSize;
Expand Down Expand Up @@ -50,6 +51,55 @@ impl Default for SymbolicExecutionOptions {
}
}

pub struct SymbolicExecutionEngine<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
{
options: SymbolicExecutionOptions,
strategy: &'a E,
solver: &'a S,
}

impl<'a, E, S> SymbolicExecutionEngine<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
{
pub fn new(options: &SymbolicExecutionOptions, strategy: &'a E, solver: &'a S) -> Self {
Self {
options: *options,
strategy,
solver,
}
}
}

impl<'a, E, S> BugFinder<SymbolicExecutionBugInfo, SymbolicExecutionError>
for SymbolicExecutionEngine<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
{
fn search_for_bugs(
&self,
program: &Program,
) -> Result<Option<GenericBug<SymbolicExecutionBugInfo>>, SymbolicExecutionError> {
let mut executor =
SymbolicExecutor::new(program, &self.options, self.strategy, self.solver);

let result = executor.run();

match result.expect_err("every run has to stop with an error") {
SymbolicExecutionError::ExecutionDepthReached(_)
| SymbolicExecutionError::ProgramExit(_)
| SymbolicExecutionError::NotReachable => Ok(None),
SymbolicExecutionError::BugFound(bug) => Ok(Some(bug)),
err => Err(err),
}
}
}

#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
pub enum Value {
Concrete(u64),
Expand Down Expand Up @@ -94,7 +144,7 @@ pub enum SymbolicExecutionError {
NotReachable,
}

pub struct SymbolicExecutionEngine<'a, E, S>
pub struct SymbolicExecutor<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
Expand All @@ -107,9 +157,10 @@ where
strategy: &'a E,
options: SymbolicExecutionOptions,
execution_depth: u64,
amount_of_file_descriptors: u64,
}

impl<'a, E, S> SymbolicExecutionEngine<'a, E, S>
impl<'a, E, S> SymbolicExecutor<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
Expand Down Expand Up @@ -170,6 +221,8 @@ where
strategy,
execution_depth: 0,
options: *options,
// stdin (0), stdout (1), stderr (2) are already opened by the system
amount_of_file_descriptors: 3,
}
}

Expand All @@ -195,33 +248,10 @@ where
}
}

pub fn search_for_bugs(&mut self) -> Result<Option<Bug>, SymbolicExecutionError> {
let result = self.run();

match result.expect_err("every run has to stop with an error") {
SymbolicExecutionError::ExecutionDepthReached(_)
| SymbolicExecutionError::ProgramExit(_)
| SymbolicExecutionError::NotReachable => Ok(None),
SymbolicExecutionError::BugFound(bug) => Ok(Some(bug)),
err => Err(err),
}
}

fn execute_query(&mut self, query: Query) -> Result<QueryResult, SymbolicExecutionError> {
self.symbolic_state
.execute_query(query)
.map_err(SymbolicExecutionError::Solver)
// .map_or(Ok(None), |result| {
// match result {
// QueryResult::Sat(witness) => basic_info_to_bug(SymbolicExecutionErrorInfo {
// witness,
// pc: self.pc,
// }),
// QueryResult::UnSat => QueryResult::UnSat,
// }

// Ok(result.map(|witness| {}))
// })
}

fn access_to_uninitialized_memory(
Expand Down Expand Up @@ -368,8 +398,6 @@ where
address
);

// self.is_running = false;

self.execute_query(Query::Reachable).and_then(|r| {
self.exit_anyway_with_bug(r, |i| self.access_to_unaligned_address_bug(i))
})
Expand All @@ -381,8 +409,6 @@ where
self.memory.len() * size_of::<u64>(),
);

// self.is_running = false;

self.execute_query(Query::Reachable).and_then(|r| {
self.exit_anyway_with_bug(r, |i| self.access_to_out_of_range_address_bug(i))
})
Expand All @@ -406,8 +432,6 @@ where
self.memory.len() * size_of::<u64>(),
);

// self.is_running = false;

self.execute_query(Query::Reachable).and_then(|r| {
self.exit_anyway_with_bug(r, |i| self.access_to_out_of_range_address_bug(i))
})
Expand Down Expand Up @@ -624,9 +648,52 @@ where
.create_operator(BVOperator::Add, old_idx, new_idx)
}

fn execute_openat(&mut self) -> Result<(), SymbolicExecutionError> {
// C signature: int openat(int dirfd, const char *pathname, int flags, mode_t mode)

let dirfd = if let Value::Concrete(d) = self.regs[Register::A0 as usize] {
d
} else {
return not_supported("can only handle concrete values for dirfd in openat syscall");
};

let pathname = if let Value::Concrete(p) = self.regs[Register::A1 as usize] {
p
} else {
return not_supported("can only handle concrete values for pathname in openat syscall");
};

let flags = if let Value::Concrete(f) = self.regs[Register::A2 as usize] {
f
} else {
return not_supported("can only handle concrete values for flags in openat syscall");
};

let mode = if let Value::Concrete(m) = self.regs[Register::A3 as usize] {
m
} else {
return not_supported("can only handle concrete values for mode in openat syscall");
};

// TODO: read actual C-string from virtual memory
trace!(
"openat: dirfd={} pathname={} flags={} mode={}",
dirfd,
pathname,
flags,
mode
);

self.regs[Register::A0 as usize] = Value::Concrete(self.amount_of_file_descriptors);

self.amount_of_file_descriptors += 1;

Ok(())
}

fn execute_read(&mut self) -> Result<(), SymbolicExecutionError> {
if !matches!(self.regs[Register::A0 as usize], Value::Concrete(0)) {
return not_supported("can not handle other fd than stdin in read syscall");
return not_supported("can not handle fd other than stdin in read syscall");
}

let buffer = if let Value::Concrete(b) = self.regs[Register::A1 as usize] {
Expand Down Expand Up @@ -703,7 +770,7 @@ where

fn execute_write(&mut self) -> 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");
return not_supported("can not handle fd other than stdout in write syscall");
}

let buffer = if let Value::Concrete(b) = self.regs[Register::A1 as usize] {
Expand Down Expand Up @@ -966,6 +1033,9 @@ where
Value::Concrete(syscall_id) if syscall_id == (SyscallId::Brk as u64) => {
self.execute_brk()
}
Value::Concrete(syscall_id) if syscall_id == (SyscallId::Openat as u64) => {
self.execute_openat()
}
Value::Concrete(syscall_id) if syscall_id == (SyscallId::Read as u64) => {
self.execute_read()
}
Expand Down
6 changes: 2 additions & 4 deletions src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,10 +70,8 @@ where
Strategy: path_exploration::ExplorationStrategy,
Solver: solver::Solver,
{
let mut engine = SymbolicExecutionEngine::new(&program, &options, strategy, solver);

engine
.search_for_bugs()
SymbolicExecutionEngine::new(&options, strategy, solver)
.search_for_bugs(&program)
.map_err(MonsterError::SymbolicExecution)
}

Expand Down
93 changes: 69 additions & 24 deletions tests/engine.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ use std::{
};
use utils::{compile_riscu, init, with_temp_dir};

const TEST_FILES: [&str; 21] = [
const TEST_FILES: [&str; 22] = [
"arithmetic.c",
"echo-line.c",
"if-else.c", // needs timeout
Expand All @@ -23,7 +23,7 @@ const TEST_FILES: [&str; 21] = [
"test-remu.c",
"test-sltu.c",
"test-sltu-2.c",
//"memory-access-1-35.c",
"memory-access-1-35.c",
"memory-invalid-read.c",
"memory-invalid-write.c",
"memory-uninitialized-write.c",
Expand Down Expand Up @@ -175,28 +175,73 @@ fn execute_riscu<S: Solver>(source: PathBuf, object: PathBuf, solver: &S) {
assert!(
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-remu.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("test-sltu.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("test-sltu-2.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 { .. }) |
("recursive-factorial-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("recursive-fibonacci-1-10.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("simple-if-else-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("simple-increasing-loop-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("two-level-nested-loop-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
("multiple-read.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. })
(
"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-remu.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
) | (
"test-sltu.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
) | (
"test-sltu-2.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
) | (
"memory-access-1-35.c",
SymbolicExecutionBug::AccessToUnitializedMemory { .. }
) | (
"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 { .. }
) | (
"recursive-factorial-1-35.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
) | (
"recursive-fibonacci-1-10.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
) | (
"simple-if-else-1-35.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
) | (
"simple-increasing-loop-1-35.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
) | (
"two-level-nested-loop-1-35.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
) | (
"multiple-read.c",
SymbolicExecutionBug::ExitCodeGreaterZero { .. }
)
),
"found right bug type (actual: {}) for {}",
bug,
Expand Down

0 comments on commit 424a3f7

Please sign in to comment.