From 64ea5678eb16da624fc905856e8198127316ce44 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 29 Apr 2018 10:01:29 +0200
Subject: [PATCH 1/8] Init tod detection

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

diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py
new file mode 100644
index 00000000..a62ee7fd
--- /dev/null
+++ b/mythril/analysis/modules/transaction_order_independence.py
@@ -0,0 +1,27 @@
+from z3 import *
+from mythril.analysis.ops import *
+from mythril.analysis import solver
+from mythril.analysis.report import Issue
+from mythril.exceptions import UnsatError
+import re
+import logging
+
+
+'''
+MODULE DESCRIPTION:
+
+'''
+
+
+def execute(statespace):
+
+    logging.debug("Executing module: ETHER_SEND")
+
+    issues = []
+
+    for call in statespace.calls:
+
+        state = call.state
+        address = state.get_current_instruction()['address']
+
+    return issues

From 1869c83cc520cc15a4657553707686471dcef9d7 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 29 Apr 2018 13:24:08 +0200
Subject: [PATCH 2/8] Init tod

---
 .../modules/transaction_order_independence.py | 46 ++++++++++++++++++-
 1 file changed, 44 insertions(+), 2 deletions(-)

diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py
index a62ee7fd..8c59c527 100644
--- a/mythril/analysis/modules/transaction_order_independence.py
+++ b/mythril/analysis/modules/transaction_order_independence.py
@@ -15,13 +15,55 @@ MODULE DESCRIPTION:
 
 def execute(statespace):
 
-    logging.debug("Executing module: ETHER_SEND")
+    logging.debug("Executing module: TOD")
 
     issues = []
 
     for call in statespace.calls:
 
         state = call.state
-        address = state.get_current_instruction()['address']
+        node = call.node
 
+        # Interesting values
+        to, value = call.to, call.value
+        storages = []
+        if to.type == VarType.SYMBOLIC:
+            storages += _dependent_on_storage(to.val)
+        if value.type == VarType.SYMBOLIC:
+            storages += _dependent_on_storage(value.val)
+        print(storages)
     return issues
+
+
+def _dependent_on_storage(expression):
+    pattern = re.compile(r"storage_([a-z0-9_&^]+)")
+    result = pattern.search(str(simplify(expression)))
+    if result is not None:
+        return [result.group()]
+    return []
+
+
+def _get_storage_variable(storage, state):
+    index = int(re.search('[0-9]+', storage))
+    try:
+        return state.environment.active_account.storage[index]
+    except KeyError:
+        return None
+
+def _can_change(constraints, variable):
+    _constraints = copy.deepcopy(constraints)
+    model = solver.get_model(_constraints)
+    initial_value = int(str(model.eval(variable, model_completion=True)))
+
+
+
+    # if type(op0) is not int:
+    #     op0_value = int(str(model.eval(op0, model_completion=True)))
+    #     model0 = _try_constraints(node.constraints, [constraint, op0 != op0_value])
+    #
+    # if type(op1) is not int:
+    #     op1_value = int(str(model.eval(op1, model_completion=True)))
+    #     model1 = _try_constraints(node.constraints, [constraint, op1 != op1_value])
+    #
+    # if model0 is None and model1 is None:
+    #     return False

From 41c116359d2bc6ff21e35c7c0cc7297c69feb13f Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 29 Apr 2018 14:02:51 +0200
Subject: [PATCH 3/8] Initial tod working version

---
 .../modules/transaction_order_independence.py | 96 ++++++++++++++-----
 1 file changed, 72 insertions(+), 24 deletions(-)

diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py
index 8c59c527..90540672 100644
--- a/mythril/analysis/modules/transaction_order_independence.py
+++ b/mythril/analysis/modules/transaction_order_independence.py
@@ -20,20 +20,31 @@ def execute(statespace):
     issues = []
 
     for call in statespace.calls:
-
-        state = call.state
+        interesting_storages = list(_get_influencing_storages(call))
+        c = list(_find_changable(statespace, interesting_storages))
         node = call.node
+        instruction = call.state.get_current_instruction()
+
+        if len(c) > 0:
+            issue = Issue(node.contract_name, node.function_name, instruction['address'], "Transaction order dependence",
+                          "Warning")
+
+            issue.description = "A possible transaction order independence vulnerability exists in function {}. The value or " \
+                                "direction of the call statement is determined from a tainted storage location".format(
+                node.function_name)
+            # issue.debug = solver.pretty_print_model(model)
+            issues.append(issue)
+
 
-        # Interesting values
-        to, value = call.to, call.value
-        storages = []
-        if to.type == VarType.SYMBOLIC:
-            storages += _dependent_on_storage(to.val)
-        if value.type == VarType.SYMBOLIC:
-            storages += _dependent_on_storage(value.val)
-        print(storages)
     return issues
 
+def _get_states_with_opcode(statespace, opcode):
+    for k in statespace.nodes:
+        node = statespace.nodes[k]
+        for state in node.states:
+            if state.get_current_instruction()["opcode"] == opcode:
+                yield state, node
+
 
 def _dependent_on_storage(expression):
     pattern = re.compile(r"storage_([a-z0-9_&^]+)")
@@ -44,26 +55,63 @@ def _dependent_on_storage(expression):
 
 
 def _get_storage_variable(storage, state):
-    index = int(re.search('[0-9]+', storage))
+    index = int(re.search('[0-9]+', storage).group())
     try:
         return state.environment.active_account.storage[index]
     except KeyError:
         return None
 
+
 def _can_change(constraints, variable):
     _constraints = copy.deepcopy(constraints)
     model = solver.get_model(_constraints)
     initial_value = int(str(model.eval(variable, model_completion=True)))
-
-
-
-    # if type(op0) is not int:
-    #     op0_value = int(str(model.eval(op0, model_completion=True)))
-    #     model0 = _try_constraints(node.constraints, [constraint, op0 != op0_value])
-    #
-    # if type(op1) is not int:
-    #     op1_value = int(str(model.eval(op1, model_completion=True)))
-    #     model1 = _try_constraints(node.constraints, [constraint, op1 != op1_value])
-    #
-    # if model0 is None and model1 is None:
-    #     return False
+    return _try_constraints(constraints, [variable != initial_value]) is not None
+
+
+def _get_influencing_storages(call):
+    state = call.state
+    node = call.node
+
+    # Get relevant storages
+    to, value = call.to, call.value
+    storages = []
+    if to.type == VarType.SYMBOLIC:
+        storages += _dependent_on_storage(to.val)
+    if value.type == VarType.SYMBOLIC:
+        storages += _dependent_on_storage(value.val)
+
+    # See if they can change within the constraints of the node
+    for storage in storages:
+        variable = _get_storage_variable(storage, state)
+        can_change = _can_change(node.constraints, variable)
+        if can_change:
+            yield storage
+
+
+def _find_changable(statespace, interesting_storages):
+    for sstore_state, node in _get_states_with_opcode(statespace, 'SSTORE'):
+        index, value = sstore_state.mstate.stack[-1], sstore_state.mstate.stack[-2]
+        try:
+            index = helper.get_concrete_int(index)
+        except AttributeError:
+            index = str(index)
+        if "storage_{}".format(index) not in interesting_storages:
+            continue
+
+        yield sstore_state, node
+
+# TODO: remove
+def _try_constraints(constraints, new_constraints):
+    """
+    Tries new constraints
+    :return Model if satisfiable otherwise None
+    """
+    _constraints = copy.deepcopy(constraints)
+    for constraint in new_constraints:
+        _constraints.append(copy.deepcopy(constraint))
+    try:
+        model = solver.get_model(_constraints)
+        return model
+    except UnsatError:
+        return None

From 9654c937f56ba0d25a577b6783f438d5d4a6b50c Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 29 Apr 2018 14:07:05 +0200
Subject: [PATCH 4/8] Clean up execute statement

---
 .../modules/transaction_order_independence.py | 33 +++++++++++--------
 1 file changed, 19 insertions(+), 14 deletions(-)

diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py
index 90540672..9e4f3c9b 100644
--- a/mythril/analysis/modules/transaction_order_independence.py
+++ b/mythril/analysis/modules/transaction_order_independence.py
@@ -6,38 +6,42 @@ from mythril.exceptions import UnsatError
 import re
 import logging
 
-
 '''
 MODULE 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(statespace):
-
+    """ Executes the analysis module"""
     logging.debug("Executing module: TOD")
 
     issues = []
 
     for call in statespace.calls:
+        # Do analysis
         interesting_storages = list(_get_influencing_storages(call))
-        c = list(_find_changable(statespace, interesting_storages))
-        node = call.node
-        instruction = call.state.get_current_instruction()
-
-        if len(c) > 0:
-            issue = Issue(node.contract_name, node.function_name, instruction['address'], "Transaction order dependence",
+        changing_sstores = list(_find_changable(statespace, interesting_storages))
+
+        # Build issue if necessary
+        if len(changing_sstores) > 0:
+            node = call.node
+            instruction = call.state.get_current_instruction()
+            issue = Issue(node.contract_name, node.function_name, instruction['address'],
+                          "Transaction order dependence",
                           "Warning")
 
-            issue.description = "A possible transaction order independence vulnerability exists in function {}. The value or " \
-                                "direction of the call statement is determined from a tainted storage location".format(
-                node.function_name)
-            # issue.debug = solver.pretty_print_model(model)
+            issue.description = \
+                "A possible transaction order independence vulnerability exists in function {}. The value or " \
+                "direction of the call statement is determined from a tainted storage location"\
+                .format(node.function_name)
             issues.append(issue)
 
-
     return issues
 
+
 def _get_states_with_opcode(statespace, opcode):
     for k in statespace.nodes:
         node = statespace.nodes[k]
@@ -101,6 +105,7 @@ def _find_changable(statespace, interesting_storages):
 
         yield sstore_state, node
 
+
 # TODO: remove
 def _try_constraints(constraints, new_constraints):
     """

From fa618d111d2da5523dfd3fc6557683eb7210d842 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 29 Apr 2018 14:14:43 +0200
Subject: [PATCH 5/8] Rename things and documentation

---
 .../modules/transaction_order_independence.py   | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py
index 9e4f3c9b..76f4d34a 100644
--- a/mythril/analysis/modules/transaction_order_independence.py
+++ b/mythril/analysis/modules/transaction_order_independence.py
@@ -23,7 +23,7 @@ def execute(statespace):
     for call in statespace.calls:
         # Do analysis
         interesting_storages = list(_get_influencing_storages(call))
-        changing_sstores = list(_find_changable(statespace, interesting_storages))
+        changing_sstores = list(_get_influencing_sstores(statespace, interesting_storages))
 
         # Build issue if necessary
         if len(changing_sstores) > 0:
@@ -41,8 +41,9 @@ def execute(statespace):
 
     return issues
 
-
+# TODO: move to __init__ or util module
 def _get_states_with_opcode(statespace, opcode):
+    """ Gets all (state, node) tuples in statespace with opcode"""
     for k in statespace.nodes:
         node = statespace.nodes[k]
         for state in node.states:
@@ -51,6 +52,7 @@ def _get_states_with_opcode(statespace, opcode):
 
 
 def _dependent_on_storage(expression):
+    """ Checks if expression is dependent on a storage symbol and returns the influencing storages"""
     pattern = re.compile(r"storage_([a-z0-9_&^]+)")
     result = pattern.search(str(simplify(expression)))
     if result is not None:
@@ -59,6 +61,12 @@ def _dependent_on_storage(expression):
 
 
 def _get_storage_variable(storage, state):
+    """
+    Get storage z3 object given storage name and the state
+    :param storage: storage name example: storage_0
+    :param state: state to retrieve the variable from
+    :return: z3 object representing storage
+    """
     index = int(re.search('[0-9]+', storage).group())
     try:
         return state.environment.active_account.storage[index]
@@ -67,6 +75,7 @@ def _get_storage_variable(storage, state):
 
 
 def _can_change(constraints, variable):
+    """ Checks if the variable can change given some constraints """
     _constraints = copy.deepcopy(constraints)
     model = solver.get_model(_constraints)
     initial_value = int(str(model.eval(variable, model_completion=True)))
@@ -74,6 +83,7 @@ def _can_change(constraints, variable):
 
 
 def _get_influencing_storages(call):
+    """ Examines a Call object and returns an iterator of all storages that influence the call value or direction"""
     state = call.state
     node = call.node
 
@@ -93,7 +103,8 @@ def _get_influencing_storages(call):
             yield storage
 
 
-def _find_changable(statespace, interesting_storages):
+def _get_influencing_sstores(statespace, interesting_storages):
+    """ Gets sstore (state, node) tuples that write to interesting_storages"""
     for sstore_state, node in _get_states_with_opcode(statespace, 'SSTORE'):
         index, value = sstore_state.mstate.stack[-1], sstore_state.mstate.stack[-2]
         try:

From 6c096bd2bb196e56785c7aeaa4d3c0e8cb8dd400 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 29 Apr 2018 14:15:20 +0200
Subject: [PATCH 6/8] Clean up imports

---
 .../analysis/modules/transaction_order_independence.py   | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py
index 76f4d34a..786fffc3 100644
--- a/mythril/analysis/modules/transaction_order_independence.py
+++ b/mythril/analysis/modules/transaction_order_independence.py
@@ -1,10 +1,10 @@
-from z3 import *
-from mythril.analysis.ops import *
+import logging
+import re
+
 from mythril.analysis import solver
+from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.exceptions import UnsatError
-import re
-import logging
 
 '''
 MODULE DESCRIPTION:
@@ -41,6 +41,7 @@ def execute(statespace):
 
     return issues
 
+
 # TODO: move to __init__ or util module
 def _get_states_with_opcode(statespace, opcode):
     """ Gets all (state, node) tuples in statespace with opcode"""

From 786df04aacca4d79188a815ffe63fdc5ee1145aa Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 29 Apr 2018 14:22:36 +0200
Subject: [PATCH 7/8] Use different re function

---
 mythril/analysis/modules/transaction_order_independence.py | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py
index 786fffc3..79dc7a2a 100644
--- a/mythril/analysis/modules/transaction_order_independence.py
+++ b/mythril/analysis/modules/transaction_order_independence.py
@@ -54,11 +54,8 @@ def _get_states_with_opcode(statespace, opcode):
 
 def _dependent_on_storage(expression):
     """ Checks if expression is dependent on a storage symbol and returns the influencing storages"""
-    pattern = re.compile(r"storage_([a-z0-9_&^]+)")
-    result = pattern.search(str(simplify(expression)))
-    if result is not None:
-        return [result.group()]
-    return []
+    pattern = re.compile(r"storage_[a-z0-9_&^]+")
+    return pattern.findall(str(simplify(expression)))
 
 
 def _get_storage_variable(storage, state):

From 53587d2cf8f3214e67465ab67df84c839c07ffb8 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Tue, 1 May 2018 16:49:35 +0200
Subject: [PATCH 8/8] Add exception handler to tod module and adapt tests

---
 .../modules/transaction_order_independence.py       |  5 ++++-
 tests/testdata/outputs_expected/calls.sol.o.json    |  8 ++++++++
 .../testdata/outputs_expected/calls.sol.o.markdown  | 11 +++++++++++
 tests/testdata/outputs_expected/calls.sol.o.text    |  8 ++++++++
 .../outputs_expected/weak_random.sol.o.json         |  8 ++++++++
 .../outputs_expected/weak_random.sol.o.markdown     | 13 ++++++++++++-
 .../outputs_expected/weak_random.sol.o.text         |  8 ++++++++
 7 files changed, 59 insertions(+), 2 deletions(-)

diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py
index 79dc7a2a..783bd6fb 100644
--- a/mythril/analysis/modules/transaction_order_independence.py
+++ b/mythril/analysis/modules/transaction_order_independence.py
@@ -75,7 +75,10 @@ def _get_storage_variable(storage, state):
 def _can_change(constraints, variable):
     """ Checks if the variable can change given some constraints """
     _constraints = copy.deepcopy(constraints)
-    model = solver.get_model(_constraints)
+    try:
+        model = solver.get_model(_constraints)
+    except UnsatError:
+        return False
     initial_value = int(str(model.eval(variable, model_completion=True)))
     return _try_constraints(constraints, [variable != initial_value]) is not None
 
diff --git a/tests/testdata/outputs_expected/calls.sol.o.json b/tests/testdata/outputs_expected/calls.sol.o.json
index ee7a0bac..cdfbbad4 100644
--- a/tests/testdata/outputs_expected/calls.sol.o.json
+++ b/tests/testdata/outputs_expected/calls.sol.o.json
@@ -42,6 +42,14 @@
             "address": 912,
             "debug": "<DEBUG-DATA>"
         },
+        {
+            "title": "Transaction order dependence",
+            "description": "A possible transaction order independence vulnerability exists in function _function_0xd24b08cc. The value or direction of the call statement is determined from a tainted storage location",
+            "function": "_function_0xd24b08cc",
+            "type": "Warning",
+            "address": 779,
+            "debug": "<DEBUG-DATA>"
+        },
         {
             "title": "Unchecked CALL return value",
             "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
diff --git a/tests/testdata/outputs_expected/calls.sol.o.markdown b/tests/testdata/outputs_expected/calls.sol.o.markdown
index 6342e72b..42ab6853 100644
--- a/tests/testdata/outputs_expected/calls.sol.o.markdown
+++ b/tests/testdata/outputs_expected/calls.sol.o.markdown
@@ -55,6 +55,17 @@ The contract account state is changed after an external call. Consider that the
 
 This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied adresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
 
+## Transaction order dependence
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `_function_0xd24b08cc`
+- PC address: 779
+
+### Description
+
+A possible transaction order independence vulnerability exists in function _function_0xd24b08cc. The value or direction of the call statement is determined from a tainted storage location
+
 ## Unchecked CALL return value
 
 - Type: Informational
diff --git a/tests/testdata/outputs_expected/calls.sol.o.text b/tests/testdata/outputs_expected/calls.sol.o.text
index 09a2b695..9e6a688f 100644
--- a/tests/testdata/outputs_expected/calls.sol.o.text
+++ b/tests/testdata/outputs_expected/calls.sol.o.text
@@ -38,6 +38,14 @@ PC address: 912
 This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied adresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
 --------------------
 
+==== Transaction order dependence ====
+Type: Warning
+Contract: Unknown
+Function name: _function_0xd24b08cc
+PC address: 779
+A possible transaction order independence vulnerability exists in function _function_0xd24b08cc. The value or direction of the call statement is determined from a tainted storage location
+--------------------
+
 ==== Unchecked CALL return value ====
 Type: Informational
 Contract: Unknown
diff --git a/tests/testdata/outputs_expected/weak_random.sol.o.json b/tests/testdata/outputs_expected/weak_random.sol.o.json
index 62158749..2338b178 100644
--- a/tests/testdata/outputs_expected/weak_random.sol.o.json
+++ b/tests/testdata/outputs_expected/weak_random.sol.o.json
@@ -33,6 +33,14 @@
             "type": "Informational",
             "address": 146,
             "debug": "<DEBUG-DATA>"
+        },
+        {
+            "title": "Transaction order dependence",
+            "description": "A possible transaction order independence vulnerability exists in function _function_0xe9874106. The value or direction of the call statement is determined from a tainted storage location",
+            "function": "_function_0xe9874106",
+            "type": "Warning",
+            "address": 1285,
+            "debug": "<DEBUG-DATA>"
         }
     ]
 }
\ No newline at end of file
diff --git a/tests/testdata/outputs_expected/weak_random.sol.o.markdown b/tests/testdata/outputs_expected/weak_random.sol.o.markdown
index 2f3319b5..b5744566 100644
--- a/tests/testdata/outputs_expected/weak_random.sol.o.markdown
+++ b/tests/testdata/outputs_expected/weak_random.sol.o.markdown
@@ -48,4 +48,15 @@ A reachable exception (opcode 0xfe) has been detected. This can be caused by typ
 
 ### Description
 
-A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. 
\ No newline at end of file
+A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. 
+
+## Transaction order dependence
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `_function_0xe9874106`
+- PC address: 1285
+
+### Description
+
+A possible transaction order independence vulnerability exists in function _function_0xe9874106. The value or direction of the call statement is determined from a tainted storage location
\ No newline at end of file
diff --git a/tests/testdata/outputs_expected/weak_random.sol.o.text b/tests/testdata/outputs_expected/weak_random.sol.o.text
index 1537e177..9e105cfe 100644
--- a/tests/testdata/outputs_expected/weak_random.sol.o.text
+++ b/tests/testdata/outputs_expected/weak_random.sol.o.text
@@ -36,3 +36,11 @@ PC address: 146
 A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. 
 --------------------
 
+==== Transaction order dependence ====
+Type: Warning
+Contract: Unknown
+Function name: _function_0xe9874106
+PC address: 1285
+A possible transaction order independence vulnerability exists in function _function_0xe9874106. The value or direction of the call statement is determined from a tainted storage location
+--------------------
+