Add differentiation between blockhash of previous and current/future block numbers

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,33 +94,53 @@ 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:
+        # we're in post hook
+
+        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:
-                if isinstance(annotation, TaintBlockHashAnnotation):
-                    state.mstate.stack[-1].annotate(PredictableValueAnnotation("BLOCKHASH"))
+
+                '''
+                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:
-        # we're in post hook
+            # 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)
+            annotation = PredictableValueAnnotation("block." + opcode.lower() + "environment variable")
             state.mstate.stack[-1].annotate(annotation)
 
     return issues

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