From 475ad946b8b17a2090a7c4f8b923aaf605e2dd2c Mon Sep 17 00:00:00 2001 From: Nikhil Date: Tue, 27 Aug 2019 19:16:00 +0530 Subject: [PATCH 01/54] Use UIP over BitVecFunc() --- mythril/laser/ethereum/instructions.py | 30 ++-------- .../laser/ethereum/keccak_function_manager.py | 58 +++++++++++++++++++ mythril/laser/ethereum/state/account.py | 33 ++--------- mythril/laser/ethereum/svm.py | 1 - mythril/laser/smt/__init__.py | 1 + mythril/laser/smt/function.py | 25 ++++++++ 6 files changed, 93 insertions(+), 55 deletions(-) create mode 100644 mythril/laser/ethereum/keccak_function_manager.py create mode 100644 mythril/laser/smt/function.py diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 5d2b9e93..b0c63a3c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -31,6 +31,7 @@ from mythril.laser.smt import symbol_factory import mythril.laser.ethereum.util as helper from mythril.laser.ethereum import util +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.call import get_call_parameters, native_call from mythril.laser.ethereum.evm_exceptions import ( VmException, @@ -947,33 +948,10 @@ class Instruction: else: # length is 0; this only matters for input of the BitVecFuncVal data = symbol_factory.BitVecVal(0, 1) - - if data.symbolic: - - annotations = set() # type: Set[Any] - - for b in state.memory[index : index + length]: - if isinstance(b, BitVec): - annotations = annotations.union(b.annotations) - - argument_hash = hash(state.memory[index]) - result = symbol_factory.BitVecFuncSym( - "KECCAC[invhash({})]".format(hash(argument_hash)), - "keccak256", - 256, - input_=data, - annotations=annotations, - ) - log.debug("Created BitVecFunc hash.") - - else: - keccak = utils.sha3(data.value.to_bytes(length, byteorder="big")) - result = symbol_factory.BitVecFuncVal( - util.concrete_int_from_bytes(keccak, 0), "keccak256", 256, input_=data - ) - log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) - + result, constraints = keccak_function_manager.create_keccak(data, length) state.stack.append(result) + state.constraints += constraints + return [global_state] @StateTransition() diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py new file mode 100644 index 00000000..ca7e406b --- /dev/null +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -0,0 +1,58 @@ +from ethereum import utils +from mythril.laser.smt import BitVec, Function, URem, symbol_factory, ULE, And, ULT, Or + +TOTAL_PARTS = 10 ** 40 +PART = (2 ** 256 - 1) // TOTAL_PARTS +INTERVAL_DIFFERENCE = 10 ** 30 + + +class KeccakFunctionManager: + def __init__(self): + self.sizes = {} + self.size_index = {} + self.index_counter = TOTAL_PARTS - 34534 + self.size_values = {} + + def create_keccak(self, data: BitVec, length: int): + length = length * 8 + assert length == data.size() + try: + func, inverse = self.sizes[length] + except KeyError: + func = Function("keccak256_{}".format(length), length, 256) + inverse = Function("keccak256_{}-1".format(length), 256, length) + self.sizes[length] = (func, inverse) + self.size_values[length] = [] + constraints = [] + if data.symbolic is False: + keccak = symbol_factory.BitVecVal( + utils.sha3(data.value.to_bytes(length // 8, byteorder="big")), 256 + ) + constraints.append(func(data) == keccak) + + constraints.append(inverse(func(data)) == data) + if data.symbolic is False: + return func(data), constraints + + constraints.append(URem(func(data), symbol_factory.BitVecVal(63, 256)) == 0) + try: + index = self.size_index[length] + except KeyError: + self.size_index[length] = self.index_counter + index = self.index_counter + self.index_counter -= INTERVAL_DIFFERENCE + + lower_bound = index * PART + upper_bound = (index + 1) * PART + + condition = And( + ULE(symbol_factory.BitVecVal(lower_bound, 256), func(data)), + ULT(func(data), symbol_factory.BitVecVal(upper_bound, 256)), + ) + for val in self.size_values[length]: + condition = Or(condition, func(data) == val) + constraints.append(condition) + return func(data), constraints + + +keccak_function_manager = KeccakFunctionManager() diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index c6afa0c3..6fee240e 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -55,7 +55,6 @@ class Storage: self._standard_storage = K(256, 256, 0) # type: BaseArray else: self._standard_storage = Array("Storage", 256, 256) - self._map_storage = {} # type: Dict[BitVec, BaseArray] self.printable_storage = {} # type: Dict[BitVec, BitVec] @@ -73,11 +72,8 @@ class Storage: return Concat(symbol_factory.BitVecVal(0, 512 - input_.size()), input_) def __getitem__(self, item: BitVec) -> BitVec: - storage, is_keccak_storage = self._get_corresponding_storage(item) - if is_keccak_storage: - sanitized_item = self._sanitize(cast(BitVecFunc, item).input_) - else: - sanitized_item = item + storage = self._standard_storage + sanitized_item = item if ( self.address and self.address.value != 0 @@ -100,7 +96,6 @@ class Storage: self.printable_storage[item] = storage[sanitized_item] except ValueError as e: log.debug("Couldn't read storage at %s: %s", item, e) - return simplify(storage[sanitized_item]) @staticmethod @@ -114,29 +109,12 @@ class Storage: index = Extract(255, 0, key.input_) return simplify(index) - def _get_corresponding_storage(self, key: BitVec) -> Tuple[BaseArray, bool]: - index = self.get_map_index(key) - if index is None: - storage = self._standard_storage - is_keccak_storage = False - else: - storage_map = self._map_storage - try: - storage = storage_map[index] - except KeyError: - if isinstance(self._standard_storage, Array): - storage_map[index] = Array("Storage", 512, 256) - else: - storage_map[index] = K(512, 256, 0) - storage = storage_map[index] - is_keccak_storage = True - return storage, is_keccak_storage + def _get_corresponding_storage(self, key: BitVec) -> BaseArray: + return self._standard_storage def __setitem__(self, key, value: Any) -> None: - storage, is_keccak_storage = self._get_corresponding_storage(key) + storage = self._get_corresponding_storage(key) self.printable_storage[key] = value - if is_keccak_storage: - key = self._sanitize(key.input_) storage[key] = value if key.symbolic is False: self.storage_keys_loaded.add(int(key.value)) @@ -147,7 +125,6 @@ class Storage: concrete=concrete, address=self.address, dynamic_loader=self.dynld ) storage._standard_storage = deepcopy(self._standard_storage) - storage._map_storage = deepcopy(self._map_storage) storage.printable_storage = copy(self.printable_storage) storage.storage_keys_loaded = copy(self.storage_keys_loaded) return storage diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 88b362c8..21e4c682 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -241,7 +241,6 @@ class LaserEVM: except NotImplementedError: log.debug("Encountered unimplemented instruction") continue - new_states = [ state for state in new_states if state.mstate.constraints.is_possible ] diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 6ab752ce..b0793562 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -22,6 +22,7 @@ from mythril.laser.smt.bitvecfunc import BitVecFunc from mythril.laser.smt.expression import Expression, simplify from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not, And from mythril.laser.smt.array import K, Array, BaseArray +from mythril.laser.smt.function import Function from mythril.laser.smt.solver import Solver, Optimize, SolverStatistics from mythril.laser.smt.model import Model from mythril.laser.smt.bool import Bool as SMTBool diff --git a/mythril/laser/smt/function.py b/mythril/laser/smt/function.py new file mode 100644 index 00000000..93115c88 --- /dev/null +++ b/mythril/laser/smt/function.py @@ -0,0 +1,25 @@ +from typing import cast +import z3 + +from mythril.laser.smt.bitvec import BitVec + + +class Function: + """An uninterpreted function.""" + + def __init__(self, name: str, domain: int, value_range: int): + """Initializes an uninterpreted function. + + :param name: Name of the Function + :param domain: The domain for the Function (10 -> all the values that a bv of size 10 could take) + :param value_range: The range for the values of the function (10 -> all the values that a bv of size 10 could take) + """ + self.domain = z3.BitVecSort(domain) + self.range = z3.BitVecSort(value_range) + self.raw = z3.Function(name, self.domain, self.range) + + def __call__(self, item: BitVec) -> BitVec: + """Function accessor, item can be symbolic.""" + return BitVec( + cast(z3.BitVecRef, self.raw(item.raw)), annotations=item.annotations + ) # type: ignore From f4dd64a60b6cf2d845ec39e4da7ebf8cd7e5dd29 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 28 Aug 2019 18:17:50 +0530 Subject: [PATCH 02/54] Make the keccak spread accross --- mythril/laser/ethereum/keccak_function_manager.py | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index ca7e406b..41fb7fad 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -26,15 +26,18 @@ class KeccakFunctionManager: constraints = [] if data.symbolic is False: keccak = symbol_factory.BitVecVal( - utils.sha3(data.value.to_bytes(length // 8, byteorder="big")), 256 + int.from_bytes( + utils.sha3(data.value.to_bytes(length // 8, byteorder="big")), "big" + ), + 256, ) + self.size_values[length].append(keccak) constraints.append(func(data) == keccak) constraints.append(inverse(func(data)) == data) if data.symbolic is False: return func(data), constraints - constraints.append(URem(func(data), symbol_factory.BitVecVal(63, 256)) == 0) try: index = self.size_index[length] except KeyError: @@ -48,9 +51,11 @@ class KeccakFunctionManager: condition = And( ULE(symbol_factory.BitVecVal(lower_bound, 256), func(data)), ULT(func(data), symbol_factory.BitVecVal(upper_bound, 256)), + URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) for val in self.size_values[length]: condition = Or(condition, func(data) == val) + constraints.append(condition) return func(data), constraints From b4e57b67e4d85ba901ca50ef7e93232550026125 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 4 Sep 2019 15:33:36 +0530 Subject: [PATCH 03/54] Add concretisation --- mythril/laser/ethereum/instructions.py | 3 + .../laser/ethereum/keccak_function_manager.py | 46 +++++++++-- mythril/laser/ethereum/svm.py | 77 ++++++++++++++++++- 3 files changed, 117 insertions(+), 9 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b0c63a3c..edec167e 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1372,6 +1372,9 @@ class Instruction: state = global_state.mstate index = state.stack.pop() state.stack.append(global_state.environment.active_account.storage[index]) + if global_state.get_current_instruction()["address"] == 447: + print(index) + return [global_state] @StateTransition() diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 41fb7fad..fc56206b 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -1,5 +1,17 @@ +from random import randint + from ethereum import utils -from mythril.laser.smt import BitVec, Function, URem, symbol_factory, ULE, And, ULT, Or +from mythril.laser.smt import ( + BitVec, + Function, + URem, + symbol_factory, + ULE, + And, + ULT, + Or, + simplify, +) TOTAL_PARTS = 10 ** 40 PART = (2 ** 256 - 1) // TOTAL_PARTS @@ -11,10 +23,21 @@ class KeccakFunctionManager: self.sizes = {} self.size_index = {} self.index_counter = TOTAL_PARTS - 34534 + self.concrete_dict = {} self.size_values = {} + def find_keccak(self, data: BitVec) -> BitVec: + return symbol_factory.BitVecVal( + int.from_bytes( + utils.sha3(data.value.to_bytes(data.size() // 8, byteorder="big")), + "big", + ), + 256, + ) + def create_keccak(self, data: BitVec, length: int): length = length * 8 + data = simplify(data) assert length == data.size() try: func, inverse = self.sizes[length] @@ -25,12 +48,7 @@ class KeccakFunctionManager: self.size_values[length] = [] constraints = [] if data.symbolic is False: - keccak = symbol_factory.BitVecVal( - int.from_bytes( - utils.sha3(data.value.to_bytes(length // 8, byteorder="big")), "big" - ), - 256, - ) + keccak = self.find_keccak(data) self.size_values[length].append(keccak) constraints.append(func(data) == keccak) @@ -53,6 +71,20 @@ class KeccakFunctionManager: ULT(func(data), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) + condition = False + try: + concrete_input = self.concrete_dict[data] + keccak = self.find_keccak(concrete_input) + except KeyError: + concrete_input = symbol_factory.BitVecVal( + randint(0, 2 ** data.size() - 1), data.size() + ) + self.concrete_dict[data] = concrete_input + keccak = self.find_keccak(concrete_input) + self.concrete_dict[func(data)] = keccak + + condition = Or(condition, And(data == concrete_input, keccak == func(data))) + for val in self.size_values[length]: condition = Or(condition, func(data) == val) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 21e4c682..a6994ee2 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -3,7 +3,7 @@ import logging from collections import defaultdict from copy import copy from datetime import datetime, timedelta -from typing import Callable, Dict, DefaultDict, List, Tuple, Optional +from typing import Callable, Dict, DefaultDict, List, Tuple, Union, Optional from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.evm_exceptions import StackUnderflowException @@ -16,6 +16,8 @@ from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy from abc import ABCMeta from mythril.laser.ethereum.time_handler import time_handler +from mythril.analysis.solver import get_model, UnsatError + from mythril.laser.ethereum.transaction import ( ContractCreationTransaction, TransactionEndSignal, @@ -23,7 +25,21 @@ from mythril.laser.ethereum.transaction import ( execute_contract_creation, execute_message_call, ) -from mythril.laser.smt import symbol_factory +from mythril.laser.smt import ( + symbol_factory, + And, + BitVecFunc, + BitVec, + Extract, + simplify, + is_true, +) + +ACTOR_ADDRESSES = [ + symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256), + symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256), + symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEE, 256), +] log = logging.getLogger(__name__) @@ -359,6 +375,63 @@ class LaserEVM: return new_global_states, op_code + def concretize_ite_storage(self, global_state): + sender = global_state.environment.sender + models_tuple = [] + sat = False + + import random, sha3 + + calldata_cond = True + for account in global_state.world_state.accounts.values(): + for key in account.storage.storage_keys_loaded: + if ( + isinstance(key, BitVecFunc) + and not isinstance(key.input_, BitVecFunc) + and isinstance(key.input_, BitVec) + and key.input_.symbolic + and key.input_.size() == 512 + and key.input_.get_extracted_input_cond(511, 256) is False + ): + pseudo_input = random.randint(0, 2 ** 160 - 1) + hex_v = hex(pseudo_input)[2:] + if len(hex_v) % 2 == 1: + hex_v += "0" + hash_val = symbol_factory.BitVecVal( + int(sha3.keccak_256(bytes.fromhex(hex_v)).hexdigest(), 16), 256 + ) + pseudo_input = symbol_factory.BitVecVal(pseudo_input, 256) + calldata_cond = And( + calldata_cond, + Extract(511, 256, key.input_) == hash_val, + Extract(511, 256, key.input_).potential_input == pseudo_input, + ) + key.input_.set_extracted_input_cond(511, 256, calldata_cond) + assert ( + key.input_.get_extracted_input_cond(511, 256) == calldata_cond + ) + + for actor in ACTOR_ADDRESSES: + try: + models_tuple.append( + ( + get_model( + constraints=global_state.mstate.constraints + + [sender == actor, calldata_cond] + ), + And(calldata_cond, sender == actor), + ) + ) + sat = True + except UnsatError: + models_tuple.append((None, And(calldata_cond, sender == actor))) + + if not sat: + return [False] + + for account in global_state.world_state.accounts.values(): + account.storage.concretize(models_tuple) + def _end_message_call( self, return_global_state: GlobalState, From c7d819b48805ff2aafcbc216a2e6cca2101cb00c Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 9 Sep 2019 17:20:08 +0530 Subject: [PATCH 04/54] Remove constraints --- mythril/analysis/solver.py | 9 +- .../laser/ethereum/keccak_function_manager.py | 48 ++++--- mythril/laser/ethereum/state/constraints.py | 1 + mythril/laser/ethereum/svm.py | 117 +++++++++++------- mythril/laser/smt/solver/solver.py | 3 + 5 files changed, 109 insertions(+), 69 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index b6959a82..80ba7229 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -20,7 +20,7 @@ log = logging.getLogger(__name__) # LRU cache works great when used in powers of 2 @lru_cache(maxsize=2 ** 23) -def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True): +def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True, weighted=()): """ :param constraints: @@ -48,7 +48,8 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True s.minimize(e) for e in maximize: s.maximize(e) - + for e in weighted: + s.add_soft(e) result = s.check() if result == sat: return s.model() @@ -97,9 +98,9 @@ def get_transaction_sequence( tx_constraints, minimize = _set_minimisation_constraints( transaction_sequence, constraints.copy(), [], 5000, global_state.world_state ) - + weighted = tx_constraints.weighted try: - model = get_model(tx_constraints, minimize=minimize) + model = get_model(tx_constraints, minimize=minimize, weighted=tuple(weighted)) except UnsatError: raise UnsatError diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index fc56206b..d6098c08 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -11,6 +11,7 @@ from mythril.laser.smt import ( ULT, Or, simplify, + Extract, ) TOTAL_PARTS = 10 ** 40 @@ -23,35 +24,61 @@ class KeccakFunctionManager: self.sizes = {} self.size_index = {} self.index_counter = TOTAL_PARTS - 34534 - self.concrete_dict = {} + self.topo_keys = [] + self.keccak_parent = {} self.size_values = {} + self.keccak_vals = {} + self.delete_constraints = [] def find_keccak(self, data: BitVec) -> BitVec: - return symbol_factory.BitVecVal( + keccak = symbol_factory.BitVecVal( int.from_bytes( utils.sha3(data.value.to_bytes(data.size() // 8, byteorder="big")), "big", ), 256, ) + func, _ = self.sizes[data.size()] + self.keccak_vals[func(data)] = keccak + return keccak def create_keccak(self, data: BitVec, length: int): length = length * 8 data = simplify(data) + if data.symbolic and data not in self.topo_keys: + if data.size() != 512: + self.keccak_parent[data] = None + self.topo_keys.append(data) + else: + p1 = simplify(Extract(511, 256, data)) + if p1.symbolic and p1 not in self.topo_keys: + self.topo_keys.append(p1) + self.keccak_parent[p1] = None + assert length == data.size() + constraints = [] try: func, inverse = self.sizes[length] except KeyError: func = Function("keccak256_{}".format(length), length, 256) inverse = Function("keccak256_{}-1".format(length), 256, length) self.sizes[length] = (func, inverse) + + keccak_0 = self.find_keccak(symbol_factory.BitVecVal(0, data.size())) + constraints.append( + func(symbol_factory.BitVecVal(0, data.size())) == keccak_0 + ) + self.size_values[length] = [] - constraints = [] + if data.symbolic is False: keccak = self.find_keccak(data) self.size_values[length].append(keccak) constraints.append(func(data) == keccak) + if data.symbolic and simplify(func(data)) not in self.topo_keys: + self.keccak_parent[simplify(func(data))] = data + self.topo_keys.append(func(data)) constraints.append(inverse(func(data)) == data) if data.symbolic is False: return func(data), constraints @@ -71,23 +98,10 @@ class KeccakFunctionManager: ULT(func(data), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) - condition = False - try: - concrete_input = self.concrete_dict[data] - keccak = self.find_keccak(concrete_input) - except KeyError: - concrete_input = symbol_factory.BitVecVal( - randint(0, 2 ** data.size() - 1), data.size() - ) - self.concrete_dict[data] = concrete_input - keccak = self.find_keccak(concrete_input) - self.concrete_dict[func(data)] = keccak - - condition = Or(condition, And(data == concrete_input, keccak == func(data))) for val in self.size_values[length]: condition = Or(condition, func(data) == val) - + self.delete_constraints.append(condition) constraints.append(condition) return func(data), constraints diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 1f675ca5..181a1393 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -29,6 +29,7 @@ class Constraints(list): super(Constraints, self).__init__(constraint_list) self._default_timeout = 100 self._is_possible = is_possible + self.weighted = [] @property def is_possible(self) -> bool: diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index a6994ee2..864d6af2 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -4,12 +4,14 @@ from collections import defaultdict from copy import copy from datetime import datetime, timedelta from typing import Callable, Dict, DefaultDict, List, Tuple, Union, Optional +import z3 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.evm_exceptions import StackUnderflowException from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.iprof import InstructionProfiler +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState @@ -28,11 +30,13 @@ from mythril.laser.ethereum.transaction import ( from mythril.laser.smt import ( symbol_factory, And, + Or, BitVecFunc, BitVec, Extract, simplify, is_true, + Concat, ) ACTOR_ADDRESSES = [ @@ -357,7 +361,10 @@ class LaserEVM: not isinstance(transaction, ContractCreationTransaction) or transaction.return_data ) and not end_signal.revert: + constraints = self.concretize_keccak(end_signal.global_state) end_signal.global_state.world_state.node = global_state.node + end_signal.global_state.world_state.node.constraints.append(constraints) + end_signal.global_state.world_state.node.constraints.weighted.append(constraints) self._add_world_state(end_signal.global_state) new_global_states = [] else: @@ -375,62 +382,76 @@ class LaserEVM: return new_global_states, op_code - def concretize_ite_storage(self, global_state): + def concretize_keccak(self, global_state): sender = global_state.environment.sender - models_tuple = [] - sat = False - - import random, sha3 - - calldata_cond = True - for account in global_state.world_state.accounts.values(): - for key in account.storage.storage_keys_loaded: - if ( - isinstance(key, BitVecFunc) - and not isinstance(key.input_, BitVecFunc) - and isinstance(key.input_, BitVec) - and key.input_.symbolic - and key.input_.size() == 512 - and key.input_.get_extracted_input_cond(511, 256) is False - ): - pseudo_input = random.randint(0, 2 ** 160 - 1) - hex_v = hex(pseudo_input)[2:] - if len(hex_v) % 2 == 1: - hex_v += "0" - hash_val = symbol_factory.BitVecVal( - int(sha3.keccak_256(bytes.fromhex(hex_v)).hexdigest(), 16), 256 - ) - pseudo_input = symbol_factory.BitVecVal(pseudo_input, 256) - calldata_cond = And( - calldata_cond, - Extract(511, 256, key.input_) == hash_val, - Extract(511, 256, key.input_).potential_input == pseudo_input, - ) - key.input_.set_extracted_input_cond(511, 256, calldata_cond) - assert ( - key.input_.get_extracted_input_cond(511, 256) == calldata_cond - ) - + model_tuples = [] for actor in ACTOR_ADDRESSES: try: - models_tuple.append( - ( + model_tuples.append( + [ get_model( constraints=global_state.mstate.constraints - + [sender == actor, calldata_cond] + + [sender == actor] ), - And(calldata_cond, sender == actor), - ) + And(sender == actor), + actor, + ] ) - sat = True except UnsatError: - models_tuple.append((None, And(calldata_cond, sender == actor))) - - if not sat: - return [False] - - for account in global_state.world_state.accounts.values(): - account.storage.concretize(models_tuple) + model_tuples.append((None, False, actor)) + from random import randint + + stored_vals = {} + for key in keccak_function_manager.topo_keys: + if keccak_function_manager.keccak_parent[key] is None: + for model_tuple in model_tuples: + if model_tuple[0] is None: + continue + + concrete_val_i = model_tuple[0].eval(key.raw, model_completion=True) + try: + concrete_val_i = BitVec(concrete_val_i) + except AttributeError: + val = randint(0, 2 ** key.size() - 1) + concrete_val_i = symbol_factory.BitVecVal(val, key.size()) + + model_tuple[1] = And(model_tuple[1], key == concrete_val_i) + if key not in stored_vals: + stored_vals[key] = {} + stored_vals[key][model_tuple[2]] = concrete_val_i + else: + parent = keccak_function_manager.keccak_parent[key] + if parent.size() == 512: + parent1 = simplify(Extract(511, 256, parent)) + parent2 = simplify(Extract(255, 0, parent)) + for model_tuple in model_tuples: + if model_tuple[0] is None: + continue + if parent.size() == 512: + concrete_parent1 = model_tuple[0].eval(parent1.raw, model_completion=True) + if concrete_parent1 is None: + concrete_parent1 = stored_vals[parent1][model_tuple[2]] + if not isinstance(concrete_parent1, BitVec): + concrete_parent1 = BitVec(concrete_parent1) + concrete_parent = Concat(concrete_parent1, parent2) + else: + concrete_parent = model_tuple[0].eval(parent.raw, model_completion=True) + if concrete_parent is None: + concrete_parent = stored_vals[parent][model_tuple[2]] + concrete_parent = BitVec(concrete_parent) + keccak_val = keccak_function_manager.find_keccak(concrete_parent) + model_tuple[1] = And(model_tuple[1], key == keccak_val) + new_condition = False + z3.set_option(max_args=10000000, max_lines=100000000, max_depth=10000000, max_visited=1000000) + for model_tuple in model_tuples: + new_condition = Or(model_tuple[1], new_condition) + new_condition = simplify(new_condition) + try: + get_model(constraints=global_state.mstate.constraints + [new_condition]) + except UnsatError: + print("SHIT", new_condition, "SHIT_ENDS") + keccak_function_manager.topo_keys = [] + return new_condition def _end_message_call( self, diff --git a/mythril/laser/smt/solver/solver.py b/mythril/laser/smt/solver/solver.py index 2f3d4ac1..4ab7f043 100644 --- a/mythril/laser/smt/solver/solver.py +++ b/mythril/laser/smt/solver/solver.py @@ -103,3 +103,6 @@ class Optimize(BaseSolver[z3.Optimize]): :param element: """ self.raw.maximize(element.raw) + + def add_soft(self, element): + self.raw.add_soft(element.raw) From 6b10d9809b38652a498fdb74912dc13f1c14054d Mon Sep 17 00:00:00 2001 From: Nikhil Date: Thu, 12 Sep 2019 17:27:41 +0530 Subject: [PATCH 05/54] Save status --- mythril/laser/ethereum/instructions.py | 3 - .../laser/ethereum/keccak_function_manager.py | 9 +-- mythril/laser/ethereum/state/constraints.py | 11 ++- mythril/laser/ethereum/svm.py | 76 ++++++++++++------- 4 files changed, 60 insertions(+), 39 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index edec167e..b0c63a3c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1372,9 +1372,6 @@ class Instruction: state = global_state.mstate index = state.stack.pop() state.stack.append(global_state.environment.active_account.storage[index]) - if global_state.get_current_instruction()["address"] == 447: - print(index) - return [global_state] @StateTransition() diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index d6098c08..9f9d3767 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -63,12 +63,6 @@ class KeccakFunctionManager: func = Function("keccak256_{}".format(length), length, 256) inverse = Function("keccak256_{}-1".format(length), 256, length) self.sizes[length] = (func, inverse) - - keccak_0 = self.find_keccak(symbol_factory.BitVecVal(0, data.size())) - constraints.append( - func(symbol_factory.BitVecVal(0, data.size())) == keccak_0 - ) - self.size_values[length] = [] if data.symbolic is False: @@ -102,7 +96,8 @@ class KeccakFunctionManager: for val in self.size_values[length]: condition = Or(condition, func(data) == val) self.delete_constraints.append(condition) - constraints.append(condition) + # constraints.append(condition) + self.size_values[length].append(func(data)) return func(data), constraints diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 181a1393..4037bb29 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -3,6 +3,7 @@ the call graph.""" from mythril.laser.smt import Solver, Bool, symbol_factory, simplify +from copy import copy from typing import Iterable, List, Optional, Union from z3 import unsat @@ -36,6 +37,7 @@ class Constraints(list): """ :return: True/False based on the existence of solution of constraints """ + return True if self._is_possible is not None: return self._is_possible solver = Solver() @@ -81,7 +83,9 @@ class Constraints(list): :return: The copied constraint List """ constraint_list = super(Constraints, self).copy() - return Constraints(constraint_list, is_possible=self._is_possible) + constraints = Constraints(constraint_list, is_possible=self._is_possible) + constraints.weighted = self.weighted + return constraints def copy(self) -> "Constraints": return self.__copy__() @@ -92,7 +96,10 @@ class Constraints(list): :param memodict: :return: The copied constraint List """ - return self.__copy__() + constraint_list = super(Constraints, self).copy() + constraints = Constraints(constraint_list, is_possible=self._is_possible) + constraints.weighted = copy(self.weighted) + return constraints def __add__(self, constraints: List[Union[bool, Bool]]) -> "Constraints": """ diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 864d6af2..509e57cd 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -222,6 +222,7 @@ class LaserEVM: i, len(self.open_states) ) ) + for hook in self._start_sym_trans_hooks: hook() @@ -355,14 +356,22 @@ class LaserEVM: ] log.debug("Ending transaction %s.", transaction) - if return_global_state is None: if ( not isinstance(transaction, ContractCreationTransaction) or transaction.return_data ) and not end_signal.revert: - constraints = self.concretize_keccak(end_signal.global_state) + constraints, deleted_constraints = self.concretize_keccak(global_state) end_signal.global_state.world_state.node = global_state.node + end_signal.global_state.world_state.node.constraints = global_state.mstate.constraints + for constraint in keccak_function_manager.delete_constraints: + try: + end_signal.global_state.world_state.node.constraints.remove(constraint) + deleted_constraints = And(constraint, deleted_constraints) + except ValueError: + # Constraint not related to this state + continue + end_signal.global_state.world_state.node.constraints.append(constraints) end_signal.global_state.world_state.node.constraints.weighted.append(constraints) self._add_world_state(end_signal.global_state) @@ -370,6 +379,15 @@ class LaserEVM: else: # First execute the post hook for the transaction ending instruction self._execute_post_hook(op_code, [end_signal.global_state]) + constraints, deleted_constraints = self.concretize_keccak(global_state) + global_state.mstate.constraints.weighted.append(constraints) + for constraint in keccak_function_manager.delete_constraints: + try: + return_global_state.mstate.constraints.remove(constraint) + deleted_constraints = And(constraint, deleted_constraints) + except ValueError: + # Constraint not related to this state + continue new_global_states = self._end_message_call( copy(return_global_state), @@ -402,19 +420,17 @@ class LaserEVM: from random import randint stored_vals = {} - for key in keccak_function_manager.topo_keys: + for index, key in enumerate(keccak_function_manager.topo_keys): if keccak_function_manager.keccak_parent[key] is None: for model_tuple in model_tuples: if model_tuple[0] is None: continue + + concrete_val_i = model_tuple[0].eval(key.raw, model_completion=True).as_long() + if concrete_val_i == 0: + concrete_val_i = randint(0, 2 ** key.size() - 1) - concrete_val_i = model_tuple[0].eval(key.raw, model_completion=True) - try: - concrete_val_i = BitVec(concrete_val_i) - except AttributeError: - val = randint(0, 2 ** key.size() - 1) - concrete_val_i = symbol_factory.BitVecVal(val, key.size()) - + concrete_val_i = symbol_factory.BitVecVal(concrete_val_i, key.size()) model_tuple[1] = And(model_tuple[1], key == concrete_val_i) if key not in stored_vals: stored_vals[key] = {} @@ -428,30 +444,36 @@ class LaserEVM: if model_tuple[0] is None: continue if parent.size() == 512: - concrete_parent1 = model_tuple[0].eval(parent1.raw, model_completion=True) - if concrete_parent1 is None: - concrete_parent1 = stored_vals[parent1][model_tuple[2]] - if not isinstance(concrete_parent1, BitVec): - concrete_parent1 = BitVec(concrete_parent1) - concrete_parent = Concat(concrete_parent1, parent2) + if parent1.symbolic: + parent1 = stored_vals[parent1][model_tuple[2]] + if not isinstance(parent1, BitVec): + parent1 = BitVec(parent1) + concrete_parent = Concat(parent1, parent2) else: - concrete_parent = model_tuple[0].eval(parent.raw, model_completion=True) - if concrete_parent is None: - concrete_parent = stored_vals[parent][model_tuple[2]] - concrete_parent = BitVec(concrete_parent) + concrete_parent = stored_vals[parent][model_tuple[2]] + keccak_val = keccak_function_manager.find_keccak(concrete_parent) + if key not in stored_vals: + stored_vals[key] = {} + stored_vals[key][model_tuple[2]] = keccak_val model_tuple[1] = And(model_tuple[1], key == keccak_val) new_condition = False z3.set_option(max_args=10000000, max_lines=100000000, max_depth=10000000, max_visited=1000000) for model_tuple in model_tuples: new_condition = Or(model_tuple[1], new_condition) - new_condition = simplify(new_condition) - try: - get_model(constraints=global_state.mstate.constraints + [new_condition]) - except UnsatError: - print("SHIT", new_condition, "SHIT_ENDS") - keccak_function_manager.topo_keys = [] - return new_condition + constraints = copy(global_state.mstate.constraints) + deleted_constraints = True + for constraint in keccak_function_manager.delete_constraints: + try: + constraints.remove(constraint) + deleted_constraints = And(constraint, deleted_constraints) + except ValueError: + # Constraint not related to this state + continue + if deleted_constraints is True: + deleted_constraints = False + + return new_condition, deleted_constraints def _end_message_call( self, From 28499ac8defba0c6a07d86b43b9cfd1bcf01790e Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 15 Sep 2019 13:28:00 +0530 Subject: [PATCH 06/54] Finish concretisation --- mythril/analysis/modules/suicide.py | 1 - mythril/analysis/solver.py | 4 +- mythril/laser/ethereum/instructions.py | 4 +- .../laser/ethereum/keccak_function_manager.py | 30 ++++++----- mythril/laser/ethereum/state/constraints.py | 17 ++++-- mythril/laser/ethereum/state/global_state.py | 3 ++ mythril/laser/ethereum/svm.py | 53 ++++++++++++++----- .../laser/ethereum/transaction/symbolic.py | 2 +- 8 files changed, 77 insertions(+), 37 deletions(-) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index b5a9b988..d91c6151 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -9,7 +9,6 @@ from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) import logging -import json log = logging.getLogger(__name__) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 80ba7229..0300f859 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -20,7 +20,9 @@ log = logging.getLogger(__name__) # LRU cache works great when used in powers of 2 @lru_cache(maxsize=2 ** 23) -def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True, weighted=()): +def get_model( + constraints, minimize=(), maximize=(), enforce_execution_time=True, weighted=() +): """ :param constraints: diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b0c63a3c..02517309 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -948,7 +948,9 @@ class Instruction: else: # length is 0; this only matters for input of the BitVecFuncVal data = symbol_factory.BitVecVal(0, 1) - result, constraints = keccak_function_manager.create_keccak(data, length) + result, constraints = keccak_function_manager.create_keccak( + data, length, global_state + ) state.stack.append(result) state.constraints += constraints diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 9f9d3767..d910c0da 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -24,7 +24,6 @@ class KeccakFunctionManager: self.sizes = {} self.size_index = {} self.index_counter = TOTAL_PARTS - 34534 - self.topo_keys = [] self.keccak_parent = {} self.size_values = {} self.keccak_vals = {} @@ -42,17 +41,17 @@ class KeccakFunctionManager: self.keccak_vals[func(data)] = keccak return keccak - def create_keccak(self, data: BitVec, length: int): + def create_keccak(self, data: BitVec, length: int, global_state): length = length * 8 data = simplify(data) - if data.symbolic and data not in self.topo_keys: + if data.symbolic and simplify(data) not in global_state.topo_keys: if data.size() != 512: self.keccak_parent[data] = None - self.topo_keys.append(data) + global_state.topo_keys.append(simplify(data)) else: p1 = simplify(Extract(511, 256, data)) - if p1.symbolic and p1 not in self.topo_keys: - self.topo_keys.append(p1) + if p1.symbolic and p1 not in global_state.topo_keys: + global_state.topo_keys.append(p1) self.keccak_parent[p1] = None assert length == data.size() @@ -65,17 +64,17 @@ class KeccakFunctionManager: self.sizes[length] = (func, inverse) self.size_values[length] = [] + constraints.append(inverse(func(data)) == data) + if data.symbolic is False: keccak = self.find_keccak(data) self.size_values[length].append(keccak) constraints.append(func(data) == keccak) + return func(data), constraints - if data.symbolic and simplify(func(data)) not in self.topo_keys: + if simplify(func(data)) not in global_state.topo_keys: self.keccak_parent[simplify(func(data))] = data - self.topo_keys.append(func(data)) - constraints.append(inverse(func(data)) == data) - if data.symbolic is False: - return func(data), constraints + global_state.topo_keys.append(simplify(func(data))) try: index = self.size_index[length] @@ -94,10 +93,13 @@ class KeccakFunctionManager: ) for val in self.size_values[length]: - condition = Or(condition, func(data) == val) + if hash(simplify(func(data))) != hash(simplify(val)): + condition = Or(condition, func(data) == val) self.delete_constraints.append(condition) - # constraints.append(condition) - self.size_values[length].append(func(data)) + + constraints.append(condition) + if func(data) not in self.size_values[length]: + self.size_values[length].append(func(data)) return func(data), constraints diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 4037bb29..20c98e76 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -37,7 +37,6 @@ class Constraints(list): """ :return: True/False based on the existence of solution of constraints """ - return True if self._is_possible is not None: return self._is_possible solver = Solver() @@ -84,7 +83,7 @@ class Constraints(list): """ constraint_list = super(Constraints, self).copy() constraints = Constraints(constraint_list, is_possible=self._is_possible) - constraints.weighted = self.weighted + constraints.weighted = copy(self.weighted) return constraints def copy(self) -> "Constraints": @@ -109,7 +108,13 @@ class Constraints(list): """ constraints_list = self._get_smt_bool_list(constraints) constraints_list = super(Constraints, self).__add__(constraints_list) - return Constraints(constraint_list=constraints_list, is_possible=None) + new_constraints = Constraints( + constraint_list=constraints_list, is_possible=None + ) + new_constraints.weighted = copy(self.weighted) + if isinstance(constraints, Constraints): + new_constraints.weighted += constraints.weighted + return new_constraints def __iadd__(self, constraints: Iterable[Union[bool, Bool]]) -> "Constraints": """ @@ -117,8 +122,10 @@ class Constraints(list): :param constraints: :return: """ - constraints = self._get_smt_bool_list(constraints) - super(Constraints, self).__iadd__(constraints) + list_constraints = self._get_smt_bool_list(constraints) + super(Constraints, self).__iadd__(list_constraints) + if isinstance(constraints, Constraints): + self.weighted += constraints.weighted self._is_possible = None return self diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index 0c43980b..5f43bbdd 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -31,6 +31,7 @@ class GlobalState: transaction_stack=None, last_return_data=None, annotations=None, + keccak_topo_list=None, ) -> None: """Constructor for GlobalState. @@ -52,6 +53,7 @@ class GlobalState: self.op_code = "" self.last_return_data = last_return_data self._annotations = annotations or [] + self.topo_keys = keccak_topo_list or [] def __copy__(self) -> "GlobalState": """ @@ -71,6 +73,7 @@ class GlobalState: transaction_stack=transaction_stack, last_return_data=self.last_return_data, annotations=[copy(a) for a in self._annotations], + keccak_topo_list=copy(self.topo_keys), ) @property diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 509e57cd..7fc8fd25 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -361,25 +361,38 @@ class LaserEVM: not isinstance(transaction, ContractCreationTransaction) or transaction.return_data ) and not end_signal.revert: - constraints, deleted_constraints = self.concretize_keccak(global_state) + constraints, deleted_constraints = self.concretize_keccak( + global_state + ) end_signal.global_state.world_state.node = global_state.node - end_signal.global_state.world_state.node.constraints = global_state.mstate.constraints + end_signal.global_state.world_state.node.constraints = ( + global_state.mstate.constraints + ) for constraint in keccak_function_manager.delete_constraints: try: - end_signal.global_state.world_state.node.constraints.remove(constraint) + end_signal.global_state.world_state.node.constraints.remove( + constraint + ) deleted_constraints = And(constraint, deleted_constraints) except ValueError: # Constraint not related to this state continue - end_signal.global_state.world_state.node.constraints.append(constraints) - end_signal.global_state.world_state.node.constraints.weighted.append(constraints) + end_signal.global_state.world_state.node.constraints.append( + Or(constraints, deleted_constraints) + ) + end_signal.global_state.world_state.node.constraints.weighted.append( + constraints + ) self._add_world_state(end_signal.global_state) new_global_states = [] else: # First execute the post hook for the transaction ending instruction self._execute_post_hook(op_code, [end_signal.global_state]) constraints, deleted_constraints = self.concretize_keccak(global_state) + global_state.mstate.constraints.append( + Or(constraints, deleted_constraints) + ) global_state.mstate.constraints.weighted.append(constraints) for constraint in keccak_function_manager.delete_constraints: try: @@ -403,6 +416,7 @@ class LaserEVM: def concretize_keccak(self, global_state): sender = global_state.environment.sender model_tuples = [] + for actor in ACTOR_ADDRESSES: try: model_tuples.append( @@ -420,17 +434,22 @@ class LaserEVM: from random import randint stored_vals = {} - for index, key in enumerate(keccak_function_manager.topo_keys): + + for index, key in enumerate(global_state.topo_keys): if keccak_function_manager.keccak_parent[key] is None: for model_tuple in model_tuples: if model_tuple[0] is None: continue - - concrete_val_i = model_tuple[0].eval(key.raw, model_completion=True).as_long() + + concrete_val_i = ( + model_tuple[0].eval(key.raw, model_completion=True).as_long() + ) if concrete_val_i == 0: concrete_val_i = randint(0, 2 ** key.size() - 1) - concrete_val_i = symbol_factory.BitVecVal(concrete_val_i, key.size()) + concrete_val_i = symbol_factory.BitVecVal( + concrete_val_i, key.size() + ) model_tuple[1] = And(model_tuple[1], key == concrete_val_i) if key not in stored_vals: stored_vals[key] = {} @@ -438,8 +457,8 @@ class LaserEVM: else: parent = keccak_function_manager.keccak_parent[key] if parent.size() == 512: - parent1 = simplify(Extract(511, 256, parent)) - parent2 = simplify(Extract(255, 0, parent)) + parent1 = Extract(511, 256, parent) + parent2 = Extract(255, 0, parent) for model_tuple in model_tuples: if model_tuple[0] is None: continue @@ -458,10 +477,15 @@ class LaserEVM: stored_vals[key][model_tuple[2]] = keccak_val model_tuple[1] = And(model_tuple[1], key == keccak_val) new_condition = False - z3.set_option(max_args=10000000, max_lines=100000000, max_depth=10000000, max_visited=1000000) + z3.set_option( + max_args=10000000, + max_lines=100000000, + max_depth=10000000, + max_visited=1000000, + ) for model_tuple in model_tuples: new_condition = Or(model_tuple[1], new_condition) - constraints = copy(global_state.mstate.constraints) + constraints = global_state.mstate.constraints deleted_constraints = True for constraint in keccak_function_manager.delete_constraints: try: @@ -470,9 +494,10 @@ class LaserEVM: except ValueError: # Constraint not related to this state continue + if deleted_constraints is True: deleted_constraints = False - + new_condition = simplify(new_condition) return new_condition, deleted_constraints def _end_message_call( diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 2212e805..e611fd43 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -143,7 +143,7 @@ def _setup_global_state_for_execution(laser_evm, transaction: BaseTransaction) - ) global_state.mstate.constraints += transaction.world_state.node.constraints - new_node.constraints = global_state.mstate.constraints.as_list + new_node.constraints = global_state.mstate.constraints global_state.world_state.transaction_sequence.append(transaction) global_state.node = new_node From da02e90a73eb62c3d619bea8a328e97e87bd569e Mon Sep 17 00:00:00 2001 From: Nikhil Date: Thu, 19 Sep 2019 23:16:48 +0530 Subject: [PATCH 07/54] Fix concretisation for longer inputs --- mythril/analysis/modules/suicide.py | 13 ++- mythril/analysis/solver.py | 25 +++++- mythril/laser/ethereum/cfg.py | 3 +- .../laser/ethereum/keccak_function_manager.py | 33 ++++++- mythril/laser/ethereum/state/global_state.py | 10 ++- mythril/laser/ethereum/state/world_state.py | 8 ++ mythril/laser/ethereum/svm.py | 88 +++++++++++++++---- mythril/laser/smt/__init__.py | 22 +++++ mythril/laser/smt/bitvec_helper.py | 10 +++ mythril/laser/smt/solver/solver.py | 4 +- 10 files changed, 183 insertions(+), 33 deletions(-) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index d91c6151..57508111 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -68,12 +68,15 @@ class SuicideModule(DetectionModule): for tx in state.world_state.transaction_sequence: if not isinstance(tx, ContractCreationTransaction): constraints.append(tx.caller == ATTACKER_ADDRESS) - + print(state.mstate.constraints) try: try: transaction_sequence = solver.get_transaction_sequence( state, - state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS], + state.mstate.constraints + + constraints + + [to == ATTACKER_ADDRESS] + + state.mstate.constraints.weighted[:1], ) description_tail = ( "Anyone can kill this contract and withdraw its balance to an arbitrary " @@ -81,10 +84,12 @@ class SuicideModule(DetectionModule): ) except UnsatError: transaction_sequence = solver.get_transaction_sequence( - state, state.mstate.constraints + constraints + state, + state.mstate.constraints + + constraints + + state.mstate.constraints.weighted[:1], ) description_tail = "Arbitrary senders can kill this contract." - issue = Issue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 0300f859..c7019c3d 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -7,8 +7,9 @@ import z3 from mythril.analysis.analysis_args import analysis_args from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.constraints import Constraints +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.transaction import BaseTransaction -from mythril.laser.smt import UGE, Optimize, symbol_factory +from mythril.laser.smt import UGE, Optimize, symbol_factory, BitVec, simplify from mythril.laser.ethereum.time_handler import time_handler from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction.transaction_models import ( @@ -106,6 +107,28 @@ def get_transaction_sequence( except UnsatError: raise UnsatError + for keccak in keccak_function_manager.keys: + if isinstance(keccak, BitVec): + try: + f1, f2, vc = keccak_function_manager.flag_conditions[simplify(keccak)] + try: + f1 = model.eval(f1.raw) + except: + pass + try: + f2 = model.eval(f2.raw) + except: + pass + try: + vc = model.eval(vc.raw) + except: + pass + + except: + f1, f2, vc = None, None, None + # print("KECCAK : {} \n\n VALUE: {}\n\n FLAG: {}\n\n F1: {}\n\n F2: {} \n\n VC: {}\n\n\n\n".format(keccak, model.eval(keccak.raw), + # model.eval(symbol_factory.BoolSym("{}_flag".format(str(simplify(keccak)))).raw), f1, f2, vc) + # ) # Include creation account in initial state # Note: This contains the code, which should not exist until after the first tx initial_world_state = transaction_sequence[0].world_state diff --git a/mythril/laser/ethereum/cfg.py b/mythril/laser/ethereum/cfg.py index 0578c602..c62f8857 100644 --- a/mythril/laser/ethereum/cfg.py +++ b/mythril/laser/ethereum/cfg.py @@ -2,6 +2,7 @@ from enum import Enum from typing import Dict, List, TYPE_CHECKING +from mythril.laser.ethereum.state.constraints import Constraints from flags import Flags if TYPE_CHECKING: @@ -46,7 +47,7 @@ class Node: :param start_addr: :param constraints: """ - constraints = constraints if constraints else [] + constraints = constraints if constraints else Constraints() self.contract_name = contract_name self.start_addr = start_addr self.states = [] # type: List[GlobalState] diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index d910c0da..06507273 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -1,5 +1,6 @@ from random import randint +from copy import copy from ethereum import utils from mythril.laser.smt import ( BitVec, @@ -12,6 +13,8 @@ from mythril.laser.smt import ( Or, simplify, Extract, + Implies, + Not, ) TOTAL_PARTS = 10 ** 40 @@ -28,6 +31,8 @@ class KeccakFunctionManager: self.size_values = {} self.keccak_vals = {} self.delete_constraints = [] + self.keys = [] + self.flag_conditions = {} def find_keccak(self, data: BitVec) -> BitVec: keccak = symbol_factory.BitVecVal( @@ -53,7 +58,6 @@ class KeccakFunctionManager: if p1.symbolic and p1 not in global_state.topo_keys: global_state.topo_keys.append(p1) self.keccak_parent[p1] = None - assert length == data.size() constraints = [] try: @@ -63,6 +67,7 @@ class KeccakFunctionManager: inverse = Function("keccak256_{}-1".format(length), 256, length) self.sizes[length] = (func, inverse) self.size_values[length] = [] + flag_var = symbol_factory.BoolSym("{}_flag".format(str(simplify(func(data))))) constraints.append(inverse(func(data)) == data) @@ -70,6 +75,7 @@ class KeccakFunctionManager: keccak = self.find_keccak(data) self.size_values[length].append(keccak) constraints.append(func(data) == keccak) + constraints.append(flag_var) return func(data), constraints if simplify(func(data)) not in global_state.topo_keys: @@ -91,15 +97,34 @@ class KeccakFunctionManager: ULT(func(data), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) - + f_cond = copy(condition) + flag_condition = False for val in self.size_values[length]: - if hash(simplify(func(data))) != hash(simplify(val)): - condition = Or(condition, func(data) == val) + if ( + hash(simplify(func(data))) != hash(simplify(val)) + and val in global_state.total_topo_keys + ): + prev_flag_var = symbol_factory.BoolSym( + "{}_flag".format(str(simplify(val))) + ) + condition = Or( + condition, And(func(data) == val, prev_flag_var, flag_var) + ) + flag_condition = Or( + flag_condition, And(func(data) == val, prev_flag_var, flag_var) + ) + + self.flag_conditions[func(data)] = (f_cond, flag_condition, None) self.delete_constraints.append(condition) constraints.append(condition) if func(data) not in self.size_values[length]: self.size_values[length].append(func(data)) + if data not in self.keys: + self.keys.append(data) + if func(data) not in self.keys: + self.keys.append(func(data)) + return func(data), constraints diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index 5f43bbdd..9d21a886 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -53,7 +53,6 @@ class GlobalState: self.op_code = "" self.last_return_data = last_return_data self._annotations = annotations or [] - self.topo_keys = keccak_topo_list or [] def __copy__(self) -> "GlobalState": """ @@ -73,9 +72,16 @@ class GlobalState: transaction_stack=transaction_stack, last_return_data=self.last_return_data, annotations=[copy(a) for a in self._annotations], - keccak_topo_list=copy(self.topo_keys), ) + @property + def topo_keys(self) -> List: + return self.world_state.topo_keys + + @property + def total_topo_keys(self): + return self.world_state.topo_keys + self.world_state.old_topo_keys + @property def accounts(self) -> Dict: """ diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 20628877..724cb471 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -32,11 +32,17 @@ class WorldState: self.node = None # type: Optional['Node'] self.transaction_sequence = transaction_sequence or [] self._annotations = annotations or [] + self.topo_keys = [] + self.old_topo_keys = [] @property def accounts(self): return self._accounts + def reset_topo_keys(self): + self.old_topo_keys += self.topo_keys + self.topo_keys = [] + def __getitem__(self, item: BitVec) -> Account: """Gets an account from the worldstate using item as key. @@ -60,6 +66,8 @@ class WorldState: transaction_sequence=self.transaction_sequence[:], annotations=new_annotations, ) + new_world_state.topo_keys = copy(self.topo_keys) + new_world_state.old_topo_keys = copy(self.old_topo_keys) new_world_state.balances = copy(self.balances) new_world_state.starting_balances = copy(self.starting_balances) for account in self._accounts.values(): diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 7fc8fd25..a5c06fb0 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -11,7 +11,10 @@ from mythril.laser.ethereum.evm_exceptions import StackUnderflowException from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.iprof import InstructionProfiler -from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager +from mythril.laser.ethereum.keccak_function_manager import ( + keccak_function_manager, + Function, +) from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState @@ -37,6 +40,8 @@ from mythril.laser.smt import ( simplify, is_true, Concat, + Implies, + Not, ) ACTOR_ADDRESSES = [ @@ -227,6 +232,8 @@ class LaserEVM: hook() execute_message_call(self, address) + for os in self.open_states: + os.reset_topo_keys() for hook in self._stop_sym_trans_hooks: hook() @@ -361,7 +368,7 @@ class LaserEVM: not isinstance(transaction, ContractCreationTransaction) or transaction.return_data ) and not end_signal.revert: - constraints, deleted_constraints = self.concretize_keccak( + constraints, deleted_constraints, v, w = self.concretize_keccak( global_state ) end_signal.global_state.world_state.node = global_state.node @@ -379,25 +386,27 @@ class LaserEVM: continue end_signal.global_state.world_state.node.constraints.append( - Or(constraints, deleted_constraints) - ) - end_signal.global_state.world_state.node.constraints.weighted.append( - constraints + And(Or(constraints, deleted_constraints), v) ) + + end_signal.global_state.world_state.node.constraints.weighted += w + self._add_world_state(end_signal.global_state) + new_global_states = [] else: # First execute the post hook for the transaction ending instruction self._execute_post_hook(op_code, [end_signal.global_state]) - constraints, deleted_constraints = self.concretize_keccak(global_state) + constraints, deleted_constraints, v, w = self.concretize_keccak( + global_state + ) global_state.mstate.constraints.append( - Or(constraints, deleted_constraints) + And(Or(constraints, deleted_constraints), v) ) - global_state.mstate.constraints.weighted.append(constraints) + global_state.mstate.constraints.weighted += w for constraint in keccak_function_manager.delete_constraints: try: return_global_state.mstate.constraints.remove(constraint) - deleted_constraints = And(constraint, deleted_constraints) except ValueError: # Constraint not related to this state continue @@ -434,22 +443,48 @@ class LaserEVM: from random import randint stored_vals = {} + var_conds = True + flag_weights = [] for index, key in enumerate(global_state.topo_keys): + flag_var = symbol_factory.BoolSym("{}_flag".format(str(simplify(key)))) + var_cond = False if keccak_function_manager.keccak_parent[key] is None: for model_tuple in model_tuples: if model_tuple[0] is None: continue - - concrete_val_i = ( - model_tuple[0].eval(key.raw, model_completion=True).as_long() - ) - if concrete_val_i == 0: + if key.size() == 256: + concrete_input = symbol_factory.BitVecVal( + randint(0, 2 ** 160 - 1), 160 + ) + func = Function("keccak256_{}".format(160), 160, 256) + inverse = Function("keccak256_{}-1".format(160), 256, 160) + hash_cond = inverse(func(concrete_input)) == concrete_input + keccak_function_manager.sizes[160] = (func, inverse) + if 160 not in keccak_function_manager.size_values: + keccak_function_manager.size_values[160] = [] + concrete_val_i = keccak_function_manager.find_keccak( + concrete_input + ) + keccak_function_manager.size_values[160].append(concrete_val_i) + hash_cond = And( + hash_cond, func(concrete_input) == concrete_val_i + ) + var_cond = Or( + var_cond, + And( + key == concrete_val_i, + hash_cond, + key == func(concrete_input), + ), + ) + else: concrete_val_i = randint(0, 2 ** key.size() - 1) - concrete_val_i = symbol_factory.BitVecVal( - concrete_val_i, key.size() - ) + concrete_val_i = symbol_factory.BitVecVal( + concrete_val_i, key.size() + ) + var_cond = Or(var_cond, key == concrete_val_i) model_tuple[1] = And(model_tuple[1], key == concrete_val_i) if key not in stored_vals: stored_vals[key] = {} @@ -476,6 +511,19 @@ class LaserEVM: stored_vals[key] = {} stored_vals[key][model_tuple[2]] = keccak_val model_tuple[1] = And(model_tuple[1], key == keccak_val) + var_cond = Or(var_cond, key == keccak_val) + try: + f1, f2, _ = keccak_function_manager.flag_conditions[simplify(key)] + var_cond = And(Or(var_cond, f2) == flag_var, f1 == Not(flag_var)) + keccak_function_manager.flag_conditions[simplify(key)] = ( + f1, + f2, + var_cond, + ) + flag_weights.append(flag_var) + except KeyError: + var_cond = True + var_conds = And(var_conds, var_cond) new_condition = False z3.set_option( max_args=10000000, @@ -497,8 +545,10 @@ class LaserEVM: if deleted_constraints is True: deleted_constraints = False + new_condition = simplify(new_condition) - return new_condition, deleted_constraints + + return new_condition, deleted_constraints, var_conds, flag_weights def _end_message_call( self, diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index b0793562..6f4bf008 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -16,6 +16,7 @@ from mythril.laser.smt.bitvec_helper import ( BVMulNoOverflow, BVSubNoUnderflow, LShR, + Implies, ) from mythril.laser.smt.bitvecfunc import BitVecFunc @@ -48,6 +49,16 @@ class SymbolFactory(Generic[T, U]): """ raise NotImplementedError + @staticmethod + def BoolSym(name: str, annotations: Annotations = None) -> T: + """ + Creates a Bool with concrete value + :param name: The name of the Bool variable + :param annotations: The annotations to initialize the bool with + :return: The freshly created Bool() + """ + raise NotImplementedError + @staticmethod def BitVecVal(value: int, size: int, annotations: Annotations = None) -> U: """Creates a new bit vector with a concrete value. @@ -126,6 +137,17 @@ class _SmtSymbolFactory(SymbolFactory[SMTBool, BitVec]): raw = z3.BoolVal(value) return SMTBool(raw, annotations) + @staticmethod + def BoolSym(name: str, annotations: Annotations = None) -> T: + """ + Creates a Bool with concrete value + :param name: The name of the Bool variable + :param annotations: The annotations to initialize the bool with + :return: The freshly created Bool() + """ + raw = z3.Bool(name) + return SMTBool(raw, annotations) + @staticmethod def BitVecVal(value: int, size: int, annotations: Annotations = None) -> BitVec: """Creates a new bit vector with a concrete value.""" diff --git a/mythril/laser/smt/bitvec_helper.py b/mythril/laser/smt/bitvec_helper.py index 8e68e0c9..56ac64b3 100644 --- a/mythril/laser/smt/bitvec_helper.py +++ b/mythril/laser/smt/bitvec_helper.py @@ -69,6 +69,16 @@ def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> Bi return BitVec(z3.If(a.raw, b.raw, c.raw), union) +def Implies(a: Union[Bool, bool], b: Union[Bool, bool]) -> Union[Bool, bool]: + if not isinstance(a, Bool): + a = Bool(z3.BoolVal(a)) + if not isinstance(b, Bool): + b = Bool(z3.BoolVal(b)) + union = a.annotations.union(b.annotations) + + return Bool(z3.Implies(a.raw, b.raw), annotations=union) + + def UGT(a: BitVec, b: BitVec) -> Bool: """Create an unsigned greater than expression. diff --git a/mythril/laser/smt/solver/solver.py b/mythril/laser/smt/solver/solver.py index 4ab7f043..1537ceaf 100644 --- a/mythril/laser/smt/solver/solver.py +++ b/mythril/laser/smt/solver/solver.py @@ -45,14 +45,14 @@ class BaseSolver(Generic[T]): self.add(*constraints) @stat_smt_query - def check(self) -> z3.CheckSatResult: + def check(self, *args) -> z3.CheckSatResult: """Returns z3 smt check result. Also suppresses the stdout when running z3 library's check() to avoid unnecessary output :return: The evaluated result which is either of sat, unsat or unknown """ old_stdout = sys.stdout sys.stdout = open(os.devnull, "w") - evaluate = self.raw.check() + evaluate = self.raw.check(args) sys.stdout = old_stdout return evaluate From b837fb7a394eeba3c983ae5cdccd385e6e688a7e Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 22 Sep 2019 16:21:32 +0100 Subject: [PATCH 08/54] Fix some errors --- mythril/analysis/modules/suicide.py | 10 +++++++--- .../laser/ethereum/keccak_function_manager.py | 4 ++-- mythril/laser/ethereum/svm.py | 18 +++++++++--------- 3 files changed, 18 insertions(+), 14 deletions(-) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index 57508111..422d8ad7 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -68,7 +68,13 @@ class SuicideModule(DetectionModule): for tx in state.world_state.transaction_sequence: if not isinstance(tx, ContractCreationTransaction): constraints.append(tx.caller == ATTACKER_ADDRESS) - print(state.mstate.constraints) + #print(state.mstate.constraints) + #for i in range(len(state.mstate.constraints)): + # try: + # solver.get_model(tuple(state.mstate.constraints[:i] + constraints)) + # print(i, "PASS") + # except UnsatError: + # print(i, "FAIL") try: try: transaction_sequence = solver.get_transaction_sequence( @@ -76,7 +82,6 @@ class SuicideModule(DetectionModule): state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS] - + state.mstate.constraints.weighted[:1], ) description_tail = ( "Anyone can kill this contract and withdraw its balance to an arbitrary " @@ -87,7 +92,6 @@ class SuicideModule(DetectionModule): state, state.mstate.constraints + constraints - + state.mstate.constraints.weighted[:1], ) description_tail = "Arbitrary senders can kill this contract." issue = Issue( diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 06507273..ff4544ca 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -108,10 +108,10 @@ class KeccakFunctionManager: "{}_flag".format(str(simplify(val))) ) condition = Or( - condition, And(func(data) == val, prev_flag_var, flag_var) + condition, And(func(data) == val, prev_flag_var) ) flag_condition = Or( - flag_condition, And(func(data) == val, prev_flag_var, flag_var) + flag_condition, And(func(data) == val, prev_flag_var) ) self.flag_conditions[func(data)] = (f_cond, flag_condition, None) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index a5c06fb0..ffcad7d7 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -466,7 +466,6 @@ class LaserEVM: concrete_val_i = keccak_function_manager.find_keccak( concrete_input ) - keccak_function_manager.size_values[160].append(concrete_val_i) hash_cond = And( hash_cond, func(concrete_input) == concrete_val_i ) @@ -475,7 +474,6 @@ class LaserEVM: And( key == concrete_val_i, hash_cond, - key == func(concrete_input), ), ) else: @@ -515,14 +513,16 @@ class LaserEVM: try: f1, f2, _ = keccak_function_manager.flag_conditions[simplify(key)] var_cond = And(Or(var_cond, f2) == flag_var, f1 == Not(flag_var)) - keccak_function_manager.flag_conditions[simplify(key)] = ( - f1, - f2, - var_cond, - ) + if simplify(key) in keccak_function_manager.flag_conditions: + keccak_function_manager.flag_conditions[simplify(key)] = ( + f1, + f2, + var_cond, + ) flag_weights.append(flag_var) - except KeyError: - var_cond = True + except KeyError as e: + print("FAIL", e) + var_cond = Or(And(flag_var, var_cond), Not(And(flag_var, var_cond))) var_conds = And(var_conds, var_cond) new_condition = False z3.set_option( From 0af62acd907e2bc446fd1b59b025073fa0316bc5 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 23 Sep 2019 22:27:44 +0100 Subject: [PATCH 09/54] Make some changes to make storage work for pseudo input --- mythril/analysis/modules/suicide.py | 15 +------ .../laser/ethereum/keccak_function_manager.py | 24 ++++++++---- mythril/laser/ethereum/state/constraints.py | 1 + mythril/laser/ethereum/svm.py | 39 ++++++++++--------- 4 files changed, 39 insertions(+), 40 deletions(-) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index 422d8ad7..b01a921c 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -68,20 +68,11 @@ class SuicideModule(DetectionModule): for tx in state.world_state.transaction_sequence: if not isinstance(tx, ContractCreationTransaction): constraints.append(tx.caller == ATTACKER_ADDRESS) - #print(state.mstate.constraints) - #for i in range(len(state.mstate.constraints)): - # try: - # solver.get_model(tuple(state.mstate.constraints[:i] + constraints)) - # print(i, "PASS") - # except UnsatError: - # print(i, "FAIL") try: try: transaction_sequence = solver.get_transaction_sequence( state, - state.mstate.constraints - + constraints - + [to == ATTACKER_ADDRESS] + state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS], ) description_tail = ( "Anyone can kill this contract and withdraw its balance to an arbitrary " @@ -89,9 +80,7 @@ class SuicideModule(DetectionModule): ) except UnsatError: transaction_sequence = solver.get_transaction_sequence( - state, - state.mstate.constraints - + constraints + state, state.mstate.constraints + constraints ) description_tail = "Arbitrary senders can kill this contract." issue = Issue( diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index ff4544ca..097b33b2 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -33,6 +33,7 @@ class KeccakFunctionManager: self.delete_constraints = [] self.keys = [] self.flag_conditions = {} + self.value_inverse = {} def find_keccak(self, data: BitVec) -> BitVec: keccak = symbol_factory.BitVecVal( @@ -67,7 +68,7 @@ class KeccakFunctionManager: inverse = Function("keccak256_{}-1".format(length), 256, length) self.sizes[length] = (func, inverse) self.size_values[length] = [] - flag_var = symbol_factory.BoolSym("{}_flag".format(str(simplify(func(data))))) + flag_var = symbol_factory.BoolSym("{}_flag".format(hash(simplify(func(data))))) constraints.append(inverse(func(data)) == data) @@ -105,14 +106,21 @@ class KeccakFunctionManager: and val in global_state.total_topo_keys ): prev_flag_var = symbol_factory.BoolSym( - "{}_flag".format(str(simplify(val))) - ) - condition = Or( - condition, And(func(data) == val, prev_flag_var) - ) - flag_condition = Or( - flag_condition, And(func(data) == val, prev_flag_var) + "{}_flag".format(hash(simplify(val))) ) + pre_cond = And(func(data) == val, inverse(func(data)) == inverse(val)) + if val.value: + k2 = self.value_inverse[val] + flag_var2 = symbol_factory.BoolSym( + "{}_flag".format(hash(simplify(k2))) + ) + + pre_cond = And(pre_cond, flag_var, flag_var2) + else: + pre_cond = And(pre_cond, prev_flag_var, flag_var) + + condition = Or(condition, pre_cond) + flag_condition = Or(flag_condition, pre_cond) self.flag_conditions[func(data)] = (f_cond, flag_condition, None) self.delete_constraints.append(condition) diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 20c98e76..47aac17f 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -37,6 +37,7 @@ class Constraints(list): """ :return: True/False based on the existence of solution of constraints """ + if self._is_possible is not None: return self._is_possible solver = Solver() diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index ffcad7d7..83810b5d 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -369,7 +369,7 @@ class LaserEVM: or transaction.return_data ) and not end_signal.revert: constraints, deleted_constraints, v, w = self.concretize_keccak( - global_state + global_state, end_signal.global_state ) end_signal.global_state.world_state.node = global_state.node end_signal.global_state.world_state.node.constraints = ( @@ -398,7 +398,7 @@ class LaserEVM: # First execute the post hook for the transaction ending instruction self._execute_post_hook(op_code, [end_signal.global_state]) constraints, deleted_constraints, v, w = self.concretize_keccak( - global_state + global_state, end_signal.global_state ) global_state.mstate.constraints.append( And(Or(constraints, deleted_constraints), v) @@ -422,7 +422,7 @@ class LaserEVM: return new_global_states, op_code - def concretize_keccak(self, global_state): + def concretize_keccak(self, global_state, gs): sender = global_state.environment.sender model_tuples = [] @@ -447,8 +447,11 @@ class LaserEVM: flag_weights = [] for index, key in enumerate(global_state.topo_keys): - flag_var = symbol_factory.BoolSym("{}_flag".format(str(simplify(key)))) + if key.value: + continue + flag_var = symbol_factory.BoolSym("{}_flag".format(hash(simplify(key)))) var_cond = False + hash_cond = True if keccak_function_manager.keccak_parent[key] is None: for model_tuple in model_tuples: if model_tuple[0] is None: @@ -466,16 +469,13 @@ class LaserEVM: concrete_val_i = keccak_function_manager.find_keccak( concrete_input ) + keccak_function_manager.value_inverse[concrete_val_i] = key + keccak_function_manager.size_values[160].append(concrete_val_i) + gs.topo_keys.append(concrete_val_i) hash_cond = And( hash_cond, func(concrete_input) == concrete_val_i ) - var_cond = Or( - var_cond, - And( - key == concrete_val_i, - hash_cond, - ), - ) + var_cond = Or(var_cond, And(key == concrete_val_i, hash_cond)) else: concrete_val_i = randint(0, 2 ** key.size() - 1) @@ -513,16 +513,17 @@ class LaserEVM: try: f1, f2, _ = keccak_function_manager.flag_conditions[simplify(key)] var_cond = And(Or(var_cond, f2) == flag_var, f1 == Not(flag_var)) - if simplify(key) in keccak_function_manager.flag_conditions: - keccak_function_manager.flag_conditions[simplify(key)] = ( - f1, - f2, - var_cond, - ) + keccak_function_manager.flag_conditions[simplify(key)] = ( + f1, + f2, + var_cond, + ) flag_weights.append(flag_var) except KeyError as e: - print("FAIL", e) - var_cond = Or(And(flag_var, var_cond), Not(And(flag_var, var_cond))) + var_cond = And( + Or(And(flag_var, var_cond), Not(And(flag_var, var_cond))), hash_cond + ) + flag_weights.append(flag_var) var_conds = And(var_conds, var_cond) new_condition = False z3.set_option( From ef587eff31239f9fed197dd89287a829e7d0f9d7 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 25 Sep 2019 14:38:06 +0100 Subject: [PATCH 10/54] Make dschief work --- mythril/laser/ethereum/instructions.py | 3 ++- .../laser/ethereum/keccak_function_manager.py | 7 +++---- mythril/laser/ethereum/state/global_state.py | 5 ++++- mythril/laser/ethereum/state/world_state.py | 9 +++++---- mythril/laser/ethereum/svm.py | 18 ++---------------- 5 files changed, 16 insertions(+), 26 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 02517309..c7a26b73 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -924,7 +924,7 @@ class Instruction: if isinstance(op0, Expression): op0 = simplify(op0) state.stack.append( - symbol_factory.BitVecSym("KECCAC_mem[" + str(op0) + "]", 256) + symbol_factory.BitVecSym("KECCAC_mem[" + str(hash(op0)) + "]", 256) ) gas_tuple = cast(Tuple, OPCODE_GAS["SHA3"]) state.min_gas_used += gas_tuple[0] @@ -948,6 +948,7 @@ class Instruction: else: # length is 0; this only matters for input of the BitVecFuncVal data = symbol_factory.BitVecVal(0, 1) + result, constraints = keccak_function_manager.create_keccak( data, length, global_state ) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 097b33b2..d9217026 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -48,6 +48,7 @@ class KeccakFunctionManager: return keccak def create_keccak(self, data: BitVec, length: int, global_state): + length = length * 8 data = simplify(data) if data.symbolic and simplify(data) not in global_state.topo_keys: @@ -100,11 +101,9 @@ class KeccakFunctionManager: ) f_cond = copy(condition) flag_condition = False + total_keys = global_state.total_topo_keys for val in self.size_values[length]: - if ( - hash(simplify(func(data))) != hash(simplify(val)) - and val in global_state.total_topo_keys - ): + if hash(simplify(func(data))) != hash(simplify(val)) and val in total_keys: prev_flag_var = symbol_factory.BoolSym( "{}_flag".format(hash(simplify(val))) ) diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index 9d21a886..ede2a6ea 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -80,7 +80,10 @@ class GlobalState: @property def total_topo_keys(self): - return self.world_state.topo_keys + self.world_state.old_topo_keys + ns = copy(self.world_state.old_topo_keys) + for t in self.world_state.topo_keys: + ns.add(t) + return ns @property def accounts(self) -> Dict: diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 724cb471..17f0038f 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -1,7 +1,7 @@ """This module contains a representation of the EVM's world state.""" from copy import copy from random import randint -from typing import Dict, List, Iterator, Optional, TYPE_CHECKING +from typing import Dict, List, Iterator, Optional, Set, TYPE_CHECKING from mythril.support.loader import DynLoader from mythril.laser.smt import symbol_factory, Array, BitVec @@ -32,15 +32,16 @@ class WorldState: self.node = None # type: Optional['Node'] self.transaction_sequence = transaction_sequence or [] self._annotations = annotations or [] - self.topo_keys = [] - self.old_topo_keys = [] + self.topo_keys = [] # type: List[BitVec] + self.old_topo_keys = set() # type: Set[BitVec] @property def accounts(self): return self._accounts def reset_topo_keys(self): - self.old_topo_keys += self.topo_keys + for t in self.topo_keys: + self.old_topo_keys.add(t) self.topo_keys = [] def __getitem__(self, item: BitVec) -> Account: diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 83810b5d..e80a1351 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -43,6 +43,7 @@ from mythril.laser.smt import ( Implies, Not, ) +from random import randint ACTOR_ADDRESSES = [ symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256), @@ -425,22 +426,8 @@ class LaserEVM: def concretize_keccak(self, global_state, gs): sender = global_state.environment.sender model_tuples = [] - for actor in ACTOR_ADDRESSES: - try: - model_tuples.append( - [ - get_model( - constraints=global_state.mstate.constraints - + [sender == actor] - ), - And(sender == actor), - actor, - ] - ) - except UnsatError: - model_tuples.append((None, False, actor)) - from random import randint + model_tuples.append([True, sender == actor, actor]) stored_vals = {} var_conds = True @@ -548,7 +535,6 @@ class LaserEVM: deleted_constraints = False new_condition = simplify(new_condition) - return new_condition, deleted_constraints, var_conds, flag_weights def _end_message_call( From 9d9da324be7aab12edfd350de52b7bcb30b77844 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 25 Sep 2019 16:59:56 +0100 Subject: [PATCH 11/54] Fix type errors --- mythril/laser/ethereum/keccak_function_manager.py | 2 +- mythril/laser/ethereum/state/constraints.py | 2 +- mythril/laser/smt/__init__.py | 2 +- mythril/laser/smt/function.py | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index d9217026..d673e694 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -100,7 +100,7 @@ class KeccakFunctionManager: URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) f_cond = copy(condition) - flag_condition = False + flag_condition = symbol_factory.Bool(False) total_keys = global_state.total_topo_keys for val in self.size_values[length]: if hash(simplify(func(data))) != hash(simplify(val)) and val in total_keys: diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 47aac17f..fe6513c7 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -30,7 +30,7 @@ class Constraints(list): super(Constraints, self).__init__(constraint_list) self._default_timeout = 100 self._is_possible = is_possible - self.weighted = [] + self.weighted = [] # type: List[Bool] @property def is_possible(self) -> bool: diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 6f4bf008..c4c01236 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -138,7 +138,7 @@ class _SmtSymbolFactory(SymbolFactory[SMTBool, BitVec]): return SMTBool(raw, annotations) @staticmethod - def BoolSym(name: str, annotations: Annotations = None) -> T: + def BoolSym(name: str, annotations: Annotations = None) -> SMTBool: """ Creates a Bool with concrete value :param name: The name of the Bool variable diff --git a/mythril/laser/smt/function.py b/mythril/laser/smt/function.py index 93115c88..77451871 100644 --- a/mythril/laser/smt/function.py +++ b/mythril/laser/smt/function.py @@ -22,4 +22,4 @@ class Function: """Function accessor, item can be symbolic.""" return BitVec( cast(z3.BitVecRef, self.raw(item.raw)), annotations=item.annotations - ) # type: ignore + ) From aee3e7b0ffbaa95d6213807d55957d4f26646dab Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 25 Sep 2019 17:23:14 +0100 Subject: [PATCH 12/54] Fix tests --- mythril/laser/ethereum/instructions.py | 4 +--- mythril/laser/ethereum/keccak_function_manager.py | 8 ++++---- mythril/laser/ethereum/state/constraints.py | 2 +- 3 files changed, 6 insertions(+), 8 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 48b89814..fb034bae 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1001,9 +1001,7 @@ class Instruction: # length is 0; this only matters for input of the BitVecFuncVal data = symbol_factory.BitVecVal(0, 1) - result, constraints = keccak_function_manager.create_keccak( - data, length, global_state - ) + result, constraints = keccak_function_manager.create_keccak(data, global_state) state.stack.append(result) state.constraints += constraints diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index d673e694..044cc299 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -47,9 +47,9 @@ class KeccakFunctionManager: self.keccak_vals[func(data)] = keccak return keccak - def create_keccak(self, data: BitVec, length: int, global_state): + def create_keccak(self, data: BitVec, global_state): - length = length * 8 + length = data.size() data = simplify(data) if data.symbolic and simplify(data) not in global_state.topo_keys: if data.size() != 512: @@ -60,7 +60,7 @@ class KeccakFunctionManager: if p1.symbolic and p1 not in global_state.topo_keys: global_state.topo_keys.append(p1) self.keccak_parent[p1] = None - assert length == data.size() + constraints = [] try: func, inverse = self.sizes[length] @@ -78,7 +78,7 @@ class KeccakFunctionManager: self.size_values[length].append(keccak) constraints.append(func(data) == keccak) constraints.append(flag_var) - return func(data), constraints + return keccak, constraints if simplify(func(data)) not in global_state.topo_keys: self.keccak_parent[simplify(func(data))] = data diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index fe6513c7..a39e6117 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -30,7 +30,7 @@ class Constraints(list): super(Constraints, self).__init__(constraint_list) self._default_timeout = 100 self._is_possible = is_possible - self.weighted = [] # type: List[Bool] + self.weighted = [] # type: List[Bool] @property def is_possible(self) -> bool: From 103d9588c871d49c6a755c29e38ba6a3a7ace007 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 25 Sep 2019 18:43:22 +0100 Subject: [PATCH 13/54] Fix create tests --- tests/instructions/create_test.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tests/instructions/create_test.py b/tests/instructions/create_test.py index 0a97565e..04f0decd 100644 --- a/tests/instructions/create_test.py +++ b/tests/instructions/create_test.py @@ -1,6 +1,6 @@ from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.cfg import Node from mythril.laser.ethereum.state.environment import Environment -from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.machine_state import MachineState from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState @@ -30,11 +30,12 @@ def execute_create(): calldata = ConcreteCalldata(0, code_raw) world_state = WorldState() + world_state.node = Node("Contract") account = world_state.create_account(balance=1000000, address=101) account.code = Disassembly("60a760006000f000") environment = Environment(account, None, calldata, None, None, None) og_state = GlobalState( - world_state, environment, None, MachineState(gas_limit=8000000) + world_state, environment, world_state.node, MachineState(gas_limit=8000000) ) og_state.transaction_stack.append( (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) From ffbd191dd16df4d206dd6c240d917e06df9d618f Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 25 Sep 2019 19:04:46 +0100 Subject: [PATCH 14/54] remove py35 support --- setup.py | 3 +-- tox.ini | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/setup.py b/setup.py index dd673b04..4161741b 100755 --- a/setup.py +++ b/setup.py @@ -19,7 +19,7 @@ DESCRIPTION = "Security analysis tool for Ethereum smart contracts" URL = "https://github.com/ConsenSys/mythril" AUTHOR = "ConsenSys Dilligence" AUTHOR_MAIL = None -REQUIRES_PYTHON = ">=3.5.0" +REQUIRES_PYTHON = ">=3.6.0" # What packages are required for this module to be executed? @@ -116,7 +116,6 @@ setup( "Intended Audience :: Science/Research", "Topic :: Software Development :: Disassemblers", "License :: OSI Approved :: MIT License", - "Programming Language :: Python :: 3.5", "Programming Language :: Python :: 3.6", "Programming Language :: Python :: 3.7", ], diff --git a/tox.ini b/tox.ini index e50f07fe..804b6791 100644 --- a/tox.ini +++ b/tox.ini @@ -1,5 +1,5 @@ [tox] -envlist = py35,py36 +envlist = py36 [testenv] deps = From 39f426f04368fbafd54faf0e8518d922e0a80d3d Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 25 Sep 2019 23:01:34 +0100 Subject: [PATCH 15/54] constrain concrete hash conditions --- mythril/laser/ethereum/svm.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 533f99fb..2f8da668 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -453,13 +453,12 @@ class LaserEVM: stored_vals = {} var_conds = True flag_weights = [] - + hash_cond = True for index, key in enumerate(global_state.topo_keys): if key.value: continue flag_var = symbol_factory.BoolSym("{}_flag".format(hash(simplify(key)))) var_cond = False - hash_cond = True if keccak_function_manager.keccak_parent[key] is None: for model_tuple in model_tuples: if model_tuple[0] is None: @@ -470,7 +469,6 @@ class LaserEVM: ) func = Function("keccak256_{}".format(160), 160, 256) inverse = Function("keccak256_{}-1".format(160), 256, 160) - hash_cond = inverse(func(concrete_input)) == concrete_input keccak_function_manager.sizes[160] = (func, inverse) if 160 not in keccak_function_manager.size_values: keccak_function_manager.size_values[160] = [] @@ -481,9 +479,11 @@ class LaserEVM: keccak_function_manager.size_values[160].append(concrete_val_i) gs.topo_keys.append(concrete_val_i) hash_cond = And( - hash_cond, func(concrete_input) == concrete_val_i + hash_cond, + func(concrete_input) == concrete_val_i, + inverse(concrete_val_i) == concrete_input, ) - var_cond = Or(var_cond, And(key == concrete_val_i, hash_cond)) + var_cond = Or(var_cond, key == concrete_val_i) else: concrete_val_i = randint(0, 2 ** key.size() - 1) @@ -554,7 +554,7 @@ class LaserEVM: if deleted_constraints is True: deleted_constraints = False - + var_conds = And(var_conds, hash_cond) new_condition = simplify(new_condition) return new_condition, deleted_constraints, var_conds, flag_weights From 9325abac443a0147deb31c25150e6ce69676b1d4 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Thu, 26 Sep 2019 19:48:30 +0100 Subject: [PATCH 16/54] Remove unused variables --- mythril/laser/ethereum/keccak_function_manager.py | 4 ---- mythril/laser/ethereum/state/global_state.py | 1 - mythril/laser/ethereum/svm.py | 6 +----- 3 files changed, 1 insertion(+), 10 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 044cc299..04238c6f 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -1,5 +1,3 @@ -from random import randint - from copy import copy from ethereum import utils from mythril.laser.smt import ( @@ -13,8 +11,6 @@ from mythril.laser.smt import ( Or, simplify, Extract, - Implies, - Not, ) TOTAL_PARTS = 10 ** 40 diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index 2571f9d9..7c05bfc6 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -31,7 +31,6 @@ class GlobalState: transaction_stack=None, last_return_data=None, annotations=None, - keccak_topo_list=None, ) -> None: """Constructor for GlobalState. diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 2f8da668..1596a95d 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -3,7 +3,7 @@ import logging from collections import defaultdict from copy import copy from datetime import datetime, timedelta -from typing import Callable, Dict, DefaultDict, List, Tuple, Union, Optional +from typing import Callable, Dict, DefaultDict, List, Tuple, Optional import z3 from mythril.analysis.potential_issues import check_potential_issues @@ -25,7 +25,6 @@ from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy from abc import ABCMeta from mythril.laser.ethereum.time_handler import time_handler -from mythril.analysis.solver import get_model, UnsatError from mythril.laser.ethereum.transaction import ( ContractCreationTransaction, @@ -38,13 +37,10 @@ from mythril.laser.smt import ( symbol_factory, And, Or, - BitVecFunc, BitVec, Extract, simplify, - is_true, Concat, - Implies, Not, ) from random import randint From 433b391557a29932990a8b1982d884e165f74cda Mon Sep 17 00:00:00 2001 From: Nikhil Date: Thu, 26 Sep 2019 21:58:04 +0100 Subject: [PATCH 17/54] Refactor code --- mythril/analysis/solver.py | 22 ----- .../laser/ethereum/keccak_function_manager.py | 90 ++++++++++--------- mythril/laser/ethereum/svm.py | 70 +++++++-------- 3 files changed, 78 insertions(+), 104 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 6a469c82..b33b3979 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -107,28 +107,6 @@ def get_transaction_sequence( except UnsatError: raise UnsatError - for keccak in keccak_function_manager.keys: - if isinstance(keccak, BitVec): - try: - f1, f2, vc = keccak_function_manager.flag_conditions[simplify(keccak)] - try: - f1 = model.eval(f1.raw) - except: - pass - try: - f2 = model.eval(f2.raw) - except: - pass - try: - vc = model.eval(vc.raw) - except: - pass - - except: - f1, f2, vc = None, None, None - # print("KECCAK : {} \n\n VALUE: {}\n\n FLAG: {}\n\n F1: {}\n\n F2: {} \n\n VC: {}\n\n\n\n".format(keccak, model.eval(keccak.raw), - # model.eval(symbol_factory.BoolSym("{}_flag".format(str(simplify(keccak)))).raw), f1, f2, vc) - # ) # Include creation account in initial state # Note: This contains the code, which should not exist until after the first tx initial_world_state = transaction_sequence[0].world_state diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 04238c6f..881fe68c 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -2,6 +2,8 @@ from copy import copy from ethereum import utils from mythril.laser.smt import ( BitVec, + Bool, + Expression, Function, URem, symbol_factory, @@ -20,16 +22,14 @@ INTERVAL_DIFFERENCE = 10 ** 30 class KeccakFunctionManager: def __init__(self): - self.sizes = {} - self.size_index = {} - self.index_counter = TOTAL_PARTS - 34534 + self.get_function = {} + self.interval_hook_for_size = {} self.keccak_parent = {} - self.size_values = {} - self.keccak_vals = {} + self.values_for_size = {} self.delete_constraints = [] - self.keys = [] self.flag_conditions = {} self.value_inverse = {} + self._index_counter = TOTAL_PARTS - 34534 def find_keccak(self, data: BitVec) -> BitVec: keccak = symbol_factory.BitVecVal( @@ -39,19 +39,21 @@ class KeccakFunctionManager: ), 256, ) - func, _ = self.sizes[data.size()] - self.keccak_vals[func(data)] = keccak + func, _ = self.get_function[data.size()] return keccak def create_keccak(self, data: BitVec, global_state): length = data.size() - data = simplify(data) - if data.symbolic and simplify(data) not in global_state.topo_keys: + simplify(data) + if data.symbolic and data not in global_state.topo_keys: + # New keccak if data.size() != 512: self.keccak_parent[data] = None - global_state.topo_keys.append(simplify(data)) + global_state.topo_keys.append(data) else: + # size of 512 usually means Concat(key, storage_slot_for_that_var) + # This is solidity specific stuff :( p1 = simplify(Extract(511, 256, data)) if p1.symbolic and p1 not in global_state.topo_keys: global_state.topo_keys.append(p1) @@ -59,19 +61,19 @@ class KeccakFunctionManager: constraints = [] try: - func, inverse = self.sizes[length] + func, inverse = self.get_function[length] except KeyError: func = Function("keccak256_{}".format(length), length, 256) inverse = Function("keccak256_{}-1".format(length), 256, length) - self.sizes[length] = (func, inverse) - self.size_values[length] = [] + self.get_function[length] = (func, inverse) + self.values_for_size[length] = [] flag_var = symbol_factory.BoolSym("{}_flag".format(hash(simplify(func(data))))) constraints.append(inverse(func(data)) == data) if data.symbolic is False: keccak = self.find_keccak(data) - self.size_values[length].append(keccak) + self.values_for_size[length].append(keccak) constraints.append(func(data) == keccak) constraints.append(flag_var) return keccak, constraints @@ -81,14 +83,14 @@ class KeccakFunctionManager: global_state.topo_keys.append(simplify(func(data))) try: - index = self.size_index[length] + index = self.interval_hook_for_size[length] except KeyError: - self.size_index[length] = self.index_counter - index = self.index_counter - self.index_counter -= INTERVAL_DIFFERENCE + self.interval_hook_for_size[length] = self._index_counter + index = self._index_counter + self._index_counter -= INTERVAL_DIFFERENCE lower_bound = index * PART - upper_bound = (index + 1) * PART + upper_bound = lower_bound + PART condition = And( ULE(symbol_factory.BitVecVal(lower_bound, 256), func(data)), @@ -98,37 +100,41 @@ class KeccakFunctionManager: f_cond = copy(condition) flag_condition = symbol_factory.Bool(False) total_keys = global_state.total_topo_keys - for val in self.size_values[length]: - if hash(simplify(func(data))) != hash(simplify(val)) and val in total_keys: - prev_flag_var = symbol_factory.BoolSym( - "{}_flag".format(hash(simplify(val))) + for val in self.values_for_size[length]: + if ( + hash(simplify(func(data))) == hash(simplify(val)) + or val not in total_keys + ): + continue + + other_keccak_condion = And( + func(data) == val, inverse(func(data)) == inverse(val) + ) + if val.value: + val_inverse = self.value_inverse[val] + flag_var2 = self.get_flag(val_inverse) + + other_keccak_condion = And(other_keccak_condion, flag_var, flag_var2) + else: + iter_val_flag_var = self.get_flag(simplify(val)) + other_keccak_condion = And( + other_keccak_condion, iter_val_flag_var, flag_var ) - pre_cond = And(func(data) == val, inverse(func(data)) == inverse(val)) - if val.value: - k2 = self.value_inverse[val] - flag_var2 = symbol_factory.BoolSym( - "{}_flag".format(hash(simplify(k2))) - ) - - pre_cond = And(pre_cond, flag_var, flag_var2) - else: - pre_cond = And(pre_cond, prev_flag_var, flag_var) - condition = Or(condition, pre_cond) - flag_condition = Or(flag_condition, pre_cond) + condition = Or(condition, other_keccak_condion) + flag_condition = Or(flag_condition, other_keccak_condion) self.flag_conditions[func(data)] = (f_cond, flag_condition, None) self.delete_constraints.append(condition) constraints.append(condition) - if func(data) not in self.size_values[length]: - self.size_values[length].append(func(data)) - if data not in self.keys: - self.keys.append(data) - if func(data) not in self.keys: - self.keys.append(func(data)) + if func(data) not in self.values_for_size[length]: + self.values_for_size[length].append(func(data)) return func(data), constraints + def get_flag(self, val: Expression) -> Bool: + return symbol_factory.BoolSym("{}_flag".format(hash(simplify(val)))) + keccak_function_manager = KeccakFunctionManager() diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 1596a95d..487c05e0 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -380,15 +380,7 @@ class LaserEVM: end_signal.global_state.world_state.node.constraints = ( global_state.mstate.constraints ) - for constraint in keccak_function_manager.delete_constraints: - try: - end_signal.global_state.world_state.node.constraints.remove( - constraint - ) - deleted_constraints = And(constraint, deleted_constraints) - except ValueError: - # Constraint not related to this state - continue + self.delete_constraints(end_signal.global_state) end_signal.global_state.world_state.node.constraints.append( And(Or(constraints, deleted_constraints), v) @@ -409,12 +401,7 @@ class LaserEVM: And(Or(constraints, deleted_constraints), v) ) global_state.mstate.constraints.weighted += w - for constraint in keccak_function_manager.delete_constraints: - try: - return_global_state.mstate.constraints.remove(constraint) - except ValueError: - # Constraint not related to this state - continue + self.delete_constraints(return_global_state) # Propogate codecall based annotations if return_global_state.get_current_instruction()["opcode"] in ( @@ -440,11 +427,19 @@ class LaserEVM: return new_global_states, op_code + def delete_constraints(self, global_state): + for constraint in keccak_function_manager.delete_constraints: + try: + global_state.world_state.node.constraints.remove(constraint) + except ValueError: + # Constraint not related to this state + continue + def concretize_keccak(self, global_state, gs): sender = global_state.environment.sender model_tuples = [] for actor in ACTOR_ADDRESSES: - model_tuples.append([True, sender == actor, actor]) + model_tuples.append([sender == actor, actor]) stored_vals = {} var_conds = True @@ -457,22 +452,24 @@ class LaserEVM: var_cond = False if keccak_function_manager.keccak_parent[key] is None: for model_tuple in model_tuples: - if model_tuple[0] is None: - continue if key.size() == 256: concrete_input = symbol_factory.BitVecVal( randint(0, 2 ** 160 - 1), 160 ) - func = Function("keccak256_{}".format(160), 160, 256) - inverse = Function("keccak256_{}-1".format(160), 256, 160) - keccak_function_manager.sizes[160] = (func, inverse) - if 160 not in keccak_function_manager.size_values: - keccak_function_manager.size_values[160] = [] + try: + func, inverse = keccak_function_manager.get_function[160] + except KeyError: + func = Function("keccak256_{}".format(160), 160, 256) + inverse = Function("keccak256_{}-1".format(160), 256, 160) + keccak_function_manager.get_function[160] = (func, inverse) + keccak_function_manager.values_for_size[160] = [] concrete_val_i = keccak_function_manager.find_keccak( concrete_input ) keccak_function_manager.value_inverse[concrete_val_i] = key - keccak_function_manager.size_values[160].append(concrete_val_i) + keccak_function_manager.values_for_size[160].append( + concrete_val_i + ) gs.topo_keys.append(concrete_val_i) hash_cond = And( hash_cond, @@ -487,32 +484,30 @@ class LaserEVM: concrete_val_i, key.size() ) var_cond = Or(var_cond, key == concrete_val_i) - model_tuple[1] = And(model_tuple[1], key == concrete_val_i) + model_tuple[0] = And(model_tuple[0], key == concrete_val_i) if key not in stored_vals: stored_vals[key] = {} - stored_vals[key][model_tuple[2]] = concrete_val_i + stored_vals[key][model_tuple[1]] = concrete_val_i else: parent = keccak_function_manager.keccak_parent[key] if parent.size() == 512: parent1 = Extract(511, 256, parent) parent2 = Extract(255, 0, parent) for model_tuple in model_tuples: - if model_tuple[0] is None: - continue if parent.size() == 512: if parent1.symbolic: - parent1 = stored_vals[parent1][model_tuple[2]] + parent1 = stored_vals[parent1][model_tuple[1]] if not isinstance(parent1, BitVec): parent1 = BitVec(parent1) concrete_parent = Concat(parent1, parent2) else: - concrete_parent = stored_vals[parent][model_tuple[2]] + concrete_parent = stored_vals[parent][model_tuple[1]] keccak_val = keccak_function_manager.find_keccak(concrete_parent) if key not in stored_vals: stored_vals[key] = {} - stored_vals[key][model_tuple[2]] = keccak_val - model_tuple[1] = And(model_tuple[1], key == keccak_val) + stored_vals[key][model_tuple[1]] = keccak_val + model_tuple[0] = And(model_tuple[0], key == keccak_val) var_cond = Or(var_cond, key == keccak_val) try: f1, f2, _ = keccak_function_manager.flag_conditions[simplify(key)] @@ -523,21 +518,16 @@ class LaserEVM: var_cond, ) flag_weights.append(flag_var) - except KeyError as e: + except KeyError: var_cond = And( Or(And(flag_var, var_cond), Not(And(flag_var, var_cond))), hash_cond ) flag_weights.append(flag_var) var_conds = And(var_conds, var_cond) new_condition = False - z3.set_option( - max_args=10000000, - max_lines=100000000, - max_depth=10000000, - max_visited=1000000, - ) + for model_tuple in model_tuples: - new_condition = Or(model_tuple[1], new_condition) + new_condition = Or(model_tuple[0], new_condition) constraints = global_state.mstate.constraints deleted_constraints = True for constraint in keccak_function_manager.delete_constraints: From c5b8ae87b2b68c1843dab19570117fdddda7ef84 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sat, 28 Sep 2019 16:42:51 +0100 Subject: [PATCH 18/54] Push concolic Node changes --- mythril/laser/ethereum/transaction/concolic.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/mythril/laser/ethereum/transaction/concolic.py b/mythril/laser/ethereum/transaction/concolic.py index 164df8db..f995a584 100644 --- a/mythril/laser/ethereum/transaction/concolic.py +++ b/mythril/laser/ethereum/transaction/concolic.py @@ -88,6 +88,9 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None: condition=None, ) ) + global_state.mstate.constraints += transaction.world_state.node.constraints + new_node.constraints = global_state.mstate.constraints + global_state.world_state.transaction_sequence.append(transaction) global_state.node = new_node new_node.states.append(global_state) From 90950756d3d7d23325ca57e0f83b488f35142444 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sat, 28 Sep 2019 17:06:37 +0100 Subject: [PATCH 19/54] Handle few edge cases --- mythril/laser/ethereum/svm.py | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 487c05e0..15d31514 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -380,7 +380,7 @@ class LaserEVM: end_signal.global_state.world_state.node.constraints = ( global_state.mstate.constraints ) - self.delete_constraints(end_signal.global_state) + self.delete_constraints(end_signal.global_state.node.constraints) end_signal.global_state.world_state.node.constraints.append( And(Or(constraints, deleted_constraints), v) @@ -401,7 +401,7 @@ class LaserEVM: And(Or(constraints, deleted_constraints), v) ) global_state.mstate.constraints.weighted += w - self.delete_constraints(return_global_state) + self.delete_constraints(return_global_state.mstate.constraints) # Propogate codecall based annotations if return_global_state.get_current_instruction()["opcode"] in ( @@ -427,10 +427,10 @@ class LaserEVM: return new_global_states, op_code - def delete_constraints(self, global_state): + def delete_constraints(self, constraints): for constraint in keccak_function_manager.delete_constraints: try: - global_state.world_state.node.constraints.remove(constraint) + constraints.remove(constraint) except ValueError: # Constraint not related to this state continue @@ -497,8 +497,9 @@ class LaserEVM: if parent.size() == 512: if parent1.symbolic: parent1 = stored_vals[parent1][model_tuple[1]] - if not isinstance(parent1, BitVec): - parent1 = BitVec(parent1) + if parent2.symbolic: + parent2 = stored_vals[parent2][model_tuple[1]] + concrete_parent = Concat(parent1, parent2) else: concrete_parent = stored_vals[parent][model_tuple[1]] From 7e84ead7dc9d6faa1c53b93bf6ff26a0da50a74a Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 29 Sep 2019 17:19:09 +0100 Subject: [PATCH 20/54] Add type hints and remove redundant storing --- mythril/laser/ethereum/instructions.py | 2 +- .../laser/ethereum/keccak_function_manager.py | 22 ++++++++++--------- mythril/laser/ethereum/svm.py | 17 +++++++------- 3 files changed, 21 insertions(+), 20 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index fb034bae..b2e65550 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -979,7 +979,7 @@ class Instruction: if isinstance(op0, Expression): op0 = simplify(op0) state.stack.append( - symbol_factory.BitVecSym("KECCAC_mem[" + str(hash(op0)) + "]", 256) + symbol_factory.BitVecSym("KECCAC_mem[{}]".format(hash(op0)), 256) ) gas_tuple = cast(Tuple, OPCODE_GAS["SHA3"]) state.min_gas_used += gas_tuple[0] diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 881fe68c..783cd662 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -1,5 +1,6 @@ from copy import copy from ethereum import utils +from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.smt import ( BitVec, Bool, @@ -14,6 +15,7 @@ from mythril.laser.smt import ( simplify, Extract, ) +from typing import Dict, Tuple, Optional, List TOTAL_PARTS = 10 ** 40 PART = (2 ** 256 - 1) // TOTAL_PARTS @@ -22,14 +24,14 @@ INTERVAL_DIFFERENCE = 10 ** 30 class KeccakFunctionManager: def __init__(self): - self.get_function = {} - self.interval_hook_for_size = {} - self.keccak_parent = {} - self.values_for_size = {} - self.delete_constraints = [] - self.flag_conditions = {} - self.value_inverse = {} - self._index_counter = TOTAL_PARTS - 34534 + self.get_function: Dict[int, Tuple[Function, Function]] = {} + self.interval_hook_for_size: Dict[int, int] = {} + self.keccak_parent: Dict[BitVec, Optional[BitVec]] = {} + self.values_for_size: Dict[int, List[BitVec]] = {} + self.delete_constraints: List[Bool] = [] + self.flag_conditions: Dict[BitVec, Tuple[Bool, Bool]] = {} + self.value_inverse: Dict[BitVec, BitVec] = {} + self._index_counter: int = TOTAL_PARTS - 34534 def find_keccak(self, data: BitVec) -> BitVec: keccak = symbol_factory.BitVecVal( @@ -42,7 +44,7 @@ class KeccakFunctionManager: func, _ = self.get_function[data.size()] return keccak - def create_keccak(self, data: BitVec, global_state): + def create_keccak(self, data: BitVec, global_state: GlobalState): length = data.size() simplify(data) @@ -124,7 +126,7 @@ class KeccakFunctionManager: condition = Or(condition, other_keccak_condion) flag_condition = Or(flag_condition, other_keccak_condion) - self.flag_conditions[func(data)] = (f_cond, flag_condition, None) + self.flag_conditions[func(data)] = (f_cond, flag_condition) self.delete_constraints.append(condition) constraints.append(condition) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 15d31514..9d817480 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -435,7 +435,7 @@ class LaserEVM: # Constraint not related to this state continue - def concretize_keccak(self, global_state, gs): + def concretize_keccak(self, global_state: GlobalState, gs: GlobalState): sender = global_state.environment.sender model_tuples = [] for actor in ACTOR_ADDRESSES: @@ -453,6 +453,7 @@ class LaserEVM: if keccak_function_manager.keccak_parent[key] is None: for model_tuple in model_tuples: if key.size() == 256: + # TODO: Support other hash lengths concrete_input = symbol_factory.BitVecVal( randint(0, 2 ** 160 - 1), 160 ) @@ -490,6 +491,7 @@ class LaserEVM: stored_vals[key][model_tuple[1]] = concrete_val_i else: parent = keccak_function_manager.keccak_parent[key] + # TODO: Generalise this than for just solc if parent.size() == 512: parent1 = Extract(511, 256, parent) parent2 = Extract(255, 0, parent) @@ -502,8 +504,10 @@ class LaserEVM: concrete_parent = Concat(parent1, parent2) else: - concrete_parent = stored_vals[parent][model_tuple[1]] - + try: + concrete_parent = stored_vals[parent][model_tuple[1]] + except KeyError: + continue keccak_val = keccak_function_manager.find_keccak(concrete_parent) if key not in stored_vals: stored_vals[key] = {} @@ -511,13 +515,8 @@ class LaserEVM: model_tuple[0] = And(model_tuple[0], key == keccak_val) var_cond = Or(var_cond, key == keccak_val) try: - f1, f2, _ = keccak_function_manager.flag_conditions[simplify(key)] + f1, f2 = keccak_function_manager.flag_conditions[simplify(key)] var_cond = And(Or(var_cond, f2) == flag_var, f1 == Not(flag_var)) - keccak_function_manager.flag_conditions[simplify(key)] = ( - f1, - f2, - var_cond, - ) flag_weights.append(flag_var) except KeyError: var_cond = And( From 759c778f3a52dc386fd88eb9d93a15a3aa19a531 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 29 Sep 2019 17:29:46 +0100 Subject: [PATCH 21/54] Fix type hints --- mythril/laser/ethereum/svm.py | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 9d817480..97aff5c4 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -441,15 +441,15 @@ class LaserEVM: for actor in ACTOR_ADDRESSES: model_tuples.append([sender == actor, actor]) - stored_vals = {} - var_conds = True + stored_vals: Dict[BitVec, Dict[BitVec, BitVec]] = {} + var_conds = symbol_factory.Bool(True) flag_weights = [] - hash_cond = True + hash_cond = symbol_factory.Bool(True) for index, key in enumerate(global_state.topo_keys): if key.value: continue flag_var = symbol_factory.BoolSym("{}_flag".format(hash(simplify(key)))) - var_cond = False + var_cond = symbol_factory.Bool(False) if keccak_function_manager.keccak_parent[key] is None: for model_tuple in model_tuples: if key.size() == 256: @@ -479,10 +479,10 @@ class LaserEVM: ) var_cond = Or(var_cond, key == concrete_val_i) else: - concrete_val_i = randint(0, 2 ** key.size() - 1) + concrete_val = randint(0, 2 ** key.size() - 1) concrete_val_i = symbol_factory.BitVecVal( - concrete_val_i, key.size() + concrete_val, key.size() ) var_cond = Or(var_cond, key == concrete_val_i) model_tuple[0] = And(model_tuple[0], key == concrete_val_i) @@ -517,19 +517,18 @@ class LaserEVM: try: f1, f2 = keccak_function_manager.flag_conditions[simplify(key)] var_cond = And(Or(var_cond, f2) == flag_var, f1 == Not(flag_var)) - flag_weights.append(flag_var) except KeyError: var_cond = And( Or(And(flag_var, var_cond), Not(And(flag_var, var_cond))), hash_cond ) - flag_weights.append(flag_var) + flag_weights.append(flag_var) var_conds = And(var_conds, var_cond) - new_condition = False + new_condition = symbol_factory.Bool(False) for model_tuple in model_tuples: new_condition = Or(model_tuple[0], new_condition) constraints = global_state.mstate.constraints - deleted_constraints = True + deleted_constraints = symbol_factory.Bool(True) for constraint in keccak_function_manager.delete_constraints: try: constraints.remove(constraint) @@ -538,8 +537,8 @@ class LaserEVM: # Constraint not related to this state continue - if deleted_constraints is True: - deleted_constraints = False + if deleted_constraints.is_true: + deleted_constraints = symbol_factory.Bool(False) var_conds = And(var_conds, hash_cond) new_condition = simplify(new_condition) return new_condition, deleted_constraints, var_conds, flag_weights From 00bf44d00d7b6cd8f84475de238d851b93c118e3 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 30 Sep 2019 20:00:54 +0100 Subject: [PATCH 22/54] Use Constraint()'s weight --- mythril/analysis/solver.py | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index b33b3979..b8eccfeb 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -21,9 +21,7 @@ log = logging.getLogger(__name__) # LRU cache works great when used in powers of 2 @lru_cache(maxsize=2 ** 23) -def get_model( - constraints, minimize=(), maximize=(), enforce_execution_time=True, weighted=() -): +def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True): """ :param constraints: @@ -42,7 +40,10 @@ def get_model( for constraint in constraints: if type(constraint) == bool and not constraint: raise UnsatError - + if isinstance(constraints, Constraints): + weighted = constraints.weighted + else: + weighted = [] constraints = [constraint for constraint in constraints if type(constraint) != bool] for constraint in constraints: @@ -103,7 +104,7 @@ def get_transaction_sequence( ) weighted = tx_constraints.weighted try: - model = get_model(tx_constraints, minimize=minimize, weighted=tuple(weighted)) + model = get_model(tx_constraints, minimize=minimize) except UnsatError: raise UnsatError From 652e791ed744f42750f38401378e51f6c093ce6c Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 30 Sep 2019 20:04:00 +0100 Subject: [PATCH 23/54] Remove weighted param --- mythril/analysis/solver.py | 1 - 1 file changed, 1 deletion(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index b8eccfeb..45c06b98 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -102,7 +102,6 @@ def get_transaction_sequence( tx_constraints, minimize = _set_minimisation_constraints( transaction_sequence, constraints.copy(), [], 5000, global_state.world_state ) - weighted = tx_constraints.weighted try: model = get_model(tx_constraints, minimize=minimize) except UnsatError: From e8330f5bb54d831e4995f994f93dee7ff8c64840 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 7 Oct 2019 15:35:56 +0100 Subject: [PATCH 24/54] Save status --- mythril/analysis/modules/exceptions.py | 5 ++--- mythril/laser/ethereum/state/constraints.py | 2 +- mythril/laser/smt/bitvec_helper.py | 2 +- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index 804df576..33709ca7 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -43,7 +43,7 @@ class ReachableExceptionsModule(DetectionModule): :param state: :return: """ - log.debug("ASSERT_FAIL in function " + state.environment.active_function_name) + log.info("ASSERT_FAIL in function " + state.environment.active_function_name) try: address = state.get_current_instruction()["address"] @@ -55,11 +55,10 @@ class ReachableExceptionsModule(DetectionModule): "Note that explicit `assert()` should only be used to check invariants. " "Use `require()` for regular input checking." ) - + print(state.mstate.constraints) transaction_sequence = solver.get_transaction_sequence( state, state.mstate.constraints ) - issue = Issue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index a39e6117..6a9fdae6 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -28,7 +28,7 @@ class Constraints(list): constraint_list = constraint_list or [] constraint_list = self._get_smt_bool_list(constraint_list) super(Constraints, self).__init__(constraint_list) - self._default_timeout = 100 + self._default_timeout = 300 self._is_possible = is_possible self.weighted = [] # type: List[Bool] diff --git a/mythril/laser/smt/bitvec_helper.py b/mythril/laser/smt/bitvec_helper.py index 56ac64b3..425e83de 100644 --- a/mythril/laser/smt/bitvec_helper.py +++ b/mythril/laser/smt/bitvec_helper.py @@ -9,7 +9,7 @@ from mythril.laser.smt.bitvecfunc import _arithmetic_helper as _func_arithmetic_ from mythril.laser.smt.bitvecfunc import _comparison_helper as _func_comparison_helper Annotations = Set[Any] - +z3.set_option(max_args=10000000, max_lines=100000000, max_depth=10000000, max_visited=1000000) def _comparison_helper( a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool From b51fd818488498454c6d91bcc7a22b87acd84366 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sat, 12 Oct 2019 21:54:00 +0100 Subject: [PATCH 25/54] Use different method --- mythril/analysis/modules/exceptions.py | 1 - mythril/analysis/solver.py | 16 ++- mythril/laser/ethereum/instructions.py | 2 +- .../laser/ethereum/keccak_function_manager.py | 111 +++++++----------- mythril/laser/ethereum/svm.py | 29 +++-- mythril/laser/smt/bitvec_helper.py | 5 +- 6 files changed, 79 insertions(+), 85 deletions(-) diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index 33709ca7..80be8f78 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -55,7 +55,6 @@ class ReachableExceptionsModule(DetectionModule): "Note that explicit `assert()` should only be used to check invariants. " "Use `require()` for regular input checking." ) - print(state.mstate.constraints) transaction_sequence = solver.get_transaction_sequence( state, state.mstate.constraints ) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 45c06b98..3b9ad108 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -126,12 +126,26 @@ def get_transaction_sequence( ).as_long() concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict) - + _replace_with_actual_sha(concrete_transactions, model) steps = {"initialState": concrete_initial_state, "steps": concrete_transactions} return steps +def _replace_with_actual_sha(concrete_transactions, model): + for tx in concrete_transactions: + if "fffffff" not in tx["input"]: + continue + find_input = symbol_factory.BitVecVal(int(tx["input"][10:74], 16), 256) + _, inverse = keccak_function_manager.get_function(160) + input_ = symbol_factory.BitVecVal( + model.eval(inverse(find_input).raw).as_long(), 160 + ) + keccak = keccak_function_manager.find_keccak(input_) + tx["input"] = tx["input"].replace(tx["input"][10:74], hex(keccak.value)[2:]) + print(find_input, input_, hex(keccak.value)) + + def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): """ Gets a concrete state """ accounts = {} diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b2e65550..01ba863c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1001,7 +1001,7 @@ class Instruction: # length is 0; this only matters for input of the BitVecFuncVal data = symbol_factory.BitVecVal(0, 1) - result, constraints = keccak_function_manager.create_keccak(data, global_state) + result, constraints = keccak_function_manager.create_keccak(data) state.stack.append(result) state.constraints += constraints diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 783cd662..1a7e69ab 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -1,6 +1,8 @@ from copy import copy from ethereum import utils +from random import randint from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.smt import ( BitVec, Bool, @@ -24,13 +26,9 @@ INTERVAL_DIFFERENCE = 10 ** 30 class KeccakFunctionManager: def __init__(self): - self.get_function: Dict[int, Tuple[Function, Function]] = {} + self.store_function: Dict[int, Tuple[Function, Function]] = {} self.interval_hook_for_size: Dict[int, int] = {} - self.keccak_parent: Dict[BitVec, Optional[BitVec]] = {} self.values_for_size: Dict[int, List[BitVec]] = {} - self.delete_constraints: List[Bool] = [] - self.flag_conditions: Dict[BitVec, Tuple[Bool, Bool]] = {} - self.value_inverse: Dict[BitVec, BitVec] = {} self._index_counter: int = TOTAL_PARTS - 34534 def find_keccak(self, data: BitVec) -> BitVec: @@ -41,49 +39,32 @@ class KeccakFunctionManager: ), 256, ) - func, _ = self.get_function[data.size()] return keccak - def create_keccak(self, data: BitVec, global_state: GlobalState): - - length = data.size() - simplify(data) - if data.symbolic and data not in global_state.topo_keys: - # New keccak - if data.size() != 512: - self.keccak_parent[data] = None - global_state.topo_keys.append(data) - else: - # size of 512 usually means Concat(key, storage_slot_for_that_var) - # This is solidity specific stuff :( - p1 = simplify(Extract(511, 256, data)) - if p1.symbolic and p1 not in global_state.topo_keys: - global_state.topo_keys.append(p1) - self.keccak_parent[p1] = None - - constraints = [] + def get_function(self, length: int) -> Tuple[Function, Function]: try: - func, inverse = self.get_function[length] + func, inverse = self.store_function[length] except KeyError: func = Function("keccak256_{}".format(length), length, 256) inverse = Function("keccak256_{}-1".format(length), 256, length) - self.get_function[length] = (func, inverse) + self.store_function[length] = (func, inverse) self.values_for_size[length] = [] - flag_var = symbol_factory.BoolSym("{}_flag".format(hash(simplify(func(data))))) + return func, inverse - constraints.append(inverse(func(data)) == data) + def create_keccak(self, data: BitVec): + length = data.size() + simplify(data) + constraints = Constraints() + func, inverse = self.get_function(length) + constraints.append(inverse(func(data)) == data) + """ if data.symbolic is False: keccak = self.find_keccak(data) self.values_for_size[length].append(keccak) constraints.append(func(data) == keccak) - constraints.append(flag_var) return keccak, constraints - - if simplify(func(data)) not in global_state.topo_keys: - self.keccak_parent[simplify(func(data))] = data - global_state.topo_keys.append(simplify(func(data))) - + """ try: index = self.interval_hook_for_size[length] except KeyError: @@ -99,44 +80,42 @@ class KeccakFunctionManager: ULT(func(data), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) - f_cond = copy(condition) - flag_condition = symbol_factory.Bool(False) - total_keys = global_state.total_topo_keys for val in self.values_for_size[length]: - if ( - hash(simplify(func(data))) == hash(simplify(val)) - or val not in total_keys - ): + if hash(simplify(func(data))) == hash(simplify(val)): continue - - other_keccak_condion = And( - func(data) == val, inverse(func(data)) == inverse(val) - ) - if val.value: - val_inverse = self.value_inverse[val] - flag_var2 = self.get_flag(val_inverse) - - other_keccak_condion = And(other_keccak_condion, flag_var, flag_var2) - else: - iter_val_flag_var = self.get_flag(simplify(val)) - other_keccak_condion = And( - other_keccak_condion, iter_val_flag_var, flag_var - ) - - condition = Or(condition, other_keccak_condion) - flag_condition = Or(flag_condition, other_keccak_condion) - - self.flag_conditions[func(data)] = (f_cond, flag_condition) - self.delete_constraints.append(condition) + condition = Or(condition, func(data) == val) constraints.append(condition) - if func(data) not in self.values_for_size[length]: - self.values_for_size[length].append(func(data)) - + # if func(data) not in self.values_for_size[length]: + # self.values_for_size[length].append(func(data)) return func(data), constraints - def get_flag(self, val: Expression) -> Bool: - return symbol_factory.BoolSym("{}_flag".format(hash(simplify(val)))) + def get_new_cond(self, val, length: int): + new_func, new_inv = self.get_function(length) + random_number = symbol_factory.BitVecSym( + "randval_{}".format(randint(0, 10000)), length + ) + cond = And( + new_func(random_number) == val, + new_inv(new_func(random_number)) == random_number, + ) + try: + index = self.interval_hook_for_size[length] + except KeyError: + self.interval_hook_for_size[length] = self._index_counter + index = self._index_counter + self._index_counter -= INTERVAL_DIFFERENCE + + lower_bound = index * PART + upper_bound = lower_bound + PART + + cond = And( + cond, + ULE(symbol_factory.BitVecVal(lower_bound, 256), new_func(random_number)), + ULT(new_func(random_number), symbol_factory.BitVecVal(upper_bound, 256)), + URem(new_func(random_number), symbol_factory.BitVecVal(64, 256)) == 0, + ) + return cond keccak_function_manager = KeccakFunctionManager() diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 97aff5c4..2ad0e31c 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -371,12 +371,17 @@ class LaserEVM: not isinstance(transaction, ContractCreationTransaction) or transaction.return_data ) and not end_signal.revert: - constraints, deleted_constraints, v, w = self.concretize_keccak( - global_state, end_signal.global_state - ) check_potential_issues(global_state) + first_arg1 = transaction.call_data.get_word_at(4) + global_state.node.constraints.weighted.append( + keccak_function_manager.get_new_cond(first_arg1, 160) + ) end_signal.global_state.world_state.node = global_state.node + """ + constraints, deleted_constraints, v, w = self.concretize_keccak( + global_state, end_signal.global_state + ) end_signal.global_state.world_state.node.constraints = ( global_state.mstate.constraints ) @@ -385,23 +390,25 @@ class LaserEVM: end_signal.global_state.world_state.node.constraints.append( And(Or(constraints, deleted_constraints), v) ) - + end_signal.global_state.world_state.node.constraints.weighted += w - + """ self._add_world_state(end_signal.global_state) new_global_states = [] else: # First execute the post hook for the transaction ending instruction self._execute_post_hook(op_code, [end_signal.global_state]) + """ constraints, deleted_constraints, v, w = self.concretize_keccak( global_state, end_signal.global_state ) global_state.mstate.constraints.append( And(Or(constraints, deleted_constraints), v) ) - global_state.mstate.constraints.weighted += w - self.delete_constraints(return_global_state.mstate.constraints) + """ + # global_state.mstate.constraints.weighted += w + # self.delete_constraints(return_global_state.mstate.constraints) # Propogate codecall based annotations if return_global_state.get_current_instruction()["opcode"] in ( @@ -427,14 +434,6 @@ class LaserEVM: return new_global_states, op_code - def delete_constraints(self, constraints): - for constraint in keccak_function_manager.delete_constraints: - try: - constraints.remove(constraint) - except ValueError: - # Constraint not related to this state - continue - def concretize_keccak(self, global_state: GlobalState, gs: GlobalState): sender = global_state.environment.sender model_tuples = [] diff --git a/mythril/laser/smt/bitvec_helper.py b/mythril/laser/smt/bitvec_helper.py index 425e83de..af03aba0 100644 --- a/mythril/laser/smt/bitvec_helper.py +++ b/mythril/laser/smt/bitvec_helper.py @@ -9,7 +9,10 @@ from mythril.laser.smt.bitvecfunc import _arithmetic_helper as _func_arithmetic_ from mythril.laser.smt.bitvecfunc import _comparison_helper as _func_comparison_helper Annotations = Set[Any] -z3.set_option(max_args=10000000, max_lines=100000000, max_depth=10000000, max_visited=1000000) +z3.set_option( + max_args=10000000, max_lines=100000000, max_depth=10000000, max_visited=1000000 +) + def _comparison_helper( a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool From b62c34705e75839f3ecbdb01d0cc2575fe1115a9 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 13 Oct 2019 00:44:14 +0100 Subject: [PATCH 26/54] refactor the code --- mythril/analysis/solver.py | 1 - 1 file changed, 1 deletion(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 3b9ad108..58d51458 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -143,7 +143,6 @@ def _replace_with_actual_sha(concrete_transactions, model): ) keccak = keccak_function_manager.find_keccak(input_) tx["input"] = tx["input"].replace(tx["input"][10:74], hex(keccak.value)[2:]) - print(find_input, input_, hex(keccak.value)) def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): From 79faa94820f0848e57dfccf61937f24154997ecd Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 13 Oct 2019 00:50:15 +0100 Subject: [PATCH 27/54] fix type fixes --- .../laser/ethereum/keccak_function_manager.py | 18 +-- mythril/laser/ethereum/svm.py | 133 ------------------ 2 files changed, 2 insertions(+), 149 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 1a7e69ab..3a73dc56 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -28,7 +28,6 @@ class KeccakFunctionManager: def __init__(self): self.store_function: Dict[int, Tuple[Function, Function]] = {} self.interval_hook_for_size: Dict[int, int] = {} - self.values_for_size: Dict[int, List[BitVec]] = {} self._index_counter: int = TOTAL_PARTS - 34534 def find_keccak(self, data: BitVec) -> BitVec: @@ -48,7 +47,6 @@ class KeccakFunctionManager: func = Function("keccak256_{}".format(length), length, 256) inverse = Function("keccak256_{}-1".format(length), 256, length) self.store_function[length] = (func, inverse) - self.values_for_size[length] = [] return func, inverse def create_keccak(self, data: BitVec): @@ -58,13 +56,7 @@ class KeccakFunctionManager: constraints = Constraints() func, inverse = self.get_function(length) constraints.append(inverse(func(data)) == data) - """ - if data.symbolic is False: - keccak = self.find_keccak(data) - self.values_for_size[length].append(keccak) - constraints.append(func(data) == keccak) - return keccak, constraints - """ + try: index = self.interval_hook_for_size[length] except KeyError: @@ -80,14 +72,8 @@ class KeccakFunctionManager: ULT(func(data), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) - for val in self.values_for_size[length]: - if hash(simplify(func(data))) == hash(simplify(val)): - continue - condition = Or(condition, func(data) == val) - constraints.append(condition) - # if func(data) not in self.values_for_size[length]: - # self.values_for_size[length].append(func(data)) + return func(data), constraints def get_new_cond(self, val, length: int): diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 2ad0e31c..3a9d8f24 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -378,37 +378,12 @@ class LaserEVM: ) end_signal.global_state.world_state.node = global_state.node - """ - constraints, deleted_constraints, v, w = self.concretize_keccak( - global_state, end_signal.global_state - ) - end_signal.global_state.world_state.node.constraints = ( - global_state.mstate.constraints - ) - self.delete_constraints(end_signal.global_state.node.constraints) - - end_signal.global_state.world_state.node.constraints.append( - And(Or(constraints, deleted_constraints), v) - ) - - end_signal.global_state.world_state.node.constraints.weighted += w - """ self._add_world_state(end_signal.global_state) new_global_states = [] else: # First execute the post hook for the transaction ending instruction self._execute_post_hook(op_code, [end_signal.global_state]) - """ - constraints, deleted_constraints, v, w = self.concretize_keccak( - global_state, end_signal.global_state - ) - global_state.mstate.constraints.append( - And(Or(constraints, deleted_constraints), v) - ) - """ - # global_state.mstate.constraints.weighted += w - # self.delete_constraints(return_global_state.mstate.constraints) # Propogate codecall based annotations if return_global_state.get_current_instruction()["opcode"] in ( @@ -434,114 +409,6 @@ class LaserEVM: return new_global_states, op_code - def concretize_keccak(self, global_state: GlobalState, gs: GlobalState): - sender = global_state.environment.sender - model_tuples = [] - for actor in ACTOR_ADDRESSES: - model_tuples.append([sender == actor, actor]) - - stored_vals: Dict[BitVec, Dict[BitVec, BitVec]] = {} - var_conds = symbol_factory.Bool(True) - flag_weights = [] - hash_cond = symbol_factory.Bool(True) - for index, key in enumerate(global_state.topo_keys): - if key.value: - continue - flag_var = symbol_factory.BoolSym("{}_flag".format(hash(simplify(key)))) - var_cond = symbol_factory.Bool(False) - if keccak_function_manager.keccak_parent[key] is None: - for model_tuple in model_tuples: - if key.size() == 256: - # TODO: Support other hash lengths - concrete_input = symbol_factory.BitVecVal( - randint(0, 2 ** 160 - 1), 160 - ) - try: - func, inverse = keccak_function_manager.get_function[160] - except KeyError: - func = Function("keccak256_{}".format(160), 160, 256) - inverse = Function("keccak256_{}-1".format(160), 256, 160) - keccak_function_manager.get_function[160] = (func, inverse) - keccak_function_manager.values_for_size[160] = [] - concrete_val_i = keccak_function_manager.find_keccak( - concrete_input - ) - keccak_function_manager.value_inverse[concrete_val_i] = key - keccak_function_manager.values_for_size[160].append( - concrete_val_i - ) - gs.topo_keys.append(concrete_val_i) - hash_cond = And( - hash_cond, - func(concrete_input) == concrete_val_i, - inverse(concrete_val_i) == concrete_input, - ) - var_cond = Or(var_cond, key == concrete_val_i) - else: - concrete_val = randint(0, 2 ** key.size() - 1) - - concrete_val_i = symbol_factory.BitVecVal( - concrete_val, key.size() - ) - var_cond = Or(var_cond, key == concrete_val_i) - model_tuple[0] = And(model_tuple[0], key == concrete_val_i) - if key not in stored_vals: - stored_vals[key] = {} - stored_vals[key][model_tuple[1]] = concrete_val_i - else: - parent = keccak_function_manager.keccak_parent[key] - # TODO: Generalise this than for just solc - if parent.size() == 512: - parent1 = Extract(511, 256, parent) - parent2 = Extract(255, 0, parent) - for model_tuple in model_tuples: - if parent.size() == 512: - if parent1.symbolic: - parent1 = stored_vals[parent1][model_tuple[1]] - if parent2.symbolic: - parent2 = stored_vals[parent2][model_tuple[1]] - - concrete_parent = Concat(parent1, parent2) - else: - try: - concrete_parent = stored_vals[parent][model_tuple[1]] - except KeyError: - continue - keccak_val = keccak_function_manager.find_keccak(concrete_parent) - if key not in stored_vals: - stored_vals[key] = {} - stored_vals[key][model_tuple[1]] = keccak_val - model_tuple[0] = And(model_tuple[0], key == keccak_val) - var_cond = Or(var_cond, key == keccak_val) - try: - f1, f2 = keccak_function_manager.flag_conditions[simplify(key)] - var_cond = And(Or(var_cond, f2) == flag_var, f1 == Not(flag_var)) - except KeyError: - var_cond = And( - Or(And(flag_var, var_cond), Not(And(flag_var, var_cond))), hash_cond - ) - flag_weights.append(flag_var) - var_conds = And(var_conds, var_cond) - new_condition = symbol_factory.Bool(False) - - for model_tuple in model_tuples: - new_condition = Or(model_tuple[0], new_condition) - constraints = global_state.mstate.constraints - deleted_constraints = symbol_factory.Bool(True) - for constraint in keccak_function_manager.delete_constraints: - try: - constraints.remove(constraint) - deleted_constraints = And(constraint, deleted_constraints) - except ValueError: - # Constraint not related to this state - continue - - if deleted_constraints.is_true: - deleted_constraints = symbol_factory.Bool(False) - var_conds = And(var_conds, hash_cond) - new_condition = simplify(new_condition) - return new_condition, deleted_constraints, var_conds, flag_weights - def _end_message_call( self, return_global_state: GlobalState, From 4c586f19813901f42793deb6a260411388e6f32c Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 13 Oct 2019 00:51:46 +0100 Subject: [PATCH 28/54] remove dead code --- mythril/laser/ethereum/keccak_function_manager.py | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 3a73dc56..f6537d17 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -1,23 +1,17 @@ -from copy import copy from ethereum import utils from random import randint -from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.smt import ( BitVec, - Bool, - Expression, Function, URem, symbol_factory, ULE, And, ULT, - Or, simplify, - Extract, ) -from typing import Dict, Tuple, Optional, List +from typing import Dict, Tuple TOTAL_PARTS = 10 ** 40 PART = (2 ** 256 - 1) // TOTAL_PARTS From f26067d186fa817bd03d6645dae756200255e12c Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 13 Oct 2019 01:16:46 +0100 Subject: [PATCH 29/54] remove dead code --- mythril/laser/ethereum/keccak_function_manager.py | 9 +++++---- tests/laser/evm_testsuite/evm_test.py | 12 ++++++++++-- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index f6537d17..452124b4 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -20,9 +20,10 @@ INTERVAL_DIFFERENCE = 10 ** 30 class KeccakFunctionManager: def __init__(self): - self.store_function: Dict[int, Tuple[Function, Function]] = {} - self.interval_hook_for_size: Dict[int, int] = {} - self._index_counter: int = TOTAL_PARTS - 34534 + self.store_function = {} # type: Dict[int, Tuple[Function, Function]] + self.interval_hook_for_size = {} # type: Dict[int, int] + self._index_counter = TOTAL_PARTS - 34534 + self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests def find_keccak(self, data: BitVec) -> BitVec: keccak = symbol_factory.BitVecVal( @@ -67,7 +68,7 @@ class KeccakFunctionManager: URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) constraints.append(condition) - + self.quick_inverse[func(data)] = data return func(data), constraints def get_new_cond(self, val, length: int): diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 244b5844..8afe3d14 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -1,5 +1,6 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.state.world_state import WorldState from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.transaction.concolic import execute_message_call @@ -117,7 +118,6 @@ def test_vmtest( # Arrange if test_name in ignored_test_names: return - world_state = WorldState() for address, details in pre_condition.items(): @@ -178,7 +178,15 @@ def test_vmtest( expected = int(value, 16) actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)] if isinstance(actual, Expression): - actual = actual.value + if ( + actual.symbolic + and actual in keccak_function_manager.quick_inverse + ): + actual = keccak_function_manager.find_keccak( + keccak_function_manager.quick_inverse[actual] + ) + else: + actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual else: if type(actual) == bytes: From 609b20f6da4f7311cc355401e87b29ad512f2710 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 13 Oct 2019 01:52:49 +0100 Subject: [PATCH 30/54] Remove useless code --- mythril/laser/ethereum/instructions.py | 4 +- .../laser/ethereum/keccak_function_manager.py | 50 ++++++------------- mythril/laser/ethereum/state/global_state.py | 11 ---- mythril/laser/ethereum/state/world_state.py | 9 ---- mythril/laser/ethereum/svm.py | 25 +--------- mythril/laser/smt/__init__.py | 1 - mythril/laser/smt/bitvec_helper.py | 18 +------ 7 files changed, 21 insertions(+), 97 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 01ba863c..5398ef14 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1001,9 +1001,9 @@ class Instruction: # length is 0; this only matters for input of the BitVecFuncVal data = symbol_factory.BitVecVal(0, 1) - result, constraints = keccak_function_manager.create_keccak(data) + result, condition = keccak_function_manager.create_keccak(data) state.stack.append(result) - state.constraints += constraints + state.constraints.append(condition) return [global_state] diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 452124b4..cc986040 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -1,6 +1,5 @@ from ethereum import utils from random import randint -from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.smt import ( BitVec, Function, @@ -9,7 +8,7 @@ from mythril.laser.smt import ( ULE, And, ULT, - simplify, + Bool, ) from typing import Dict, Tuple @@ -44,42 +43,23 @@ class KeccakFunctionManager: self.store_function[length] = (func, inverse) return func, inverse - def create_keccak(self, data: BitVec): - + def create_keccak(self, data: BitVec) -> Tuple[BitVec, Bool]: length = data.size() - simplify(data) - constraints = Constraints() - func, inverse = self.get_function(length) - constraints.append(inverse(func(data)) == data) - - try: - index = self.interval_hook_for_size[length] - except KeyError: - self.interval_hook_for_size[length] = self._index_counter - index = self._index_counter - self._index_counter -= INTERVAL_DIFFERENCE - - lower_bound = index * PART - upper_bound = lower_bound + PART - - condition = And( - ULE(symbol_factory.BitVecVal(lower_bound, 256), func(data)), - ULT(func(data), symbol_factory.BitVecVal(upper_bound, 256)), - URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, - ) - constraints.append(condition) + func, _ = self.get_function(length) + condition = self._create_condition(func_input=data, func_output=func(data)) self.quick_inverse[func(data)] = data - return func(data), constraints + return func(data), condition - def get_new_cond(self, val, length: int): - new_func, new_inv = self.get_function(length) + def get_new_cond(self, val, length: int) -> Bool: random_number = symbol_factory.BitVecSym( "randval_{}".format(randint(0, 10000)), length ) - cond = And( - new_func(random_number) == val, - new_inv(new_func(random_number)) == random_number, - ) + return self._create_condition(func_input=random_number, func_output=val) + + def _create_condition(self, func_input: BitVec, func_output: BitVec) -> Bool: + length = func_input.size() + func, inv = self.get_function(length) + cond = And(func(func_input) == func_output, inv(func(func_input)) == func_input) try: index = self.interval_hook_for_size[length] except KeyError: @@ -92,9 +72,9 @@ class KeccakFunctionManager: cond = And( cond, - ULE(symbol_factory.BitVecVal(lower_bound, 256), new_func(random_number)), - ULT(new_func(random_number), symbol_factory.BitVecVal(upper_bound, 256)), - URem(new_func(random_number), symbol_factory.BitVecVal(64, 256)) == 0, + ULE(symbol_factory.BitVecVal(lower_bound, 256), func(func_input)), + ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)), + URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0, ) return cond diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index b14c5f02..0e15209d 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -80,17 +80,6 @@ class GlobalState: annotations=[copy(a) for a in self._annotations], ) - @property - def topo_keys(self) -> List: - return self.world_state.topo_keys - - @property - def total_topo_keys(self): - ns = copy(self.world_state.old_topo_keys) - for t in self.world_state.topo_keys: - ns.add(t) - return ns - @property def accounts(self) -> Dict: """ diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 17f0038f..901fd6ca 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -32,18 +32,11 @@ class WorldState: self.node = None # type: Optional['Node'] self.transaction_sequence = transaction_sequence or [] self._annotations = annotations or [] - self.topo_keys = [] # type: List[BitVec] - self.old_topo_keys = set() # type: Set[BitVec] @property def accounts(self): return self._accounts - def reset_topo_keys(self): - for t in self.topo_keys: - self.old_topo_keys.add(t) - self.topo_keys = [] - def __getitem__(self, item: BitVec) -> Account: """Gets an account from the worldstate using item as key. @@ -67,8 +60,6 @@ class WorldState: transaction_sequence=self.transaction_sequence[:], annotations=new_annotations, ) - new_world_state.topo_keys = copy(self.topo_keys) - new_world_state.old_topo_keys = copy(self.old_topo_keys) new_world_state.balances = copy(self.balances) new_world_state.starting_balances = copy(self.starting_balances) for account in self._accounts.values(): diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 3a9d8f24..c2d883bb 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -4,7 +4,6 @@ from collections import defaultdict from copy import copy from datetime import datetime, timedelta from typing import Callable, Dict, DefaultDict, List, Tuple, Optional -import z3 from mythril.analysis.potential_issues import check_potential_issues from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType @@ -12,10 +11,7 @@ from mythril.laser.ethereum.evm_exceptions import StackUnderflowException from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.iprof import InstructionProfiler -from mythril.laser.ethereum.keccak_function_manager import ( - keccak_function_manager, - Function, -) +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( MutationAnnotation, @@ -33,23 +29,8 @@ from mythril.laser.ethereum.transaction import ( execute_contract_creation, execute_message_call, ) -from mythril.laser.smt import ( - symbol_factory, - And, - Or, - BitVec, - Extract, - simplify, - Concat, - Not, -) -from random import randint +from mythril.laser.smt import symbol_factory -ACTOR_ADDRESSES = [ - symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256), - symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256), - symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEE, 256), -] log = logging.getLogger(__name__) @@ -233,8 +214,6 @@ class LaserEVM: hook() execute_message_call(self, address) - for os in self.open_states: - os.reset_topo_keys() for hook in self._stop_sym_trans_hooks: hook() diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index c4c01236..89fe147b 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -16,7 +16,6 @@ from mythril.laser.smt.bitvec_helper import ( BVMulNoOverflow, BVSubNoUnderflow, LShR, - Implies, ) from mythril.laser.smt.bitvecfunc import BitVecFunc diff --git a/mythril/laser/smt/bitvec_helper.py b/mythril/laser/smt/bitvec_helper.py index af03aba0..c1f60607 100644 --- a/mythril/laser/smt/bitvec_helper.py +++ b/mythril/laser/smt/bitvec_helper.py @@ -1,17 +1,13 @@ -from typing import Union, overload, List, Set, cast, Any, Optional, Callable -from operator import lshift, rshift, ne, eq +from typing import Union, overload, List, Set, cast, Any, Callable import z3 -from mythril.laser.smt.bool import Bool, And, Or +from mythril.laser.smt.bool import Bool, Or from mythril.laser.smt.bitvec import BitVec from mythril.laser.smt.bitvecfunc import BitVecFunc from mythril.laser.smt.bitvecfunc import _arithmetic_helper as _func_arithmetic_helper from mythril.laser.smt.bitvecfunc import _comparison_helper as _func_comparison_helper Annotations = Set[Any] -z3.set_option( - max_args=10000000, max_lines=100000000, max_depth=10000000, max_visited=1000000 -) def _comparison_helper( @@ -72,16 +68,6 @@ def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> Bi return BitVec(z3.If(a.raw, b.raw, c.raw), union) -def Implies(a: Union[Bool, bool], b: Union[Bool, bool]) -> Union[Bool, bool]: - if not isinstance(a, Bool): - a = Bool(z3.BoolVal(a)) - if not isinstance(b, Bool): - b = Bool(z3.BoolVal(b)) - union = a.annotations.union(b.annotations) - - return Bool(z3.Implies(a.raw, b.raw), annotations=union) - - def UGT(a: BitVec, b: BitVec) -> Bool: """Create an unsigned greater than expression. From 967e948e7ac24adf6b4cae653a526bd398e0f3a9 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 13 Oct 2019 02:59:15 +0100 Subject: [PATCH 31/54] Remove changes in setup.py --- setup.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/setup.py b/setup.py index 5bb1cc0f..5955ab26 100755 --- a/setup.py +++ b/setup.py @@ -19,7 +19,7 @@ DESCRIPTION = "Security analysis tool for Ethereum smart contracts" URL = "https://github.com/ConsenSys/mythril" AUTHOR = "ConsenSys Dilligence" AUTHOR_MAIL = None -REQUIRES_PYTHON = ">=3.6.0" +REQUIRES_PYTHON = ">=3.5.0" # What packages are required for this module to be executed? @@ -118,6 +118,7 @@ setup( "Intended Audience :: Science/Research", "Topic :: Software Development :: Disassemblers", "License :: OSI Approved :: MIT License", + "Programming Language :: Python :: 3.5", "Programming Language :: Python :: 3.6", "Programming Language :: Python :: 3.7", ], From 92e727e31767af97795e1ea80dd4076a85f3a3e4 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 13 Oct 2019 13:03:15 +0100 Subject: [PATCH 32/54] Refactor code and support other args --- mythril/analysis/modules/suicide.py | 1 + mythril/analysis/solver.py | 48 +++++++++++-------- .../laser/ethereum/keccak_function_manager.py | 35 +++++++++----- mythril/laser/ethereum/state/constraints.py | 10 +--- mythril/laser/ethereum/svm.py | 5 -- mythril/laser/smt/solver/solver.py | 3 -- 6 files changed, 55 insertions(+), 47 deletions(-) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index 25123747..c6d0a6e4 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -10,6 +10,7 @@ from mythril.laser.ethereum.transaction.transaction_models import ( ) import logging + log = logging.getLogger(__name__) DESCRIPTION = """ diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 58d51458..74d838f1 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -1,15 +1,18 @@ """This module contains analysis module helpers to solve path constraints.""" from functools import lru_cache -from typing import Dict, Tuple, Union +from typing import Dict, List, Tuple, Union from z3 import sat, unknown, FuncInterp import z3 from mythril.analysis.analysis_args import analysis_args from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.constraints import Constraints -from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager +from mythril.laser.ethereum.keccak_function_manager import ( + keccak_function_manager, + hash_matcher, +) from mythril.laser.ethereum.transaction import BaseTransaction -from mythril.laser.smt import UGE, Optimize, symbol_factory, BitVec, simplify +from mythril.laser.smt import UGE, Optimize, symbol_factory from mythril.laser.ethereum.time_handler import time_handler from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction.transaction_models import ( @@ -40,10 +43,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True for constraint in constraints: if type(constraint) == bool and not constraint: raise UnsatError - if isinstance(constraints, Constraints): - weighted = constraints.weighted - else: - weighted = [] + constraints = [constraint for constraint in constraints if type(constraint) != bool] for constraint in constraints: @@ -52,8 +52,6 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True s.minimize(e) for e in maximize: s.maximize(e) - for e in weighted: - s.add_soft(e) result = s.check() if result == sat: return s.model() @@ -126,23 +124,35 @@ def get_transaction_sequence( ).as_long() concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict) - _replace_with_actual_sha(concrete_transactions, model) + if isinstance(transaction_sequence[0], ContractCreationTransaction): + _replace_with_actual_sha(concrete_transactions[1:], model) + else: + _replace_with_actual_sha(concrete_transactions, model) steps = {"initialState": concrete_initial_state, "steps": concrete_transactions} return steps -def _replace_with_actual_sha(concrete_transactions, model): +def _replace_with_actual_sha( + concrete_transactions: List[Dict[str, str]], model: z3.Model +): for tx in concrete_transactions: - if "fffffff" not in tx["input"]: + if hash_matcher not in tx["input"]: continue - find_input = symbol_factory.BitVecVal(int(tx["input"][10:74], 16), 256) - _, inverse = keccak_function_manager.get_function(160) - input_ = symbol_factory.BitVecVal( - model.eval(inverse(find_input).raw).as_long(), 160 - ) - keccak = keccak_function_manager.find_keccak(input_) - tx["input"] = tx["input"].replace(tx["input"][10:74], hex(keccak.value)[2:]) + for i in range(0, len(tx["input"]) - 73, 64): + if hash_matcher not in tx["input"][i + 10 : i + 74]: + continue + find_input = symbol_factory.BitVecVal( + int(tx["input"][10 + i : 74 + i], 16), 256 + ) + _, inverse = keccak_function_manager.get_function(160) + input_ = symbol_factory.BitVecVal( + model.eval(inverse(find_input).raw).as_long(), 160 + ) + keccak = keccak_function_manager.find_keccak(input_) + tx["input"] = tx["input"].replace( + tx["input"][10 + i : 74 + i], hex(keccak.value)[2:] + ) def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index cc986040..e3ed72d3 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -1,5 +1,4 @@ from ethereum import utils -from random import randint from mythril.laser.smt import ( BitVec, Function, @@ -15,6 +14,7 @@ from typing import Dict, Tuple TOTAL_PARTS = 10 ** 40 PART = (2 ** 256 - 1) // TOTAL_PARTS INTERVAL_DIFFERENCE = 10 ** 30 +hash_matcher = "fffffff" # This is usually the prefix for the hash in the output class KeccakFunctionManager: @@ -25,6 +25,11 @@ class KeccakFunctionManager: self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests def find_keccak(self, data: BitVec) -> BitVec: + """ + Calculates concrete keccak + :param data: input bitvecval + :return: concrete keccak output + """ keccak = symbol_factory.BitVecVal( int.from_bytes( utils.sha3(data.value.to_bytes(data.size() // 8, byteorder="big")), @@ -35,6 +40,11 @@ class KeccakFunctionManager: return keccak def get_function(self, length: int) -> Tuple[Function, Function]: + """ + Returns the keccak functions for the corresponding length + :param length: input size + :return: tuple of keccak and it's inverse + """ try: func, inverse = self.store_function[length] except KeyError: @@ -44,22 +54,25 @@ class KeccakFunctionManager: return func, inverse def create_keccak(self, data: BitVec) -> Tuple[BitVec, Bool]: + """ + Creates Keccak of the data + :param data: input + :return: Tuple of keccak and the condition it should satisfy + """ length = data.size() + condition = self._create_condition(func_input=data) func, _ = self.get_function(length) - condition = self._create_condition(func_input=data, func_output=func(data)) self.quick_inverse[func(data)] = data return func(data), condition - def get_new_cond(self, val, length: int) -> Bool: - random_number = symbol_factory.BitVecSym( - "randval_{}".format(randint(0, 10000)), length - ) - return self._create_condition(func_input=random_number, func_output=val) - - def _create_condition(self, func_input: BitVec, func_output: BitVec) -> Bool: + def _create_condition(self, func_input: BitVec) -> Bool: + """ + Creates the constraints for hash + :param func_input: input of the hash + :return: condition + """ length = func_input.size() func, inv = self.get_function(length) - cond = And(func(func_input) == func_output, inv(func(func_input)) == func_input) try: index = self.interval_hook_for_size[length] except KeyError: @@ -71,7 +84,7 @@ class KeccakFunctionManager: upper_bound = lower_bound + PART cond = And( - cond, + inv(func(func_input)) == func_input, ULE(symbol_factory.BitVecVal(lower_bound, 256), func(func_input)), ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0, diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 6a9fdae6..0357b493 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -28,9 +28,8 @@ class Constraints(list): constraint_list = constraint_list or [] constraint_list = self._get_smt_bool_list(constraint_list) super(Constraints, self).__init__(constraint_list) - self._default_timeout = 300 + self._default_timeout = 100 self._is_possible = is_possible - self.weighted = [] # type: List[Bool] @property def is_possible(self) -> bool: @@ -84,7 +83,6 @@ class Constraints(list): """ constraint_list = super(Constraints, self).copy() constraints = Constraints(constraint_list, is_possible=self._is_possible) - constraints.weighted = copy(self.weighted) return constraints def copy(self) -> "Constraints": @@ -98,7 +96,6 @@ class Constraints(list): """ constraint_list = super(Constraints, self).copy() constraints = Constraints(constraint_list, is_possible=self._is_possible) - constraints.weighted = copy(self.weighted) return constraints def __add__(self, constraints: List[Union[bool, Bool]]) -> "Constraints": @@ -112,9 +109,6 @@ class Constraints(list): new_constraints = Constraints( constraint_list=constraints_list, is_possible=None ) - new_constraints.weighted = copy(self.weighted) - if isinstance(constraints, Constraints): - new_constraints.weighted += constraints.weighted return new_constraints def __iadd__(self, constraints: Iterable[Union[bool, Bool]]) -> "Constraints": @@ -125,8 +119,6 @@ class Constraints(list): """ list_constraints = self._get_smt_bool_list(constraints) super(Constraints, self).__iadd__(list_constraints) - if isinstance(constraints, Constraints): - self.weighted += constraints.weighted self._is_possible = None return self diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index c2d883bb..f2300660 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -351,11 +351,6 @@ class LaserEVM: or transaction.return_data ) and not end_signal.revert: check_potential_issues(global_state) - first_arg1 = transaction.call_data.get_word_at(4) - global_state.node.constraints.weighted.append( - keccak_function_manager.get_new_cond(first_arg1, 160) - ) - end_signal.global_state.world_state.node = global_state.node self._add_world_state(end_signal.global_state) diff --git a/mythril/laser/smt/solver/solver.py b/mythril/laser/smt/solver/solver.py index 1537ceaf..aa79dc85 100644 --- a/mythril/laser/smt/solver/solver.py +++ b/mythril/laser/smt/solver/solver.py @@ -103,6 +103,3 @@ class Optimize(BaseSolver[z3.Optimize]): :param element: """ self.raw.maximize(element.raw) - - def add_soft(self, element): - self.raw.add_soft(element.raw) From 16dbd05d93a64b7ab7aca32491d76227d31b1ff5 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Sun, 13 Oct 2019 13:28:27 +0100 Subject: [PATCH 33/54] change the log to debug --- mythril/analysis/modules/exceptions.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index 80be8f78..903360e1 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -43,7 +43,7 @@ class ReachableExceptionsModule(DetectionModule): :param state: :return: """ - log.info("ASSERT_FAIL in function " + state.environment.active_function_name) + log.debug("ASSERT_FAIL in function " + state.environment.active_function_name) try: address = state.get_current_instruction()["address"] From 2f80f78b82fc88aeb51446ec79873428c85de824 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 14 Oct 2019 15:26:49 +0100 Subject: [PATCH 34/54] Use concrete hashes too --- mythril/analysis/solver.py | 23 +++++++++++++++---- .../laser/ethereum/keccak_function_manager.py | 23 ++++++++++++++----- tests/laser/evm_testsuite/evm_test.py | 12 +--------- 3 files changed, 37 insertions(+), 21 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 74d838f1..69688768 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -145,10 +145,25 @@ def _replace_with_actual_sha( find_input = symbol_factory.BitVecVal( int(tx["input"][10 + i : 74 + i], 16), 256 ) - _, inverse = keccak_function_manager.get_function(160) - input_ = symbol_factory.BitVecVal( - model.eval(inverse(find_input).raw).as_long(), 160 - ) + input_ = None + for size in (160, 256, 512): + _, inverse = keccak_function_manager.get_function(size) + try: + input_ = symbol_factory.BitVecVal( + model.eval(inverse(find_input).raw).as_long(), size + ) + except AttributeError: + continue + hex_input = hex(input_.value)[2:] + found = False + for new_tx in concrete_transactions: + if hex_input in new_tx["input"]: + found = True + break + if found: + break + if input_ is None: + continue keccak = keccak_function_manager.find_keccak(input_) tx["input"] = tx["input"].replace( tx["input"][10 + i : 74 + i], hex(keccak.value)[2:] diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index e3ed72d3..3bc3f26d 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -8,8 +8,9 @@ from mythril.laser.smt import ( And, ULT, Bool, + Or, ) -from typing import Dict, Tuple +from typing import Dict, Tuple, List TOTAL_PARTS = 10 ** 40 PART = (2 ** 256 - 1) // TOTAL_PARTS @@ -22,7 +23,7 @@ class KeccakFunctionManager: self.store_function = {} # type: Dict[int, Tuple[Function, Function]] self.interval_hook_for_size = {} # type: Dict[int, int] self._index_counter = TOTAL_PARTS - 34534 - self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests + self.concrete_hash_vals = {} # type: Dict[int, List[BitVec]] def find_keccak(self, data: BitVec) -> BitVec: """ @@ -50,6 +51,7 @@ class KeccakFunctionManager: except KeyError: func = Function("keccak256_{}".format(length), length, 256) inverse = Function("keccak256_{}-1".format(length), 256, length) + self.concrete_hash_vals[length] = [] self.store_function[length] = (func, inverse) return func, inverse @@ -60,10 +62,17 @@ class KeccakFunctionManager: :return: Tuple of keccak and the condition it should satisfy """ length = data.size() - condition = self._create_condition(func_input=data) - func, _ = self.get_function(length) - self.quick_inverse[func(data)] = data - return func(data), condition + func, inverse = self.get_function(length) + + if data.symbolic: + condition = self._create_condition(func_input=data) + output = func(data) + else: + concrete_val = self.find_keccak(data) + condition = And(func(data) == concrete_val, inverse(func(data)) == data) + self.concrete_hash_vals[length].append(concrete_val) + output = concrete_val + return output, condition def _create_condition(self, func_input: BitVec) -> Bool: """ @@ -89,6 +98,8 @@ class KeccakFunctionManager: ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0, ) + for val in self.concrete_hash_vals[length]: + cond = Or(cond, func(func_input) == val) return cond diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 8afe3d14..9fbb9dfa 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -1,11 +1,9 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.state.account import Account -from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.state.world_state import WorldState from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.transaction.concolic import execute_message_call from mythril.laser.smt import Expression, BitVec, symbol_factory -from mythril.analysis.solver import get_model from datetime import datetime import binascii @@ -178,15 +176,7 @@ def test_vmtest( expected = int(value, 16) actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)] if isinstance(actual, Expression): - if ( - actual.symbolic - and actual in keccak_function_manager.quick_inverse - ): - actual = keccak_function_manager.find_keccak( - keccak_function_manager.quick_inverse[actual] - ) - else: - actual = actual.value + actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual else: if type(actual) == bytes: From 203e8f6febbca9eccab16afc09ec2fb1d5e72c28 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 14 Oct 2019 19:58:28 +0100 Subject: [PATCH 35/54] Update mythril/laser/ethereum/svm.py Co-Authored-By: Nathan --- mythril/laser/ethereum/svm.py | 1 - 1 file changed, 1 deletion(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index f2300660..9c1129a3 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -11,7 +11,6 @@ from mythril.laser.ethereum.evm_exceptions import StackUnderflowException from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.iprof import InstructionProfiler -from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( MutationAnnotation, From 3f4ee27c1fdf8209c27b4e1abc19cbbaf032b506 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 21 Oct 2019 16:04:07 +0100 Subject: [PATCH 36/54] Update mythril/laser/ethereum/state/world_state.py Co-Authored-By: Nathan --- mythril/laser/ethereum/state/world_state.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 901fd6ca..20628877 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -1,7 +1,7 @@ """This module contains a representation of the EVM's world state.""" from copy import copy from random import randint -from typing import Dict, List, Iterator, Optional, Set, TYPE_CHECKING +from typing import Dict, List, Iterator, Optional, TYPE_CHECKING from mythril.support.loader import DynLoader from mythril.laser.smt import symbol_factory, Array, BitVec From 33cab6830d84c739673801068895200a33b6d760 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 21 Oct 2019 16:34:28 +0100 Subject: [PATCH 37/54] Handle sha3() case --- mythril/laser/ethereum/instructions.py | 7 +++++-- mythril/laser/ethereum/keccak_function_manager.py | 10 ++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 6b18bb0e..b6a72e24 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -999,13 +999,16 @@ class Instruction: b if isinstance(b, BitVec) else symbol_factory.BitVecVal(b, 8) for b in state.memory[index : index + length] ] + if len(data_list) > 1: data = simplify(Concat(data_list)) elif len(data_list) == 1: data = data_list[0] else: - # length is 0; this only matters for input of the BitVecFuncVal - data = symbol_factory.BitVecVal(0, 1) + # TODO: handle finding x where func(x)==func("") + result = keccak_function_manager.get_empty_keccak_hash() + state.stack.append(result) + return [global_state] result, condition = keccak_function_manager.create_keccak(data) state.stack.append(result) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 3bc3f26d..2ad51b1e 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -55,6 +55,16 @@ class KeccakFunctionManager: self.store_function[length] = (func, inverse) return func, inverse + @staticmethod + def get_empty_keccak_hash() -> BitVec: + """ + returns sha3("") + :return: + """ + val = 89477152217924674838424037953991966239322087453347756267410168184682657981552 + val = symbol_factory.BitVecVal(val, 256) + return val + def create_keccak(self, data: BitVec) -> Tuple[BitVec, Bool]: """ Creates Keccak of the data From 0f15c76596173ee20ddfa26229004755ef5190a5 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 21 Oct 2019 17:02:47 +0100 Subject: [PATCH 38/54] add some changes --- mythril/analysis/solver.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 69688768..46e8c690 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -22,6 +22,7 @@ import logging log = logging.getLogger(__name__) + # LRU cache works great when used in powers of 2 @lru_cache(maxsize=2 ** 23) def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True): @@ -140,13 +141,12 @@ def _replace_with_actual_sha( if hash_matcher not in tx["input"]: continue for i in range(0, len(tx["input"]) - 73, 64): - if hash_matcher not in tx["input"][i + 10 : i + 74]: + data_slice = tx["input"][i + 10 : i + 74] + if hash_matcher not in data_slice or len(data_slice) != 64: continue - find_input = symbol_factory.BitVecVal( - int(tx["input"][10 + i : 74 + i], 16), 256 - ) + find_input = symbol_factory.BitVecVal(int(data_slice, 16), 256) input_ = None - for size in (160, 256, 512): + for size in keccak_function_manager.store_function: _, inverse = keccak_function_manager.get_function(size) try: input_ = symbol_factory.BitVecVal( From 5d79fd399dda0e96b0cdf050fd2d63aece146898 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 21 Oct 2019 18:27:37 +0100 Subject: [PATCH 39/54] Handle constructor args --- mythril/analysis/solver.py | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 46e8c690..ecb33f6c 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -126,7 +126,8 @@ def get_transaction_sequence( concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict) if isinstance(transaction_sequence[0], ContractCreationTransaction): - _replace_with_actual_sha(concrete_transactions[1:], model) + code = transaction_sequence[0].code + _replace_with_actual_sha(concrete_transactions, model, code) else: _replace_with_actual_sha(concrete_transactions, model) steps = {"initialState": concrete_initial_state, "steps": concrete_transactions} @@ -135,13 +136,17 @@ def get_transaction_sequence( def _replace_with_actual_sha( - concrete_transactions: List[Dict[str, str]], model: z3.Model + concrete_transactions: List[Dict[str, str]], model: z3.Model, code=None ): for tx in concrete_transactions: if hash_matcher not in tx["input"]: continue - for i in range(0, len(tx["input"]) - 73, 64): - data_slice = tx["input"][i + 10 : i + 74] + if code is not None and code.bytecode in tx["input"]: + s_index = len(code.bytecode) + 10 + else: + s_index = 10 + for i in range(s_index, len(tx["input"]), 64): + data_slice = tx["input"][i : i + 64] if hash_matcher not in data_slice or len(data_slice) != 64: continue find_input = symbol_factory.BitVecVal(int(data_slice, 16), 256) @@ -165,8 +170,11 @@ def _replace_with_actual_sha( if input_ is None: continue keccak = keccak_function_manager.find_keccak(input_) - tx["input"] = tx["input"].replace( - tx["input"][10 + i : 74 + i], hex(keccak.value)[2:] + hex_keccak = hex(keccak.value) + if len(hex_keccak) != 66: + hex_keccak = "0x" + "0" * (66 - len(hex_keccak)) + hex_keccak[2:] + tx["input"] = tx["input"][:s_index] + tx["input"][s_index:].replace( + tx["input"][i : 64 + i], hex_keccak[2:] ) From 32ef5f475e00bb04a96657f206161f61b04ec050 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 21 Oct 2019 18:46:45 +0100 Subject: [PATCH 40/54] Fix type hints --- mythril/laser/ethereum/keccak_function_manager.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index 2ad51b1e..fcd20731 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -62,8 +62,7 @@ class KeccakFunctionManager: :return: """ val = 89477152217924674838424037953991966239322087453347756267410168184682657981552 - val = symbol_factory.BitVecVal(val, 256) - return val + return symbol_factory.BitVecVal(val, 256) def create_keccak(self, data: BitVec) -> Tuple[BitVec, Bool]: """ From a5628219dc3e49f7cb959faa2725413d04a94d80 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 21 Oct 2019 21:21:44 +0100 Subject: [PATCH 41/54] Don't handle concrete vals in keccak_func_manager --- mythril/laser/ethereum/keccak_function_manager.py | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index fcd20731..d0f69d94 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -23,7 +23,6 @@ class KeccakFunctionManager: self.store_function = {} # type: Dict[int, Tuple[Function, Function]] self.interval_hook_for_size = {} # type: Dict[int, int] self._index_counter = TOTAL_PARTS - 34534 - self.concrete_hash_vals = {} # type: Dict[int, List[BitVec]] def find_keccak(self, data: BitVec) -> BitVec: """ @@ -51,7 +50,6 @@ class KeccakFunctionManager: except KeyError: func = Function("keccak256_{}".format(length), length, 256) inverse = Function("keccak256_{}-1".format(length), 256, length) - self.concrete_hash_vals[length] = [] self.store_function[length] = (func, inverse) return func, inverse @@ -73,14 +71,8 @@ class KeccakFunctionManager: length = data.size() func, inverse = self.get_function(length) - if data.symbolic: - condition = self._create_condition(func_input=data) - output = func(data) - else: - concrete_val = self.find_keccak(data) - condition = And(func(data) == concrete_val, inverse(func(data)) == data) - self.concrete_hash_vals[length].append(concrete_val) - output = concrete_val + condition = self._create_condition(func_input=data) + output = func(data) return output, condition def _create_condition(self, func_input: BitVec) -> Bool: @@ -107,8 +99,6 @@ class KeccakFunctionManager: ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0, ) - for val in self.concrete_hash_vals[length]: - cond = Or(cond, func(func_input) == val) return cond From 856547fa97273d7cf8543022b5e32976cab296d9 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Mon, 21 Oct 2019 21:53:10 +0100 Subject: [PATCH 42/54] Fix tests --- mythril/laser/ethereum/keccak_function_manager.py | 5 +++-- tests/laser/evm_testsuite/evm_test.py | 11 ++++++++++- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index d0f69d94..f79838a8 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -23,6 +23,7 @@ class KeccakFunctionManager: self.store_function = {} # type: Dict[int, Tuple[Function, Function]] self.interval_hook_for_size = {} # type: Dict[int, int] self._index_counter = TOTAL_PARTS - 34534 + self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests def find_keccak(self, data: BitVec) -> BitVec: """ @@ -72,8 +73,8 @@ class KeccakFunctionManager: func, inverse = self.get_function(length) condition = self._create_condition(func_input=data) - output = func(data) - return output, condition + self.quick_inverse[func(data)] = data + return func(data), condition def _create_condition(self, func_input: BitVec) -> Bool: """ diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 9fbb9dfa..9b9b913f 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -1,6 +1,7 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.transaction.concolic import execute_message_call from mythril.laser.smt import Expression, BitVec, symbol_factory @@ -176,7 +177,15 @@ def test_vmtest( expected = int(value, 16) actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)] if isinstance(actual, Expression): - actual = actual.value + if ( + actual.symbolic + and actual in keccak_function_manager.quick_inverse + ): + actual = keccak_function_manager.find_keccak( + keccak_function_manager.quick_inverse[actual] + ) + else: + actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual else: if type(actual) == bytes: From a423c79f85b8c20930f9d301ebb1aac4a8b83112 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 22 Oct 2019 13:01:54 +0100 Subject: [PATCH 43/54] Update mythril/analysis/solver.py Co-Authored-By: JoranHonig --- mythril/analysis/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index ecb33f6c..32250850 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -142,7 +142,7 @@ def _replace_with_actual_sha( if hash_matcher not in tx["input"]: continue if code is not None and code.bytecode in tx["input"]: - s_index = len(code.bytecode) + 10 + s_index = len(code.bytecode) + 2 else: s_index = 10 for i in range(s_index, len(tx["input"]), 64): From cc9a7d6ebcead8ec3da2028ec2e9e6249504edb4 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 22 Oct 2019 14:31:44 +0100 Subject: [PATCH 44/54] Update mythril/laser/smt/__init__.py Co-Authored-By: JoranHonig --- mythril/laser/smt/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 89fe147b..b132cbbb 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -139,7 +139,7 @@ class _SmtSymbolFactory(SymbolFactory[SMTBool, BitVec]): @staticmethod def BoolSym(name: str, annotations: Annotations = None) -> SMTBool: """ - Creates a Bool with concrete value + Creates a boolean symbol :param name: The name of the Bool variable :param annotations: The annotations to initialize the bool with :return: The freshly created Bool() From f61f6c03643fab9b696ccd7a8b7629f8701f1d7e Mon Sep 17 00:00:00 2001 From: Nikhil Date: Tue, 22 Oct 2019 15:06:23 +0100 Subject: [PATCH 45/54] Make some changes --- mythril/analysis/solver.py | 2 +- mythril/laser/ethereum/keccak_function_manager.py | 13 ++++++++++++- mythril/laser/ethereum/state/constraints.py | 8 ++------ tests/laser/evm_testsuite/evm_test.py | 2 +- 4 files changed, 16 insertions(+), 9 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index ecb33f6c..4404224f 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -169,7 +169,7 @@ def _replace_with_actual_sha( break if input_ is None: continue - keccak = keccak_function_manager.find_keccak(input_) + keccak = keccak_function_manager.find_concrete_keccak(input_) hex_keccak = hex(keccak.value) if len(hex_keccak) != 66: hex_keccak = "0x" + "0" * (66 - len(hex_keccak)) + hex_keccak[2:] diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index f79838a8..6d5262ee 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -19,13 +19,24 @@ hash_matcher = "fffffff" # This is usually the prefix for the hash in the outpu class KeccakFunctionManager: + """ + A bunch of uninterpreted functions are considered like keccak256_160 ,... + where keccak256_160 means the input of keccak256() is 160 bit number. + the range of these functions are constrained to some mutually disjoint intervals + All the hashes modulo 64 are 0 as we need a spread among hashes for array type data structures + All the functions are kind of one to one due to constraint of the existence of inverse + for each encountered input. + For more info https://files.sri.inf.ethz.ch/website/papers/sp20-verx.pdf + """ + def __init__(self): self.store_function = {} # type: Dict[int, Tuple[Function, Function]] self.interval_hook_for_size = {} # type: Dict[int, int] self._index_counter = TOTAL_PARTS - 34534 self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests - def find_keccak(self, data: BitVec) -> BitVec: + @staticmethod + def find_concrete_keccak(data: BitVec) -> BitVec: """ Calculates concrete keccak :param data: input bitvecval diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 0357b493..b4b101a3 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -95,8 +95,7 @@ class Constraints(list): :return: The copied constraint List """ constraint_list = super(Constraints, self).copy() - constraints = Constraints(constraint_list, is_possible=self._is_possible) - return constraints + return Constraints(constraint_list, is_possible=self._is_possible) def __add__(self, constraints: List[Union[bool, Bool]]) -> "Constraints": """ @@ -106,10 +105,7 @@ class Constraints(list): """ constraints_list = self._get_smt_bool_list(constraints) constraints_list = super(Constraints, self).__add__(constraints_list) - new_constraints = Constraints( - constraint_list=constraints_list, is_possible=None - ) - return new_constraints + return Constraints(constraint_list=constraints_list, is_possible=None) def __iadd__(self, constraints: Iterable[Union[bool, Bool]]) -> "Constraints": """ diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 9b9b913f..8bbca5ca 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -181,7 +181,7 @@ def test_vmtest( actual.symbolic and actual in keccak_function_manager.quick_inverse ): - actual = keccak_function_manager.find_keccak( + actual = keccak_function_manager.find_concrete_keccak( keccak_function_manager.quick_inverse[actual] ) else: From dba325272d4efeca8b4f9e180346dbf0d4822fe1 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Tue, 22 Oct 2019 15:08:55 +0100 Subject: [PATCH 46/54] Make some changes --- mythril/laser/ethereum/state/constraints.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index b4b101a3..9524e4df 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -82,8 +82,7 @@ class Constraints(list): :return: The copied constraint List """ constraint_list = super(Constraints, self).copy() - constraints = Constraints(constraint_list, is_possible=self._is_possible) - return constraints + return Constraints(constraint_list, is_possible=self._is_possible) def copy(self) -> "Constraints": return self.__copy__() From 851fb8ff5bc77d231bcb19a4fb59c7831b4fa3ce Mon Sep 17 00:00:00 2001 From: Nikhil Date: Tue, 22 Oct 2019 15:17:32 +0100 Subject: [PATCH 47/54] Add some documentation --- mythril/analysis/solver.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 6e16347a..21c26f0f 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -146,6 +146,8 @@ def _replace_with_actual_sha( else: s_index = 10 for i in range(s_index, len(tx["input"]), 64): + # We can do this because the data is aligned as blocks of 32 bytes + # For more info https://solidity.readthedocs.io/en/v0.5.12/abi-spec.html, data_slice = tx["input"][i : i + 64] if hash_matcher not in data_slice or len(data_slice) != 64: continue From 95c7d04ada24821c14d935ecca7254a466ecd6ed Mon Sep 17 00:00:00 2001 From: Nikhil Date: Tue, 22 Oct 2019 15:49:36 +0100 Subject: [PATCH 48/54] Add unit tests for keccak --- tests/laser/keccak_tests.py | 113 ++++++++++++++++++++++++++++++++++++ 1 file changed, 113 insertions(+) create mode 100644 tests/laser/keccak_tests.py diff --git a/tests/laser/keccak_tests.py b/tests/laser/keccak_tests.py new file mode 100644 index 00000000..d8f17eec --- /dev/null +++ b/tests/laser/keccak_tests.py @@ -0,0 +1,113 @@ +from mythril.laser.smt import Solver, symbol_factory, And +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager +import z3 +import pytest + + +@pytest.mark.parametrize( + "input1, input2, expected", + [ + (symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(101, 8), z3.unsat), + (symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(100, 16), z3.unsat), + (symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(100, 8), z3.sat), + ( + symbol_factory.BitVecSym("N1", 256), + symbol_factory.BitVecSym("N2", 256), + z3.sat, + ), + ], +) +def test_keccak_basic(input1, input2, expected): + s = Solver() + + o1, c1 = keccak_function_manager.create_keccak(input1) + o2, c2 = keccak_function_manager.create_keccak(input2) + s.add(c1) + s.add(c2) + + s.add(o1 == o2) + assert s.check() == expected + + +def test_keccak_complex_eq(): + """ + check for keccak(keccak(b)*2) == keccak(keccak(a)*2) && a != b + :return: + """ + s = Solver() + a = symbol_factory.BitVecSym("a", 160) + b = symbol_factory.BitVecSym("b", 160) + o1, c1 = keccak_function_manager.create_keccak(a) + o2, c2 = keccak_function_manager.create_keccak(b) + s.add(And(c1, c2)) + two = symbol_factory.BitVecVal(2, 256) + o1 = two * o1 + o2 = two * o2 + o1, c1 = keccak_function_manager.create_keccak(o1) + o2, c2 = keccak_function_manager.create_keccak(o2) + + s.add(And(c1, c2)) + s.add(o1 == o2) + s.add(a != b) + + assert s.check() == z3.unsat + + +def test_keccak_complex_eq2(): + """ + check for keccak(keccak(b)*2) == keccak(keccak(a)*2) + This isn't combined with prev test because incremental solving here requires extra-extra work + (solution is literally the opposite of prev one) so it will take forever to solve. + :return: + """ + s = Solver() + a = symbol_factory.BitVecSym("a", 160) + b = symbol_factory.BitVecSym("b", 160) + o1, c1 = keccak_function_manager.create_keccak(a) + o2, c2 = keccak_function_manager.create_keccak(b) + s.add(And(c1, c2)) + two = symbol_factory.BitVecVal(2, 256) + o1 = two * o1 + o2 = two * o2 + o1, c1 = keccak_function_manager.create_keccak(o1) + o2, c2 = keccak_function_manager.create_keccak(o2) + + s.add(And(c1, c2)) + s.add(o1 == o2) + + assert s.check() == z3.sat + + +def test_keccak_simple_number(): + """ + check for keccak(b) == 10 + :return: + """ + s = Solver() + a = symbol_factory.BitVecSym("a", 160) + ten = symbol_factory.BitVecVal(10, 256) + o, c = keccak_function_manager.create_keccak(a) + + s.add(c) + s.add(ten == o) + + assert s.check() == z3.unsat + + +def test_keccak_other_num(): + """ + check keccak(keccak(a)*2) == b + :return: + """ + s = Solver() + a = symbol_factory.BitVecSym("a", 160) + b = symbol_factory.BitVecSym("b", 256) + o, c = keccak_function_manager.create_keccak(a) + two = symbol_factory.BitVecVal(2, 256) + o = two * o + s.add(c) + o, c = keccak_function_manager.create_keccak(o) + s.add(c) + s.add(b == o) + + assert s.check() == z3.sat From cc002b4e7125ab38467971089b99bfbf0e69d56e Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 22 Oct 2019 15:51:20 +0100 Subject: [PATCH 49/54] Revert "Fix propagation of JumpdestCountAnnotation (#1237)" (#1253) This reverts commit f1a0c9db04167eaece00b408fd91003216871cb1. --- .../laser/ethereum/strategy/extensions/bounded_loops.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py index 56c1f55b..5a7583ab 100644 --- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py +++ b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py @@ -3,6 +3,7 @@ from mythril.laser.ethereum.strategy.basic import BasicSearchStrategy from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.transaction import ContractCreationTransaction from typing import Dict, cast, List +from copy import copy import logging @@ -16,7 +17,9 @@ class JumpdestCountAnnotation(StateAnnotation): self._reached_count = {} # type: Dict[str, int] def __copy__(self): - return self + result = JumpdestCountAnnotation() + result._reached_count = copy(self._reached_count) + return result class BoundedLoopsStrategy(BasicSearchStrategy): @@ -45,6 +48,7 @@ class BoundedLoopsStrategy(BasicSearchStrategy): :return: Global state """ + while True: state = self.super_strategy.get_strategic_global_state() @@ -56,7 +60,6 @@ class BoundedLoopsStrategy(BasicSearchStrategy): if len(annotations) == 0: annotation = JumpdestCountAnnotation() - log.debug("Adding JumpdestCountAnnotation to GlobalState") state.annotate(annotation) else: annotation = annotations[0] From 06f5734cf6127753126f169190d0d74a3cbfedf3 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 23 Oct 2019 21:50:34 +0100 Subject: [PATCH 50/54] Skip 0x --- mythril/analysis/solver.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 21c26f0f..6e688922 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -172,11 +172,11 @@ def _replace_with_actual_sha( if input_ is None: continue keccak = keccak_function_manager.find_concrete_keccak(input_) - hex_keccak = hex(keccak.value) - if len(hex_keccak) != 66: - hex_keccak = "0x" + "0" * (66 - len(hex_keccak)) + hex_keccak[2:] + hex_keccak = hex(keccak.value)[2:] + if len(hex_keccak) != 64: + hex_keccak = "0" * (64 - len(hex_keccak)) + hex_keccak tx["input"] = tx["input"][:s_index] + tx["input"][s_index:].replace( - tx["input"][i : 64 + i], hex_keccak[2:] + tx["input"][i : 64 + i], hex_keccak ) From bb8586b65b60e611047e192c0fd12aefc3296a41 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Wed, 23 Oct 2019 22:21:04 +0100 Subject: [PATCH 51/54] Iterate over single indices than chunks of 32 --- mythril/analysis/solver.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 6e688922..f0675e4d 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -145,9 +145,7 @@ def _replace_with_actual_sha( s_index = len(code.bytecode) + 2 else: s_index = 10 - for i in range(s_index, len(tx["input"]), 64): - # We can do this because the data is aligned as blocks of 32 bytes - # For more info https://solidity.readthedocs.io/en/v0.5.12/abi-spec.html, + for i in range(s_index, len(tx["input"])): data_slice = tx["input"][i : i + 64] if hash_matcher not in data_slice or len(data_slice) != 64: continue From 60ab21ebedc75f61e1f16f432bccfcad8f93b448 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Thu, 24 Oct 2019 14:22:39 +0100 Subject: [PATCH 52/54] Some review fixes --- mythril/laser/smt/__init__.py | 2 +- tests/laser/keccak_tests.py | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index b132cbbb..86ded2ed 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -51,7 +51,7 @@ class SymbolFactory(Generic[T, U]): @staticmethod def BoolSym(name: str, annotations: Annotations = None) -> T: """ - Creates a Bool with concrete value + Creates a boolean symbol :param name: The name of the Bool variable :param annotations: The annotations to initialize the bool with :return: The freshly created Bool() diff --git a/tests/laser/keccak_tests.py b/tests/laser/keccak_tests.py index d8f17eec..4e018148 100644 --- a/tests/laser/keccak_tests.py +++ b/tests/laser/keccak_tests.py @@ -15,6 +15,16 @@ import pytest symbol_factory.BitVecSym("N2", 256), z3.sat, ), + ( + symbol_factory.BitVecVal(100, 256), + symbol_factory.BitVecSym("N1", 256), + z3.sat, + ), + ( + symbol_factory.BitVecVal(100, 8), + symbol_factory.BitVecSym("N1", 256), + z3.unsat, + ), ], ) def test_keccak_basic(input1, input2, expected): From 84b803d30b6128a014e6cb72f3efccd1e7083ed9 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Thu, 24 Oct 2019 14:30:14 +0100 Subject: [PATCH 53/54] Add more tests --- tests/laser/keccak_tests.py | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/tests/laser/keccak_tests.py b/tests/laser/keccak_tests.py index 4e018148..8a3ae00e 100644 --- a/tests/laser/keccak_tests.py +++ b/tests/laser/keccak_tests.py @@ -32,13 +32,28 @@ def test_keccak_basic(input1, input2, expected): o1, c1 = keccak_function_manager.create_keccak(input1) o2, c2 = keccak_function_manager.create_keccak(input2) - s.add(c1) - s.add(c2) + s.add(And(c1, c2)) s.add(o1 == o2) assert s.check() == expected +def test_keccak_symbol_and_val(): + """ + check keccak(100) == keccak(n) && n == 10 + :return: + """ + s = Solver() + hundred = symbol_factory.BitVecVal(100, 256) + n = symbol_factory.BitVecSym("n", 256) + o1, c1 = keccak_function_manager.create_keccak(hundred) + o2, c2 = keccak_function_manager.create_keccak(n) + s.add(And(c1, c2)) + s.add(o1 == o2) + s.add(n == symbol_factory.BitVecVal(10, 256)) + assert s.check() == z3.unsat + + def test_keccak_complex_eq(): """ check for keccak(keccak(b)*2) == keccak(keccak(a)*2) && a != b From 6ba7c8e96b3b6511efb19a48ea28ac7a65f75be5 Mon Sep 17 00:00:00 2001 From: Nikhil Date: Thu, 24 Oct 2019 19:56:39 +0100 Subject: [PATCH 54/54] Revert a line change --- mythril/laser/ethereum/state/constraints.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 9524e4df..419bc873 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -3,7 +3,6 @@ the call graph.""" from mythril.laser.smt import Solver, Bool, symbol_factory, simplify -from copy import copy from typing import Iterable, List, Optional, Union from z3 import unsat @@ -93,8 +92,7 @@ class Constraints(list): :param memodict: :return: The copied constraint List """ - constraint_list = super(Constraints, self).copy() - return Constraints(constraint_list, is_possible=self._is_possible) + return self.__copy__() def __add__(self, constraints: List[Union[bool, Bool]]) -> "Constraints": """