diff --git a/mythril/analysis/modules/transaction_order_independence.py b/mythril/analysis/modules/transaction_order_independence.py new file mode 100644 index 00000000..783bd6fb --- /dev/null +++ b/mythril/analysis/modules/transaction_order_independence.py @@ -0,0 +1,134 @@ +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 + +''' +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)) + changing_sstores = list(_get_influencing_sstores(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) + issues.append(issue) + + 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: + if state.get_current_instruction()["opcode"] == opcode: + yield state, node + + +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_&^]+") + return pattern.findall(str(simplify(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] + except KeyError: + return None + + +def _can_change(constraints, variable): + """ Checks if the variable can change given some constraints """ + _constraints = copy.deepcopy(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 + + +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 + + # 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 _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: + 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 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": "" }, + { + "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": "" + }, { "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": "" + }, + { + "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": "" } ] } \ 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 +-------------------- +