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": "" }, + { + "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 +-------------------- +