diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index fb72c93e..3ef4a338 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -50,7 +50,7 @@ def _analyze_states(state: GlobalState) -> List[Issue]: if call.type is not "DELEGATECALL": return [] - if call.node.function_name is not "fallback": + if state.environment.active_function_name is not "fallback": return [] state = call.state @@ -77,8 +77,8 @@ def _concrete_call( return [] issue = Issue( - contract=call.node.contract_name, - function_name=call.node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=address, swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT, bytecode=state.environment.code.bytecode, diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 1450f93a..7a931997 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -71,13 +71,13 @@ def _analyze_states(state: GlobalState) -> list: "The contract sends Ether depending on the values of the following variables:\n" ) - # First check: look for predictable state variables in node & call recipient constraints + # First check: look for predictable state variables in state & call recipient constraints vars = ["coinbase", "gaslimit", "timestamp", "number"] found = [] for var in vars: - for constraint in call.node.constraints[:] + [call.to]: + for constraint in call.state.mstate.constraints[:] + [call.to]: if var in str(constraint): found.append(var) @@ -94,8 +94,8 @@ def _analyze_states(state: GlobalState) -> list: ) issue = Issue( - contract=call.node.contract_name, - function_name=call.node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=address, swc_id=swc_id, bytecode=call.state.environment.code.bytecode, @@ -112,7 +112,7 @@ def _analyze_states(state: GlobalState) -> list: # Second check: blockhash - for constraint in call.node.constraints[:] + [call.to]: + for constraint in call.state.mstate.constraints[:] + [call.to]: if "blockhash" in str(constraint): if "number" in str(constraint): m = re.search(r"blockhash\w+(\s-\s(\d+))*", str(constraint)) @@ -145,8 +145,8 @@ def _analyze_states(state: GlobalState) -> list: description += ", this expression will always be equal to zero." issue = Issue( - contract=call.node.contract_name, - function_name=call.node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=address, bytecode=call.state.environment.code.bytecode, title="Dependence on Predictable Variable", @@ -186,8 +186,8 @@ def _analyze_states(state: GlobalState) -> list: ) ) issue = Issue( - contract=call.node.contract_name, - function_name=call.node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=address, bytecode=call.state.environment.code.bytecode, title="Dependence on Predictable Variable", @@ -212,7 +212,7 @@ def solve(call: Call) -> bool: :return: """ try: - model = solver.get_model(call.node.constraints) + model = solver.get_model(call.state.mstate.constraints) log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] MODEL: " + str(model)) pretty_model = solver.pretty_print_model(model) diff --git a/mythril/analysis/modules/deprecated_ops.py b/mythril/analysis/modules/deprecated_ops.py index a23b55bd..6e8adacc 100644 --- a/mythril/analysis/modules/deprecated_ops.py +++ b/mythril/analysis/modules/deprecated_ops.py @@ -30,13 +30,13 @@ def _analyze_state(state): "Use of msg.origin is deprecated and the instruction may be removed in the future. " "Use msg.sender instead.\nSee also: " "https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin".format( - node.function_name + state.environment.active_function_name ) ) swc_id = DEPRECATED_FUNCTIONS_USAGE elif instruction["opcode"] == "CALLCODE": - log.debug("CALLCODE in function " + node.function_name) + log.debug("CALLCODE in function " + state.environment.active_function_name) title = "Use of callcode" description_head = "Use of callcode is deprecated." description_tail = ( @@ -45,10 +45,12 @@ def _analyze_state(state): "therefore deprecated and may be removed in the future. Use the delegatecall method instead." ) swc_id = DEPRECATED_FUNCTIONS_USAGE + else: + return issue = Issue( - contract=node.contract_name, - function_name=node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=instruction["address"], title=title, bytecode=state.environment.code.bytecode, diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index ccdb5167..d382ca07 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -67,7 +67,6 @@ class EtherThief(DetectionModule): :return: """ instruction = state.get_current_instruction() - node = state.node if instruction["opcode"] != "CALL": return [] @@ -80,7 +79,7 @@ class EtherThief(DetectionModule): eth_sent_total = symbol_factory.BitVecVal(0, 256) - constraints = copy(node.constraints) + constraints = copy(state.mstate.constraints) for tx in state.world_state.transaction_sequence: if tx.caller == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF: @@ -101,8 +100,8 @@ class EtherThief(DetectionModule): debug = json.dumps(transaction_sequence, indent=4) issue = Issue( - contract=node.contract_name, - function_name=node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=instruction["address"], swc_id=UNPROTECTED_ETHER_WITHDRAWAL, title="Unprotected Ether Withdrawal", diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index d819d0ea..8eaf6400 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -19,9 +19,8 @@ def _analyze_state(state) -> list: :return: """ log.info("Exceptions module: found ASSERT_FAIL instruction") - node = state.node - log.debug("ASSERT_FAIL in function " + node.function_name) + log.debug("ASSERT_FAIL in function " + state.environment.active_function_name) try: address = state.get_current_instruction()["address"] @@ -34,12 +33,14 @@ def _analyze_state(state) -> list: "Use `require()` for regular input checking." ) - transaction_sequence = solver.get_transaction_sequence(state, node.constraints) + transaction_sequence = solver.get_transaction_sequence( + state, state.mstate.constraints + ) debug = json.dumps(transaction_sequence, indent=4) issue = Issue( - contract=node.contract_name, - function_name=node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=address, swc_id=ASSERT_VIOLATION, title="Exception State", diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index 00545bc1..95eb428e 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/mythril/analysis/modules/external_calls.py @@ -8,6 +8,7 @@ from mythril.analysis.report import Issue from mythril.laser.smt import UGT, symbol_factory from mythril.laser.ethereum.state.global_state import GlobalState from mythril.exceptions import UnsatError +from copy import copy import logging import json @@ -28,14 +29,13 @@ def _analyze_state(state): :param state: :return: """ - node = state.node gas = state.mstate.stack[-1] to = state.mstate.stack[-2] address = state.get_current_instruction()["address"] try: - constraints = node.constraints + constraints = copy(state.mstate.constraints) transaction_sequence = solver.get_transaction_sequence( state, constraints + [UGT(gas, symbol_factory.BitVecVal(2300, 256))] ) @@ -56,8 +56,8 @@ def _analyze_state(state): ) issue = Issue( - contract=node.contract_name, - function_name=node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=address, swc_id=REENTRANCY, title="External Call To User-Supplied Address", @@ -83,8 +83,8 @@ def _analyze_state(state): ) issue = Issue( - contract=node.contract_name, - function_name=state.node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=address, swc_id=REENTRANCY, title="External Call To Fixed Address", diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index d98ed069..0c6582a0 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -120,7 +120,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): c = Not(BVAddNoOverflow(op0, op1, False)) # Check satisfiable - model = self._try_constraints(state.node.constraints, [c]) + model = self._try_constraints(state.mstate.constraints, [c]) if model is None: return @@ -132,7 +132,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): c = Not(BVMulNoOverflow(op0, op1, False)) # Check satisfiable - model = self._try_constraints(state.node.constraints, [c]) + model = self._try_constraints(state.mstate.constraints, [c]) if model is None: return @@ -144,7 +144,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): c = Not(BVSubNoUnderflow(op0, op1, False)) # Check satisfiable - model = self._try_constraints(state.node.constraints, [c]) + model = self._try_constraints(state.mstate.constraints, [c]) if model is None: return @@ -172,7 +172,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): ) else: constraint = op0.value ** op1.value >= 2 ** 256 - model = self._try_constraints(state.node.constraints, [constraint]) + model = self._try_constraints(state.mstate.constraints, [constraint]) if model is None: return annotation = OverUnderflowAnnotation(state, "exponentiation", constraint) @@ -286,7 +286,6 @@ class IntegerOverflowUnderflowModule(DetectionModule): ): continue - node = ostate.node try: transaction_sequence = solver.get_transaction_sequence( @@ -297,8 +296,8 @@ class IntegerOverflowUnderflowModule(DetectionModule): _type = "Underflow" if annotation.operator == "subtraction" else "Overflow" issue = Issue( - contract=node.contract_name, - function_name=node.function_name, + contract=ostate.environment.active_account.contract_name, + function_name=ostate.environment.active_function_name, address=ostate.get_current_instruction()["address"], swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW, bytecode=ostate.environment.code.bytecode, @@ -319,8 +318,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): @staticmethod def _try_constraints(constraints, new_constraints): - """ - Tries new constraints + """ Tries new constraints :return Model if satisfiable otherwise None """ try: diff --git a/mythril/analysis/modules/multiple_sends.py b/mythril/analysis/modules/multiple_sends.py index a4c650da..1afaaed2 100644 --- a/mythril/analysis/modules/multiple_sends.py +++ b/mythril/analysis/modules/multiple_sends.py @@ -55,7 +55,6 @@ def _analyze_state(state: GlobalState): :param state: the current state :return: returns the issues for that corresponding state """ - node = state.node instruction = state.get_current_instruction() annotations = cast( @@ -95,8 +94,8 @@ def _analyze_state(state: GlobalState): ) issue = Issue( - contract=node.contract_name, - function_name=node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=instruction["address"], swc_id=MULTIPLE_SENDS, bytecode=state.environment.code.bytecode, diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index b9cfce4e..62bc3e00 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -48,13 +48,14 @@ class SuicideModule(DetectionModule): def _analyze_state(self, state): log.info("Suicide module: Analyzing suicide instruction") - node = state.node instruction = state.get_current_instruction() if self._cache_address.get(instruction["address"], False): return [] to = state.mstate.stack[-1] - log.debug("[SUICIDE] SUICIDE in function " + node.function_name) + log.debug( + "[SUICIDE] SUICIDE in function " + state.environment.active_function_name + ) description_head = "The contract can be killed by anyone." @@ -62,7 +63,7 @@ class SuicideModule(DetectionModule): try: transaction_sequence = solver.get_transaction_sequence( state, - node.constraints + state.mstate.constraints + [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF], ) description_tail = ( @@ -71,7 +72,7 @@ class SuicideModule(DetectionModule): ) except UnsatError: transaction_sequence = solver.get_transaction_sequence( - state, node.constraints + state, state.mstate.constraints ) description_tail = "Arbitrary senders can kill this contract." @@ -79,8 +80,8 @@ class SuicideModule(DetectionModule): self._cache_address[instruction["address"]] = True issue = Issue( - contract=node.contract_name, - function_name=node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=instruction["address"], swc_id=UNPROTECTED_SELFDESTRUCT, bytecode=state.environment.code.bytecode, diff --git a/mythril/analysis/modules/unchecked_retval.py b/mythril/analysis/modules/unchecked_retval.py index 5beb0fda..45fdceec 100644 --- a/mythril/analysis/modules/unchecked_retval.py +++ b/mythril/analysis/modules/unchecked_retval.py @@ -61,7 +61,6 @@ class UncheckedRetvalModule(DetectionModule): def _analyze_state(state: GlobalState) -> list: instruction = state.get_current_instruction() - node = state.node annotations = cast( List[UncheckedRetvalAnnotation], @@ -80,7 +79,7 @@ def _analyze_state(state: GlobalState) -> list: issues = [] for retval in retvals: try: - solver.get_model(node.constraints + [retval["retval"] == 0]) + solver.get_model(state.mstate.constraints + [retval["retval"] == 0]) except UnsatError: continue @@ -91,8 +90,8 @@ def _analyze_state(state: GlobalState) -> list: ) issue = Issue( - contract=node.contract_name, - function_name=node.function_name, + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, address=retval["address"], bytecode=state.environment.code.bytecode, title="Unchecked Call Return Value", diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 27df993e..bb86b7a8 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -136,7 +136,7 @@ def get_callee_account( log.debug("Attempting to load dependency") try: - code = dynamic_loader.dynld(environment.active_account.address, callee_address) + code = dynamic_loader.dynld(callee_address) except ValueError as error: log.debug("Unable to execute dynamic loader because: {}".format(str(error))) raise error diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 09152f80..b6bb61cd 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1097,7 +1097,7 @@ class Instruction: return [global_state] try: - code = self.dynamic_loader.dynld(environment.active_account.address, addr) + code = self.dynamic_loader.dynld(addr) except (ValueError, AttributeError) as e: log.debug("error accessing contract storage due to: " + str(e)) state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256)) diff --git a/mythril/laser/ethereum/plugins/implementations/coverage.py b/mythril/laser/ethereum/plugins/implementations/coverage.py new file mode 100644 index 00000000..9310afb8 --- /dev/null +++ b/mythril/laser/ethereum/plugins/implementations/coverage.py @@ -0,0 +1,59 @@ +from mythril.laser.ethereum.svm import LaserEVM +from mythril.laser.ethereum.plugins.plugin import LaserPlugin +from mythril.laser.ethereum.state.global_state import GlobalState + +from typing import Dict, Tuple, List + +import logging + +log = logging.getLogger(__name__) + + +class InstructionCoveragePlugin(LaserPlugin): + """InstructionCoveragePlugin + + This plugin measures the instruction coverage of mythril. + The instruction coverage is the ratio between the instructions that have been executed + and the total amount of instructions. + + Note that with lazy constraint solving enabled that this metric will be "unsound" as + reachability will not be considered for the calculation of instruction coverage. + + """ + + def initialize(self, symbolic_vm: LaserEVM): + """Initializes the instruction coverage plugin + + Introduces hooks for each instruction + :param symbolic_vm: + :return: + """ + coverage = {} # type: Dict[str, Tuple[int, List[bool]]] + + @symbolic_vm.laser_hook("stop_sym_exec") + def stop_sym_exec_hook(): + # Print results + for code, code_cov in coverage.items(): + cov_percentage = sum(code_cov[1]) / float(code_cov[0]) * 100 + + log.info( + "Achieved {:.2f}% coverage for code: {}".format( + cov_percentage, code + ) + ) + + @symbolic_vm.laser_hook("execute_state") + def execute_state_hook(global_state: GlobalState): + # Record coverage + code = global_state.environment.code.bytecode + + if code not in coverage.keys(): + number_of_instructions = len( + global_state.environment.code.instruction_list + ) + coverage[code] = ( + number_of_instructions, + [False] * number_of_instructions, + ) + + coverage[code][1][global_state.mstate.pc] = True diff --git a/mythril/laser/ethereum/plugins/plugin_factory.py b/mythril/laser/ethereum/plugins/plugin_factory.py index 98b5414a..1ce61b34 100644 --- a/mythril/laser/ethereum/plugins/plugin_factory.py +++ b/mythril/laser/ethereum/plugins/plugin_factory.py @@ -21,3 +21,12 @@ class PluginFactory: ) return MutationPruner() + + @staticmethod + def build_instruction_coverage_plugin() -> LaserPlugin: + """ Creates an instance of the instruction coverage plugin""" + from mythril.laser.ethereum.plugins.implementations.coverage import ( + InstructionCoveragePlugin, + ) + + return InstructionCoveragePlugin() diff --git a/mythril/support/loader.py b/mythril/support/loader.py index 6e434439..f46feff5 100644 --- a/mythril/support/loader.py +++ b/mythril/support/loader.py @@ -58,17 +58,15 @@ class DynLoader: return data - def dynld(self, contract_address, dependency_address): + def dynld(self, dependency_address): """ - - :param contract_address: :param dependency_address: :return: """ if not self.contract_loading: raise ValueError("Cannot load contract when contract_loading flag is false") - log.debug("Dynld at contract " + contract_address + ": " + dependency_address) + log.debug("Dynld at contract " + dependency_address) # Ensure that dependency_address is the correct length, with 0s prepended as needed. dependency_address = (