First implementation of blockhash handling

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"],
+            pre_hooks=["BLOCKHASH", "JUMPI"],
-            post_hooks=predictable_ops,
+            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
 

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()

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