From 62aede8e0bd3ac41a374dfb3f043317b04575129 Mon Sep 17 00:00:00 2001 From: Nathan Date: Fri, 14 Dec 2018 22:09:22 -0500 Subject: [PATCH 01/24] Report issues when exception occurs --- mythril/analysis/security.py | 8 +++++++ mythril/mythril.py | 46 +++++++++++++++++++++--------------- 2 files changed, 35 insertions(+), 19 deletions(-) diff --git a/mythril/analysis/security.py b/mythril/analysis/security.py index 4908b3a6..93a882da 100644 --- a/mythril/analysis/security.py +++ b/mythril/analysis/security.py @@ -69,6 +69,14 @@ def fire_lasers(statespace, module_names=()): log.info("Executing " + module.detector.name) issues += module.detector.execute(statespace) + issues += retrieve_callback_issues(module_names) + return issues + + +def retrieve_callback_issues(module_names=()): + log.info("Starting analysis") + + issues = [] for module in get_detection_modules( entrypoint="callback", include_modules=module_names ): diff --git a/mythril/mythril.py b/mythril/mythril.py index 86bb4da0..a4a0506b 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -6,9 +6,9 @@ """ import logging -import json import os import re +import traceback from pathlib import Path from ethereum import utils @@ -31,7 +31,7 @@ from mythril.exceptions import CompilerError, NoContractFoundError, CriticalErro from mythril.analysis.symbolic import SymExecWrapper from mythril.analysis.callgraph import generate_graph from mythril.analysis.traceexplore import get_serializable_statespace -from mythril.analysis.security import fire_lasers +from mythril.analysis.security import fire_lasers, retrieve_callback_issues from mythril.analysis.report import Report from mythril.ethereum.interface.leveldb.client import EthLevelDB @@ -481,23 +481,31 @@ class Mythril(object): all_issues = [] for contract in contracts or self.contracts: - sym = SymExecWrapper( - contract, - address, - strategy, - dynloader=DynLoader( - self.eth, - storage_loading=self.onchain_storage_access, - contract_loading=self.dynld, - ), - max_depth=max_depth, - execution_timeout=execution_timeout, - create_timeout=create_timeout, - transaction_count=transaction_count, - modules=modules, - ) - - issues = fire_lasers(sym, modules) + try: + sym = SymExecWrapper( + contract, + address, + strategy, + dynloader=DynLoader( + self.eth, + storage_loading=self.onchain_storage_access, + contract_loading=self.dynld, + ), + max_depth=max_depth, + execution_timeout=execution_timeout, + create_timeout=create_timeout, + transaction_count=transaction_count, + modules=modules, + ) + issues = fire_lasers(sym, modules) + except KeyboardInterrupt: + log.critical("Keyboard Interrupt") + issues = retrieve_callback_issues(modules) + except Exception: + log.critical( + "Exception occurred, aborting analysis\n" + traceback.format_exc() + ) + issues = retrieve_callback_issues(modules) if type(contract) == SolidityContract: for issue in issues: From a60e14c903de48ad234da6ae0376a86bc9633907 Mon Sep 17 00:00:00 2001 From: Nathan Date: Sat, 15 Dec 2018 14:21:22 -0500 Subject: [PATCH 02/24] Remove unhelpful log message --- mythril/analysis/security.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/mythril/analysis/security.py b/mythril/analysis/security.py index 93a882da..db272a49 100644 --- a/mythril/analysis/security.py +++ b/mythril/analysis/security.py @@ -74,8 +74,6 @@ def fire_lasers(statespace, module_names=()): def retrieve_callback_issues(module_names=()): - log.info("Starting analysis") - issues = [] for module in get_detection_modules( entrypoint="callback", include_modules=module_names From de5eb94fc0cfe7042e8af50416abb75c5b5c7eb5 Mon Sep 17 00:00:00 2001 From: Nathan Date: Mon, 17 Dec 2018 13:46:22 -0500 Subject: [PATCH 03/24] Command users to report issues to GitHub --- mythril/mythril.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/mythril.py b/mythril/mythril.py index a4a0506b..d3c87825 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -503,7 +503,7 @@ class Mythril(object): issues = retrieve_callback_issues(modules) except Exception: log.critical( - "Exception occurred, aborting analysis\n" + traceback.format_exc() + "Exception occurred, aborting analysis. Please report this issue to the Mythril GitHub page.\n" + traceback.format_exc() ) issues = retrieve_callback_issues(modules) From c025b9642a6f23e58b6ab3dcd63250d7feb4e201 Mon Sep 17 00:00:00 2001 From: Nathan Date: Mon, 17 Dec 2018 13:46:56 -0500 Subject: [PATCH 04/24] Apply black --- mythril/mythril.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/mythril.py b/mythril/mythril.py index d3c87825..03991b5f 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -503,7 +503,8 @@ class Mythril(object): issues = retrieve_callback_issues(modules) except Exception: log.critical( - "Exception occurred, aborting analysis. Please report this issue to the Mythril GitHub page.\n" + traceback.format_exc() + "Exception occurred, aborting analysis. Please report this issue to the Mythril GitHub page.\n" + + traceback.format_exc() ) issues = retrieve_callback_issues(modules) From 94464235574036e84ec2cac7d54927d36f2de96b Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 19 Dec 2018 14:16:29 +0530 Subject: [PATCH 05/24] Remove calldata type --- mythril/laser/ethereum/call.py | 15 +++------------ mythril/laser/ethereum/instructions.py | 17 +++++++---------- mythril/laser/ethereum/state/calldata.py | 6 ------ mythril/laser/ethereum/state/environment.py | 5 +---- mythril/laser/ethereum/transaction/concolic.py | 3 +-- mythril/laser/ethereum/transaction/symbolic.py | 8 +------- .../ethereum/transaction/transaction_models.py | 14 +------------- 7 files changed, 14 insertions(+), 54 deletions(-) diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 9b9801c7..c2925c4a 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -3,11 +3,7 @@ from typing import Union from mythril.laser.smt import simplify, Expression, symbol_factory import mythril.laser.ethereum.util as util from mythril.laser.ethereum.state.account import Account -from mythril.laser.ethereum.state.calldata import ( - CalldataType, - SymbolicCalldata, - ConcreteCalldata, -) +from mythril.laser.ethereum.state.calldata import SymbolicCalldata, ConcreteCalldata from mythril.laser.ethereum.state.global_state import GlobalState from mythril.support.loader import DynLoader import re @@ -40,9 +36,7 @@ def get_call_parameters( callee_address = get_callee_address(global_state, dynamic_loader, to) callee_account = None - call_data, call_data_type = get_call_data( - global_state, memory_input_offset, memory_input_size - ) + call_data = get_call_data(global_state, memory_input_offset, memory_input_size) if int(callee_address, 16) >= 5 or int(callee_address, 16) == 0: callee_account = get_callee_account( @@ -54,7 +48,6 @@ def get_call_parameters( callee_account, call_data, value, - call_data_type, gas, memory_out_offset, memory_out_size, @@ -181,11 +174,9 @@ def get_call_data( ) ] call_data = ConcreteCalldata(transaction_id, calldata_from_mem) - call_data_type = CalldataType.CONCRETE log.debug("Calldata: " + str(call_data)) except TypeError: log.debug("Unsupported symbolic calldata offset") - call_data_type = CalldataType.SYMBOLIC call_data = SymbolicCalldata("{}_internalcall".format(transaction_id)) - return call_data, call_data_type + return call_data diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 127c9162..cc541698 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -39,7 +39,7 @@ from mythril.laser.ethereum.evm_exceptions import ( ) from mythril.laser.ethereum.gas import OPCODE_GAS from mythril.laser.ethereum.keccak import KeccakFunctionManager -from mythril.laser.ethereum.state.calldata import CalldataType +from mythril.laser.ethereum.state.calldata import SymbolicCalldata, ConcreteCalldata from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction import ( MessageCallTransaction, @@ -1282,7 +1282,7 @@ 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( + callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( global_state, self.dynamic_loader, True ) except ValueError as e: @@ -1302,7 +1302,7 @@ class Instruction: if 0 < int(callee_address, 16) < 5: log.debug("Native contract called: " + callee_address) - if call_data == [] and call_data_type == CalldataType.SYMBOLIC: + if call_data == [] and isinstance(call_data, SymbolicCalldata): log.debug("CALL with symbolic data not supported") return [global_state] @@ -1354,7 +1354,6 @@ class Instruction: ), callee_account=callee_account, call_data=call_data, - call_data_type=call_data_type, call_value=value, ) raise TransactionStartSignal(transaction, self.op_code) @@ -1427,7 +1426,7 @@ class Instruction: environment = global_state.environment try: - callee_address, callee_account, call_data, value, call_data_type, gas, _, _ = get_call_parameters( + callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters( global_state, self.dynamic_loader, True ) except ValueError as e: @@ -1450,7 +1449,6 @@ class Instruction: caller=environment.address, callee_account=environment.active_account, call_data=call_data, - call_data_type=call_data_type, call_value=value, ) raise TransactionStartSignal(transaction, self.op_code) @@ -1460,7 +1458,7 @@ class Instruction: instr = global_state.get_current_instruction() try: - callee_address, _, _, value, _, _, memory_out_offset, memory_out_size = get_call_parameters( + callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters( global_state, self.dynamic_loader, True ) except ValueError as e: @@ -1521,7 +1519,7 @@ class Instruction: environment = global_state.environment try: - callee_address, callee_account, call_data, value, call_data_type, gas, _, _ = get_call_parameters( + callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters( global_state, self.dynamic_loader ) except ValueError as e: @@ -1544,7 +1542,6 @@ class Instruction: caller=environment.sender, callee_account=environment.active_account, call_data=call_data, - call_data_type=call_data_type, call_value=environment.callvalue, ) raise TransactionStartSignal(transaction, self.op_code) @@ -1554,7 +1551,7 @@ class Instruction: instr = global_state.get_current_instruction() try: - callee_address, _, _, value, _, _, memory_out_offset, memory_out_size = get_call_parameters( + callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters( global_state, self.dynamic_loader ) except ValueError as e: diff --git a/mythril/laser/ethereum/state/calldata.py b/mythril/laser/ethereum/state/calldata.py index e01c3634..ae480c20 100644 --- a/mythril/laser/ethereum/state/calldata.py +++ b/mythril/laser/ethereum/state/calldata.py @@ -1,4 +1,3 @@ -from enum import Enum from typing import Union, Any from mythril.laser.smt import K, Array, If, simplify, Concat, Expression, BitVec @@ -10,11 +9,6 @@ from z3 import Model from z3.z3types import Z3Exception -class CalldataType(Enum): - CONCRETE = 1 - SYMBOLIC = 2 - - class BaseCalldata: """ Base calldata class diff --git a/mythril/laser/ethereum/state/environment.py b/mythril/laser/ethereum/state/environment.py index 739e649c..8db1d56a 100644 --- a/mythril/laser/ethereum/state/environment.py +++ b/mythril/laser/ethereum/state/environment.py @@ -4,7 +4,7 @@ from z3 import ExprRef, BitVecVal from mythril.laser.smt import symbol_factory from mythril.laser.ethereum.state.account import Account -from mythril.laser.ethereum.state.calldata import CalldataType, BaseCalldata +from mythril.laser.ethereum.state.calldata import BaseCalldata class Environment: @@ -21,7 +21,6 @@ class Environment: callvalue: ExprRef, origin: ExprRef, code=None, - calldata_type=CalldataType.SYMBOLIC, ): # Metadata @@ -35,7 +34,6 @@ class Environment: self.sender = sender self.calldata = calldata - self.calldata_type = calldata_type self.gasprice = gasprice self.origin = origin self.callvalue = callvalue @@ -52,5 +50,4 @@ class Environment: gasprice=self.gasprice, callvalue=self.callvalue, origin=self.origin, - calldata_type=self.calldata_type, ) diff --git a/mythril/laser/ethereum/transaction/concolic.py b/mythril/laser/ethereum/transaction/concolic.py index 27c9de1a..a1889a20 100644 --- a/mythril/laser/ethereum/transaction/concolic.py +++ b/mythril/laser/ethereum/transaction/concolic.py @@ -2,7 +2,7 @@ from typing import List, Union from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.cfg import Node, Edge, JumpType -from mythril.laser.ethereum.state.calldata import CalldataType, ConcreteCalldata +from mythril.laser.ethereum.state.calldata import ConcreteCalldata from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction.transaction_models import ( MessageCallTransaction, @@ -39,7 +39,6 @@ def execute_message_call( caller=caller_address, callee_account=open_world_state[callee_address], call_data=ConcreteCalldata(next_transaction_id, data), - call_data_type=CalldataType.SYMBOLIC, call_value=value, ) diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 117322d8..350fdd45 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -4,11 +4,7 @@ import logging from mythril.laser.smt import symbol_factory from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.cfg import Node, Edge, JumpType -from mythril.laser.ethereum.state.calldata import ( - CalldataType, - BaseCalldata, - SymbolicCalldata, -) +from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.transaction.transaction_models import ( MessageCallTransaction, @@ -47,7 +43,6 @@ def execute_message_call(laser_evm, callee_address: str) -> None: caller=symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256), callee_account=open_world_state[callee_address], call_data=SymbolicCalldata(next_transaction_id), - call_data_type=CalldataType.SYMBOLIC, call_value=symbol_factory.BitVecSym( "call_value{}".format(next_transaction_id), 256 ), @@ -87,7 +82,6 @@ def execute_contract_creation( caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256), callee_account=new_account, call_data=[], - call_data_type=CalldataType.SYMBOLIC, call_value=symbol_factory.BitVecSym( "call_value{}".format(next_transaction_id), 256 ), diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 55423d66..b6a1cd53 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -3,11 +3,7 @@ from mythril.disassembler.disassembly import Disassembly from mythril.laser.smt import symbol_factory from mythril.laser.ethereum.state.environment import Environment -from mythril.laser.ethereum.state.calldata import ( - BaseCalldata, - ConcreteCalldata, - SymbolicCalldata, -) +from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.state.global_state import GlobalState @@ -57,7 +53,6 @@ class BaseTransaction: gas_limit=None, origin=None, code=None, - call_data_type=None, call_value=None, init_call_data=True, ): @@ -86,11 +81,6 @@ class BaseTransaction: else: self.call_data = call_data if isinstance(call_data, BaseCalldata) else None - self.call_data_type = ( - call_data_type - if call_data_type is not None - else symbol_factory.BitVecSym("call_data_type{}".format(identifier), 256) - ) self.call_value = ( call_value if call_value is not None @@ -122,7 +112,6 @@ class MessageCallTransaction(BaseTransaction): self.call_value, self.origin, code=self.code or self.callee_account.code, - calldata_type=self.call_data_type, ) return super().initial_global_state_from_environment( environment, active_function="fallback" @@ -153,7 +142,6 @@ class ContractCreationTransaction(BaseTransaction): self.call_value, self.origin, self.code, - calldata_type=self.call_data_type, ) return super().initial_global_state_from_environment( environment, active_function="constructor" From 3f2ff85683b07f6ca3b3d26160fb676452968708 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Thu, 20 Dec 2018 13:24:45 +0530 Subject: [PATCH 06/24] Merge with master --- mythril/laser/ethereum/call.py | 55 +++++++++++++++++- mythril/laser/ethereum/instructions.py | 74 +++++++++---------------- mythril/laser/ethereum/state/account.py | 11 ++-- tests/native_test.py | 6 +- 4 files changed, 90 insertions(+), 56 deletions(-) diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index c2925c4a..112e0cfc 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -1,9 +1,16 @@ import logging -from typing import Union +from typing import Union, List + +from mythril.laser.ethereum import natives +from mythril.laser.ethereum.gas import OPCODE_GAS from mythril.laser.smt import simplify, Expression, symbol_factory import mythril.laser.ethereum.util as util from mythril.laser.ethereum.state.account import Account -from mythril.laser.ethereum.state.calldata import SymbolicCalldata, ConcreteCalldata +from mythril.laser.ethereum.state.calldata import ( + BaseCalldata, + SymbolicCalldata, + ConcreteCalldata, +) from mythril.laser.ethereum.state.global_state import GlobalState from mythril.support.loader import DynLoader import re @@ -180,3 +187,47 @@ def get_call_data( call_data = SymbolicCalldata("{}_internalcall".format(transaction_id)) return call_data + + +def native_call( + global_state: GlobalState, + callee_address: str, + call_data: BaseCalldata, + memory_out_offset: Union[int, Expression], + memory_out_size: Union[int, Expression], +) -> Union[List[GlobalState], None]: + if not 0 < int(callee_address, 16) < 5: + return None + + log.debug("Native contract called: " + callee_address) + try: + mem_out_start = util.get_concrete_int(memory_out_offset) + mem_out_sz = util.get_concrete_int(memory_out_size) + except TypeError: + log.debug("CALL with symbolic start or offset not supported") + return [global_state] + + contract_list = ["ecrecover", "sha256", "ripemd160", "identity"] + call_address_int = int(callee_address, 16) + native_gas_min, native_gas_max = OPCODE_GAS["NATIVE_COST"]( + global_state.mstate.calculate_extension_size(mem_out_start, mem_out_sz), + contract_list[call_address_int - 1], + ) + global_state.mstate.min_gas_used += native_gas_min + global_state.mstate.max_gas_used += native_gas_max + global_state.mstate.mem_extend(mem_out_start, mem_out_sz) + try: + data = natives.native_contracts(call_address_int, call_data) + except natives.NativeContractException: + for i in range(mem_out_sz): + global_state.mstate.memory[mem_out_start + i] = global_state.new_bitvec( + contract_list[call_address_int - 1] + "(" + str(call_data) + ")", 8 + ) + return [global_state] + + for i in range( + min(len(data), mem_out_sz) + ): # If more data is used then it's chopped off + global_state.mstate.memory[mem_out_start + i] = data[i] + # TODO: maybe use BitVec here constrained to 1 + return [global_state] diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index cc541698..340976cf 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -26,10 +26,9 @@ from mythril.laser.smt import ( ) from mythril.laser.smt import symbol_factory -import mythril.laser.ethereum.natives as natives import mythril.laser.ethereum.util as helper from mythril.laser.ethereum import util -from mythril.laser.ethereum.call import get_call_parameters +from mythril.laser.ethereum.call import get_call_parameters, native_call from mythril.laser.ethereum.evm_exceptions import ( VmException, StackUnderflowException, @@ -39,7 +38,6 @@ from mythril.laser.ethereum.evm_exceptions import ( ) from mythril.laser.ethereum.gas import OPCODE_GAS from mythril.laser.ethereum.keccak import KeccakFunctionManager -from mythril.laser.ethereum.state.calldata import SymbolicCalldata, ConcreteCalldata from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction import ( MessageCallTransaction, @@ -48,7 +46,6 @@ from mythril.laser.ethereum.transaction import ( ) from mythril.support.loader import DynLoader -from mythril.analysis.solver import get_model log = logging.getLogger(__name__) @@ -1300,49 +1297,11 @@ class Instruction: global_state.new_bitvec("retval_" + str(instr["address"]), 256) ) - if 0 < int(callee_address, 16) < 5: - log.debug("Native contract called: " + callee_address) - if call_data == [] and isinstance(call_data, SymbolicCalldata): - log.debug("CALL with symbolic data not supported") - return [global_state] - - try: - mem_out_start = helper.get_concrete_int(memory_out_offset) - mem_out_sz = helper.get_concrete_int(memory_out_size) - except TypeError: - log.debug("CALL with symbolic start or offset not supported") - return [global_state] - - contract_list = ["ecrecover", "sha256", "ripemd160", "identity"] - call_address_int = int(callee_address, 16) - native_gas_min, native_gas_max = OPCODE_GAS["NATIVE_COST"]( - global_state.mstate.calculate_extension_size(mem_out_start, mem_out_sz), - contract_list[call_address_int - 1], - ) - global_state.mstate.min_gas_used += native_gas_min - global_state.mstate.max_gas_used += native_gas_max - global_state.mstate.mem_extend(mem_out_start, mem_out_sz) - try: - data = natives.native_contracts(call_address_int, call_data) - except natives.NativeContractException: - for i in range(mem_out_sz): - global_state.mstate.memory[ - mem_out_start + i - ] = global_state.new_bitvec( - contract_list[call_address_int - 1] - + "(" - + str(call_data) - + ")", - 8, - ) - return [global_state] - - for i in range( - min(len(data), mem_out_sz) - ): # If more data is used then it's chopped off - global_state.mstate.memory[mem_out_start + i] = data[i] - # TODO: maybe use BitVec here constrained to 1 - return [global_state] + native_result = native_call( + global_state, callee_address, call_data, memory_out_offset, memory_out_size + ) + if native_result: + return native_result transaction = MessageCallTransaction( world_state=global_state.world_state, @@ -1610,7 +1569,28 @@ class Instruction: def staticcall_(self, global_state: GlobalState) -> List[GlobalState]: # TODO: implement me instr = global_state.get_current_instruction() + 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 + ) + except ValueError as e: + log.debug( + "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( + e + ) + ) + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + return [global_state] + global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) ) + native_result = native_call( + global_state, callee_address, call_data, memory_out_offset, memory_out_size + ) + if native_result: + return native_result + return [global_state] diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 25504a39..561c45cd 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -31,11 +31,14 @@ class Storage: and (self.dynld and self.dynld.storage_loading) ): try: - self._storage[item] = int( - self.dynld.read_storage( - contract_address=self.address, index=int(item) + self._storage[item] = symbol_factory.BitVecVal( + int( + self.dynld.read_storage( + contract_address=self.address, index=int(item) + ), + 16, ), - 16, + 256, ) return self._storage[item] except ValueError: diff --git a/tests/native_test.py b/tests/native_test.py index 815e950d..e4996ee9 100644 --- a/tests/native_test.py +++ b/tests/native_test.py @@ -14,12 +14,12 @@ IDENTITY_TEST = [(0, False) for _ in range(2)] # These are Random numbers to check whether the 'if condition' is entered or not # (True means entered) SHA256_TEST[0] = (hex(5555555555555555), True) -SHA256_TEST[1] = (hex(323232325445454546), True) +SHA256_TEST[1] = (hex(323232325445454546), False) SHA256_TEST[2] = (hex(34756834765834658), True) -SHA256_TEST[3] = (hex(8756476956956795876987), True) +SHA256_TEST[3] = (hex(8756476956956795876987), False) RIPEMD160_TEST[0] = (hex(999999999999999999993), True) -RIPEMD160_TEST[1] = (hex(1111111111112), True) +RIPEMD160_TEST[1] = (hex(1111111111112), False) ECRECOVER_TEST[0] = (hex(674837568743979857398564869), True) ECRECOVER_TEST[1] = (hex(3487683476979311), False) From 80b64db594feef47f3e2a3c6d67b19c3a9650bbf Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Thu, 20 Dec 2018 17:31:53 +0530 Subject: [PATCH 07/24] Remove extra parameter in staticcall --- mythril/laser/ethereum/instructions.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 340976cf..ad694e83 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1570,7 +1570,7 @@ class Instruction: # TODO: implement me instr = global_state.get_current_instruction() try: - callee_address, callee_account, call_data, value, call_data_type, gas, memory_out_offset, memory_out_size = get_call_parameters( + callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( global_state, self.dynamic_loader ) except ValueError as e: From 53df2b9cc9a31532f66c360596cbdda44372baa4 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Thu, 20 Dec 2018 17:33:31 +0530 Subject: [PATCH 08/24] Assert each test in native tests --- tests/native_test.py | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/tests/native_test.py b/tests/native_test.py index e4996ee9..e36f68a2 100644 --- a/tests/native_test.py +++ b/tests/native_test.py @@ -75,13 +75,8 @@ def _all_info(laser): def _test_natives(laser_info, test_list, test_name): - success = 0 for i, j in test_list: - if (str(i) in laser_info or str(int(i, 16)) in laser_info) == j: - success += 1 - else: - print("Failed:", str(int(i, 16)), str(j)) - assert success == len(test_list) + assert (str(i) in laser_info or str(int(i, 16)) in laser_info) == j class NativeTests(BaseTestCase): @@ -99,7 +94,6 @@ class NativeTests(BaseTestCase): laser_info = str(_all_info(laser)) - print(laser_info) _test_natives(laser_info, SHA256_TEST, "SHA256") _test_natives(laser_info, RIPEMD160_TEST, "RIPEMD160") _test_natives(laser_info, ECRECOVER_TEST, "ECRECOVER") From 7f80ab772f19b2bd5b434663725f7b403743012c Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 24 Dec 2018 12:05:10 +0700 Subject: [PATCH 09/24] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index a8b063a2..df757b9f 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ Mythril Classic is an open-source security analysis tool for Ethereum smart cont Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs. -Oh and by the way, we're also building an easy-to-use security analysis platform (a.k.a. "the INFURA for smart contract security") that anybody can use to create purpose-built security tools. It's called [MythX](https://mythril.ai) and you should definitely [check it out](https://media.consensys.net/mythril-platform-api-is-upping-the-smart-contract-security-game-eee1d2642488). +Oh and by the way, we're also building an easy-to-use security analysis platform (a.k.a. "the INFURA for smart contract security") that anybody can use to create purpose-built security tools. It's called [MythX](https://mythx.io) and you should definitely [check it out](https://mythx.io). ## Installation and setup From a00aad5f0ae48ad8cc2fd1ccb72a64d5184d4994 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 24 Dec 2018 12:11:08 +0700 Subject: [PATCH 10/24] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index df757b9f..36acb27e 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ Mythril Classic is an open-source security analysis tool for Ethereum smart cont Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs. -Oh and by the way, we're also building an easy-to-use security analysis platform (a.k.a. "the INFURA for smart contract security") that anybody can use to create purpose-built security tools. It's called [MythX](https://mythx.io) and you should definitely [check it out](https://mythx.io). +Oh and by the way, we're also building an [easy-to-use security analysis platform called MythX](https://mythx.io) that integrates seamlessly with Truffle, Visual Studio Code, Github and other environments. If you're looking for tooling to plug into your SDLC you should check it out. ## Installation and setup From b025fa813d04338e8746cea3780bc027e6c9af1c Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 26 Dec 2018 15:45:25 +0530 Subject: [PATCH 11/24] Move eth-tester version --- requirements.txt | 2 +- setup.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/requirements.txt b/requirements.txt index c34147e3..815a2771 100644 --- a/requirements.txt +++ b/requirements.txt @@ -10,7 +10,7 @@ eth-hash>=0.1.0 eth-keyfile>=0.5.1 eth-keys>=0.2.0b3 eth-rlp>=0.1.0 -eth-tester>=0.1.0b21 +eth-tester==0.1.0b32 eth-typing>=2.0.0 eth-utils>=1.0.1 jinja2>=2.9 diff --git a/setup.py b/setup.py index f1427861..0b40ac80 100755 --- a/setup.py +++ b/setup.py @@ -87,7 +87,7 @@ setup( "eth-keyfile>=0.5.1", "eth-keys>=0.2.0b3", "eth-rlp>=0.1.0", - "eth-tester>=0.1.0b21", + "eth-tester==0.1.0b32", "eth-typing>=2.0.0", "coverage", "jinja2>=2.9", From 5e7d149e0f227ccc428f0aac11033e639d4d889a Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Thu, 27 Dec 2018 14:27:06 +0530 Subject: [PATCH 12/24] Put BitVecVals in stack --- mythril/laser/ethereum/instructions.py | 4 +++- mythril/laser/ethereum/state/account.py | 2 +- mythril/laser/ethereum/state/memory.py | 8 ++++++-- 3 files changed, 10 insertions(+), 4 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index af736235..ed02ad9d 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -371,7 +371,9 @@ class Instruction: ) else: - state.stack.append(pow(base.value, exponent.value, 2 ** 256)) + state.stack.append( + symbol_factory.BitVecVal(pow(base.value, exponent.value, 2 ** 256), 256) + ) return [global_state] diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 561c45cd..e4bbaf63 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -44,7 +44,7 @@ class Storage: except ValueError: pass if self.concrete: - return 0 + return symbol_factory.BitVecVal(0, 256) self._storage[item] = symbol_factory.BitVecVal(0, 256) return self._storage[item] diff --git a/mythril/laser/ethereum/state/memory.py b/mythril/laser/ethereum/state/memory.py index 91af2ed0..1777b959 100644 --- a/mythril/laser/ethereum/state/memory.py +++ b/mythril/laser/ethereum/state/memory.py @@ -29,8 +29,12 @@ class Memory: :return: 32 byte word at the specified index """ try: - return util.concrete_int_from_bytes( - bytes([util.get_concrete_int(b) for b in self[index : index + 32]]), 0 + return symbol_factory.BitVecVal( + util.concrete_int_from_bytes( + bytes([util.get_concrete_int(b) for b in self[index : index + 32]]), + 0, + ), + 256, ) except: result = simplify( From af298a218bbffbebc8d48f31d1a1d235bec4f9d2 Mon Sep 17 00:00:00 2001 From: Nathan Date: Thu, 27 Dec 2018 10:48:10 -0800 Subject: [PATCH 13/24] Implement sigalrm timeout --- mythril/alarm.py | 25 ++++++++++++++++ mythril/exceptions.py | 4 +++ mythril/laser/ethereum/svm.py | 54 +++++++++++++++++++---------------- 3 files changed, 58 insertions(+), 25 deletions(-) create mode 100644 mythril/alarm.py diff --git a/mythril/alarm.py b/mythril/alarm.py new file mode 100644 index 00000000..4c546bf4 --- /dev/null +++ b/mythril/alarm.py @@ -0,0 +1,25 @@ +import signal +from types import FrameType +from mythril.exceptions import OutOfTimeError + + +def sigalrm_handler(signum: int, frame: FrameType) -> None: + raise OutOfTimeError + + +def start_timeout(timeout: int) -> None: + """ + Starts a timeout + :param timeout: Time in seconds to set the timeout for + :return: None + """ + signal.signal(signal.SIGALRM, sigalrm_handler) + signal.alarm(timeout) + + +def disable_timeout() -> None: + """ + Ensures that the timeout is disabled + :return: None + """ + signal.alarm(0) diff --git a/mythril/exceptions.py b/mythril/exceptions.py index bbcb5110..055a03b4 100644 --- a/mythril/exceptions.py +++ b/mythril/exceptions.py @@ -2,6 +2,10 @@ class MythrilBaseException(Exception): pass +class OutOfTimeError(MythrilBaseException): + pass + + class CompilerError(MythrilBaseException): pass diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 085e3c14..04788961 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -5,6 +5,8 @@ from datetime import datetime, timedelta from functools import reduce from typing import List, Tuple, Union, Callable, Dict +from mythril import alarm +from mythril.exceptions import OutOfTimeError 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 @@ -99,29 +101,37 @@ class LaserEVM: self, main_address=None, creation_code=None, contract_name=None ) -> None: log.debug("Starting LASER execution") - self.time = datetime.now() - if main_address: - log.info("Starting message call transaction to {}".format(main_address)) - self._execute_transactions(main_address) + try: + alarm.start_timeout(self.execution_timeout) + self.time = datetime.now() - elif creation_code: - log.info("Starting contract creation transaction") - created_account = execute_contract_creation( - self, creation_code, contract_name - ) - log.info( - "Finished contract creation, found {} open states".format( - len(self.open_states) + if main_address: + log.info("Starting message call transaction to {}".format(main_address)) + self._execute_transactions(main_address) + + elif creation_code: + log.info("Starting contract creation transaction") + created_account = execute_contract_creation( + self, creation_code, contract_name ) - ) - if len(self.open_states) == 0: - log.warning( - "No contract was created during the execution of contract creation " - "Increase the resources for creation execution (--max-depth or --create-timeout)" + log.info( + "Finished contract creation, found {} open states".format( + len(self.open_states) + ) ) + if len(self.open_states) == 0: + log.warning( + "No contract was created during the execution of contract creation " + "Increase the resources for creation execution (--max-depth or --create-timeout)" + ) + + self._execute_transactions(created_account.address) - self._execute_transactions(created_account.address) + except OutOfTimeError: + log.warning("Timeout occurred, ending symbolic execution") + finally: + alarm.disable_timeout() log.info("Finished symbolic execution") log.info( @@ -172,13 +182,7 @@ class LaserEVM: def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]: final_states = [] for global_state in self.strategy: - if self.execution_timeout and not create: - if ( - self.time + timedelta(seconds=self.execution_timeout) - <= datetime.now() - ): - return final_states + [global_state] if track_gas else None - elif self.create_timeout and create: + if self.create_timeout and create: if self.time + timedelta(seconds=self.create_timeout) <= datetime.now(): return final_states + [global_state] if track_gas else None From 98914418267ffde98c4880fec6b2d19da8974a61 Mon Sep 17 00:00:00 2001 From: Aleksandr Sobolev Date: Fri, 28 Dec 2018 23:09:11 +0700 Subject: [PATCH 14/24] Configure call to webhook in Circle CI build --- .circleci/config.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.circleci/config.yml b/.circleci/config.yml index 0638f0dd..8b537d6a 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -74,6 +74,12 @@ jobs: # command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi # working_directory: /home + - run: + name: Call webhook + command: | + curl -I -X POST -H -d "https://circleci.com/api/v1/project/${ORGANIZATION}/${WEBHOOK_PROJECT}/tree/master?circle-token=${CIRCLE_TOKEN}" | head -n 1 | cut -d$' ' -f2 + + pypi_release: <<: *defaults steps: From d5e1301922a0e8eb34f8687cb45d809406f70e4b Mon Sep 17 00:00:00 2001 From: Nathan Date: Fri, 28 Dec 2018 10:42:40 -0800 Subject: [PATCH 15/24] Handle None execution_timeout --- mythril/laser/ethereum/svm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 04788961..9f9d96ed 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -70,7 +70,7 @@ class LaserEVM: self.max_depth = max_depth self.transaction_count = transaction_count - self.execution_timeout = execution_timeout + self.execution_timeout = execution_timeout or 0 self.create_timeout = create_timeout self.time = None From e7e2d5093f705170432c95c130ee703de77cfba9 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sat, 29 Dec 2018 12:14:01 +0530 Subject: [PATCH 16/24] Add function name to node initialization --- mythril/laser/ethereum/cfg.py | 10 ++++++++-- mythril/laser/ethereum/transaction/symbolic.py | 5 ++++- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/cfg.py b/mythril/laser/ethereum/cfg.py index 93950104..553ad082 100644 --- a/mythril/laser/ethereum/cfg.py +++ b/mythril/laser/ethereum/cfg.py @@ -19,13 +19,19 @@ class NodeFlags(Flags): class Node: - def __init__(self, contract_name: str, start_addr=0, constraints=None): + def __init__( + self, + contract_name: str, + start_addr=0, + constraints=None, + function_name="unknown", + ): constraints = constraints if constraints else [] self.contract_name = contract_name self.start_addr = start_addr self.states = [] self.constraints = constraints - self.function_name = "unknown" + self.function_name = function_name self.flags = NodeFlags() # Self-assign a unique ID diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 117322d8..6659c6f0 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -104,7 +104,10 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None: global_state = transaction.initial_global_state() global_state.transaction_stack.append((transaction, None)) - new_node = Node(global_state.environment.active_account.contract_name) + new_node = Node( + global_state.environment.active_account.contract_name, + function_name=global_state.environment.active_function_name, + ) laser_evm.nodes[new_node.uid] = new_node if transaction.world_state.node: From cfaa92f1f85196d5365bb228d2ecabb9436030be Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sat, 29 Dec 2018 15:08:27 +0700 Subject: [PATCH 17/24] Log number of open states at start of TX --- mythril/laser/ethereum/svm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 085e3c14..0bc67ef4 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -149,7 +149,7 @@ class LaserEVM: initial_coverage = self._get_covered_instructions() self.time = datetime.now() - log.info("Starting message call transaction, iteration: {}".format(i)) + log.info("Starting message call transaction, iteration: {}, {} initial states".format(i, len(self.open_states))) execute_message_call(self, address) From 89c5b4d9eabf5772ad63afba4f1030289d49866f Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sat, 29 Dec 2018 15:11:37 +0700 Subject: [PATCH 18/24] Black black black --- mythril/laser/ethereum/svm.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 0bc67ef4..62b9df28 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -149,7 +149,11 @@ class LaserEVM: initial_coverage = self._get_covered_instructions() self.time = datetime.now() - log.info("Starting message call transaction, iteration: {}, {} initial states".format(i, len(self.open_states))) + log.info( + "Starting message call transaction, iteration: {}, {} initial states".format( + i, len(self.open_states) + ) + ) execute_message_call(self, address) From 45f1a57c5f06d17aedf46d0a8898147f83200eba Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 31 Dec 2018 15:47:24 +0530 Subject: [PATCH 19/24] Save the entire statespace only when needed --- mythril/analysis/modules/base.py | 3 +- mythril/analysis/symbolic.py | 11 +++++-- mythril/laser/ethereum/svm.py | 32 ++++++++++++------- .../laser/ethereum/transaction/symbolic.py | 19 +++++------ mythril/mythril.py | 1 + mythril/support/truffle.py | 2 ++ 6 files changed, 44 insertions(+), 24 deletions(-) diff --git a/mythril/analysis/modules/base.py b/mythril/analysis/modules/base.py index e7ece1e8..c143947c 100644 --- a/mythril/analysis/modules/base.py +++ b/mythril/analysis/modules/base.py @@ -35,7 +35,8 @@ class DetectionModule: "DetectionModule " "name={0.name} " "swc_id={0.swc_id} " - "hooks={0.hooks} " + "pre_hooks={0.pre_hooks} " + "post_hooks={0.post_hooks} " "description={0.description}" ">" ).format(self) diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 2d7aeab7..395d311e 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -1,4 +1,4 @@ -from mythril.analysis.security import get_detection_module_hooks +from mythril.analysis.security import get_detection_module_hooks, get_detection_modules from mythril.laser.ethereum import svm from mythril.laser.ethereum.state.account import Account from mythril.solidity.soliditycontract import SolidityContract, EVMContract @@ -29,6 +29,7 @@ class SymExecWrapper: create_timeout=None, transaction_count=2, modules=(), + compulsory_statespace=True, ): if strategy == "dfs": @@ -48,7 +49,9 @@ class SymExecWrapper: dynamic_loader=dynloader, contract_name=contract.name, ) - + requires_statespace = ( + compulsory_statespace or len(get_detection_modules("post", modules)) > 0 + ) self.accounts = {address: account} self.laser = svm.LaserEVM( @@ -59,6 +62,7 @@ class SymExecWrapper: strategy=s_strategy, create_timeout=create_timeout, transaction_count=transaction_count, + requires_statespace=requires_statespace, ) self.laser.register_hooks( hook_type="pre", @@ -80,6 +84,9 @@ class SymExecWrapper: else: self.laser.sym_exec(address) + if not requires_statespace: + return + self.nodes = self.laser.nodes self.edges = self.laser.edges diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 62b9df28..33952224 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -49,6 +49,7 @@ class LaserEVM: create_timeout=10, strategy=DepthFirstSearchStrategy, transaction_count=2, + requires_statespace=False, ): world_state = WorldState() world_state.accounts = accounts @@ -56,8 +57,6 @@ class LaserEVM: self.world_state = world_state self.open_states = [world_state] - self.nodes = {} - self.edges = [] self.coverage = {} self.total_states = 0 @@ -71,6 +70,11 @@ class LaserEVM: self.execution_timeout = execution_timeout self.create_timeout = create_timeout + self.requires_statespace = requires_statespace + if self.requires_statespace: + self.nodes = {} + self.edges = [] + self.time = None self.pre_hooks = defaultdict(list) @@ -124,12 +128,13 @@ class LaserEVM: self._execute_transactions(created_account.address) log.info("Finished symbolic execution") - log.info( - "%d nodes, %d edges, %d total states", - len(self.nodes), - len(self.edges), - self.total_states, - ) + if self.requires_statespace: + log.info( + "%d nodes, %d edges, %d total states", + len(self.nodes), + len(self.edges), + self.total_states, + ) for code, coverage in self.coverage.items(): cov = ( reduce(lambda sum_, val: sum_ + 1 if val else sum_, coverage[1]) @@ -362,10 +367,13 @@ class LaserEVM: old_node = state.node state.node = new_node new_node.constraints = state.mstate.constraints - self.nodes[new_node.uid] = new_node - self.edges.append( - Edge(old_node.uid, new_node.uid, edge_type=edge_type, condition=condition) - ) + if self.requires_statespace: + self.nodes[new_node.uid] = new_node + self.edges.append( + Edge( + old_node.uid, new_node.uid, edge_type=edge_type, condition=condition + ) + ) if edge_type == JumpType.RETURN: new_node.flags |= NodeFlags.CALL_RETURN diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 117322d8..56ccb8d9 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -105,17 +105,18 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None: global_state.transaction_stack.append((transaction, None)) new_node = Node(global_state.environment.active_account.contract_name) - - laser_evm.nodes[new_node.uid] = new_node + if laser_evm.requires_statespace: + laser_evm.nodes[new_node.uid] = new_node if transaction.world_state.node: - laser_evm.edges.append( - Edge( - transaction.world_state.node.uid, - new_node.uid, - edge_type=JumpType.Transaction, - condition=None, + if laser_evm.requires_statespace: + laser_evm.edges.append( + Edge( + transaction.world_state.node.uid, + new_node.uid, + edge_type=JumpType.Transaction, + condition=None, + ) ) - ) global_state.mstate.constraints += transaction.world_state.node.constraints new_node.constraints = global_state.mstate.constraints diff --git a/mythril/mythril.py b/mythril/mythril.py index 03991b5f..2addc074 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -496,6 +496,7 @@ class Mythril(object): create_timeout=create_timeout, transaction_count=transaction_count, modules=modules, + compulsory_statespace=False, ) issues = fire_lasers(sym, modules) except KeyboardInterrupt: diff --git a/mythril/support/truffle.py b/mythril/support/truffle.py index d38d04de..4d071566 100644 --- a/mythril/support/truffle.py +++ b/mythril/support/truffle.py @@ -56,6 +56,8 @@ def analyze_truffle_project(sigs, args): create_timeout=args.create_timeout, execution_timeout=args.execution_timeout, transaction_count=args.transaction_count, + modules=args.modules, + compulsory_statespace=False, ) issues = fire_lasers(sym) From 2bb3845754eeedf60d4dea6e1195ac50af405161 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 31 Dec 2018 16:02:17 +0530 Subject: [PATCH 20/24] Fix the tests for statespace --- mythril/laser/ethereum/svm.py | 2 +- mythril/support/truffle.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 33952224..2907f5be 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -49,7 +49,7 @@ class LaserEVM: create_timeout=10, strategy=DepthFirstSearchStrategy, transaction_count=2, - requires_statespace=False, + requires_statespace=True, ): world_state = WorldState() world_state.accounts = accounts diff --git a/mythril/support/truffle.py b/mythril/support/truffle.py index 4d071566..6822b136 100644 --- a/mythril/support/truffle.py +++ b/mythril/support/truffle.py @@ -56,7 +56,7 @@ def analyze_truffle_project(sigs, args): create_timeout=args.create_timeout, execution_timeout=args.execution_timeout, transaction_count=args.transaction_count, - modules=args.modules, + modules=args.modules or [], compulsory_statespace=False, ) issues = fire_lasers(sym) From 5c99537365b73e98330152c5dc72ad72c98e621f Mon Sep 17 00:00:00 2001 From: Nathan Date: Mon, 31 Dec 2018 11:12:07 -0800 Subject: [PATCH 21/24] Remove now unneeded nested if --- mythril/laser/ethereum/svm.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 9f9d96ed..fe5cd141 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -182,9 +182,12 @@ class LaserEVM: def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]: final_states = [] for global_state in self.strategy: - if self.create_timeout and create: - if self.time + timedelta(seconds=self.create_timeout) <= datetime.now(): - return final_states + [global_state] if track_gas else None + if ( + self.create_timeout + and create + and self.time + timedelta(seconds=self.create_timeout) <= datetime.now() + ): + return final_states + [global_state] if track_gas else None try: new_states, op_code = self.execute_state(global_state) From baf4f95a7d38cf4cf48fabf019188d26bb0612cc Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 1 Jan 2019 17:24:14 +0530 Subject: [PATCH 22/24] Add the function_name of node in concolic.py --- mythril/laser/ethereum/transaction/concolic.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/transaction/concolic.py b/mythril/laser/ethereum/transaction/concolic.py index 27c9de1a..d869725b 100644 --- a/mythril/laser/ethereum/transaction/concolic.py +++ b/mythril/laser/ethereum/transaction/concolic.py @@ -54,7 +54,10 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None: global_state = transaction.initial_global_state() global_state.transaction_stack.append((transaction, None)) - new_node = Node(global_state.environment.active_account.contract_name) + new_node = Node( + global_state.environment.active_account.contract_name, + function_name=global_state.environment.active_function_name, + ) laser_evm.nodes[new_node.uid] = new_node if transaction.world_state.node: From 30746d95d9cae1821492955cf33a2df1a5f9cdec Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 1 Jan 2019 17:42:07 +0530 Subject: [PATCH 23/24] Add the node check in concolic.py --- mythril/laser/ethereum/transaction/concolic.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/transaction/concolic.py b/mythril/laser/ethereum/transaction/concolic.py index 27c9de1a..5cad3177 100644 --- a/mythril/laser/ethereum/transaction/concolic.py +++ b/mythril/laser/ethereum/transaction/concolic.py @@ -56,8 +56,9 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None: new_node = Node(global_state.environment.active_account.contract_name) - laser_evm.nodes[new_node.uid] = new_node - if transaction.world_state.node: + if laser_evm.requires_statespace: + laser_evm.nodes[new_node.uid] = new_node + if transaction.world_state.node and laser_evm.requires_statespace: laser_evm.edges.append( Edge( transaction.world_state.node.uid, @@ -66,6 +67,7 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None: condition=None, ) ) + global_state.node = new_node new_node.states.append(global_state) laser_evm.work_list.append(global_state) From e8e4131b9e2447ce5d476912d72b3d6734214ee5 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 2 Jan 2019 19:47:49 +0530 Subject: [PATCH 24/24] Reformat file with black --- mythril/laser/ethereum/transaction/symbolic.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index ecc7d3f9..89e8c6e5 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -103,8 +103,8 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None: function_name=global_state.environment.active_function_name, ) if laser_evm.requires_statespace: - laser_evm.nodes[new_node.uid] = new_node - + laser_evm.nodes[new_node.uid] = new_node + if transaction.world_state.node: if laser_evm.requires_statespace: laser_evm.edges.append(