radius - fast symbolic execution with r2

radius is a rust rewrite of ESILSolve with some architectural improvements. It uses boolector as the SMT solver rather than z3. It executes about 1000x faster than ESILSolve on average. radius gains additional speed over other rust based symbex tools by using u64 primitives for concrete values instead of constant valued bitvectors which incur significant overhead for all operations.

Building

Install radare2 with git clone https://github.com/radareorg/radare2.git radare2/sys/install.sh Then clone and build radius with cargo build --release

Example

```rust use radius2::radius::Radius;

fn main() { let mut radius = Radius::new("tests/r100"); let mut state = radius.callstate(0x004006fd); let addr: u64 = 0x100000; let flagval = state.symbolicvalue("flag", 12*8); state.memory.writevalue(addr, &flagval, 12); state.registers.set("rdi", state.concretevalue(addr, 64));

radius.breakpoint(0x004007a1);
radius.avoid(&[0x00400790]);
let mut new_state = radius.run(state, 1).unwrap();
let flag = new_state.evaluate_string_value(&flag_val).unwrap();
println!("FLAG: {}", flag);
assert_eq!(flag, "Code_Talkers");

} ```

radius CLI tool

radius can also be installed from crates.io and easily included in packages. radius also has a CLI tool that can be installed with cargo install radius2

``` radius2 1.0.6 Austin Emmitt aemmitt@nowsecure.com Symbolic Execution tool using r2 and boolector

USAGE: radius2 [FLAGS] [OPTIONS] --path

FLAGS: -F, --frida Create initial state from frida hook -h, --help Prints help information -z, --lazy Evaluate symbolic PC values lazily --no-sims Do not simulate imports -2, --stderr Show stderr output -0, --stdin Use stdin for target program -1, --stdout Show stdout output --strict Panic on invalid instructions and ESIL -V, --version Prints version information -v, --verbose Show verbose / debugging output

OPTIONS: -a, --address