Add Transaction order dependence

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

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:
         """

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(

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

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

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

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

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."""