Seer: Symbolic Execution Engine for Rust
Seer is a fork of miri that adds support for symbolic execution, using z3 as a solver backend.
Given a program written in Rust, Seer attempts to exhaustively enumerate the possible execution paths through it. To achieve this, Seer represents the program's input in a symbolic form, maintaining a set of constraints on it. When Seer reaches a branch point in the program, it invokes its solver backend to compute which continuations are possible given the current constraints. The possible continuations are then enqueued for exploration, augmented with the respective new constraints learned from the branch condition.
Seer considers any bytes read in through ::std::io::stdin() as symbolic input. This means that once Seer finds an interesting input for your program, you can easily compile your program with plain rustc and run it on that input.
example: decode base64 given only an encoder
Suppose we are given a base64 encoder function:
fn base64_encode(input: &[u8]) -> String { ... }
and suppose that we would like to decode a base64-encoded string, but we don't want to bother to actually write the corresponding base64_decode() function. We can write the following program and ask Seer to execute it:
fn main() {
let value_to_decode = "aGVsbG8gd29ybGQh";
let mut data: Vec<u8> = vec![0; (value_to_decode.len() + 3) / 4 * 3];
std::io::stdin().read_exact(&mut data[..]).unwrap();
let result = base64_encode(&data[..]);
if result.starts_with(value_to_decode) {
panic!("we found it!");
}
}
Seer will then attempt to find input values that can trigger the panic. It succeeds after a few seconds:
$ cargo run --bin seer -- example/standalone/base64.rs
Finished dev [unoptimized + debuginfo] target(s) in 0.0 secs
Running `target/debug/seer example/standalone/base64.rs`
ExecutionComplete { input: [104, 101, 108, 108, 111, 32, 119, 111, 114, 108, 100, 33], result: Err(Panic) }
as string: Ok("hello world!")
hit an error. halting
There is our answer! Our string decodes as "hello world!"
using the helper crate
The helper crate provides some extra conveniences. The input that triggers a panic can be split by variable and types that implement Debug are printed in their debug representation instead of using the underlying bytes:
#[macro_use]
extern crate seer_helper;
seer_helper_init!();
#[derive(Debug)]
struct MyStruct {
a: u32,
b: u64,
}
fn main() {
let mut t = MyStruct { a: 0, b: 0 };
seer_helper::mksym(&mut t);
if t.a == 123 && t.b == 321 {
panic!();
}
}
For the formatting to work, it is necessary to build MIR for the standard library, so we will use Xargo:
$ RUSTFLAGS="-Z always-encode-mir" xargo seer
...
ExecutionComplete { input: [stdin: [], t: "MyStruct { a: 123, b: 321 }"], result: Err(NoMirFor("std::sys::unix::fast_thread_local::register_dtor::::__cxa_thread_atexit_impl")) }
hit an error. halting
The full example crate can be found here.
limitations
Seer is currently in the proof-of-concept stage and therefore has lots of unimplemented!() holes in it. In particular, it does not yet handle:
- allocations with size depending on symbolic input
- pointer-to-pointer with symbolic offset
- overflow checking on symbolic arithmetic
- ... lots of other things that you will quickly discover if you try to use it!
long-term vision
The goal is that Seer will help in two primary use cases:
- in exploratory tests, as a complementary approach to fuzzing
- in program verification, to exhaustively check that error states cannot be reached
19 Dec 14, 2022
961 Jan 5, 2023
397 Jan 6, 2023
1.1k Jan 4, 2023
0 Dec 24, 2021
253 Dec 31, 2022
35 Sep 24, 2022
548 Dec 26, 2022
377 Jan 1, 2023
3.6k Dec 30, 2022
427 Dec 24, 2022
26 Dec 4, 2022
43 Dec 17, 2022
1.5k Jan 1, 2023
26 Nov 28, 2022
0 Nov 29, 2022
4 Oct 5, 2022
9 Nov 9, 2022
6 Sep 29, 2022