From 2c6fcc4db74b02c711bfdca8237f18e86041fa0c Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 4 Feb 2020 18:11:38 +0000 Subject: [PATCH] Add a minimal TOD module --- .../modules/transaction_order_dependence.py | 157 ++++++++---------- mythril/laser/smt/expression.py | 3 + 2 files changed, 74 insertions(+), 86 deletions(-) diff --git a/mythril/analysis/modules/transaction_order_dependence.py b/mythril/analysis/modules/transaction_order_dependence.py index 01217e2a..a4b22a42 100644 --- a/mythril/analysis/modules/transaction_order_dependence.py +++ b/mythril/analysis/modules/transaction_order_dependence.py @@ -7,17 +7,11 @@ from mythril.analysis.potential_issues import ( get_potential_issues_annotation, ) from mythril.analysis.swc_data import TX_ORDER_DEPENDENCE -from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.ethereum.transaction.symbolic import ACTORS -from mythril.laser.ethereum.transaction.transaction_models import ( - ContractCreationTransaction, -) from mythril.analysis.modules.base import DetectionModule -from mythril.laser.smt import UGT, symbol_factory, Or, BitVec -from mythril.laser.ethereum.natives import PRECOMPILE_COUNT +from mythril.laser.smt import Or from mythril.laser.ethereum.state.global_state import GlobalState from mythril.exceptions import UnsatError -from copy import copy import logging log = logging.getLogger(__name__) @@ -31,21 +25,14 @@ an informational issue. """ -def _is_precompile_call(global_state: GlobalState): - to = global_state.mstate.stack[-2] # type: BitVec - constraints = copy(global_state.world_state.constraints) - constraints += [ - Or( - to < symbol_factory.BitVecVal(1, 256), - to > symbol_factory.BitVecVal(PRECOMPILE_COUNT, 256), - ) - ] +class BalanceAnnotation: + def __init__(self, caller): + self.caller = caller + - try: - solver.get_model(constraints) - return False - except UnsatError: - return True +class StorageAnnotation: + def __init__(self, caller): + self.caller = caller class TransactionOrderDependence(DetectionModule): @@ -59,6 +46,7 @@ class TransactionOrderDependence(DetectionModule): description=DESCRIPTION, entrypoint="callback", pre_hooks=["CALL"], + post_hooks=["BALANCE", "SLOAD"], ) def _execute(self, state: GlobalState) -> None: @@ -72,88 +60,85 @@ class TransactionOrderDependence(DetectionModule): annotation = get_potential_issues_annotation(state) annotation.potential_issues.extend(potential_issues) + @staticmethod + def annotate_balance_storage_vals(state, opcode): + val = state.mstate.stack[-1] + if opcode == "BALANCE": + annotation = BalanceAnnotation + else: + annotation = StorageAnnotation + if len(val.get_annotations(annotation)) == 0: + state.mstate.stack[-1].annotate(annotation(state.environment.sender)) + return [] + def _analyze_state(self, state: GlobalState): """ :param state: :return: """ - gas = state.mstate.stack[-1] - to = state.mstate.stack[-2] + opcode = state.get_current_instruction()["opcode"] + if opcode != "CALL": + opcode = state.environment.code.instruction_list[state.mstate.pc - 1][ + "opcode" + ] + if opcode in ("BALANCE", "SLOAD"): + self.annotate_balance_storage_vals(state, opcode) + return [] + + value = state.mstate.stack[-3] + if ( + len(value.get_annotations(StorageAnnotation)) + + len(value.get_annotations(BalanceAnnotation)) + == 0 + ): + return [] + callers = [] + + storage_annotations = value.get_annotations(StorageAnnotation) + if len(storage_annotations) == 1: + callers.append(storage_annotations[0].caller) + balance_annotations = value.get_annotations(BalanceAnnotation) + if len(balance_annotations) == 1: + callers.append(balance_annotations[0].caller) address = state.get_current_instruction()["address"] + call_constraint = False + for caller in callers: + call_constraint = Or(call_constraint, ACTORS.attacker == caller) try: - constraints = Constraints([UGT(gas, symbol_factory.BitVecVal(2300, 256))]) + constraints = state.world_state.constraints + [call_constraint] - solver.get_transaction_sequence( - state, constraints + state.world_state.constraints + solver.get_transaction_sequence(state, constraints) + + description_head = "Transaction Order dependence." + description_tail = ( + "The callee address of an external message call can be set by " + "the caller. Note that the callee can contain arbitrary code and may re-enter any function " + "in this contract. Review the business logic carefully to prevent averse effects on the " + "contract state." ) - # Check whether we can also set the callee address - - try: - new_constraints = constraints + [to == ACTORS.attacker] - - solver.get_transaction_sequence( - state, new_constraints + state.world_state.constraints - ) - - description_head = "A call to a user-supplied address is executed." - description_tail = ( - "The callee address of an external message call can be set by " - "the caller. Note that the callee can contain arbitrary code and may re-enter any function " - "in this contract. Review the business logic carefully to prevent averse effects on the " - "contract state." - ) - - issue = PotentialIssue( - contract=state.environment.active_account.contract_name, - function_name=state.environment.active_function_name, - address=address, - swc_id=TransactionOrderDependence, - title="External Call To User-Supplied Address", - bytecode=state.environment.code.bytecode, - severity="Medium", - description_head=description_head, - description_tail=description_tail, - constraints=new_constraints, - detector=self, - ) - - except UnsatError: - if _is_precompile_call(state): - return [] - - log.debug( - "[EXTERNAL_CALLS] Callee address cannot be modified. Reporting informational issue." - ) - - description_head = "The contract executes an external message call." - description_tail = ( - "An external function call to a fixed contract address is executed. Make sure " - "that the callee contract has been reviewed carefully." - ) - - issue = PotentialIssue( - contract=state.environment.active_account.contract_name, - function_name=state.environment.active_function_name, - address=address, - swc_id=TX_ORDER_DEPENDENCE, - title="Transaction Order Dependence", - bytecode=state.environment.code.bytecode, - severity="Low", - description_head=description_head, - description_tail=description_tail, - constraints=constraints, - detector=self, - ) + issue = PotentialIssue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=address, + swc_id=TX_ORDER_DEPENDENCE, + title="Transaction Order Dependence", + bytecode=state.environment.code.bytecode, + severity="Medium", + description_head=description_head, + description_tail=description_tail, + constraints=constraints, + detector=self, + ) except UnsatError: - log.debug("[EXTERNAL_CALLS] No model found.") + log.debug("[Transaction Order Dependence] No model found.") return [] return [issue] -detector = ExternalCalls() +detector = TransactionOrderDependence() diff --git a/mythril/laser/smt/expression.py b/mythril/laser/smt/expression.py index 9fa7cef1..c549f818 100644 --- a/mythril/laser/smt/expression.py +++ b/mythril/laser/smt/expression.py @@ -54,6 +54,9 @@ class Expression(Generic[T]): def __hash__(self) -> int: return self.raw.__hash__() + def get_annotations(self, annotation: Any): + return list(filter(lambda x: isinstance(x, annotation), self.annotations)) + G = TypeVar("G", bound=Expression)