Skip to content

Commit

Permalink
add docs and fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
aemmitt-ns committed Jun 7, 2023
1 parent be2c7fc commit 4a9c354
Show file tree
Hide file tree
Showing 18 changed files with 313 additions and 184 deletions.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ git clone https://github.com/radareorg/radare2.git
radare2/sys/install.sh
```

Install radius2 with `cargo install radius2` or include radius2 as a dependency using `radius2 = "1.0.19"`
Install radius2 with `cargo install radius2` or include radius2 as a dependency using `radius2 = "1.0.23"`

### Supported Architectures

Expand Down Expand Up @@ -62,7 +62,7 @@ fn main() {
radius2 can also be installed from crates.io and easily included in packages. radius2 also has a CLI tool that can be installed with `cargo install radius2`

```
radius2 1.0.19
radius2 1.0.23
Austin Emmitt (@alkalinesec) <[email protected]>
A symbolic execution tool using r2 and boolector
Expand Down
3 changes: 2 additions & 1 deletion radius/Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
[package]
name = "radius2"
description = "a fast symbolic execution framework using r2"
version = "1.0.22"
version = "1.0.23"
authors = ["aemmitt-ns <[email protected]>"]
license = "MIT"
edition = "2018"
Expand All @@ -16,6 +16,7 @@ serde = { version = "1.0.117", features = ["derive"] }
boolector = "0.4.3"
clap = "2.33.3"
rand = "0.8.4"
colored = "2.0.0"

[features]
default = ["boolector/vendor-lgl"]
Expand Down
4 changes: 2 additions & 2 deletions radius/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ git clone https://github.com/radareorg/radare2.git
radare2/sys/install.sh
```

Install radius2 with `cargo install radius2` or include radius2 as a dependency using `radius2 = "1.0.19"`
Install radius2 with `cargo install radius2` or include radius2 as a dependency using `radius2 = "1.0.23"`

### Supported Architectures

Expand Down Expand Up @@ -62,7 +62,7 @@ fn main() {
radius2 can also be installed from crates.io and easily included in packages. radius2 also has a CLI tool that can be installed with `cargo install radius2`

```
radius2 1.0.19
radius2 1.0.23
Austin Emmitt (@alkalinesec) <[email protected]>
A symbolic execution tool using r2 and boolector
Expand Down
17 changes: 14 additions & 3 deletions radius/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,29 @@ extern crate boolector;
extern crate r2pipe;
extern crate serde_json;

/// Memory used in a program state
pub mod memory;
pub mod operations;
mod operations;
/// Process the IL to execute instructions
pub mod processor;
/// Interact with the radare2 instance
pub mod r2_api;
/// Start symbolic execution for a given binary
pub mod radius;
/// Registers and their values for a given state
pub mod registers;
/// Simulated libc functions and syscalls
pub mod sims;
/// Utilities for using the SMT solver to evaluate symbolic values
pub mod solver;
/// A program state, containing the registers, memory, and solver context
pub mod state;
pub mod test;
mod test;
/// Asbstraction for concrete and symbolic values used during execution
pub mod value;

pub use crate::radius::{Radius, RadiusOption};
pub use crate::registers::Registers;
pub use crate::sims::{Sim, SimMethod};
pub use crate::state::State;
pub use crate::value::{Value, vc};
pub use crate::value::{vc, Value};
62 changes: 40 additions & 22 deletions radius/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ use crate::r2_api::hex_encode;
use crate::radius::{Radius, RadiusOption, RunMode};
use boolector::BV;
use clap::{App, Arg};
use colored::*;
use std::path::Path;
use std::time::Instant;
use std::{fs, process};
Expand All @@ -14,8 +15,8 @@ use std::collections::HashMap;

//use ahash::AHashMap;
//type HashMap<P, Q> = AHashMap<P, Q>;
use std::collections::VecDeque;
use serde::{Deserialize, Serialize};
use std::collections::VecDeque;

pub mod memory;
pub mod operations;
Expand Down Expand Up @@ -44,7 +45,7 @@ macro_rules! collect {
pub struct JsonOutput {
pub symbols: HashMap<String, String>,
pub stdout: String,
pub stderr: String
pub stderr: String,
}

fn main() {
Expand Down Expand Up @@ -608,8 +609,8 @@ fn main() {
};

if is_ref {
let addr = state.memory_alloc(&Value::Concrete(length as u64/8, 0));
state.memory_write_value(&addr, &value, length as usize/8);
let addr = state.memory_alloc(&Value::Concrete(length as u64 / 8, 0));
state.memory_write_value(&addr, &value, length as usize / 8);
value = addr;
length = state.memory.bits as u32;
}
Expand Down Expand Up @@ -651,18 +652,13 @@ fn main() {
}

if let Some(mut end_state) = result {

// collect the ESIL strings to evaluate after running
let constraints: Vec<&str> = collect!(matches, "constrain_after");
for i in 0..matches.occurrences_of("constrain_after") as usize {
let name = constraints[2 * i];
let con = constraints[2 * i + 1];

let cons = if con.starts_with('@') {
&con[1..]
} else {
con
};
let cons = if con.starts_with('@') { &con[1..] } else { con };

if symbol_map.contains_key(name) {
let bv = &symbol_map[name];
Expand All @@ -681,7 +677,9 @@ fn main() {
}
let solve_start = Instant::now();

if !do_json { println!() };
if !do_json {
println!()
};
for symbol in symbol_map.keys() {
let val = Value::Symbolic(end_state.translate(&symbol_map[symbol]).unwrap(), 0);

Expand All @@ -691,49 +689,69 @@ fn main() {
let hex = end_state.solver.hex_solution(&bv).unwrap_or_default();
if !do_json {
if sym_type == "str" && str_opt.is_some() {
println!(" {} : {:?}", symbol, str_opt.unwrap());
println!(" {} : {:?}", symbol.green(), str_opt.unwrap());
} else {
println!(" {} : 0x{}", symbol, hex);
println!(" {} : 0x{}", symbol.green(), hex);
}
} else {
json_out.symbols.insert(symbol.to_owned().to_owned(), hex.to_owned());
json_out
.symbols
.insert(symbol.to_owned().to_owned(), hex.to_owned());
}
} else if !do_json {
println!(" {} : no satisfiable value", symbol);
println!(" {} : no satisfiable value", symbol.red());
} else {
json_out.symbols.insert(symbol.to_owned().to_owned(), "unsat".to_owned());
}
json_out
.symbols
.insert(symbol.to_owned().to_owned(), "unsat".to_owned());
}
}
if !do_json { println!() };
if !do_json {
println!()
};

if profile {
println!("solve time:\t{}", solve_start.elapsed().as_micros());
}

// dump program output
let head = "=".repeat(37);
let foot = "=".repeat(80);
if occurs!(matches, "stdout") {
let out = end_state.dump_file_string(1).unwrap_or_default();
if !do_json {
println!("{}stdout{}\n{}\n{}======{}", head, head, out, head, head);
println!(
"{}stdout{}\n{}\n{}",
head.blue(),
head.blue(),
out,
foot.blue()
);
} else {
json_out.stdout = out;
}
}
if occurs!(matches, "stderr") {
let out = end_state.dump_file_string(2).unwrap_or_default();
if !do_json {
println!("\n{}stderr{}\n{}\n{}======{}", head, head, out, head, head);
println!(
"{}stderr{}\n{}\n{}",
head.red(),
head.red(),
out,
foot.red()
);
} else {
json_out.stderr = out;
}
}
}

if do_json {
println!("{}", serde_json::to_string(&json_out).unwrap_or_default());
}
} else { // TODO this is temporary until I integrate a real testcase gen mode in processor
} else {
// TODO this is temporary until I integrate a real testcase gen mode in processor
let mut pcs: HashMap<u64, usize> = HashMap::new();
let mut states = VecDeque::new();
let mut solutions: HashMap<Vec<u8>, usize> = HashMap::new();
Expand Down
Loading

0 comments on commit 4a9c354

Please sign in to comment.