diff --git a/mythril/analysis/modules/transaction_order_dependence.py b/mythril/analysis/modules/transaction_order_dependence.py new file mode 100644 index 00000000..5b5e0095 --- /dev/null +++ b/mythril/analysis/modules/transaction_order_dependence.py @@ -0,0 +1,100 @@ +import logging + +from mythril.analysis.solver import get_model +from mythril.analysis.report import Issue +from mythril.laser.ethereum.state.annotation import StateAnnotation +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.smt import get_variables_from_constraints +from mythril.analysis.swc_data import TX_ORDER_DEPENDENCE +from mythril.analysis.modules.base import DetectionModule +from mythril.exceptions import UnsatError + + +log = logging.getLogger(__name__) + + +class StorageAnnotation(StateAnnotation): + def __init__(self, storage_state: GlobalState): + self.storage_state = storage_state + + +def get_transitive_annotations(value, constraints): + queue = [value] + visited = set() + visited.add(value) + annotations = [] + for value in queue: + annotations += value.annotations + for constraint in constraints: + var_list = list(get_variables_from_constraints(constraint)) + if value not in var_list: + continue + for var in var_list: + if var not in queue: + continue + visited.add(var) + queue.append(var) + return annotations + + +class TxOrderDependenceModule(DetectionModule): + def __init__(self): + super().__init__( + name="Transaction Order Dependence", + swc_id=TX_ORDER_DEPENDENCE, + pre_hooks=["CALL", "STATICCALL", "CALLCODE", "SSTORE"], + entrypoint="callback", + description=( + "This module finds the existance of transaction order dependence " + "vulnerabilities. The following webpage contains an extensive description " + "of the vulnerability: " + "https://consensys.github.io/smart-contract-best-practices/known_attacks/#transaction-ordering-dependence-tod-front-running" + ), + ) + + def execute(self, state: GlobalState): + """ Executes the analysis module""" + log.debug("Executing module: TOD") + opcode = state.get_current_instruction()["opcode"] + if opcode == "SSTORE": + value = state.mstate.stack[-2] + value.annotate(StorageAnnotation(state)) + state.mstate.stack[-2] = value + value = state.mstate.stack[-3] + annotations = get_transitive_annotations(value, state.mstate.constraints) + for annotation in annotations: + if not isinstance(annotation, StorageAnnotation): + continue + if int(annotation.storage_state.current_transaction.id) >= int( + state.current_transaction.id + ): + continue + try: + get_model( + state.mstate.constraints + + [ + state.current_transaction.caller + != annotation.storage_state.current_transaction.caller + ] + ) + except UnsatError: + continue + description_tail = "A transaction order dependence vulnerability may exist in this contract. The value or target of the call statement is loaded from a writable storage location." + + issue = Issue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=annotation.storage_state.environment.active_function_address, + title="Transaction Order Dependence", + bytecode=state.environment.code.bytecode, + swc_id=TX_ORDER_DEPENDENCE, + severity="Medium", + description_head="The call outcome may depend on transaction order.", + description_tail=description_tail, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + ) + self.issues.append(issue) + return self.issues + + +detector = TxOrderDependenceModule() diff --git a/mythril/laser/ethereum/state/environment.py b/mythril/laser/ethereum/state/environment.py index a3300f9a..395c0b73 100644 --- a/mythril/laser/ethereum/state/environment.py +++ b/mythril/laser/ethereum/state/environment.py @@ -50,6 +50,7 @@ class Environment: self.gasprice = gasprice self.origin = origin self.callvalue = callvalue + self.active_function_address = 0 def __str__(self) -> str: """ diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index fae71dc8..eaa3d873 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -440,6 +440,7 @@ class LaserEVM: environment.active_function_name = disassembly.address_to_function_name[ address ] + environment.active_function_address = address new_node.flags |= NodeFlags.FUNC_ENTRY log.debug( diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index f5863c1c..fdf50fbf 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -111,6 +111,9 @@ class BaseTransaction: # Initialize the execution environment global_state = GlobalState(self.world_state, environment, None) global_state.environment.active_function_name = active_function + global_state.environment.active_function_address = ( + environment.active_function_address + ) sender = environment.sender receiver = environment.active_account.address diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index d849d0c4..45125e6f 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -185,6 +185,29 @@ class _Z3SymbolFactory(SymbolFactory[z3.BoolRef, z3.BitVecRef]): return z3.BitVec(name, size) +def _visitor(e, seen): + if e in seen: + return + seen[e] = True + yield e + if z3.is_app(e): + for ch in e.children(): + for e in _visitor(ch, seen): + yield e + return + if z3.is_quantifier(e): + for e in _visitor(e.body(), seen): + yield e + return + + +def get_variables_from_constraints(constraint): + seen = {} + for e in _visitor(constraint, seen): + if z3.is_const(e) and e.decl().kind() == z3.Z3_OP_UNINTERPRETED: + yield e + + # This is the instance that other parts of mythril should use # Type hints are not allowed here in 3.5 diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index 05081137..67224243 100644 --- a/mythril/laser/smt/bitvec.py +++ b/mythril/laser/smt/bitvec.py @@ -243,6 +243,9 @@ class BitVec(Expression[z3.BitVecRef]): """ return self._handle_shift(other, rshift) + def __hash__(self): + return self.raw.__hash__() + def _comparison_helper( a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index f73ef504..46287be5 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -223,3 +223,6 @@ class BitVecFunc(BitVec): :return The resulting right shifted output: """ return _arithmetic_helper(self, other, operator.rshift) + + def __hash__(self): + return self.raw.__hash__() diff --git a/mythril/laser/smt/bool.py b/mythril/laser/smt/bool.py index 1dd1cc76..5cfcbb83 100644 --- a/mythril/laser/smt/bool.py +++ b/mythril/laser/smt/bool.py @@ -80,6 +80,9 @@ class Bool(Expression[z3.BoolRef]): else: return False + def __hash__(self): + return self.raw.__hash__() + def And(*args: Union[Bool, bool]) -> Bool: """Create an And expression."""