Ready to roll

runec/interact.rs

@@ -10,6 +10,22 @@ use libsmt::logics::qf_abv::QF_ABV_Fn;
 use libsmt::backends::z3;
 use console::Console;
 
+const HELP: &'static str = "runec help menu:
+
+Branch Follow Commands:
+  T     Follow `True` branch
+  F     Follow `False` branch
+
+Interpretter Commands:
+  C     Continue Execution
+  S     Single Step Instruction
+  D     Print Debug information
+  ?     Add Assertion
+  Q     Query Constraint Solver
+  X     Add safety assertions
+  H     Print Help Menu
+";
+
 #[derive(Clone, Copy, Debug, PartialEq)]
 pub enum Command {
     FollowTrue,
@@ -18,6 +34,9 @@ pub enum Command {
     Step,
     Debug,
     Assertion,
+    Query,
+    Help,
+    Safety,
     Invalid,
 }
 
@@ -40,6 +59,9 @@ impl From<char> for Command {
             'S' => Command::Step,
             'D' => Command::Debug,
             '?' => Command::Assertion,
+            'Q' => Command::Query,
+            'H' => Command::Help,
+            'X' => Command::Safety,
             _ => Command::Invalid,
         }
     }
@@ -55,11 +77,38 @@ pub struct InteractiveExplorer {
 }
 
 impl InteractiveExplorer {
+    pub fn help(&self) {
+        self.console.print_info(HELP);
+    }
+
+    // Adds Assertions for safety.
+    pub fn safety(&self, ctx: &mut RuneContext) {
+        let rbp = ctx.reg_read("rbp");
+        let const_8 = ctx.define_const(8, 64);
+        let ret_addr = ctx.eval(bitvec::OpCodes::BvAdd, vec![rbp, const_8]);
+        // Add an assertion to check if that memory address can be junk (0x41414141)
+        let const_trash = ctx.define_const(0x41414141, 64);
+        let mem_at_addr = ctx.mem_read(ret_addr, 64);
+        ctx.eval(core::OpCodes::Cmp, vec![mem_at_addr, const_trash]);
+    }
+
     pub fn print_debug(&self, ctx: &RuneContext) {
         self.console.print_info("DEBUG");
         self.console.print_info(&format!("Constraints:\n{}", ctx.solver.generate_asserts()));
     }
 
+    pub fn query_constraints(&self, ctx: &mut RuneContext) {
+        let mut z3: z3::Z3 = Default::default();
+        let result = ctx.solve(&mut z3);
+
+        self.console.print_success("Results:");
+        for (k, v) in &ctx.syms {
+            if let Some(res) = result.get(v) {
+                self.console.print_success(&format!("{} = {:#x}", k, res))
+            }
+        }
+    }
+
     pub fn add_assertion(&self, ctx: &mut RuneContext) {
         self.console.print_info("Adding assertions");
         self.console.print_info("(operation) (register) (register/constant in hex)");
@@ -101,20 +150,8 @@ impl InteractiveExplorer {
                     ctx.reg_read(tokens[2])
                 }
             };
-
             ctx.eval(cmd, vec![op_1, op_2]);
-
-            self.print_debug(ctx);
-
-            let mut z3: z3::Z3 = Default::default();
-            let result = ctx.solve(&mut z3);
-
-            self.console.print_success("Results:");
-            for (k, v) in &ctx.syms {
-                if let Some(res) = result.get(v) {
-                    self.console.print_success(&format!("{} = {:#x}", k, res))
-                }
-            }
+            self.console.print_success("Constraint Added!");
         }
     }
 }
@@ -147,6 +184,18 @@ impl PathExplorer for InteractiveExplorer {
                         self.add_assertion(ctx);
                         continue;
                     }
+                    Command::Query => {
+                        self.query_constraints(ctx);
+                        continue;
+                    }
+                    Command::Help => {
+                        self.help();
+                        continue;
+                    }
+                    Command::Safety => {
+                        self.safety(ctx);
+                        continue;
+                    }
                     _ => {
                         continue;
                     }
@@ -173,12 +222,12 @@ impl PathExplorer for InteractiveExplorer {
         if let Some(cmd) = self.cmd_q.pop() {
             match cmd {
                 Command::FollowTrue => {
-                    let one = ctx.define_const(1, 1);
+                    let one = ctx.define_const(1, 64);
                     ctx.eval(core::OpCodes::Cmp, &[condition, one]);
                     RuneControl::ExploreTrue
                 }
                 Command::FollowFalse => {
-                    let zero = ctx.define_const(0, 1);
+                    let zero = ctx.define_const(0, 64);
                     ctx.eval(core::OpCodes::Cmp, &[condition, zero]);
                     RuneControl::ExploreFalse
                 }

runec/main.rs

@@ -101,7 +101,7 @@ fn main() {
         breakpoints.push(addr);
     }
 
-    let mut ctx = utils::new_ctx(args.flag_start, Some(sym_vars), Some(const_vars));
+    let ctx = utils::new_ctx(args.flag_start, Some(sym_vars), Some(const_vars));
     let mut explorer = InteractiveExplorer::new();
     explorer.bp = breakpoints;
     let mut stream = R2::new(Some(args.arg_file)).expect("Unable to spawn r2");

src/context/context.rs

@@ -31,6 +31,8 @@ pub trait Context: Clone + Debug
     fn solve<S: SMTProc>(&mut self, &mut S) -> HashMap<<Self as RegisterRead>::VarRef, u64>;
 
     fn var_named<T: AsRef<str>>(& self, T) -> Option<<Self as RegisterRead>::VarRef>;
+    fn set_e_old(&mut self, <Self as RegisterRead>::VarRef);
+    fn set_e_cur(&mut self, <Self as RegisterRead>::VarRef);
 }
 
 pub trait RegisterRead: Sized {

src/context/rune_ctx.rs

@@ -181,6 +181,14 @@ impl RuneMemory {
 }
 
 impl Context for RuneContext {
+    fn set_e_old(&mut self, i: NodeIndex) {
+        self.e_old = Some(i);
+    }
+
+    fn set_e_cur(&mut self, i: NodeIndex) {
+        self.e_cur = Some(i);
+    }
+
     fn e_old(&self) -> NodeIndex {
         assert!(self.e_old.is_some(), "e_old accessed before being set!");
         self.e_old.unwrap()

src/engine/rune.rs

@@ -77,7 +77,7 @@ where Ctx: Context<IFn=qf_abv::QF_ABV_Fn>,
             Token::EAddress => {
                 let ip = self.ctx.ip();
                 self.ctx.define_const(ip, 64)
-            },
+            }
             Token::EOld => self.ctx.e_old(),
             Token::ECur => self.ctx.e_cur(),
             Token::ELastsz => self.ctx.define_const(64, 64),
@@ -91,8 +91,7 @@ where Ctx: Context<IFn=qf_abv::QF_ABV_Fn>,
                   lhs: Option<Token>,
                   rhs: Option<Token>,
                   control: &mut RuneControl)
-                  -> EngineResult<Option<<Ctx as RegisterRead>::VarRef>>
-    {
+                  -> EngineResult<Option<<Ctx as RegisterRead>::VarRef>> {
         // Reset previously set `control`
         *control = RuneControl::Continue;
 
@@ -108,9 +107,9 @@ where Ctx: Context<IFn=qf_abv::QF_ABV_Fn>,
         if token.is_arity_zero() {
             return Ok(None);
         }
-        //println!("****");
+        // println!("****");
 
-        //println!("OPERANDS TO {:?}: {:?} {:?}", token, lhs, rhs);
+        // println!("OPERANDS TO {:?}: {:?} {:?}", token, lhs, rhs);
         let l_op = self.process_in(lhs.as_ref()).expect("LHS is ERR");
         let r_op = self.process_in(rhs.as_ref()).expect("RHS is ERR");
         // Since the operator arity us _atleast_ one. assert! that lhs is some.
@@ -129,7 +128,7 @@ where Ctx: Context<IFn=qf_abv::QF_ABV_Fn>,
                             self.ctx.set_ip(const_);
                         }
                     } else {
-                        //println!("REGISTER WRITE: {:?} = {:?}", reg, r_op);
+                        // println!("REGISTER WRITE: {:?} = {:?}", reg, r_op);
                         self.ctx.reg_write(reg, r_op.unwrap());
                     }
                     Ok(None)
@@ -155,14 +154,21 @@ where Ctx: Context<IFn=qf_abv::QF_ABV_Fn>,
                 self.ctx.mem_read(l_op.unwrap(), size as u64)
             }
             Token::ECmp | Token::ELt | Token::EGt => {
-                // This case is a bit different as we want the result to be a bitvector rather than
+                // This case is a bit different as we want the result to be a bitvector rather
+                // than
                 // a bool. Hence we adopt the following stratergy:
                 // (ite (= lhs rhs) (_ bv1 64) (_ bv0 64))
+                // FIXME: Set esil_old and esil_cur
+                let e_cur = self.ctx.eval(bitvec::OpCodes::BvSub,
+                                          vec![l_op.as_ref().unwrap().clone(),
+                                               r_op.as_ref().unwrap().clone()]);
+                self.ctx.set_e_cur(e_cur);
+                self.ctx.set_e_old(l_op.as_ref().unwrap().clone());
                 let const_0 = self.ctx.define_const(0, 64);
                 let const_1 = self.ctx.define_const(1, 64);
                 let eq = self.ctx.eval(token.to_smt(), vec![l_op.unwrap(), r_op.unwrap()]);
                 self.ctx.eval(core::OpCodes::ITE, vec![eq, const_1, const_0])
-            },
+            }
             Token::EPop => unimplemented!(),
             Token::EGoto => unimplemented!(),
             Token::EBreak => unimplemented!(),
@@ -198,7 +204,7 @@ where Ctx: Context<IFn=qf_abv::QF_ABV_Fn>,
         let mut control = RuneControl::Continue;
 
         loop {
-            //println!("{}", self.ctx.ip());
+            // println!("{}", self.ctx.ip());
             let opinfo = if let Some(opinfo_) = self.stream.at(self.ctx.ip()) {
                 opinfo_
             } else {
@@ -212,25 +218,22 @@ where Ctx: Context<IFn=qf_abv::QF_ABV_Fn>,
 
             let esil = opinfo.esil.as_ref().unwrap();
 
-            //println!("{}", esil);
+            // println!("{}", esil);
 
             // Increment ip by instruction width
             let width = opinfo.size.as_ref().unwrap();
             self.ctx.increment_ip(*width);
 
             while let Some(ref token) = p.parse::<_, Tokenizer>(esil) {
-                //println!("{:?}", token);
+                // println!("{:?}", token);
                 // If skip is active, we do not want to modify the esil stack
                 let (lhs, rhs) = if self.skip {
                     (None, None)
                 } else {
                     p.fetch_operands(token)
                 };
 
-                if let Ok(Some(ref res)) = self.process_op(token.clone(),
-                                                           lhs,
-                                                           rhs,
-                                                           &mut control) {
+                if let Ok(Some(ref res)) = self.process_op(token.clone(), lhs, rhs, &mut control) {
                     let rt = self.process_out(res);
                     p.push(rt);
                 }
@@ -240,10 +243,10 @@ where Ctx: Context<IFn=qf_abv::QF_ABV_Fn>,
                 match control {
                     RuneControl::ExploreTrue => {
                         self.skip = false;
-                    },
+                    }
                     RuneControl::ExploreFalse => {
                         self.skip = true;
-                    },
+                    }
                     RuneControl::Continue => continue,
                     _ => break,
                 }