From 4b0cb3e397e4b4c93a57a96db83d0b969fb09b4b Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 12 Dec 2018 12:37:40 +0100 Subject: [PATCH] Make calldata compatible with partial abstraction, and add missing features to smt --- mythril/analysis/modules/integer.py | 9 ++++++- mythril/analysis/solver.py | 3 ++- mythril/laser/ethereum/call.py | 4 +++- mythril/laser/ethereum/instructions.py | 7 ++---- mythril/laser/ethereum/keccak.py | 1 + mythril/laser/ethereum/state/calldata.py | 19 +++++++++------ mythril/laser/ethereum/state/memory.py | 20 ++++++++++++---- mythril/laser/ethereum/taint_analysis.py | 1 + mythril/laser/smt/__init__.py | 7 +++++- mythril/laser/smt/bitvec.py | 30 ++++++++++++++++++++++++ mythril/laser/smt/bool.py | 1 + mythril/laser/smt/expression.py | 3 +++ mythril/laser/smt/solver.py | 19 +++++++++++++++ 13 files changed, 103 insertions(+), 21 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 247a78d4..08ce8943 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -5,7 +5,14 @@ from mythril.exceptions import UnsatError from mythril.laser.ethereum.taint_analysis import TaintRunner from mythril.analysis.modules.base import DetectionModule -from mythril.laser.smt import BVAddNoOverflow, BVSubNoUnderflow, BVMulNoOverflow, BitVec, symbol_factory, Not +from mythril.laser.smt import ( + BVAddNoOverflow, + BVSubNoUnderflow, + BVMulNoOverflow, + BitVec, + symbol_factory, + Not, +) import copy import logging diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index a202beb4..c9f685b2 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -115,7 +115,8 @@ def get_transaction_sequence(global_state, constraints): ) concrete_transactions[tx_id]["call_value"] = ( - "0x%x" % model.eval(transaction.call_value.raw, model_completion=True).as_long() + "0x%x" + % model.eval(transaction.call_value.raw, model_completion=True).as_long() ) concrete_transactions[tx_id]["caller"] = "0x" + ( "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long() diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 6a6f71b1..b77b532a 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -60,7 +60,9 @@ def get_call_parameters( def get_callee_address( - global_state: GlobalState, dynamic_loader: DynLoader, symbolic_to_address: Expression + global_state: GlobalState, + dynamic_loader: DynLoader, + symbolic_to_address: Expression, ): """ Gets the address of the callee diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index d4cedb18..458168b7 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -86,9 +86,7 @@ class StateTransition(object): value = global_state.current_transaction.gas_limit.value if value is None: return - global_state.current_transaction.gas_limit = ( - value - ) + global_state.current_transaction.gas_limit = value if ( global_state.mstate.min_gas_used >= global_state.current_transaction.gas_limit @@ -139,7 +137,6 @@ class Instruction: op = "swap" elif self.op_code.startswith("LOG"): op = "log" - print(global_state.get_current_instruction()) instruction_mutator = ( getattr(self, op + "_", None) if not post @@ -1141,7 +1138,7 @@ class Instruction: instr = disassembly.instruction_list[index] - condi = simplify(condition) if isinstance(condition, Bool) else condition != 0 + condi = simplify(condition) if isinstance(condition, Bool) else condition != 0 if instr["opcode"] == "JUMPDEST": if (type(condi) == bool and condi) or ( isinstance(condi, Bool) and not is_false(condi) diff --git a/mythril/laser/ethereum/keccak.py b/mythril/laser/ethereum/keccak.py index 8b5f08b7..862a318f 100644 --- a/mythril/laser/ethereum/keccak.py +++ b/mythril/laser/ethereum/keccak.py @@ -1,5 +1,6 @@ from mythril.laser.smt import Expression + class KeccakFunctionManager: def __init__(self): self.keccak_expression_mapping = {} diff --git a/mythril/laser/ethereum/state/calldata.py b/mythril/laser/ethereum/state/calldata.py index 33ac2437..b52c7579 100644 --- a/mythril/laser/ethereum/state/calldata.py +++ b/mythril/laser/ethereum/state/calldata.py @@ -9,6 +9,7 @@ from mythril.laser.ethereum.util import get_concrete_int from z3 import Model from z3.z3types import Z3Exception + class CalldataType(Enum): CONCRETE = 1 SYMBOLIC = 2 @@ -142,22 +143,26 @@ class SymbolicCalldata(BaseCalldata): Initializes the SymbolicCalldata object :param tx_id: Id of the transaction that the calldata is for. """ - self._size = BitVec(str(tx_id) + "_calldatasize", 256) - self._calldata = Array( - "{}_calldata".format(tx_id), 256, 8 - ) + self._size = symbol_factory.BitVecSym(str(tx_id) + "_calldatasize", 256) + self._calldata = Array("{}_calldata".format(tx_id), 256, 8) super().__init__(tx_id) def _load(self, item: Union[int, Expression]) -> Any: item = symbol_factory.BitVecVal(item, 256) if isinstance(item, int) else item - return simplify(If(item < self._size, simplify(self._calldata[item]), 0)) + return simplify( + If( + item < self._size, + simplify(self._calldata[item]), + symbol_factory.BitVecVal(0, 8), + ) + ) def concrete(self, model: Model) -> list: - concrete_length = get_concrete_int(model.eval(self.size, model_completion=True)) + concrete_length = model.eval(self.size.raw, model_completion=True).as_long() result = [] for i in range(concrete_length): value = self._load(i) - c_value = get_concrete_int(model.eval(value, model_completion=True)) + c_value = model.eval(value.raw, model_completion=True).as_long() result.append(c_value) return result diff --git a/mythril/laser/ethereum/state/memory.py b/mythril/laser/ethereum/state/memory.py index 3fbed554..dd3187f0 100644 --- a/mythril/laser/ethereum/state/memory.py +++ b/mythril/laser/ethereum/state/memory.py @@ -1,6 +1,14 @@ from typing import Union from z3 import Z3Exception -from mythril.laser.smt import BitVec, symbol_factory, If, Concat, simplify, Bool, Extract +from mythril.laser.smt import ( + BitVec, + symbol_factory, + If, + Concat, + simplify, + Bool, + Extract, +) from mythril.laser.ethereum import util @@ -36,9 +44,7 @@ class Memory: assert result.size() == 256 return result - def write_word_at( - self, index: int, value: Union[int, BitVec, bool, Bool] - ) -> None: + def write_word_at(self, index: int, value: Union[int, BitVec, bool, Bool]) -> None: """ Writes a 32 byte word to memory at the specified index` :param index: index to write to @@ -58,7 +64,11 @@ class Memory: self[index : index + 32] = _bytes except (Z3Exception, AttributeError): # BitVector or BoolRef if isinstance(value, Bool): - value_to_write = If(value, symbol_factory.BitVecVal(1, 256), symbol_factory.BitVecVal(0, 256)) + value_to_write = If( + value, + symbol_factory.BitVecVal(1, 256), + symbol_factory.BitVecVal(0, 256), + ) else: value_to_write = value assert value_to_write.size() == 256 diff --git a/mythril/laser/ethereum/taint_analysis.py b/mythril/laser/ethereum/taint_analysis.py index 98aa28aa..7b6d4c08 100644 --- a/mythril/laser/ethereum/taint_analysis.py +++ b/mythril/laser/ethereum/taint_analysis.py @@ -8,6 +8,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState from mythril.analysis.symbolic import SymExecWrapper from mythril.laser.smt import Expression + class TaintRecord: """ TaintRecord contains tainting information for a specific (state, node) diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 0c648e2f..77d09b93 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -8,11 +8,16 @@ from mythril.laser.smt.bitvec import ( URem, SRem, UDiv, + UGE, + Sum, + BVAddNoOverflow, + BVMulNoOverflow, + BVSubNoUnderflow, ) from mythril.laser.smt.expression import Expression, simplify from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not from mythril.laser.smt.array import K, Array, BaseArray -from mythril.laser.smt.solver import Solver +from mythril.laser.smt.solver import Solver, Optimize import z3 diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index 68b19fd6..a0234508 100644 --- a/mythril/laser/smt/bitvec.py +++ b/mythril/laser/smt/bitvec.py @@ -57,6 +57,8 @@ class BitVec(Expression): def __and__(self, other: "BV") -> "BV": """ Create an and expression """ + if not isinstance(other, BitVec): + other = BitVec(z3.BitVecVal(other, 256)) union = self.annotations + other.annotations return BitVec(self.raw & other.raw, annotations=union) @@ -99,6 +101,12 @@ class BitVec(Expression): def If(a: Bool, b: BitVec, c: BitVec): """ Create an if-then-else expression """ + if not isinstance(a, Expression): + a = Bool(z3.BoolVal(a)) + if not isinstance(b, Expression): + b = BitVec(z3.BitVecVal(b, 256)) + if not isinstance(c, Expression): + c = BitVec(z3.BitVecVal(c, 256)) union = a.annotations + b.annotations + c.annotations return BitVec(z3.If(a.raw, b.raw, c.raw), union) @@ -109,6 +117,11 @@ def UGT(a: BitVec, b: BitVec) -> Bool: return Bool(z3.UGT(a.raw, b.raw), annotations) +def UGE(a: BitVec, b:BitVec) -> Bool: + annotations = a.annotations + b.annotations + return Bool(z3.UGE(a.raw, b.raw), annotations) + + def ULT(a: BitVec, b: BitVec) -> Bool: """ Create an unsigned less than expression """ annotations = a.annotations + b.annotations @@ -159,3 +172,20 @@ def Sum(*args) -> BitVec: for bv in args: annotations += bv.annotations return BitVec(nraw, annotations) + + +def BVAddNoOverflow(a: BitVec, b: BitVec, signed: bool) -> Bool: + return Bool(z3.BVAddNoOverflow(a.raw, b.raw, signed)) + + +def BVMulNoOverflow(a: BitVec, b: BitVec, signed: bool) -> Bool: + return Bool(z3.BVMulNoOverflow(a.raw, b.raw, signed)) + + +def BVSubNoUnderflow(a: BitVec, b: BitVec, signed: bool) -> Bool: + if not isinstance(a, Expression): + a = BitVec(z3.BitVecVal(a, 256)) + if not isinstance(b, Expression): + b = BitVec(z3.BitVecVal(b, 256)) + + return Bool(z3.BVSubNoUnderflow(a.raw, b.raw, signed)) diff --git a/mythril/laser/smt/bool.py b/mythril/laser/smt/bool.py index d17ce070..a5c229ab 100644 --- a/mythril/laser/smt/bool.py +++ b/mythril/laser/smt/bool.py @@ -48,6 +48,7 @@ class Bool(Expression): if self.value is not None: return self.value else: + return False raise AttributeError("Can not evalutate symbolic bool value") def Or(a: Bool, b: Bool): diff --git a/mythril/laser/smt/expression.py b/mythril/laser/smt/expression.py index fbf7a812..798b375d 100644 --- a/mythril/laser/smt/expression.py +++ b/mythril/laser/smt/expression.py @@ -26,6 +26,9 @@ class Expression: """ Simplifies this expression """ self.raw = z3.simplify(self.raw) + def __repr__(self): + return self.raw.__repr__() + def simplify(expression: Expression): """ Simplifies the expression """ diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py index 507a6d60..d42e9e60 100644 --- a/mythril/laser/smt/solver.py +++ b/mythril/laser/smt/solver.py @@ -1,5 +1,6 @@ import z3 from mythril.laser.smt.bool import Bool +from mythril.laser.smt.expression import Expression class Solver: @@ -16,11 +17,17 @@ class Solver: def add(self, constraints: list) -> None: """ Adds the constraints to this solver """ + if not isinstance(constraints, list): + self.raw.add(constraints.raw) + return constraints = [c.raw for c in constraints] self.raw.add(constraints) def append(self, constraints: list) -> None: """ Adds the constraints to this solver """ + if not isinstance(constraints, list): + self.raw.append(constraints.raw) + return constraints = [c.raw for c in constraints] self.raw.add(constraints) @@ -35,3 +42,15 @@ class Solver: def pop(self, num) -> None: self.raw.pop(num) + + +class Optimize(Solver): + def __init__(self): + super().__init__() + self.raw = z3.Optimize() + + def minimize(self, element: Expression): + self.raw.minimize(element.raw) + + def maximize(self, element: Expression): + self.raw.maximize(element.raw)