From cad6f5ae35828c36b9969c9b27436dcc2a2c0793 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 13 May 2019 23:39:38 +0200 Subject: [PATCH] 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)))