From fda18b3e77b3980d7aa89de27e9edb938207ebbc Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Thu, 2 May 2019 12:19:17 +0200 Subject: [PATCH 01/33] Change timeout logic --- mythril/interfaces/cli.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index adb0e8f2..0fbbab7e 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -216,7 +216,7 @@ def create_parser(parser: argparse.ArgumentParser) -> None: options.add_argument( "--execution-timeout", type=int, - default=600, + default=86400, help="The amount of seconds to spend on symbolic execution", ) options.add_argument( From 409d2171ca8ca95274a528add9e5436559e88c6b Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 8 May 2019 16:31:11 -0700 Subject: [PATCH 02/33] Refactor predictable vars module --- .../modules/dependence_on_predictable_vars.py | 169 ++---------------- 1 file changed, 18 insertions(+), 151 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 7a931997..37fe33d2 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -1,22 +1,17 @@ """This module contains the detection code for predictable variable dependence.""" import logging -import re -from mythril.analysis import solver -from mythril.analysis.call_helpers import get_call_from_state from mythril.analysis.modules.base import DetectionModule -from mythril.analysis.ops import Call, VarType from mythril.analysis.report import Issue from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS -from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.global_state import GlobalState log = logging.getLogger(__name__) class PredictableDependenceModule(DetectionModule): - """This module detects whether Ether is sent using predictable + """This module detects whether control flow decisions are made using predictable parameters.""" def __init__(self) -> None: @@ -25,12 +20,11 @@ class PredictableDependenceModule(DetectionModule): name="Dependence of Predictable Variables", swc_id="{} {}".format(TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS), description=( - "Check for CALLs that send >0 Ether as a result of computation " - "based on predictable variables such as block.coinbase, " - "block.gaslimit, block.timestamp, block.number" + "Check whether control flow decisions are influenced by block.coinbase," + "block.gaslimit, block.timestamp or block.number." ), entrypoint="callback", - pre_hooks=["CALL", "CALLCODE", "DELEGATECALL", "STATICCALL"], + pre_hooks=["JUMPI"], ) def execute(self, state: GlobalState) -> list: @@ -39,7 +33,7 @@ class PredictableDependenceModule(DetectionModule): :param state: :return: """ - log.debug("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") + log.info("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") self._issues.extend(_analyze_states(state)) return self.issues @@ -54,171 +48,44 @@ def _analyze_states(state: GlobalState) -> list: :return: """ issues = [] - call = get_call_from_state(state) - if call is None: - return [] - if "callvalue" in str(call.value): - log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] Skipping refund function") - return [] - # We're only interested in calls that send Ether - if call.value.type == VarType.CONCRETE and call.value.val == 0: - return [] - - address = call.state.get_current_instruction()["address"] - - description = ( - "The contract sends Ether depending on the values of the following variables:\n" - ) - - # First check: look for predictable state variables in state & call recipient constraints + # Look for predictable state variables in jump condition vars = ["coinbase", "gaslimit", "timestamp", "number"] found = [] + description = "A control flow decision is made based on " + for var in vars: - for constraint in call.state.mstate.constraints[:] + [call.to]: - if var in str(constraint): - found.append(var) + if var in str(state.mstate.stack[-2]): + found.append(var) if len(found): for item in found: - description += "- block.{}\n".format(item) - if solve(call): + description += "block.{}. ".format(item) swc_id = TIMESTAMP_DEPENDENCE if item == "timestamp" else WEAK_RANDOMNESS description += ( "Note that the values of variables like coinbase, gaslimit, block number and timestamp " - "are predictable and/or can be manipulated by a malicious miner. " - "Don't use them for random number generation or to make critical decisions." + "are predictable and can be manipulated by a malicious miner. " + "Don't use them for random number generation or to make critical control flow decisions." ) issue = Issue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, - address=address, + address=state.get_current_instruction()['address'], swc_id=swc_id, - bytecode=call.state.environment.code.bytecode, + bytecode=state.environment.code.bytecode, title="Dependence on predictable environment variable", severity="Low", - description_head="Sending of Ether depends on a predictable variable.", + description_head="A control flow decision is made based on a predictable variable.", description_tail=description, gas_used=( - call.state.mstate.min_gas_used, - call.state.mstate.max_gas_used, + state.mstate.min_gas_used, + state.mstate.max_gas_used, ), ) issues.append(issue) - # Second check: blockhash - - 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)) - if m and solve(call): - - found_item = m.group(1) - - if found_item: # block.blockhash(block.number - N) - description = ( - "The predictable expression 'block.blockhash(block.number - " - + m.group(2) - + ")' is used to determine Ether recipient" - ) - if int(m.group(2)) > 255: - description += ( - ", this expression will always be equal to zero." - ) - elif "storage" in str( - constraint - ): # block.blockhash(block.number - storage_0) - description = ( - "The predictable expression 'block.blockhash(block.number - " - + "some_storage_var)' is used to determine Ether recipient" - ) - else: # block.blockhash(block.number) - description = ( - "The predictable expression 'block.blockhash(block.number)'" - + " is used to determine Ether recipient" - ) - description += ", this expression will always be equal to zero." - - issue = Issue( - 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", - severity="Low", - description_head="Sending of Ether depends on the blockhash.", - description_tail=description, - swc_id=WEAK_RANDOMNESS, - gas_used=( - call.state.mstate.min_gas_used, - call.state.mstate.max_gas_used, - ), - ) - issues.append(issue) - break - else: - - r = re.search(r"storage_([a-z0-9_&^]+)", str(constraint)) - if r: # block.blockhash(storage_0) - - """We actually can do better here by adding a constraint - blockhash_block_storage_0 == 0 and checking model - satisfiability. - - When this is done, severity can be raised from - 'Informational' to 'Warning'. Checking that storage - at given index can be tainted is not necessary, - since it usually contains block.number of the - 'commit' transaction in commit-reveal workflow. - """ - - index = r.group(1) - if index and solve(call): - description = ( - "A block hash is calculated using the block.blockhash(uint blockNumber) method. " - "The block number is obtained from storage index {}".format( - index - ) - ) - issue = Issue( - 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", - severity="Low", - description_head="Sending of Ether depends on the blockhash.", - description_tail=description, - swc_id=WEAK_RANDOMNESS, - gas_used=( - call.state.mstate.min_gas_used, - call.state.mstate.max_gas_used, - ), - ) - issues.append(issue) - break return issues - - -def solve(call: Call) -> bool: - """ - - :param call: - :return: - """ - try: - model = solver.get_model(call.state.mstate.constraints) - log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] MODEL: " + str(model)) - pretty_model = solver.pretty_print_model(model) - - log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] main model: \n%s" % pretty_model) - return True - - except UnsatError: - log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] no model found") - return False From 444cee64942f0fb7a37b8a883168db26783f32ed Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 8 May 2019 16:31:39 -0700 Subject: [PATCH 03/33] Black --- mythril/analysis/modules/dependence_on_predictable_vars.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 37fe33d2..dd0092a8 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -74,17 +74,14 @@ def _analyze_states(state: GlobalState) -> list: issue = Issue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, - address=state.get_current_instruction()['address'], + address=state.get_current_instruction()["address"], swc_id=swc_id, bytecode=state.environment.code.bytecode, title="Dependence on predictable environment variable", severity="Low", description_head="A control flow decision is made based on a predictable variable.", description_tail=description, - gas_used=( - state.mstate.min_gas_used, - state.mstate.max_gas_used, - ), + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) issues.append(issue) From e6254b9edb942854843d1c1c17c38bcd473d8a90 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 8 May 2019 16:38:42 -0700 Subject: [PATCH 04/33] Revert log.info -> log.debug --- mythril/analysis/modules/dependence_on_predictable_vars.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index dd0092a8..8615b000 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -33,7 +33,7 @@ class PredictableDependenceModule(DetectionModule): :param state: :return: """ - log.info("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") + log.debug("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") self._issues.extend(_analyze_states(state)) return self.issues From 5ec39fdce5aee3b94a1859c6338ee3a9d3b51870 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Fri, 10 May 2019 21:12:22 +0200 Subject: [PATCH 05/33] Revert "Change timeout logic" This reverts commit fda18b3e77b3980d7aa89de27e9edb938207ebbc. --- mythril/interfaces/cli.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 0fbbab7e..adb0e8f2 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -216,7 +216,7 @@ def create_parser(parser: argparse.ArgumentParser) -> None: options.add_argument( "--execution-timeout", type=int, - default=86400, + default=600, help="The amount of seconds to spend on symbolic execution", ) options.add_argument( From a3f951d9c704d1659227b79ecf098df679aad88d Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 10 May 2019 16:38:00 -0400 Subject: [PATCH 06/33] [WIP] refactor to use annotations --- .../modules/dependence_on_predictable_vars.py | 86 +++++++++++-------- 1 file changed, 49 insertions(+), 37 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 8615b000..9ce230cc 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -9,6 +9,15 @@ from mythril.laser.ethereum.state.global_state import GlobalState log = logging.getLogger(__name__) +predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"] + + +class PredictableValueAnnotation: + """ Symbol Annotation used if a variable is initialized from a predictable environment variable""" + + def __init__(self, opcode) -> None: + self.opcode = opcode + class PredictableDependenceModule(DetectionModule): """This module detects whether control flow decisions are made using predictable @@ -25,6 +34,7 @@ class PredictableDependenceModule(DetectionModule): ), entrypoint="callback", pre_hooks=["JUMPI"], + post_hooks=predictable_ops ) def execute(self, state: GlobalState) -> list: @@ -33,12 +43,11 @@ class PredictableDependenceModule(DetectionModule): :param state: :return: """ - log.debug("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") - self._issues.extend(_analyze_states(state)) - return self.issues + log.info("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") -detector = PredictableDependenceModule() + self._issues.extend(_analyze_states(state)) + return self.issues def _analyze_states(state: GlobalState) -> list: @@ -51,38 +60,41 @@ def _analyze_states(state: GlobalState) -> list: # Look for predictable state variables in jump condition - vars = ["coinbase", "gaslimit", "timestamp", "number"] - found = [] - - description = "A control flow decision is made based on " - - for var in vars: - if var in str(state.mstate.stack[-2]): - found.append(var) - - if len(found): - for item in found: - description += "block.{}. ".format(item) - swc_id = TIMESTAMP_DEPENDENCE if item == "timestamp" else WEAK_RANDOMNESS - - description += ( - "Note that the values of variables like coinbase, gaslimit, block number and timestamp " - "are predictable and can be manipulated by a malicious miner. " - "Don't use them for random number generation or to make critical control flow decisions." - ) - - issue = Issue( - contract=state.environment.active_account.contract_name, - function_name=state.environment.active_function_name, - address=state.get_current_instruction()["address"], - swc_id=swc_id, - bytecode=state.environment.code.bytecode, - title="Dependence on predictable environment variable", - severity="Low", - description_head="A control flow decision is made based on a predictable variable.", - description_tail=description, - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), - ) - issues.append(issue) + if state.get_current_instruction()["opcode"] == "JUMPI": + for annotation in state.mstate.stack[-2].annotations: + if isinstance(annotation, PredictableValueAnnotation): + description = "A control flow decision is made based on block.{}. ".format(annotation.opcode) + + description += ( + "Note that the values of variables like coinbase, gaslimit, block number and timestamp " + "are predictable and can be manipulated by a malicious miner. " + "Don't use them for random number generation or to make critical control flow decisions." + ) + + issue = Issue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=state.get_current_instruction()["address"], + swc_id=TIMESTAMP_DEPENDENCE, + bytecode=state.environment.code.bytecode, + title="Dependence on predictable environment variable", + severity="Low", + description_head="A control flow decision is made based on a predictable variable.", + description_tail=description, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + ) + issues.append(issue) + else: + # we're in post hook + + instructions = state.environment.code.instruction_list + opcode = instructions[state.mstate.pc - 1]["opcode"] + + logging.info("annotating " + str(opcode)) + annotation = PredictableValueAnnotation(opcode) + state.mstate.stack[-1].annotate(annotation) return issues + + +detector = PredictableDependenceModule() From 84849b734b78dc09626c19d14a2776e0f5af49fc Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 10 May 2019 16:39:07 -0400 Subject: [PATCH 07/33] Remove loggimng --- mythril/analysis/modules/dependence_on_predictable_vars.py | 1 - 1 file changed, 1 deletion(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 9ce230cc..b041f0fc 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -90,7 +90,6 @@ def _analyze_states(state: GlobalState) -> list: instructions = state.environment.code.instruction_list opcode = instructions[state.mstate.pc - 1]["opcode"] - logging.info("annotating " + str(opcode)) annotation = PredictableValueAnnotation(opcode) state.mstate.stack[-1].annotate(annotation) From c7e401c6bc36db4ddc37a324675806abf16c3335 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 10 May 2019 16:40:05 -0400 Subject: [PATCH 08/33] Ohoo black --- mythril/analysis/modules/dependence_on_predictable_vars.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index b041f0fc..3ebea3e5 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -34,7 +34,7 @@ class PredictableDependenceModule(DetectionModule): ), entrypoint="callback", pre_hooks=["JUMPI"], - post_hooks=predictable_ops + post_hooks=predictable_ops, ) def execute(self, state: GlobalState) -> list: @@ -63,7 +63,9 @@ def _analyze_states(state: GlobalState) -> list: if state.get_current_instruction()["opcode"] == "JUMPI": for annotation in state.mstate.stack[-2].annotations: if isinstance(annotation, PredictableValueAnnotation): - description = "A control flow decision is made based on block.{}. ".format(annotation.opcode) + description = "A control flow decision is made based on block.{}. ".format( + annotation.opcode + ) description += ( "Note that the values of variables like coinbase, gaslimit, block number and timestamp " From 9175a1975fd84519534589e88f0827c73e188b42 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 13 May 2019 22:26:37 +0200 Subject: [PATCH 09/33] First implementation of blockhash handling --- .../modules/dependence_on_predictable_vars.py | 34 +++++++++++++++++-- mythril/laser/ethereum/instructions.py | 2 +- mythril/laser/ethereum/state/environment.py | 1 + 3 files changed, 34 insertions(+), 3 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 3ebea3e5..26f414a5 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -4,14 +4,23 @@ import logging from mythril.analysis.modules.base import DetectionModule from mythril.analysis.report import Issue +from mythril.exceptions import UnsatError +from mythril.analysis import solver +from mythril.laser.smt import ULT from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.annotation import StateAnnotation +import traceback log = logging.getLogger(__name__) predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"] +def is_prehook(): + return "pre_hook" in traceback.format_stack()[-2] + + class PredictableValueAnnotation: """ Symbol Annotation used if a variable is initialized from a predictable environment variable""" @@ -19,6 +28,12 @@ class PredictableValueAnnotation: self.opcode = opcode +class TaintBlockHashAnnotation(StateAnnotation): + + def __init__(self) -> None: + pass + + class PredictableDependenceModule(DetectionModule): """This module detects whether control flow decisions are made using predictable parameters.""" @@ -33,8 +48,8 @@ class PredictableDependenceModule(DetectionModule): "block.gaslimit, block.timestamp or block.number." ), entrypoint="callback", - pre_hooks=["JUMPI"], - post_hooks=predictable_ops, + pre_hooks=["BLOCKHASH", "JUMPI"], + post_hooks=["BLOCKHASH"] + predictable_ops, ) def execute(self, state: GlobalState) -> list: @@ -86,6 +101,21 @@ def _analyze_states(state: GlobalState) -> list: gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) issues.append(issue) + elif state.get_current_instruction()["opcode"] == "BLOCKHASH": + if is_prehook(): + + param = state.mstate.stack[-1] + + try: + solver.get_model(ULT(param, state.environment.block_number)) + state.annotate(TaintBlockHashAnnotation) + + except UnsatError: + pass + else: + for annotation in state.annotations: + if isinstance(annotation, TaintBlockHashAnnotation): + state.mstate.stack[-1].annotate(PredictableValueAnnotation("BLOCKHASH")) else: # we're in post hook diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b6bb61cd..1aba8420 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1243,7 +1243,7 @@ class Instruction: :param global_state: :return: """ - global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256)) + global_state.mstate.stack.append(global_state.environment.block_number) return [global_state] @StateTransition() diff --git a/mythril/laser/ethereum/state/environment.py b/mythril/laser/ethereum/state/environment.py index 69830007..a8c257fd 100644 --- a/mythril/laser/ethereum/state/environment.py +++ b/mythril/laser/ethereum/state/environment.py @@ -40,6 +40,7 @@ class Environment: self.active_function_name = "" self.address = symbol_factory.BitVecVal(int(active_account.address, 16), 256) + self.block_number = symbol_factory.BitVecSym("block_number", 256) # Ib self.code = active_account.code if code is None else code From cad6f5ae35828c36b9969c9b27436dcc2a2c0793 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 13 May 2019 23:39:38 +0200 Subject: [PATCH 10/33] Add differentiation between blockhash of previous and current/future block numbers --- .../modules/dependence_on_predictable_vars.py | 60 ++++++++++++------- mythril/laser/ethereum/instructions.py | 6 +- 2 files changed, 42 insertions(+), 24 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 26f414a5..c2dd61a0 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -6,7 +6,7 @@ from mythril.analysis.modules.base import DetectionModule from mythril.analysis.report import Issue from mythril.exceptions import UnsatError from mythril.analysis import solver -from mythril.laser.smt import ULT +from mythril.laser.smt import ULT, symbol_factory from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.annotation import StateAnnotation @@ -18,7 +18,7 @@ predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"] def is_prehook(): - return "pre_hook" in traceback.format_stack()[-2] + return "pre_hook" in traceback.format_stack()[-4] class PredictableValueAnnotation: @@ -28,7 +28,7 @@ class PredictableValueAnnotation: self.opcode = opcode -class TaintBlockHashAnnotation(StateAnnotation): +class OldBlockNumberUsedAnnotation(StateAnnotation): def __init__(self) -> None: pass @@ -59,7 +59,7 @@ class PredictableDependenceModule(DetectionModule): :return: """ - log.info("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") + log.debug("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") self._issues.extend(_analyze_states(state)) return self.issues @@ -78,14 +78,12 @@ def _analyze_states(state: GlobalState) -> list: if state.get_current_instruction()["opcode"] == "JUMPI": for annotation in state.mstate.stack[-2].annotations: if isinstance(annotation, PredictableValueAnnotation): - description = "A control flow decision is made based on block.{}. ".format( - annotation.opcode - ) - + description = "The " + annotation.opcode + " is used in an if-statement. " description += ( "Note that the values of variables like coinbase, gaslimit, block number and timestamp " - "are predictable and can be manipulated by a malicious miner. " - "Don't use them for random number generation or to make critical control flow decisions." + "are predictable and can be manipulated by a malicious miner. Also keep in mind that attackers " + "know hashes of earlier blocks. Don't use any of those environment variables for random number " + "generation or to make critical control flow decisions." ) issue = Issue( @@ -96,34 +94,54 @@ def _analyze_states(state: GlobalState) -> list: bytecode=state.environment.code.bytecode, title="Dependence on predictable environment variable", severity="Low", - description_head="A control flow decision is made based on a predictable variable.", + description_head="Control flow decision is made based on a predictable variable.", description_tail=description, gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) issues.append(issue) + + # Now the magic starts! + elif state.get_current_instruction()["opcode"] == "BLOCKHASH": if is_prehook(): param = state.mstate.stack[-1] try: - solver.get_model(ULT(param, state.environment.block_number)) - state.annotate(TaintBlockHashAnnotation) + constraint =[ULT(param, state.environment.block_number), + ULT(state.environment.block_number, symbol_factory.BitVecVal(2 ** 255, 256))] + + # Why the second constraint? Because otherwise, Z3 returns a solution where param overflows. + + solver.get_model(constraint) + state.annotate(OldBlockNumberUsedAnnotation) except UnsatError: pass - else: - for annotation in state.annotations: - if isinstance(annotation, TaintBlockHashAnnotation): - state.mstate.stack[-1].annotate(PredictableValueAnnotation("BLOCKHASH")) + else: # we're in post hook - instructions = state.environment.code.instruction_list - opcode = instructions[state.mstate.pc - 1]["opcode"] + if state.environment.code.instruction_list[state.mstate.pc - 1]["opcode"] == "BLOCKHASH": + # if we're in the post hook of a BLOCKHASH op, check if an old block number was used to create it. + + for annotation in state.annotations: + + ''' + FIXME: for some reason, isinstance(annotation, OldBlockNumberUsedAnnotation) always returns false. + I added a string comparison as a workaround. + ''' + + if isinstance(annotation, OldBlockNumberUsedAnnotation) or "OldBlockNumber" in str(annotation): + state.mstate.stack[-1].annotate(PredictableValueAnnotation("block hash of a previous block")) + else: + # Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is called. + + instructions = state.environment.code.instruction_list + opcode = instructions[state.mstate.pc - 1]["opcode"] - annotation = PredictableValueAnnotation(opcode) - state.mstate.stack[-1].annotate(annotation) + annotation = PredictableValueAnnotation("block." + opcode.lower() + "environment variable") + state.mstate.stack[-1].annotate(annotation) return issues diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 1aba8420..4ada9216 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -913,7 +913,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(op0) + "]", 256, op0.annotations) ) gas_tuple = cast(Tuple, OPCODE_GAS["SHA3"]) state.min_gas_used += gas_tuple[0] @@ -941,7 +941,7 @@ class Instruction: if data.symbolic: argument_str = str(state.memory[index]).replace(" ", "_") result = symbol_factory.BitVecFuncSym( - "KECCAC[{}]".format(argument_str), "keccak256", 256, input_=data + "KECCAC[{}]".format(argument_str), "keccak256", 256, input_=data, annotations=op0.annotations ) log.debug("Created BitVecFunc hash.") @@ -949,7 +949,7 @@ class Instruction: 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 + util.concrete_int_from_bytes(keccak, 0), "keccak256", 256, input_=data, annotations=op0.annotations ) log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) From 3d35f905e4990a5c97dfba3f31b32c6b2e2098dc Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 13 May 2019 23:41:36 +0200 Subject: [PATCH 11/33] Traditionally, add black formatting --- .../modules/dependence_on_predictable_vars.py | 37 +++++++++++++------ mythril/laser/ethereum/instructions.py | 16 ++++++-- 2 files changed, 39 insertions(+), 14 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index c2dd61a0..dd1e189f 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -29,7 +29,6 @@ class PredictableValueAnnotation: class OldBlockNumberUsedAnnotation(StateAnnotation): - def __init__(self) -> None: pass @@ -78,7 +77,9 @@ def _analyze_states(state: GlobalState) -> list: if state.get_current_instruction()["opcode"] == "JUMPI": for annotation in state.mstate.stack[-2].annotations: if isinstance(annotation, PredictableValueAnnotation): - description = "The " + annotation.opcode + " is used in an if-statement. " + description = ( + "The " + annotation.opcode + " is used in an if-statement. " + ) description += ( "Note that the values of variables like coinbase, gaslimit, block number and timestamp " "are predictable and can be manipulated by a malicious miner. Also keep in mind that attackers " @@ -108,8 +109,13 @@ def _analyze_states(state: GlobalState) -> list: param = state.mstate.stack[-1] try: - constraint =[ULT(param, state.environment.block_number), - ULT(state.environment.block_number, symbol_factory.BitVecVal(2 ** 255, 256))] + constraint = [ + ULT(param, state.environment.block_number), + ULT( + state.environment.block_number, + symbol_factory.BitVecVal(2 ** 255, 256), + ), + ] # Why the second constraint? Because otherwise, Z3 returns a solution where param overflows. @@ -122,25 +128,34 @@ def _analyze_states(state: GlobalState) -> list: else: # we're in post hook - if state.environment.code.instruction_list[state.mstate.pc - 1]["opcode"] == "BLOCKHASH": + if ( + state.environment.code.instruction_list[state.mstate.pc - 1]["opcode"] + == "BLOCKHASH" + ): # if we're in the post hook of a BLOCKHASH op, check if an old block number was used to create it. for annotation in state.annotations: - ''' + """ FIXME: for some reason, isinstance(annotation, OldBlockNumberUsedAnnotation) always returns false. I added a string comparison as a workaround. - ''' - - if isinstance(annotation, OldBlockNumberUsedAnnotation) or "OldBlockNumber" in str(annotation): - state.mstate.stack[-1].annotate(PredictableValueAnnotation("block hash of a previous block")) + """ + + if isinstance( + annotation, OldBlockNumberUsedAnnotation + ) or "OldBlockNumber" in str(annotation): + state.mstate.stack[-1].annotate( + PredictableValueAnnotation("block hash of a previous block") + ) else: # Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is called. instructions = state.environment.code.instruction_list opcode = instructions[state.mstate.pc - 1]["opcode"] - annotation = PredictableValueAnnotation("block." + opcode.lower() + "environment variable") + annotation = PredictableValueAnnotation( + "block." + opcode.lower() + "environment variable" + ) state.mstate.stack[-1].annotate(annotation) return issues diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 4ada9216..c8090400 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -913,7 +913,9 @@ class Instruction: if isinstance(op0, Expression): op0 = simplify(op0) state.stack.append( - symbol_factory.BitVecSym("KECCAC_mem[" + str(op0) + "]", 256, op0.annotations) + symbol_factory.BitVecSym( + "KECCAC_mem[" + str(op0) + "]", 256, op0.annotations + ) ) gas_tuple = cast(Tuple, OPCODE_GAS["SHA3"]) state.min_gas_used += gas_tuple[0] @@ -941,7 +943,11 @@ class Instruction: if data.symbolic: argument_str = str(state.memory[index]).replace(" ", "_") result = symbol_factory.BitVecFuncSym( - "KECCAC[{}]".format(argument_str), "keccak256", 256, input_=data, annotations=op0.annotations + "KECCAC[{}]".format(argument_str), + "keccak256", + 256, + input_=data, + annotations=op0.annotations, ) log.debug("Created BitVecFunc hash.") @@ -949,7 +955,11 @@ class Instruction: 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, annotations=op0.annotations + util.concrete_int_from_bytes(keccak, 0), + "keccak256", + 256, + input_=data, + annotations=op0.annotations, ) log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) From dc1963c316af782928ad2678410e0c7499a74976 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 13 May 2019 23:51:49 +0200 Subject: [PATCH 12/33] Improve report formatting --- mythril/analysis/modules/dependence_on_predictable_vars.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index dd1e189f..09da72e7 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -78,7 +78,7 @@ def _analyze_states(state: GlobalState) -> list: for annotation in state.mstate.stack[-2].annotations: if isinstance(annotation, PredictableValueAnnotation): description = ( - "The " + annotation.opcode + " is used in an if-statement. " + "The " + annotation.opcode + " is used in a conditional statement. " ) description += ( "Note that the values of variables like coinbase, gaslimit, block number and timestamp " @@ -95,7 +95,7 @@ def _analyze_states(state: GlobalState) -> list: bytecode=state.environment.code.bytecode, title="Dependence on predictable environment variable", severity="Low", - description_head="Control flow decision is made based on a predictable variable.", + description_head="A control flow decision is made based on a predictable variable.", description_tail=description, gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) @@ -154,7 +154,7 @@ def _analyze_states(state: GlobalState) -> list: opcode = instructions[state.mstate.pc - 1]["opcode"] annotation = PredictableValueAnnotation( - "block." + opcode.lower() + "environment variable" + "block." + opcode.lower() + " environment variable" ) state.mstate.stack[-1].annotate(annotation) From 1b891fafaec18738cee4de4590ea3d177494f4f1 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 00:12:26 +0200 Subject: [PATCH 13/33] Fix wrong instantiation of OldBlockNumberUsedAnnotation --- mythril/analysis/modules/dependence_on_predictable_vars.py | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 09da72e7..7d9b2d5e 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -120,7 +120,7 @@ def _analyze_states(state: GlobalState) -> list: # Why the second constraint? Because otherwise, Z3 returns a solution where param overflows. solver.get_model(constraint) - state.annotate(OldBlockNumberUsedAnnotation) + state.annotate(OldBlockNumberUsedAnnotation()) except UnsatError: pass @@ -141,9 +141,7 @@ def _analyze_states(state: GlobalState) -> list: I added a string comparison as a workaround. """ - if isinstance( - annotation, OldBlockNumberUsedAnnotation - ) or "OldBlockNumber" in str(annotation): + if isinstance(annotation, OldBlockNumberUsedAnnotation): state.mstate.stack[-1].annotate( PredictableValueAnnotation("block hash of a previous block") ) From 982cb8ee746d88977faeda92d92ace0e6147a0d7 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 05:15:19 +0200 Subject: [PATCH 14/33] Narrow down findings to instances of CALL and SUICIDE reached via predictable control flow decision --- .../modules/dependence_on_predictable_vars.py | 52 +++++++++++++------ 1 file changed, 36 insertions(+), 16 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 7d9b2d5e..532682de 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -15,6 +15,7 @@ import traceback log = logging.getLogger(__name__) predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"] +critical_ops = ["CALL", "SUICIDE"] def is_prehook(): @@ -22,13 +23,23 @@ def is_prehook(): class PredictableValueAnnotation: - """ Symbol Annotation used if a variable is initialized from a predictable environment variable""" + """Symbol annotation used if a variable is initialized from a predictable environment variable.""" - def __init__(self, opcode) -> None: - self.opcode = opcode + def __init__(self, operation) -> None: + self.operation = operation + + +class PredictablePathAnnotation(StateAnnotation): + """State annotation used when a path is chosen based on a predictable variable.""" + + def __init__(self, operation, location) -> None: + self.operation = operation + self.location = location class OldBlockNumberUsedAnnotation(StateAnnotation): + """State annotation set in blockhash prehook if the input value is lower than the current block number.""" + def __init__(self) -> None: pass @@ -43,11 +54,11 @@ class PredictableDependenceModule(DetectionModule): name="Dependence of Predictable Variables", swc_id="{} {}".format(TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS), description=( - "Check whether control flow decisions are influenced by block.coinbase," + "Check whether important control flow decisions are influenced by block.coinbase," "block.gaslimit, block.timestamp or block.number." ), entrypoint="callback", - pre_hooks=["BLOCKHASH", "JUMPI"], + pre_hooks=["BLOCKHASH", "JUMPI"] + critical_ops, post_hooks=["BLOCKHASH"] + predictable_ops, ) @@ -70,15 +81,20 @@ def _analyze_states(state: GlobalState) -> list: :param state: :return: """ - issues = [] # Look for predictable state variables in jump condition - if state.get_current_instruction()["opcode"] == "JUMPI": - for annotation in state.mstate.stack[-2].annotations: - if isinstance(annotation, PredictableValueAnnotation): + issues = [] + opcode = state.get_current_instruction()["opcode"] + + if opcode in critical_ops: + for annotation in state.annotations: + + if isinstance(annotation, PredictablePathAnnotation): description = ( - "The " + annotation.opcode + " is used in a conditional statement. " + "The " + + annotation.operation + + " is used in to determine an important control flow decision. " ) description += ( "Note that the values of variables like coinbase, gaslimit, block number and timestamp " @@ -101,6 +117,15 @@ def _analyze_states(state: GlobalState) -> list: ) issues.append(issue) + elif opcode == "JUMPI": + for annotation in state.mstate.stack[-2].annotations: + if isinstance(annotation, PredictableValueAnnotation): + state.annotate( + PredictablePathAnnotation( + annotation.operation, state.get_current_instruction()["address"] + ) + ) + # Now the magic starts! elif state.get_current_instruction()["opcode"] == "BLOCKHASH": @@ -117,7 +142,7 @@ def _analyze_states(state: GlobalState) -> list: ), ] - # Why the second constraint? Because otherwise, Z3 returns a solution where param overflows. + # Why the second constraint? Because without it Z3 returns a solution where param overflows. solver.get_model(constraint) state.annotate(OldBlockNumberUsedAnnotation()) @@ -136,11 +161,6 @@ def _analyze_states(state: GlobalState) -> list: for annotation in state.annotations: - """ - FIXME: for some reason, isinstance(annotation, OldBlockNumberUsedAnnotation) always returns false. - I added a string comparison as a workaround. - """ - if isinstance(annotation, OldBlockNumberUsedAnnotation): state.mstate.stack[-1].annotate( PredictableValueAnnotation("block hash of a previous block") From c35b6b35bdc02c26ad401f809d8d3645d74efdb9 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 05:40:02 +0200 Subject: [PATCH 15/33] Correctly propagate annotations in sha3 (from indexed memory) --- .../analysis/modules/dependence_on_predictable_vars.py | 1 + mythril/laser/ethereum/instructions.py | 10 ++++------ 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 532682de..49b3a73c 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -118,6 +118,7 @@ def _analyze_states(state: GlobalState) -> list: issues.append(issue) elif opcode == "JUMPI": + for annotation in state.mstate.stack[-2].annotations: if isinstance(annotation, PredictableValueAnnotation): state.annotate( diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index c8090400..dcea0d20 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -913,9 +913,7 @@ class Instruction: if isinstance(op0, Expression): op0 = simplify(op0) state.stack.append( - symbol_factory.BitVecSym( - "KECCAC_mem[" + str(op0) + "]", 256, op0.annotations - ) + symbol_factory.BitVecSym("KECCAC_mem[" + str(op0) + "]", 256) ) gas_tuple = cast(Tuple, OPCODE_GAS["SHA3"]) state.min_gas_used += gas_tuple[0] @@ -947,7 +945,7 @@ class Instruction: "keccak256", 256, input_=data, - annotations=op0.annotations, + annotations=state.memory[index].annotations, ) log.debug("Created BitVecFunc hash.") @@ -959,9 +957,9 @@ class Instruction: "keccak256", 256, input_=data, - annotations=op0.annotations, + annotations=state.memory[index].annotations, ) - log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) + log.info("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) state.stack.append(result) return [global_state] From f2eae2f092c9f4a39018973fbb5a89e52b79b9d6 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 05:52:21 +0200 Subject: [PATCH 16/33] Minor changes --- mythril/analysis/modules/dependence_on_predictable_vars.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 49b3a73c..789a5ac7 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -88,6 +88,8 @@ def _analyze_states(state: GlobalState) -> list: opcode = state.get_current_instruction()["opcode"] if opcode in critical_ops: + logging.info(str(state.annotations)) + for annotation in state.annotations: if isinstance(annotation, PredictablePathAnnotation): @@ -167,7 +169,7 @@ def _analyze_states(state: GlobalState) -> list: PredictableValueAnnotation("block hash of a previous block") ) else: - # Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is called. + # Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is executed. instructions = state.environment.code.instruction_list opcode = instructions[state.mstate.pc - 1]["opcode"] From b14efd30b1be8d1f09b82aaf4909e019444ff066 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 05:59:47 +0200 Subject: [PATCH 17/33] Remove debugging (and take a break) --- 1 | 286 ++++++++++++++++++ .../modules/dependence_on_predictable_vars.py | 1 - 2 files changed, 286 insertions(+), 1 deletion(-) create mode 100644 1 diff --git a/1 b/1 new file mode 100644 index 00000000..07770b5e --- /dev/null +++ b/1 @@ -0,0 +1,286 @@ +mythril.support.signatures [INFO]: Using signature database at /Users/bernhardmueller/.mythril/signatures.db +mythril.analysis.security [INFO]: Found 0 detection modules +mythril.laser.ethereum.svm [INFO]: LASER EVM initialized with dynamic loader: +mythril.laser.ethereum.plugins.plugin_loader [INFO]: Loading plugin: +mythril.laser.ethereum.plugins.plugin_loader [INFO]: Loading plugin: +mythril.analysis.security [INFO]: Found 11 detection modules +mythril.analysis.security [INFO]: Found 11 detection modules +mythril.laser.ethereum.svm [DEBUG]: Starting LASER execution +mythril.laser.ethereum.svm [INFO]: Starting contract creation transaction +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE +mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[64]: 96 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH8 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLVALUE +mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating NUMBER +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SUB +mythril.laser.ethereum.instructions [DEBUG]: Evaluating BLOCKHASH +mythril.laser.ethereum.instructions [DEBUG]: Evaluating TIMESTAMP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MLOAD +mythril.laser.ethereum.instructions [DEBUG]: MLOAD[64] +mythril.laser.ethereum.instructions [DEBUG]: Load from memory[64]: 96 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP4 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating NOT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating NOT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE +mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[96]: 115792089237316195423570985008687907853269984665640564039457584007913129639935 - +0 & +115792089237316195423570985008687907853269984665640564039457584007913129639935 - +0 & +1_blockhash_block_block_number - 1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADD +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP3 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE +mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[128]: 1_timestamp +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADD +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP3 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MLOAD +mythril.laser.ethereum.instructions [DEBUG]: MLOAD[64] +mythril.laser.ethereum.instructions [DEBUG]: Load from memory[64]: 96 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SUB +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SHA3 +mythril.laser.ethereum.instructions [DEBUG]: Created BitVecFunc hash. +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DIV +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating EXP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SLOAD +mythril.laser.ethereum.instructions [DEBUG]: Storage access at index 0 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MUL +mythril.laser.ethereum.instructions [DEBUG]: Evaluating NOT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP4 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MUL +mythril.laser.ethereum.instructions [DEBUG]: Evaluating OR +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SSTORE +mythril.laser.ethereum.instructions [DEBUG]: Write to storage[0] +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating CODECOPY +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating RETURN +mythril.laser.ethereum.svm [INFO]: Finished contract creation, found 1 open states +mythril.laser.ethereum.svm [INFO]: Starting message call transaction, iteration: 0, 1 initial states +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE +mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[64]: 96 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLDATASIZE +mythril.laser.ethereum.instructions [DEBUG]: Evaluating LT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLDATALOAD +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH29 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DIV +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH4 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH4 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI +mythril.laser.ethereum.svm [DEBUG]: - Entering function MAIN:unknown +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH4 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI +mythril.laser.ethereum.svm [DEBUG]: - Entering function MAIN:unknown +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLDATALOAD +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLVALUE +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADD +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADDRESS +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH20 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH8 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating BALANCE +mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLVALUE +mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ +mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MLOAD +mythril.laser.ethereum.instructions [DEBUG]: MLOAD[64] +mythril.laser.ethereum.instructions [DEBUG]: Load from memory[64]: 96 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP3 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SLOAD +mythril.laser.ethereum.instructions [DEBUG]: Storage access at index 0 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating EXP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DIV +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE +mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[96]: If(If(If(If(2_balance_at_1461501637330902918203684832716283019655932542975 & +51421440056055728346017419001665401074216449311 == + 0, + 0, + 1) == + 0, + 1, + 0) == + 0, + 1, + 0) == + 0, + 1, + 0) +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADD +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND +mythril.laser.ethereum.instructions [DEBUG]: Evaluating MLOAD +mythril.laser.ethereum.instructions [DEBUG]: MLOAD[64] +mythril.laser.ethereum.instructions [DEBUG]: Load from memory[64]: 96 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ +mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SUB +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI +mythril.laser.ethereum.instructions [DEBUG]: Pruned unreachable states. +mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating RETURN +mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMP +mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST +mythril.laser.ethereum.instructions [DEBUG]: Evaluating STOP +mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin [INFO]: Number of new instructions covered in tx 0: 131 +mythril.laser.ethereum.svm [INFO]: Starting message call transaction, iteration: 1, 0 initial states +mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin [INFO]: Number of new instructions covered in tx 1: 0 +mythril.laser.ethereum.svm [INFO]: Finished symbolic execution +mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin [INFO]: Achieved 31.85% coverage for code: 6060604052670de0b6b3a76400003414151561001a57600080fd5b600143034042604051808360001916600019168152602001828152602001925050506040518091039020600190046000806101000a81548160ff021916908360ff160217905550610164806100706000396000f30060606040526004361061004c576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634ba4c16b14610051578063b2fa1c9e1461006c575b600080fd5b61006a600480803560ff16906020019091905050610099565b005b341561007757600080fd5b61007f610117565b604051808215151515815260200191505060405180910390f35b670de0b6b3a7640000341415156100af57600080fd5b6000809054906101000a900460ff1660ff168160ff161415610114573373ffffffffffffffffffffffffffffffffffffffff166108fc671bc16d674ec800009081150290604051600060405180830381858888f19350505050151561011357600080fd5b5b50565b6000803073ffffffffffffffffffffffffffffffffffffffff1631149050905600a165627a7a72305820e70964dd89df0e5b2cf45faf9eecd590a00131d465ed3f65857d843d01c130270029 +mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin [INFO]: Achieved 77.98% coverage for code: 60606040526004361061004c576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634ba4c16b14610051578063b2fa1c9e1461006c575b600080fd5b61006a600480803560ff16906020019091905050610099565b005b341561007757600080fd5b61007f610117565b604051808215151515815260200191505060405180910390f35b670de0b6b3a7640000341415156100af57600080fd5b6000809054906101000a900460ff1660ff168160ff161415610114573373ffffffffffffffffffffffffffffffffffffffff166108fc671bc16d674ec800009081150290604051600060405180830381858888f19350505050151561011357600080fd5b5b50565b6000803073ffffffffffffffffffffffffffffffffffffffff1631149050905600a165627a7a72305820e70964dd89df0e5b2cf45faf9eecd590a00131d465ed3f65857d843d01c130270029 +mythril.analysis.security [INFO]: Starting analysis +mythril.analysis.security [INFO]: Found 0 detection modules +mythril.analysis.security [INFO]: Found 11 detection modules +mythril.analysis.security [DEBUG]: Retrieving results for DELEGATECALL Usage in Fallback Function +mythril.analysis.security [DEBUG]: Retrieving results for Dependence of Predictable Variables +mythril.analysis.security [DEBUG]: Retrieving results for Deprecated Operations +mythril.analysis.security [DEBUG]: Retrieving results for Ether Thief +mythril.analysis.security [DEBUG]: Retrieving results for Reachable Exceptions +mythril.analysis.security [DEBUG]: Retrieving results for External calls +mythril.analysis.security [DEBUG]: Retrieving results for Integer Overflow and Underflow +mythril.analysis.security [DEBUG]: Retrieving results for Multiple Sends +mythril.analysis.security [DEBUG]: Retrieving results for State Change After External calls +mythril.analysis.security [DEBUG]: Retrieving results for Unprotected Selfdestruct +mythril.analysis.security [DEBUG]: Retrieving results for Unchecked Return Value +mythril.analysis.security [INFO]: Found 11 detection modules +mythril.mythril.mythril_analyzer [INFO]: Solver statistics: +Query count: 35 +Solver time: 0.3555266857147217 diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 789a5ac7..3ad31ecf 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -88,7 +88,6 @@ def _analyze_states(state: GlobalState) -> list: opcode = state.get_current_instruction()["opcode"] if opcode in critical_ops: - logging.info(str(state.annotations)) for annotation in state.annotations: From 07ab25323cc9c20d7b0820b487bf132eb88b041e Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 06:12:44 +0200 Subject: [PATCH 18/33] Don't attempt to access annotations from concrete ints --- mythril/laser/ethereum/instructions.py | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index dcea0d20..4194d136 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -953,13 +953,9 @@ class Instruction: 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, - annotations=state.memory[index].annotations, + util.concrete_int_from_bytes(keccak, 0), "keccak256", 256, input_=data ) - log.info("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) + log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) state.stack.append(result) return [global_state] From 00de5335070c4dda6c6fd53edb37f9133af4ff64 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 06:21:23 +0200 Subject: [PATCH 19/33] Hopefully fix CircleCI complaint --- mythril/analysis/modules/dependence_on_predictable_vars.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 3ad31ecf..94268961 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -173,10 +173,11 @@ def _analyze_states(state: GlobalState) -> list: instructions = state.environment.code.instruction_list opcode = instructions[state.mstate.pc - 1]["opcode"] - annotation = PredictableValueAnnotation( - "block." + opcode.lower() + " environment variable" + state.mstate.stack[-1].annotate( + PredictableValueAnnotation( + "block." + opcode.lower() + " environment variable" + ) ) - state.mstate.stack[-1].annotate(annotation) return issues From 474582f8266fd3634b419ccd99455b570fd86ac6 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 18:48:09 +0200 Subject: [PATCH 20/33] General refactoring --- .../modules/dependence_on_predictable_vars.py | 91 +++++++++---------- mythril/laser/ethereum/instructions.py | 7 +- 2 files changed, 50 insertions(+), 48 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 94268961..34e1826c 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -82,56 +82,57 @@ def _analyze_states(state: GlobalState) -> list: :return: """ - # Look for predictable state variables in jump condition - issues = [] - opcode = state.get_current_instruction()["opcode"] - if opcode in critical_ops: + if is_prehook(): - for annotation in state.annotations: + opcode = state.get_current_instruction()["opcode"] - if isinstance(annotation, PredictablePathAnnotation): - description = ( - "The " - + annotation.operation - + " is used in to determine an important control flow decision. " - ) - description += ( - "Note that the values of variables like coinbase, gaslimit, block number and timestamp " - "are predictable and can be manipulated by a malicious miner. Also keep in mind that attackers " - "know hashes of earlier blocks. Don't use any of those environment variables for random number " - "generation or to make critical control flow decisions." - ) + if opcode in critical_ops: - issue = Issue( - contract=state.environment.active_account.contract_name, - function_name=state.environment.active_function_name, - address=state.get_current_instruction()["address"], - swc_id=TIMESTAMP_DEPENDENCE, - bytecode=state.environment.code.bytecode, - title="Dependence on predictable environment variable", - severity="Low", - description_head="A control flow decision is made based on a predictable variable.", - description_tail=description, - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), - ) - issues.append(issue) + for annotation in state.annotations: - elif opcode == "JUMPI": + if isinstance(annotation, PredictablePathAnnotation): + description = ( + "The " + + annotation.operation + + " is used in to determine an important control flow decision. " + ) + description += ( + "Note that the values of variables like coinbase, gaslimit, block number and timestamp " + "are predictable and can be manipulated by a malicious miner. Also keep in mind that attackers " + "know hashes of earlier blocks. Don't use any of those environment variables for random number " + "generation or to make critical control flow decisions." + ) - for annotation in state.mstate.stack[-2].annotations: - if isinstance(annotation, PredictableValueAnnotation): - state.annotate( - PredictablePathAnnotation( - annotation.operation, state.get_current_instruction()["address"] + issue = Issue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=state.get_current_instruction()["address"], + swc_id=TIMESTAMP_DEPENDENCE, + bytecode=state.environment.code.bytecode, + title="Dependence on predictable environment variable", + severity="Low", + description_head="A control flow decision is made based on a predictable variable.", + description_tail=description, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) - ) + issues.append(issue) + + elif opcode == "JUMPI": + + # Look for predictable state variables in jump condition - # Now the magic starts! + for annotation in state.mstate.stack[-2].annotations: + if isinstance(annotation, PredictableValueAnnotation): + state.annotate( + PredictablePathAnnotation( + annotation.operation, + state.get_current_instruction()["address"], + ) + ) - elif state.get_current_instruction()["opcode"] == "BLOCKHASH": - if is_prehook(): + elif opcode == "BLOCKHASH": param = state.mstate.stack[-1] @@ -155,10 +156,9 @@ def _analyze_states(state: GlobalState) -> list: else: # we're in post hook - if ( - state.environment.code.instruction_list[state.mstate.pc - 1]["opcode"] - == "BLOCKHASH" - ): + opcode = state.environment.code.instruction_list[state.mstate.pc - 1]["opcode"] + + if opcode == "BLOCKHASH": # if we're in the post hook of a BLOCKHASH op, check if an old block number was used to create it. for annotation in state.annotations: @@ -170,9 +170,6 @@ def _analyze_states(state: GlobalState) -> list: else: # Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is executed. - instructions = state.environment.code.instruction_list - opcode = instructions[state.mstate.pc - 1]["opcode"] - state.mstate.stack[-1].annotate( PredictableValueAnnotation( "block." + opcode.lower() + " environment variable" diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 4194d136..d4f000df 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -203,6 +203,9 @@ class Instruction: end_time = datetime.now() self.iprof.record(op, start_time, end_time) + for st in global_state.mstate.stack: + logging.debug(st) + return result @StateTransition() @@ -895,7 +898,7 @@ class Instruction: return [global_state] @StateTransition(enable_gas=False) - def sha3_(self, global_state: GlobalState) -> List[GlobalState]: + def sha3_(selxf, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: @@ -1591,6 +1594,8 @@ class Instruction: op0, condition = state.stack.pop(), state.stack.pop() + logging.debug(str(condition)) + try: jump_addr = util.get_concrete_int(op0) except TypeError: From cc63cda26ffae5e766dd53771d74b49096cec093 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 15 May 2019 06:07:44 +0200 Subject: [PATCH 21/33] Refine module --- .../modules/dependence_on_predictable_vars.py | 32 +++++++++++++++---- 1 file changed, 25 insertions(+), 7 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 34e1826c..5cb26202 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -15,10 +15,13 @@ import traceback log = logging.getLogger(__name__) predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"] -critical_ops = ["CALL", "SUICIDE"] +final_ops = ["CALL", "SUICIDE", "STOP"] +# One of Bernhard's trademark hacks! + def is_prehook(): + """Check if we are in prehook.""" return "pre_hook" in traceback.format_stack()[-4] @@ -32,7 +35,7 @@ class PredictableValueAnnotation: class PredictablePathAnnotation(StateAnnotation): """State annotation used when a path is chosen based on a predictable variable.""" - def __init__(self, operation, location) -> None: + def __init__(self, operation: str, location: int) -> None: self.operation = operation self.location = location @@ -58,7 +61,7 @@ class PredictableDependenceModule(DetectionModule): "block.gaslimit, block.timestamp or block.number." ), entrypoint="callback", - pre_hooks=["BLOCKHASH", "JUMPI"] + critical_ops, + pre_hooks=["BLOCKHASH", "JUMPI"] + final_ops, post_hooks=["BLOCKHASH"] + predictable_ops, ) @@ -88,7 +91,7 @@ def _analyze_states(state: GlobalState) -> list: opcode = state.get_current_instruction()["opcode"] - if opcode in critical_ops: + if opcode in final_ops: for annotation in state.annotations: @@ -105,14 +108,28 @@ def _analyze_states(state: GlobalState) -> list: "generation or to make critical control flow decisions." ) + ''' + Usually report low severity except in cases where thje hash of a previous block is used to + determine control flow. + ''' + + severity = "Medium" if "hash" in annotation.operation else "Low" + + ''' + Note: We report the location of the JUMPI that lead to this path. Usually this maps to an if or + require statement. + ''' + + swc_id = TIMESTAMP_DEPENDENCE if "timestamp" in annotation.operation else WEAK_RANDOMNESS + issue = Issue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, - address=state.get_current_instruction()["address"], - swc_id=TIMESTAMP_DEPENDENCE, + address=annotation.location, + swc_id=swc_id, bytecode=state.environment.code.bytecode, title="Dependence on predictable environment variable", - severity="Low", + severity=severity, description_head="A control flow decision is made based on a predictable variable.", description_tail=description, gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), @@ -124,6 +141,7 @@ def _analyze_states(state: GlobalState) -> list: # Look for predictable state variables in jump condition for annotation in state.mstate.stack[-2].annotations: + if isinstance(annotation, PredictableValueAnnotation): state.annotate( PredictablePathAnnotation( From 19ce7c7526358f88dc1021a1219d7b4eef24ce39 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 15 May 2019 06:09:53 +0200 Subject: [PATCH 22/33] Of course, black has to be done --- .../modules/dependence_on_predictable_vars.py | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 5cb26202..cab8bee3 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -20,6 +20,7 @@ final_ops = ["CALL", "SUICIDE", "STOP"] # One of Bernhard's trademark hacks! + def is_prehook(): """Check if we are in prehook.""" return "pre_hook" in traceback.format_stack()[-4] @@ -108,19 +109,23 @@ def _analyze_states(state: GlobalState) -> list: "generation or to make critical control flow decisions." ) - ''' + """ Usually report low severity except in cases where thje hash of a previous block is used to determine control flow. - ''' + """ severity = "Medium" if "hash" in annotation.operation else "Low" - ''' + """ Note: We report the location of the JUMPI that lead to this path. Usually this maps to an if or require statement. - ''' + """ - swc_id = TIMESTAMP_DEPENDENCE if "timestamp" in annotation.operation else WEAK_RANDOMNESS + swc_id = ( + TIMESTAMP_DEPENDENCE + if "timestamp" in annotation.operation + else WEAK_RANDOMNESS + ) issue = Issue( contract=state.environment.active_account.contract_name, From 32275d07e4997ff34866e92d00236b5073b66e1b Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 15 May 2019 15:25:07 +0200 Subject: [PATCH 23/33] Fix norhh bugs --- mythril/analysis/modules/dependence_on_predictable_vars.py | 2 +- mythril/laser/ethereum/instructions.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index cab8bee3..e97728c8 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -15,7 +15,7 @@ import traceback log = logging.getLogger(__name__) predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"] -final_ops = ["CALL", "SUICIDE", "STOP"] +final_ops = ["CALL", "SUICIDE", "STOP", "RETURN"] # One of Bernhard's trademark hacks! diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index d4f000df..fe0ce2e8 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -898,7 +898,7 @@ class Instruction: return [global_state] @StateTransition(enable_gas=False) - def sha3_(selxf, global_state: GlobalState) -> List[GlobalState]: + def sha3_(self, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: From 2ab2d7720f409c6f94e51b18dc632fb27c354cea Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 15 May 2019 15:25:52 +0200 Subject: [PATCH 24/33] Delete stray file --- 1 | 286 -------------------------------------------------------------- 1 file changed, 286 deletions(-) delete mode 100644 1 diff --git a/1 b/1 deleted file mode 100644 index 07770b5e..00000000 --- a/1 +++ /dev/null @@ -1,286 +0,0 @@ -mythril.support.signatures [INFO]: Using signature database at /Users/bernhardmueller/.mythril/signatures.db -mythril.analysis.security [INFO]: Found 0 detection modules -mythril.laser.ethereum.svm [INFO]: LASER EVM initialized with dynamic loader: -mythril.laser.ethereum.plugins.plugin_loader [INFO]: Loading plugin: -mythril.laser.ethereum.plugins.plugin_loader [INFO]: Loading plugin: -mythril.analysis.security [INFO]: Found 11 detection modules -mythril.analysis.security [INFO]: Found 11 detection modules -mythril.laser.ethereum.svm [DEBUG]: Starting LASER execution -mythril.laser.ethereum.svm [INFO]: Starting contract creation transaction -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE -mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[64]: 96 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH8 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLVALUE -mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating NUMBER -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SUB -mythril.laser.ethereum.instructions [DEBUG]: Evaluating BLOCKHASH -mythril.laser.ethereum.instructions [DEBUG]: Evaluating TIMESTAMP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MLOAD -mythril.laser.ethereum.instructions [DEBUG]: MLOAD[64] -mythril.laser.ethereum.instructions [DEBUG]: Load from memory[64]: 96 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP4 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating NOT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating NOT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE -mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[96]: 115792089237316195423570985008687907853269984665640564039457584007913129639935 - -0 & -115792089237316195423570985008687907853269984665640564039457584007913129639935 - -0 & -1_blockhash_block_block_number - 1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADD -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP3 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE -mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[128]: 1_timestamp -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADD -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP3 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MLOAD -mythril.laser.ethereum.instructions [DEBUG]: MLOAD[64] -mythril.laser.ethereum.instructions [DEBUG]: Load from memory[64]: 96 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SUB -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SHA3 -mythril.laser.ethereum.instructions [DEBUG]: Created BitVecFunc hash. -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DIV -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating EXP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SLOAD -mythril.laser.ethereum.instructions [DEBUG]: Storage access at index 0 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MUL -mythril.laser.ethereum.instructions [DEBUG]: Evaluating NOT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP4 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MUL -mythril.laser.ethereum.instructions [DEBUG]: Evaluating OR -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SSTORE -mythril.laser.ethereum.instructions [DEBUG]: Write to storage[0] -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating CODECOPY -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating RETURN -mythril.laser.ethereum.svm [INFO]: Finished contract creation, found 1 open states -mythril.laser.ethereum.svm [INFO]: Starting message call transaction, iteration: 0, 1 initial states -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE -mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[64]: 96 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLDATASIZE -mythril.laser.ethereum.instructions [DEBUG]: Evaluating LT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLDATALOAD -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH29 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DIV -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH4 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH4 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI -mythril.laser.ethereum.svm [DEBUG]: - Entering function MAIN:unknown -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH4 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI -mythril.laser.ethereum.svm [DEBUG]: - Entering function MAIN:unknown -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLDATALOAD -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLVALUE -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADD -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADDRESS -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH20 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH8 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating BALANCE -mythril.laser.ethereum.instructions [DEBUG]: Evaluating CALLVALUE -mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ -mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MLOAD -mythril.laser.ethereum.instructions [DEBUG]: MLOAD[64] -mythril.laser.ethereum.instructions [DEBUG]: Load from memory[64]: 96 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating REVERT -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP3 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SLOAD -mythril.laser.ethereum.instructions [DEBUG]: Storage access at index 0 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating EXP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DIV -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MSTORE -mythril.laser.ethereum.instructions [DEBUG]: MSTORE to mem[96]: If(If(If(If(2_balance_at_1461501637330902918203684832716283019655932542975 & -51421440056055728346017419001665401074216449311 == - 0, - 0, - 1) == - 0, - 1, - 0) == - 0, - 1, - 0) == - 0, - 1, - 0) -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ADD -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating AND -mythril.laser.ethereum.instructions [DEBUG]: Evaluating MLOAD -mythril.laser.ethereum.instructions [DEBUG]: MLOAD[64] -mythril.laser.ethereum.instructions [DEBUG]: Load from memory[64]: 96 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating EQ -mythril.laser.ethereum.instructions [DEBUG]: Evaluating DUP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating ISZERO -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating PUSH2 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SUB -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPI -mythril.laser.ethereum.instructions [DEBUG]: Pruned unreachable states. -mythril.laser.ethereum.instructions [DEBUG]: Evaluating SWAP1 -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating RETURN -mythril.laser.ethereum.instructions [DEBUG]: Evaluating POP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMP -mythril.laser.ethereum.instructions [DEBUG]: Evaluating JUMPDEST -mythril.laser.ethereum.instructions [DEBUG]: Evaluating STOP -mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin [INFO]: Number of new instructions covered in tx 0: 131 -mythril.laser.ethereum.svm [INFO]: Starting message call transaction, iteration: 1, 0 initial states -mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin [INFO]: Number of new instructions covered in tx 1: 0 -mythril.laser.ethereum.svm [INFO]: Finished symbolic execution -mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin [INFO]: Achieved 31.85% coverage for code: 6060604052670de0b6b3a76400003414151561001a57600080fd5b600143034042604051808360001916600019168152602001828152602001925050506040518091039020600190046000806101000a81548160ff021916908360ff160217905550610164806100706000396000f30060606040526004361061004c576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634ba4c16b14610051578063b2fa1c9e1461006c575b600080fd5b61006a600480803560ff16906020019091905050610099565b005b341561007757600080fd5b61007f610117565b604051808215151515815260200191505060405180910390f35b670de0b6b3a7640000341415156100af57600080fd5b6000809054906101000a900460ff1660ff168160ff161415610114573373ffffffffffffffffffffffffffffffffffffffff166108fc671bc16d674ec800009081150290604051600060405180830381858888f19350505050151561011357600080fd5b5b50565b6000803073ffffffffffffffffffffffffffffffffffffffff1631149050905600a165627a7a72305820e70964dd89df0e5b2cf45faf9eecd590a00131d465ed3f65857d843d01c130270029 -mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin [INFO]: Achieved 77.98% coverage for code: 60606040526004361061004c576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634ba4c16b14610051578063b2fa1c9e1461006c575b600080fd5b61006a600480803560ff16906020019091905050610099565b005b341561007757600080fd5b61007f610117565b604051808215151515815260200191505060405180910390f35b670de0b6b3a7640000341415156100af57600080fd5b6000809054906101000a900460ff1660ff168160ff161415610114573373ffffffffffffffffffffffffffffffffffffffff166108fc671bc16d674ec800009081150290604051600060405180830381858888f19350505050151561011357600080fd5b5b50565b6000803073ffffffffffffffffffffffffffffffffffffffff1631149050905600a165627a7a72305820e70964dd89df0e5b2cf45faf9eecd590a00131d465ed3f65857d843d01c130270029 -mythril.analysis.security [INFO]: Starting analysis -mythril.analysis.security [INFO]: Found 0 detection modules -mythril.analysis.security [INFO]: Found 11 detection modules -mythril.analysis.security [DEBUG]: Retrieving results for DELEGATECALL Usage in Fallback Function -mythril.analysis.security [DEBUG]: Retrieving results for Dependence of Predictable Variables -mythril.analysis.security [DEBUG]: Retrieving results for Deprecated Operations -mythril.analysis.security [DEBUG]: Retrieving results for Ether Thief -mythril.analysis.security [DEBUG]: Retrieving results for Reachable Exceptions -mythril.analysis.security [DEBUG]: Retrieving results for External calls -mythril.analysis.security [DEBUG]: Retrieving results for Integer Overflow and Underflow -mythril.analysis.security [DEBUG]: Retrieving results for Multiple Sends -mythril.analysis.security [DEBUG]: Retrieving results for State Change After External calls -mythril.analysis.security [DEBUG]: Retrieving results for Unprotected Selfdestruct -mythril.analysis.security [DEBUG]: Retrieving results for Unchecked Return Value -mythril.analysis.security [INFO]: Found 11 detection modules -mythril.mythril.mythril_analyzer [INFO]: Solver statistics: -Query count: 35 -Solver time: 0.3555266857147217 From 4ee2270168e5ea254d13b1485f976d1b1fa2aeff Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 19 May 2019 14:08:52 +0200 Subject: [PATCH 25/33] Update mythril/analysis/modules/dependence_on_predictable_vars.py Co-Authored-By: Nikhil Parasaram --- mythril/analysis/modules/dependence_on_predictable_vars.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index e97728c8..c1d2a2b1 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -195,7 +195,7 @@ def _analyze_states(state: GlobalState) -> list: state.mstate.stack[-1].annotate( PredictableValueAnnotation( - "block." + opcode.lower() + " environment variable" + "block.{} environment variable".format(opcode.lower()) ) ) From dce7d9dc7c667f5de329fdea5185eea419408fa9 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 19 May 2019 14:10:33 +0200 Subject: [PATCH 26/33] Add suggestion from norhh --- mythril/analysis/modules/dependence_on_predictable_vars.py | 1 + 1 file changed, 1 insertion(+) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index c1d2a2b1..efc326dd 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -190,6 +190,7 @@ def _analyze_states(state: GlobalState) -> list: state.mstate.stack[-1].annotate( PredictableValueAnnotation("block hash of a previous block") ) + break else: # Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is executed. From d1d4460605368335abeb55d62e0790571a5355b8 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 19 May 2019 14:17:16 +0200 Subject: [PATCH 27/33] Add norhh suggestion #2 --- mythril/laser/ethereum/instructions.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index fe0ce2e8..32b48ce7 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -942,13 +942,19 @@ class Instruction: data = symbol_factory.BitVecVal(0, 1) if data.symbolic: + + annotations = [] + + for b in state.memory[index : index + length]: + annotations.append(b.annotations) + argument_str = str(state.memory[index]).replace(" ", "_") result = symbol_factory.BitVecFuncSym( "KECCAC[{}]".format(argument_str), "keccak256", 256, input_=data, - annotations=state.memory[index].annotations, + annotations=annotations, ) log.debug("Created BitVecFunc hash.") From 2a6b282ecaea494b5c7b7980f0c0d3e8fb64ca39 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 19 May 2019 14:29:06 +0200 Subject: [PATCH 28/33] Check if variable is BitVec before copying annotations --- mythril/laser/ethereum/instructions.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 59bb7dc0..ef15c879 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -946,7 +946,8 @@ class Instruction: annotations = [] for b in state.memory[index : index + length]: - annotations.append(b.annotations) + if isinstance(b, BitVec): + annotations.append(b.annotations) argument_str = str(state.memory[index]).replace(" ", "_") result = symbol_factory.BitVecFuncSym( From 990e84f66a84822ea373b96ee9ccec065cc4fc3a Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 19 May 2019 14:36:12 +0200 Subject: [PATCH 29/33] Re-add block_number class variable to environment --- mythril/laser/ethereum/state/environment.py | 1 + 1 file changed, 1 insertion(+) diff --git a/mythril/laser/ethereum/state/environment.py b/mythril/laser/ethereum/state/environment.py index 0f467413..a3300f9a 100644 --- a/mythril/laser/ethereum/state/environment.py +++ b/mythril/laser/ethereum/state/environment.py @@ -40,6 +40,7 @@ class Environment: self.active_function_name = "" self.address = active_account.address + self.block_number = symbol_factory.BitVecSym("block_number", 256) # Ib self.code = active_account.code if code is None else code From 23478f43ecc8dc406acbf48b98f893ff8c55911e Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 19 May 2019 16:00:54 +0200 Subject: [PATCH 30/33] Add typehints, remove debug statements --- .../analysis/modules/dependence_on_predictable_vars.py | 9 +++------ mythril/laser/ethereum/instructions.py | 5 ----- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index efc326dd..8aaa375c 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -18,18 +18,15 @@ predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"] final_ops = ["CALL", "SUICIDE", "STOP", "RETURN"] -# One of Bernhard's trademark hacks! - - -def is_prehook(): - """Check if we are in prehook.""" +def is_prehook() -> bool: + """Check if we are in prehook. One of Bernhard's trademark hacks!""" return "pre_hook" in traceback.format_stack()[-4] class PredictableValueAnnotation: """Symbol annotation used if a variable is initialized from a predictable environment variable.""" - def __init__(self, operation) -> None: + def __init__(self, operation: str) -> None: self.operation = operation diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index ef15c879..f17d4401 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -203,9 +203,6 @@ class Instruction: end_time = datetime.now() self.iprof.record(op, start_time, end_time) - for st in global_state.mstate.stack: - logging.debug(st) - return result @StateTransition() @@ -1601,8 +1598,6 @@ class Instruction: op0, condition = state.stack.pop(), state.stack.pop() - logging.debug(str(condition)) - try: jump_addr = util.get_concrete_int(op0) except TypeError: From 2cfa81ba2ce1c708c459a8c98ef3e67b106acd70 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 19 May 2019 16:02:05 +0200 Subject: [PATCH 31/33] Fix typo in commnent --- mythril/analysis/modules/dependence_on_predictable_vars.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 8aaa375c..5bb7e59e 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -107,7 +107,7 @@ def _analyze_states(state: GlobalState) -> list: ) """ - Usually report low severity except in cases where thje hash of a previous block is used to + Usually report low severity except in cases where the hash of a previous block is used to determine control flow. """ From c03ddd4ae066e2c5851ac5fc4514d5219dcf4fe3 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 20 May 2019 10:38:45 +0200 Subject: [PATCH 32/33] Modify report text --- mythril/analysis/modules/dependence_on_predictable_vars.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 5bb7e59e..d2dbdcd1 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -97,7 +97,7 @@ def _analyze_states(state: GlobalState) -> list: description = ( "The " + annotation.operation - + " is used in to determine an important control flow decision. " + + " is used in to determine a control flow decision. " ) description += ( "Note that the values of variables like coinbase, gaslimit, block number and timestamp " From 66ec7de153d336582dc1dd7c3510d7784efb17e9 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 21 May 2019 19:06:19 +0200 Subject: [PATCH 33/33] Make code nicer: --- .../modules/dependence_on_predictable_vars.py | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index d2dbdcd1..a8c7ac75 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -10,6 +10,7 @@ from mythril.laser.smt import ULT, symbol_factory from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.annotation import StateAnnotation +from typing import cast, List import traceback log = logging.getLogger(__name__) @@ -151,6 +152,7 @@ def _analyze_states(state: GlobalState) -> list: state.get_current_instruction()["address"], ) ) + break elif opcode == "BLOCKHASH": @@ -181,13 +183,15 @@ def _analyze_states(state: GlobalState) -> list: if opcode == "BLOCKHASH": # if we're in the post hook of a BLOCKHASH op, check if an old block number was used to create it. - for annotation in state.annotations: + annotations = cast( + List[OldBlockNumberUsedAnnotation], + list(state.get_annotations(OldBlockNumberUsedAnnotation)), + ) - if isinstance(annotation, OldBlockNumberUsedAnnotation): - state.mstate.stack[-1].annotate( - PredictableValueAnnotation("block hash of a previous block") - ) - break + if len(annotations): + state.mstate.stack[-1].annotate( + PredictableValueAnnotation("block hash of a previous block") + ) else: # Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is executed.