From df886eb81c2a33c67999e60b4ebb4c2e45f01ea1 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Mon, 3 Feb 2020 22:29:20 +0000
Subject: [PATCH] Add a TOD module file

---
 .../modules/transaction_order_dependence.py   | 159 ++++++++++++++++++
 1 file changed, 159 insertions(+)
 create mode 100644 mythril/analysis/modules/transaction_order_dependence.py

diff --git a/mythril/analysis/modules/transaction_order_dependence.py b/mythril/analysis/modules/transaction_order_dependence.py
new file mode 100644
index 00000000..01217e2a
--- /dev/null
+++ b/mythril/analysis/modules/transaction_order_dependence.py
@@ -0,0 +1,159 @@
+"""This module contains the detection code for transaction order dependence
+calls."""
+
+from mythril.analysis import solver
+from mythril.analysis.potential_issues import (
+    PotentialIssue,
+    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.ethereum.state.global_state import GlobalState
+from mythril.exceptions import UnsatError
+from copy import copy
+import logging
+
+log = logging.getLogger(__name__)
+
+DESCRIPTION = """
+
+Search for low level calls (e.g. call.value()) that forward all gas to the callee.
+Report a warning if the callee address can be set by the sender, otherwise create 
+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),
+        )
+    ]
+
+    try:
+        solver.get_model(constraints)
+        return False
+    except UnsatError:
+        return True
+
+
+class TransactionOrderDependence(DetectionModule):
+    """This module searches for transaction order dependence."""
+
+    def __init__(self):
+        """"""
+        super().__init__(
+            name="Transaction Order Dependence",
+            swc_id=TX_ORDER_DEPENDENCE,
+            description=DESCRIPTION,
+            entrypoint="callback",
+            pre_hooks=["CALL"],
+        )
+
+    def _execute(self, state: GlobalState) -> None:
+        """
+
+        :param state:
+        :return:
+        """
+        potential_issues = self._analyze_state(state)
+
+        annotation = get_potential_issues_annotation(state)
+        annotation.potential_issues.extend(potential_issues)
+
+    def _analyze_state(self, state: GlobalState):
+        """
+
+        :param state:
+        :return:
+        """
+        gas = state.mstate.stack[-1]
+        to = state.mstate.stack[-2]
+
+        address = state.get_current_instruction()["address"]
+
+        try:
+            constraints = Constraints([UGT(gas, symbol_factory.BitVecVal(2300, 256))])
+
+            solver.get_transaction_sequence(
+                state, constraints + state.world_state.constraints
+            )
+
+            # 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,
+                )
+
+        except UnsatError:
+            log.debug("[EXTERNAL_CALLS] No model found.")
+            return []
+
+        return [issue]
+
+
+detector = ExternalCalls()