Skip to content

Commit

Permalink
feat: treat out-of-range accesses as bugs (#20)
Browse files Browse the repository at this point in the history
  • Loading branch information
mstarzinger committed Mar 7, 2021
1 parent 38e8458 commit 23191ac
Show file tree
Hide file tree
Showing 4 changed files with 53 additions and 3 deletions.
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 + 2147483648

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 + 2147483648

write(1, x, 1);

return 0;
}
26 changes: 24 additions & 2 deletions src/engine/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -512,7 +512,18 @@ 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 access buffer");
trace!(
"read: buffer {:#x} - {:#x} out of virtual address range (0x0 - {:#x}) => computing reachability",
buffer,
buffer + size,
self.memory.len() * 8,
);

self.is_running = false;

return self.execute_query(Query::Reachable, |info| Bug::AccessToOutOfRangeAddress {
info,
});
}

let size_of_u64 = size_of::<u64>() as u64;
Expand Down Expand Up @@ -589,7 +600,18 @@ where
trace!("write: fd={} buffer={:#x} size={}", 1, buffer, size,);

if !self.is_in_vaddr_range(buffer) || !self.is_in_vaddr_range(buffer + size) {
return not_supported("write syscall failed to access buffer");
trace!(
"write: buffer {:#x} - {:#x} out of virtual address range (0x0 - {:#x}) => computing reachability",
buffer,
buffer + size,
self.memory.len() * 8,
);

self.is_running = false;

return self.execute_query(Query::Reachable, |info| Bug::AccessToOutOfRangeAddress {
info,
});
}

self.regs[Register::A0 as usize] = Value::Concrete(size);
Expand Down
6 changes: 5 additions & 1 deletion tests/engine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ use std::{
};
use utils::{compile_riscu, init, with_temp_dir};

const TEST_FILES: [&str; 15] = [
const TEST_FILES: [&str; 17] = [
"arithmetic.c",
"echo-line.c",
"if-else.c", // needs timeout
Expand All @@ -24,6 +24,8 @@ const TEST_FILES: [&str; 15] = [
"simple-assignment-1-35.c",
"test-sltu.c",
//"memory-access-1-35.c",
"memory-invalid-read.c",
"memory-invalid-write.c",
"nested-if-else-reverse-1-35",
"nested-recursion-1-35.c",
"recursive-ackermann-1-35.c",
Expand Down Expand Up @@ -182,6 +184,8 @@ fn execute_riscu<S: Solver>(source: PathBuf, object: PathBuf, solver: &S) {
("simple-assignment-1-35.c", Bug::ExitCodeGreaterZero { .. }) |
("test-sltu.c", Bug::ExitCodeGreaterZero { .. }) |
//("memory-access-1-35.c", Bug::
("memory-invalid-read.c", Bug::AccessToOutOfRangeAddress { .. }) |
("memory-invalid-write.c", Bug::AccessToOutOfRangeAddress { .. }) |
("nested-if-else-reverse-1-35", Bug::ExitCodeGreaterZero { .. }) |
("nested-recursion-1-35.c", Bug::ExitCodeGreaterZero { .. }) |
("recursive-ackermann-1-35.c", Bug::ExitCodeGreaterZero { .. }) |
Expand Down

0 comments on commit 23191ac

Please sign in to comment.