Skip to content

Commit

Permalink
check source map skipping for concolic execution (#193)
Browse files Browse the repository at this point in the history 
* concolic: skip cases based on source map

* add sourcemap for buildjobresult

* add skip concolic

* fix parse build job result srcmap

* add build job result download code

* add skip for concolic host

* fix empty source map

* fix empty source map for some remote cases

* fix merge conflict
  • Loading branch information
@publicqi
publicqi authored Oct 2, 2023
1 parent f8b83a0 commit 6c66a07
Show file tree
Hide file tree
Showing 7 changed files with 301 additions and 30 deletions.
4 changes: 4 additions & 0 deletions cli/src/evm.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -579,6 +579,10 @@ pub fn evm_main(args: EvmArgs) {
selfdestruct_bug: args.selfdestruct_oracle,
arbitrary_external_call: args.arbitrary_external_call_oracle,
builder,
local_files_basedir_pattern: match target_type {
EVMTargetType::Glob => Some(args.target),
_ => None
},
};

match config.fuzzer_type {
Expand Down
82 changes: 64 additions & 18 deletions src/evm/concolic/concolic_host.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ use crate::evm::middlewares::middleware::MiddlewareType::Concolic;
use crate::evm::middlewares::middleware::{add_corpus, Middleware, MiddlewareType};

use crate::evm::host::{FuzzHost, JMP_MAP};
use crate::evm::srcmap::parser::SourceMapLocation;
use crate::generic_vm::vm_executor::MAP_SIZE;
use crate::generic_vm::vm_state::VMStateT;
use crate::input::VMInputT;
Expand Down Expand Up @@ -35,15 +36,13 @@ use z3::{ast::Ast, Config, Context, Params, Solver};
use crate::bv_from_u256;
use crate::evm::concolic::concolic_stage::ConcolicPrioritizationMetadata;
use crate::evm::concolic::expr::{ConcolicOp, Expr, simplify, simplify_concat_select};
use crate::evm::types::{as_u64, EVMAddress, EVMU256, is_zero};
use crate::evm::types::{as_u64, EVMAddress, EVMU256, is_zero, ProjectSourceMapTy};
use crate::evm::blaz::builder::{ArtifactInfoMetadata, BuildJobResult};
use lazy_static::lazy_static;


lazy_static! {
static ref ALREADY_SOLVED: RwLock<HashSet<String>> = RwLock::new(HashSet::new());
}

// 1s
}// 1s
pub static mut CONCOLIC_TIMEOUT : u32 = 1000;

#[derive(Debug, Clone, Serialize, Deserialize)]
Expand Down Expand Up @@ -590,10 +589,12 @@ pub struct ConcolicHost<I, VS> {
pub ctxs: Vec<ConcolicCallCtx>,
// For current PC, the number of times it has been visited
pub phantom: PhantomData<(I, VS)>,

pub source_map: ProjectSourceMapTy
}

impl<I, VS> ConcolicHost<I, VS> {
pub fn new(testcase_ref: Arc<EVMInput>) -> Self {
pub fn new(testcase_ref: Arc<EVMInput>, sourcemap: ProjectSourceMapTy) -> Self {
Self {
symbolic_stack: Vec::new(),
symbolic_memory: SymbolicMemory::new(),
Expand All @@ -603,6 +604,7 @@ impl<I, VS> ConcolicHost<I, VS> {
testcase_ref,
phantom: Default::default(),
ctxs: vec![],
source_map: sourcemap
}
}

Expand Down Expand Up @@ -1200,6 +1202,47 @@ where
as_u64(fast_peek!(0))
};

/*
* Skip rules:
* 1. r"^(library|contract|function)(.|\n)*\}$" // skip library, contract, function
* TODO: 2. global variable signature?
*/

// Get the source map of current pc
let mut need_solve = true;
let pc = interp.program_counter();
let address = interp.contract.address;
// println!("[concolic] address: {:?} pc: {:x}", address, pc);
// println!("input: {:?}", self.input_bytes);
if let Some(Some(srcmap)) = self.source_map.get(&address) {
// println!("source line: {:?}", srcmap.get(&pc).unwrap());
let source_map_loc = if srcmap.get(&pc).is_some() {
srcmap.get(&pc).unwrap()
} else {
&SourceMapLocation {
file: None,
file_idx: None,
offset: 0,
length: 0,
skip_on_concolic :false
}
};
if let Some(_file) = &source_map_loc.file {
if source_map_loc.skip_on_concolic {
need_solve = false;
}
}
else {
// FIXME: This might not hold true for all cases
println!("[concolic] skip solve for None file");
need_solve = false;
}
}
else {
// Is this possible?
// panic!("source line: None");
}

let real_path_constraint = if br {
// path_condition = false
stack_bv!(1).lnot()
Expand All @@ -1208,21 +1251,24 @@ where
stack_bv!(1)
};

if !real_path_constraint.is_concrete() {
let intended_path_constraint = real_path_constraint.clone().lnot();
let constraint_hash = intended_path_constraint.pretty_print_str();
if need_solve {
// println!("[concolic] still need to solve");
if !real_path_constraint.is_concrete() {
let intended_path_constraint = real_path_constraint.clone().lnot();
let constraint_hash = intended_path_constraint.pretty_print_str();

if !ALREADY_SOLVED.read().expect("concolic crashed").contains(&constraint_hash) {
#[cfg(feature = "z3_debug")]
println!("[concolic] to solve {:?}", intended_path_constraint.pretty_print_str());
self.constraints.push(intended_path_constraint);
if !ALREADY_SOLVED.read().expect("concolic crashed").contains(&constraint_hash) {
#[cfg(feature = "z3_debug")]
println!("[concolic] to solve {:?}", intended_path_constraint.pretty_print_str());
self.constraints.push(intended_path_constraint);

solutions.extend(self.solve());
#[cfg(feature = "z3_debug")]
println!("[concolic] Solutions: {:?}", solutions);
self.constraints.pop();
solutions.extend(self.solve());
#[cfg(feature = "z3_debug")]
println!("[concolic] Solutions: {:?}", solutions);
self.constraints.pop();

ALREADY_SOLVED.write().expect("concolic crashed").insert(constraint_hash);
ALREADY_SOLVED.write().expect("concolic crashed").insert(constraint_hash);
}
}
}

Expand Down
11 changes: 8 additions & 3 deletions src/evm/concolic/concolic_stage.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ use serde::{Deserialize, Serialize};
use crate::evm::concolic::concolic_host::{ConcolicHost, Field, Solution};
use crate::evm::input::{ConciseEVMInput, EVMInput, EVMInputT};
use crate::evm::middlewares::middleware::MiddlewareType;
use crate::evm::types::{EVMFuzzExecutor, EVMFuzzState, EVMQueueExecutor};
use crate::evm::types::{EVMFuzzExecutor, EVMFuzzState, EVMQueueExecutor, ProjectSourceMapTy};
use crate::evm::vm::{EVMExecutor, EVMState};
use crate::executor::FuzzExecutor;
use crate::generic_vm::vm_executor::GenericVM;
Expand All @@ -30,6 +30,7 @@ pub struct ConcolicStage<OT> {
pub known_state_input: HashSet<(usize, usize)>,
pub vm_executor: Rc<RefCell<EVMQueueExecutor>>,
pub phantom: std::marker::PhantomData<OT>,
pub sourcemap: ProjectSourceMapTy,
}

impl<OT> UsesState for ConcolicStage<OT> {
Expand All @@ -39,13 +40,16 @@ impl<OT> UsesState for ConcolicStage<OT> {
impl <OT> ConcolicStage<OT> {
pub fn new(enabled: bool,
allow_symbolic_addresses: bool,
vm_executor: Rc<RefCell<EVMQueueExecutor>>) -> Self {
vm_executor: Rc<RefCell<EVMQueueExecutor>>,
source_map: ProjectSourceMapTy,
) -> Self {
Self {
enabled,
allow_symbolic_addresses,
known_state_input: HashSet::new(),
vm_executor,
phantom: std::marker::PhantomData,
sourcemap: source_map,
}
}
}
Expand Down Expand Up @@ -112,7 +116,8 @@ where
vm.host.add_middlewares(
Rc::new(RefCell::new(
ConcolicHost::new(
testcase_ref.clone()
testcase_ref.clone(),
self.sourcemap.clone()
)
))
);
Expand Down
37 changes: 37 additions & 0 deletions src/evm/config.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ use std::cell::RefCell;
use std::collections::HashSet;
use std::fs::File;
use std::rc::Rc;
use std::fmt::{self, Debug};
use crate::evm::blaz::builder::BuildJob;
use crate::evm::blaz::offchain_artifacts::OffChainArtifact;
use crate::evm::blaz::offchain_config::OffchainConfig;
Expand All @@ -19,6 +20,7 @@ pub enum FuzzerTypes {
BASIC,
}

#[derive(Copy, Clone)]
pub enum StorageFetchingMode {
Dump,
All,
Expand Down Expand Up @@ -77,4 +79,39 @@ pub struct Config<VS, Addr, Code, By, Loc, SlotTy, Out, I, S, CI> {
pub selfdestruct_bug: bool,
pub arbitrary_external_call: bool,
pub builder: Option<BuildJob>,
pub local_files_basedir_pattern: Option<String>,
}

impl<VS, Addr, Code, By, Loc, SlotTy, Out, I, S, CI> Debug for Config<VS, Addr, Code, By, Loc, SlotTy, Out, I, S, CI> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
f.debug_struct("Config")
.field("onchain", &self.onchain)
// .field("onchain_storage_fetching", &self.onchain_storage_fetching)
.field("flashloan", &self.flashloan)
.field("concolic", &self.concolic)
.field("concolic_caller", &self.concolic_caller)
// .field("fuzzer_type", &self.fuzzer_type)
.field("contract_loader", &self.contract_loader)
// .field("oracle", &self.oracle)
// .field("producers", &self.producers)
.field("price_oracle", &self.price_oracle)
.field("replay_file", &self.replay_file)
// .field("flashloan_oracle", &self.flashloan_oracle)
.field("selfdestruct_oracle", &self.selfdestruct_oracle)
.field("state_comp_oracle", &self.state_comp_oracle)
.field("state_comp_matching", &self.state_comp_matching)
.field("work_dir", &self.work_dir)
.field("write_relationship", &self.write_relationship)
.field("run_forever", &self.run_forever)
.field("sha3_bypass", &self.sha3_bypass)
.field("base_path", &self.base_path)
.field("echidna_oracle", &self.echidna_oracle)
.field("panic_on_bug", &self.panic_on_bug)
.field("spec_id", &self.spec_id)
.field("only_fuzz", &self.only_fuzz)
.field("typed_bug", &self.typed_bug)
.field("selfdestruct_bug", &self.selfdestruct_bug)
// .field("builder", &self.builder)
.finish()
}
}
Loading

0 comments on commit 6c66a07

Please sign in to comment.