diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index ae7ef8fe..703bba6d 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -13,6 +13,7 @@ from mythril.laser.ethereum import util from mythril.laser.ethereum.call import get_call_parameters from mythril.laser.ethereum.state import GlobalState, MachineState, Environment, CalldataType import mythril.laser.ethereum.natives as natives +from mythril.laser.ethereum.transaction import CallTransaction, TransactionEndSignal, TransactionStartSignal TT256 = 2 ** 256 TT256M1 = 2 ** 256 - 1 @@ -35,8 +36,8 @@ def instruction(func): for state in new_global_states: state.mstate.pc += 1 return new_global_states - return wrapper + return wrapper class Instruction: """ @@ -47,7 +48,7 @@ class Instruction: self.dynamic_loader = dynamic_loader self.op_code = op_code - def evaluate(self, global_state): + def evaluate(self, global_state, post=False): """ Performs the mutation for this instruction """ # Generalize some ops logging.debug("Evaluating {}".format(self.op_code)) @@ -61,7 +62,7 @@ class Instruction: elif self.op_code.startswith("LOG"): op = "log" - instruction_mutator = getattr(self, op + '_', None) + instruction_mutator = getattr(self, op + '_', None) if not post else getattr(self, op + '_' + 'post', None) if instruction_mutator is None: raise NotImplementedError @@ -708,7 +709,8 @@ class Instruction: try: global_state.environment.active_account = deepcopy(global_state.environment.active_account) - global_state.accounts[global_state.environment.active_account.address] = global_state.environment.active_account + global_state.accounts[ + global_state.environment.active_account.address] = global_state.environment.active_account global_state.environment.active_account.storage[index] = value except KeyError: @@ -828,24 +830,15 @@ class Instruction: @instruction def return_(self, global_state): - # TODO: memory state = global_state.mstate offset, length = state.stack.pop(), state.stack.pop() try: - _ = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)] + return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)] except AttributeError: logging.debug("Return with symbolic length or offset. Not supported") + global_state.transaction_stack[-1][0].end(global_state, [BitVec("return_data")]) - return_value = BitVec("retval_" + global_state.environment.active_function_name, 256) - - if not global_state.call_stack: - return [] - - new_global_state = deepcopy(global_state.call_stack.pop()) - new_global_state.node = global_state.node - # TODO: copy memory - - return [new_global_state] + global_state.transaction_stack[-1][0].end(global_state, return_data) @instruction def suicide_(self, global_state): @@ -865,11 +858,7 @@ class Instruction: @instruction def stop_(self, global_state): - if len(global_state.call_stack) is 0: - return [] - new_global_state = deepcopy(global_state.call_stack.pop()) - new_global_state.node = global_state.node - return [new_global_state] + return [] @instruction def call_(self, global_state): @@ -877,7 +866,8 @@ class Instruction: environment = global_state.environment try: - callee_address, callee_account, call_data, value, call_data_type, gas, memory_out_offset, memory_out_size = get_call_parameters(global_state, self.dynamic_loader, True) + callee_address, callee_account, call_data, value, call_data_type, gas, memory_out_offset, memory_out_size = get_call_parameters( + global_state, self.dynamic_loader, True) except ValueError as e: logging.info( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) @@ -907,8 +897,8 @@ class Instruction: except natives.NativeContractException: contract_list = ['ecerecover', 'sha256', 'ripemd160', 'identity'] for i in range(mem_out_sz): - global_state.mstate.memory[mem_out_start+i] = BitVec(contract_list[call_address_int - 1]+ - "(" + str(call_data) + ")", 256) + global_state.mstate.memory[mem_out_start + i] = BitVec(contract_list[call_address_int - 1] + + "(" + str(call_data) + ")", 256) return [global_state] @@ -918,19 +908,15 @@ class Instruction: # TODO: maybe use BitVec here constrained to 1 return [global_state] - callee_environment = Environment(callee_account, - BitVecVal(int(environment.active_account.address, 16), 256), - call_data, - environment.gasprice, - value, - environment.origin, - calldata_type=call_data_type) - new_global_state = GlobalState(global_state.accounts, callee_environment, global_state.node, MachineState(gas)) - new_global_state.call_stack.append(global_state) - new_global_state.mstate.pc = -1 - new_global_state.mstate.depth = global_state.mstate.depth + 1 - new_global_state.mstate.constraints = copy(global_state.mstate.constraints) - return [new_global_state] + transaction = CallTransaction(global_state.accounts, + callee_account, + BitVecVal(int(environment.active_account.address, 16), 256), + call_data, + environment.gasprice, + value, + environment.origin, + call_data_type) + raise TransactionStartSignal(transaction, self.op_code) @instruction def callcode_(self, global_state): @@ -938,7 +924,8 @@ class Instruction: environment = global_state.environment try: - callee_address, callee_account, call_data, value, call_data_type, gas, _, _ = get_call_parameters(global_state, self.dynamic_loader, True) + callee_address, callee_account, call_data, value, call_data_type, gas, _, _ = get_call_parameters( + global_state, self.dynamic_loader, True) except ValueError as e: logging.info( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) @@ -968,7 +955,8 @@ class Instruction: environment = global_state.environment try: - callee_address, callee_account, call_data, _, call_data_type, gas, _, _ = get_call_parameters(global_state, self.dynamic_loader) + callee_address, callee_account, call_data, _, call_data_type, gas, _, _ = get_call_parameters(global_state, + self.dynamic_loader) except ValueError as e: logging.info( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) @@ -991,7 +979,6 @@ class Instruction: return [new_global_state] - @instruction def staticcall_(self, global_state): # TODO: implement me diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 92ba393d..738b5ea4 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -144,22 +144,21 @@ class GlobalState: """ GlobalState represents the current globalstate """ - def __init__(self, accounts, environment, node, machine_state=None, call_stack=None): + def __init__(self, accounts, environment, node, machine_state=None, transaction_stack=None): """ Constructor for GlobalState""" self.node = node self.accounts = accounts self.environment = environment self.mstate = machine_state if machine_state else MachineState(gas=10000000) - self.call_stack = call_stack if call_stack else [] + self.transaction_stack = transaction_stack if transaction_stack else [] self.op_code = "" - def __copy__(self): accounts = copy(self.accounts) environment = copy(self.environment) mstate = deepcopy(self.mstate) - call_stack = copy(self.call_stack) - return GlobalState(accounts, environment, self.node, mstate, call_stack=call_stack) + transaction_stack = deepcopy(self.transaction_stack) + return GlobalState(accounts, environment, self.node, mstate, transaction_stack=transaction_stack) #TODO: remove this, as two instructions are confusing def get_current_instruction(self): diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 61899681..92d945c0 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -1,7 +1,7 @@ from z3 import BitVec import logging from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState -from mythril.laser.ethereum.transaction import MessageCall +from mythril.laser.ethereum.transaction import MessageCall, TransactionStartSignal, TransactionEndSignal from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy @@ -70,31 +70,34 @@ class LaserEVM: try: new_states, op_code = self.execute_state(global_state) except NotImplementedError: - logging.info("Encountered unimplemented instruction: {}".format(op_code)) + logging.info("Encountered unimplemented instruction") continue - - if len(new_states) == 0: - # TODO: let global state use worldstate - open_world_state = WorldState() - open_world_state.accounts = global_state.accounts - open_world_state.node = global_state.node - self.open_states.append(open_world_state) + except TransactionStartSignal as e: + new_global_state = transaction.initial_global_state() + new_global_state.transaction_stack.append(e.transaction, global_state) + new_states, op_code = [e.transaction.initial_global_state()], e.op_code + except TransactionEndSignal as e: + transaction, return_global_state = e.global_state.transaction_stack.pop() + if return_global_state is None: + self.open_states.append(e.global_state) + continue + new_states, op_code = self.execute_state(return_global_state, post=True) self.manage_cfg(op_code, new_states) self.work_list += new_states self.total_states += len(new_states) - def execute_state(self, global_state): + def execute_state(self, global_state, post=False): instructions = global_state.environment.code.instruction_list op_code = instructions[global_state.mstate.pc]['opcode'] # Only count coverage for the main contract - if len(global_state.call_stack) == 0: + if len(global_state.transaction_stack) == 0: self.instructions_covered[global_state.mstate.pc] = True self._execute_pre_hook(op_code, global_state) - new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(global_state) + new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(global_state, post) self._execute_post_hook(op_code, new_global_states) return new_global_states, op_code @@ -189,3 +192,16 @@ class LaserEVM: return function return hook_decorator + + # def start_transaction(self, type, world_state, account, caller, + # call_data, gas_price, call_value, origin, call_data_type): + # environment = Environment( + # account, + # caller, + # call_data, + # gas_price, + # call_value, + # origin, + # call_data_type, + # ) + # new_node = Node(environment.active_account.contract_name) diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py index dedad9b1..089c9a5a 100644 --- a/mythril/laser/ethereum/transaction.py +++ b/mythril/laser/ethereum/transaction.py @@ -5,6 +5,63 @@ from mythril.laser.ethereum.cfg import Node, Edge, JumpType from z3 import BitVec +class TransactionEndSignal(IndexError): + def __init__(self, global_state): + self.global_state = global_state + + +class TransactionStartSignal(Exception): + + def __init__(self, transaction, op_code): + self.transaction = transaction + self.op_code = op_code + + +class CallTransaction: + def __init__(self, + world_state, + callee_account, + caller, + call_data=(), + gas_price=BitVec("gasprice", 256), + call_value=BitVec("callvalue", 256), + origin=BitVec("origin", 256), + call_data_type=BitVec("call_data_type", 256) + ): + self.world_state = world_state + self.callee_account = callee_account + self.caller = caller + self.call_data = call_data + self.gas_price = gas_price + self.call_value = call_value + self.origin = origin + self.call_data_type = call_data_type + + self.return_data = None + + def initial_global_state(self): + # Initialize the execution environment + environment = Environment( + self.callee_account, + self.caller, + self.call_data, + self.gas_price, + self.call_value, + self.origin, + code=self.callee_account.code, + calldata_type=self.call_data_type, + ) + + global_state = GlobalState(self.world_state.accounts, environment, None) + global_state.environment.active_function_name = 'fallback' + + return global_state + + def end(self, global_state, return_data=None): + self.return_data = return_data + raise TransactionEndSignal(global_state) + + class Transaction: def __init__(self): self.open_states = None @@ -40,27 +97,27 @@ class MessageCall(Transaction): for open_world_state in open_states: - # Initialize the execution environment - environment = Environment( + transaction = CallTransaction( + open_world_state, open_world_state[self.callee_address], self.caller, [], self.gas_price, self.call_value, self.origin, - calldata_type=CalldataType.SYMBOLIC, + CalldataType.SYMBOLIC, ) - new_node = Node(environment.active_account.contract_name) - evm.instructions_covered = [False for _ in environment.code.instruction_list] + global_state = transaction.initial_global_state() + global_state.transaction_stack.append((transaction, None)) + + new_node = Node(global_state.environment.active_account.contract_name) + evm.instructions_covered = [False for _ in global_state.environment.code.instruction_list] evm.nodes[new_node.uid] = new_node if open_world_state.node: evm.edges.append(Edge(open_world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction, condition=None)) - - global_state = GlobalState(open_world_state.accounts, environment, new_node) - global_state.environment.active_function_name = 'fallback()' + global_state.node = new_node new_node.states.append(global_state) - evm.work_list.append(global_state) evm.exec()