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

[source code]

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!"

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