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