Concolic Bug Fix + Z3 Timeout (#217)

* fix concolic dont solve inside loop * skip for already solved constraints * bug fix * fix crash * oops * oops +=1
fuzzland · Oct 1, 2023 · 52110e6 · 52110e6
1 parent b2bbaa3
commit 52110e6
Show file tree

Hide file tree

Showing 4 changed files with 40 additions and 8 deletions.
diff --git a/cli/src/evm.rs b/cli/src/evm.rs
@@ -153,6 +153,10 @@ pub struct EvmArgs {
     #[arg(long, default_value = "false")]
     concolic_caller: bool,
 
+    /// Time limit for concolic execution (ms) (Default: 1000, 0 for no limit)
+    #[arg(long, default_value = "1000")]
+    concolic_timeout: u32,
+
     /// Enable flashloan
     #[arg(short, long, default_value = "false")]
     flashloan: bool,
@@ -532,6 +536,7 @@ pub fn evm_main(args: EvmArgs) {
         onchain,
         concolic: args.concolic,
         concolic_caller: args.concolic_caller,
+        concolic_timeout: args.concolic_timeout,
         oracle: oracles,
         producers,
         flashloan: args.flashloan,

diff --git a/src/evm/concolic/concolic_host.rs b/src/evm/concolic/concolic_host.rs
@@ -43,6 +43,9 @@ lazy_static! {
     static ref ALREADY_SOLVED: RwLock<HashSet<String>> = RwLock::new(HashSet::new());
 }
 
+// 1s
+pub static mut CONCOLIC_TIMEOUT : u32 = 1000;
+
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub enum Field {
     Caller, CallDataValue
@@ -272,11 +275,17 @@ impl<'a> Solving<'a> {
         }
     }
 
-    pub fn solve(&mut self) -> Vec<Solution> {
+    pub fn solve(&mut self, optimistic: bool) -> Vec<Solution> {
         let context = self.context;
         let solver = Solver::new(&context);
         // println!("Constraints: {:?}", self.constraints);
-        for cons in self.constraints {
+        for (nth, cons) in self.constraints.iter().enumerate() {
+
+            // only solve the last constraint
+            if optimistic && nth != self.constraints.len() - 1 {
+                continue;
+            }
+
             let bv = self.generate_z3_bv(&cons.lhs.as_ref().unwrap(), &context);
 
             macro_rules! expect_bv_or_continue {
@@ -331,7 +340,11 @@ impl<'a> Solving<'a> {
 
         // println!("Solver: {:?}", solver);
         let mut p = Params::new(&context);
-        p.set_u32("timeout", 1000);
+
+        if unsafe { CONCOLIC_TIMEOUT > 0 } {
+            p.set_u32("timeout", unsafe { CONCOLIC_TIMEOUT });
+        }
+
         solver.set_params(&p);
         let result = solver.check();
         match result {
@@ -358,8 +371,14 @@ impl<'a> Solving<'a> {
                     fields: self.constrained_field.clone(),
                 }]
             }
-            z3::SatResult::Unsat => vec![],
-            z3::SatResult::Unknown => vec![],
+            z3::SatResult::Unsat | z3::SatResult::Unknown => {
+                if optimistic || self.constraints.len() <= 1 {
+                    return vec![];
+                } else {
+                    // optimistic solving
+                    self.solve(true)
+                }
+            },
         }
     }
 }
@@ -498,7 +517,7 @@ impl SymbolicMemory {
             all_bytes = Box::new(
                 Expr {
                     lhs: Some(all_bytes),
-                    rhs: if let Some(by) = self.memory[idx + i].clone() {
+                    rhs: if self.memory.len() > idx + i && let Some(by) = self.memory[idx + i].clone() {
                         Some(by)
                     } else {
                         Some(Box::new(Expr {
@@ -663,7 +682,7 @@ impl<I, VS> ConcolicHost<I, VS> {
         let balance = BV::new_const(&context, "balance", 256);
 
         let mut solving = Solving::new(&context, &self.input_bytes, &balance, &callvalue, &caller, &self.constraints);
-        solving.solve()
+        solving.solve(false)
     }
 
     pub fn get_input_slice_from_ctx(&self, idx: usize, length: usize) -> Box<Expr> {

diff --git a/src/evm/config.rs b/src/evm/config.rs
@@ -53,6 +53,7 @@ pub struct Config<VS, Addr, Code, By, Loc, SlotTy, Out, I, S, CI> {
     pub flashloan: bool,
     pub concolic: bool,
     pub concolic_caller: bool,
+    pub concolic_timeout: u32,
     pub fuzzer_type: FuzzerTypes,
     pub contract_loader: ContractLoader,
     pub oracle: Vec<Rc<RefCell<dyn Oracle<VS, Addr, Code, By, Loc, SlotTy, Out, I, S, CI>>>>,

diff --git a/src/fuzzers/evm_fuzzer.rs b/src/fuzzers/evm_fuzzer.rs
@@ -44,7 +44,7 @@ use crate::evm::input::{ConciseEVMInput, EVMInput, EVMInputT, EVMInputTy};
 
 use crate::evm::abi::ABIAddressToInstanceMap;
 use crate::evm::blaz::builder::{ArtifactInfoMetadata, BuildJob};
-use crate::evm::concolic::concolic_host::ConcolicHost;
+use crate::evm::concolic::concolic_host::{ConcolicHost, CONCOLIC_TIMEOUT};
 use crate::evm::concolic::concolic_stage::{ConcolicFeedbackWrapper, ConcolicStage};
 use crate::evm::cov_stage::CoverageStage;
 use crate::evm::feedbacks::Sha3WrappedFeedback;
@@ -278,6 +278,13 @@ pub fn evm_fuzzer(
     let mut feedback = MaxMapFeedback::new(&jmp_observer);
     feedback.init_state(state).expect("Failed to init state");
     // let calibration = CalibrationStage::new(&feedback);
+
+    if config.concolic {
+        unsafe {
+            unsafe { CONCOLIC_TIMEOUT = config.concolic_timeout };
+        }
+    }
+
     let concolic_stage = ConcolicStage::new(
         config.concolic,
         config.concolic_caller,