State setup from forge; analyzing "prove" funcs

.gitignore

@@ -17,4 +17,5 @@ Cargo.lock
 
 /log/
 
-.DS_store
+.DS_store
+.vscode

esvm/src/lib.rs

@@ -37,7 +37,7 @@ mod se;
 mod test_helpers;
 
 use std::{
-    collections::HashSet,
+    collections::{HashMap, HashSet},
     fmt,
     iter::FromIterator,
     sync::{Arc, Mutex},
@@ -65,7 +65,7 @@ pub use crate::se::{
 
 use crate::bytecode::Instr;
 
-#[derive(Serialize, Deserialize)]
+#[derive(Serialize, Deserialize, Debug)]
 pub struct AnalysisResult {
     pub address: Address,
     pub blocks: Vec<usize>,
@@ -94,6 +94,44 @@ pub struct TimeoutAnalysis {
     pub timeout: Duration,
 }
 
+//
+pub fn forge_analysis(
+    analyzed_address: String,
+    signatures: Vec<String>,
+    storage_info: HashMap<String, (String, HashMap<String, String>)>,
+) //  -> AnalysisResult {
+{
+    let se_env = SeEnviroment::from_forge(analyzed_address, signatures, storage_info);
+
+    // TODO(baolean): configure a solver and its timeout
+    let pool = Solvers::Yice {
+        count: CONFIG.read().unwrap().cores,
+        timeout: 10_000,
+    };
+    {
+        let mut config = CONFIG.write().unwrap();
+        // Symexec config
+        config.loop_bound = 5;
+        config.call_depth_limit = 5;
+        // Executing "prove_xxx" functions
+        config.message_bound = 1;
+        config.arithmetic_simplification = true;
+        // Using concrete calldatacopy
+        config.concrete_copy = true;
+        config.concrete_load = true;
+    }
+
+    let conf = CONFIG.read().unwrap().clone();
+    let res = symbolic_analysis(se_env, conf, pool);
+
+    for l in format!("{}", res).lines() {
+        println!("{}", l);
+    }
+
+    // TODO(baolean): return results; decode tx data in Foundry
+    // return res;
+}
+
 pub fn symbolic_analysis(se_env: SeEnviroment, config: SeConfig, pool: Solvers) -> AnalysisResult {
     let mut analysis_result = AnalysisResult {
         address: BitVec::as_bigint(&se_env.env.get_account(&se_env.to).addr)
@@ -510,7 +548,7 @@ impl fmt::Display for PrecompiledContracts {
     }
 }
 
-#[derive(Serialize, Deserialize)]
+#[derive(Serialize, Deserialize, Debug)]
 pub struct LoadedAccount {
     pub id: usize,
     pub address: Address,
@@ -569,12 +607,12 @@ impl fmt::Display for LoadedAccount {
         if let Some(ref cov) = self.code_coverage {
             writeln!(f, "Code covered: {:.2}%", 100.0 * cov)?;
         }
-        if !self.initial_storage.is_empty() {
-            writeln!(f, "Initial Storage:")?;
-        }
-        for (addr, value) in &self.initial_storage {
-            writeln!(f, "\t{:x} : {:x}", addr, value)?;
-        }
+        // if !self.initial_storage.is_empty() {
+        //     writeln!(f, "Initial Storage:")?;
+        // }
+        // for (addr, value) in &self.initial_storage {
+        //     writeln!(f, "\t{:x} : {:x}", addr, value)?;
+        // }
         Ok(())
     }
 }

esvm/src/se/env.rs

@@ -124,6 +124,14 @@ fn parse_yaml_value(val: &Yaml) -> BVal {
     }
 }
 
+fn parse_hex_string(s: &String) -> BVal {
+    if s.starts_with("0x") {
+        const_vec(&hexdecode::decode(&s[2..].as_bytes()).unwrap())
+    } else {
+        const_vec(&hexdecode::decode(&s.as_bytes()).unwrap())
+    }
+}
+
 impl SeEnviroment {
     pub fn from_chain(addr: &str) -> Option<Self> {
         if CONFIG.read().unwrap().parity.is_none() {
@@ -251,6 +259,82 @@ impl SeEnviroment {
             memory,
         }
     }
+
+    // Setting up initial state from Foundry's compilation info
+    pub fn from_forge(
+        analyzed_address: String,
+        signatures: Vec<String>,
+        storage_info: HashMap<String, (String, HashMap<String, String>)>,
+    ) -> Self {
+        let mut env = Env::new();
+        let mut memory = symbolic_memory::new_memory();
+        let attacker = env.new_attacker_account(&mut memory);
+        let _hijack = env.new_hijack_account(&mut memory);
+        let mut victim = AccountId(0);
+        let mut id;
+
+        let victim_addr = const_vec(&hexdecode::decode(analyzed_address.as_bytes()).unwrap());
+
+        env.func_selectors = Some(signatures);
+
+        for (addr, info) in storage_info {
+            let account_addr = const_vec(&hexdecode::decode(addr.as_bytes()).unwrap());
+            // TODO: configure the balance
+            let account_balance = const_usize(1000 as usize);
+
+            let name = if account_addr == victim_addr {
+                "victim"
+            } else {
+                "other"
+            };
+
+            let code = hexdecode::decode(info.0.as_bytes()).unwrap();
+            id = env.new_account(
+                &mut memory,
+                &name,
+                &account_addr,
+                Some(code),
+                &account_balance,
+            );
+
+            let mut initial_storage = Vec::new();
+            let mut account = env.get_account_mut(&id);
+            for (addr, val) in info.1 {
+                let addr = parse_hex_string(&addr);
+                let val = parse_hex_string(&val);
+
+                initial_storage.push((
+                    BitVec::as_bigint(&addr).unwrap().into(),
+                    BitVec::as_bigint(&val).unwrap().into(),
+                ));
+
+                account.storage = word_write(&mut memory, account.storage, &addr, &val);
+            }
+
+            account.initial_storage = Some(initial_storage);
+
+            env.get_account_mut(&id).initial_balance =
+                Some(BitVec::as_bigint(&account_balance).unwrap().into());
+
+            // save id
+            let mut loaded_accounts = env.loaded_accounts.unwrap_or_else(Vec::new);
+            loaded_accounts.push(id);
+            env.loaded_accounts = Some(loaded_accounts);
+
+            if account_addr == victim_addr {
+                victim = id;
+            }
+        }
+
+        let memory = Arc::new(memory);
+
+        SeEnviroment {
+            env,
+            from: attacker,
+            to: victim,
+            memory,
+        }
+    }
 }
 
 #[derive(Debug, Hash, Clone, Copy, PartialEq, Eq)]
@@ -321,6 +405,9 @@ pub struct Env {
 
     addresses: HashMap<BVal, AccountId>,
 
+    /// Selectors of functions to be analyzed
+    func_selectors: Option<Vec<String>>,
+
     /// Transactions present in the enviroment
     transactions: HashMap<TxId, Transaction>,
     tx_counter: usize,
@@ -344,6 +431,8 @@ impl Env {
         let accounts = HashMap::new();
         let acc_counter = 0;
 
+        let func_selectors = None;
+
         let transactions = HashMap::new();
         let tx_counter = 0;
         let block = Block::new();
@@ -364,6 +453,7 @@ impl Env {
             accounts,
             transactions,
             acc_counter,
+            func_selectors,
             tx_counter,
             addresses,
             constraints,
@@ -839,6 +929,10 @@ impl Env {
     pub fn get_tx_mut(&mut self, id: &TxId) -> &mut Transaction {
         self.transactions.get_mut(id).unwrap()
     }
+
+    pub fn get_selectors(&self) -> &Option<Vec<String>> {
+        &self.func_selectors
+    }
 }
 
 #[derive(Debug, Clone, PartialEq)]

esvm/src/se/expr/boolector.rs

@@ -64,7 +64,7 @@ impl BoolectorInstance {
         } else if output.contains("sat") {
             true
         } else if output.contains("unknown") {
-            warn!("Solver timed out after {} seconds", self.timeout);
+            println!("Solver timed out after {} seconds", self.timeout);
             false
         } else {
             debug!(

esvm/src/se/expr/yice.rs

@@ -79,7 +79,7 @@ impl YiceInstance {
         } else if output.contains("sat") {
             true
         } else if output.contains("unknown") {
-            warn!("Solver timed out after {} seconds", self.timeout);
+            println!("Solver timed out after {} seconds", self.timeout);
             false
         } else {
             debug!(

esvm/src/se/expr/z3.rs

@@ -241,7 +241,7 @@ impl Z3Instance {
         if res.contains("unknown") {
             if self.warnings {
                 // timeout is specified in miliseconds
-                warn!("Solver timed out after {} seconds.", self.timeout / 1_000);
+                println!("Solver timed out after {} seconds.", self.timeout / 1_000);
                 debug!("{}", self.debug_ouput());
             }
             return false;

esvm/src/se/symbolic_analysis.rs

@@ -218,7 +218,7 @@ pub enum AnalysisMode {
 }
 
 impl AnalysisMode {
-    fn is_exeution(&self) -> bool {
+    fn is_execution(&self) -> bool {
         if let AnalysisMode::Execution = self {
             true
         } else {
@@ -339,7 +339,7 @@ impl Analysis {
     }
 
     pub fn symbolic_round(&mut self) {
-        assert!(self.mode.is_exeution());
+        assert!(self.mode.is_execution());
         self.graph.analyze_graph();
 
         self.end_states = Some(self.graph.end_states());
@@ -348,7 +348,7 @@ impl Analysis {
     pub fn exploration_result(mut self) -> ExplorationResult {
         assert!(self.end_states.is_some());
         let end_states = self.end_states.take().unwrap();
-        info!(
+        println!(
             "Found {} potential attack states, analyzing...",
             end_states.len()
         );
@@ -483,7 +483,7 @@ impl Analysis {
                             result.lock().unwrap().push(attack);
                         }
                     } else {
-                        debug!(
+                        println!(
                             "Found attack, {}, but could not generate tx data!",
                             AttackType::CanChangeOwner
                         );
@@ -492,24 +492,22 @@ impl Analysis {
             }
         }
         if let Some(HaltingReason::Revert) = potential_attack_state.halting_reason {
-            if potential_attack_state.account().assert_fail &&
-                    potential_attack_state.check_sat() {
-
+            if potential_attack_state.account().assert_fail && potential_attack_state.check_sat() {
                 println!("That is an assert failure!");
-            
+
                 if let Some(data) = self.generate_tx_datas(&potential_attack_state) {
                     if self
                         .verify_tx_assert(&potential_attack_state, &data)
                         .is_some()
                     {
-                    let attack = Attack {
-                        txs: data,
-                        attack_type: AttackType::AssertFailed,
+                        let attack = Attack {
+                            txs: data,
+                            attack_type: AttackType::AssertFailed,
                         };
                         result.lock().unwrap().push(attack);
                     }
                 } else {
-                    debug!(
+                    println!(
                         "Found attack, {}, but could not generate tx data!",
                         AttackType::AssertFailed
                     );
@@ -613,7 +611,32 @@ impl Analysis {
                 *victim,
                 *initial_tx,
             ),
-            None => SeState::new(Arc::clone(&context), memory, &env, *victim, *initial_tx),
+            None => {
+                let mut new_state =
+                    SeState::new(Arc::clone(&context), memory, &env, *victim, *initial_tx);
+
+                // Restricting the analysis to "prove_xxx" functions
+                // Loading the calldata from memory
+                let load = mload(&new_state.memory, new_state.input_tx().data, &const256("0"));
+
+                if let Some(selectors) = env.get_selectors() {
+                    let mut constraints: Vec<Arc<FVal>> = vec![];
+                    for s in selectors.iter() {
+                        let prove_selector = const_vec(&hexdecode::decode(s.as_bytes()).unwrap());
+                        // Selecting the first 4 bytes from the calldata
+                        let shiftval = const_u256(U256::from(224));
+                        let shiftop = lshr(&load, &shiftval);
+                        let prove_constraint = eql(&prove_selector, &shiftop);
+                        constraints.push(prove_constraint);
+                    }
+                    // The calldata's selector should be pointing to either of the "prove_xxx" functions
+                    let constraint = constraints
+                        .iter()
+                        .fold(const_u256(U256::from(0)), |acc, x| or(&acc, &x));
+                    new_state.push_constraint(constraint);
+                }
+                new_state
+            }
         };
         SymbolicGraph::new(state)
     }
@@ -696,10 +719,9 @@ impl Analysis {
         }
 
         let evm = self.execute_concrete_evm(state, attack_data)?;
-
         for ins in evm.result.ok()?.trace {
+            // Detecting assert violations in solc >= 0.8
             if let Instruction::Revert { panic, .. } = ins.instruction {
-                info!("the panic code is {:?}", panic);
                 if panic == WU256::from(U256::from(0x01)) {
                     return Some(());
                 }