Seer：Rust 的符号执行引擎

Seer 是 miri 的分支，增加了符号执行的支持，使用 z3 作为求解器后端。

给定一个程序，Seer 尝试枚举通过该程序的所有可能的执行路径。Seer 以 符号 形式表示程序输入，并保持对其的约束集合。当 Seer 达到程序中的分支点时，它将调用其求解器后端来计算在当前约束下哪些分支是可行的。然后，可行的分支被排队以供探索，并增加了从分支条件中学到的新约束。

Seer 将通过 ::std::io::stdin() 读取的任何字节视为符号输入。这意味着一旦 Seer 找到您程序的有意思的输入，您就可以轻松地使用 plain rustc 编译您的程序，并在该输入上运行它。

示例：只给出编码器解码 base64

[源代码]

假设我们被给出一个 base64 编码器函数

fn base64_encode(input: &[u8]) -> String { ... }

假设我们想 解码 一个 base64 编码的字符串，但我们不想麻烦去实际编写相应的 base64_decode() 函数。我们可以编写以下程序，并要求 Seer 执行它

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 将尝试找到可以触发 panic 的输入值。几秒钟后成功

$ 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

这就是我们的答案！我们的字符串解码为 "hello world!"

局限性

Seer 目前处于概念验证阶段，因此存在许多 未实现！() 漏洞。特别是，它尚未处理

• 依赖于符号输入大小的分配
• 符号偏移的指针到指针
• 符号算术的溢出检查
• ... 以及你尝试使用时会很快发现的许多其他事情！

长期愿景

目标是让 Seer 帮助解决两个主要用例

• 在探索性测试中，作为模糊测试的补充方法
• 在程序验证中，彻底检查无法达到错误状态