Add a minimal TOD module

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

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)