diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index d2e75b56..5bb3e10e 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -19,6 +19,8 @@ from mythril.laser.smt import ( UGT, BitVec, is_true, + Bool, + BitVecFunc, is_false, URem, SRem, @@ -1369,42 +1371,20 @@ class Instruction: state = global_state.mstate index = state.stack.pop() log.debug("Storage access at index " + str(index)) - - try: - index = util.get_concrete_int(index) - return self._sload_helper(global_state, index) - - except TypeError: - if not keccak_function_manager.is_keccak(index): - return self._sload_helper(global_state, str(index)) - - storage_keys = global_state.environment.active_account.storage.keys() - keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys)) - - results = [] # type: List[GlobalState] - constraints = [] - - for keccak_key in keccak_keys: - key_argument = keccak_function_manager.get_argument(keccak_key) - index_argument = keccak_function_manager.get_argument(index) - constraints.append((keccak_key, key_argument == index_argument)) - - for (keccak_key, constraint) in constraints: - if constraint in state.constraints: - results += self._sload_helper( - global_state, keccak_key, [constraint] - ) - if len(results) > 0: - return results - - for (keccak_key, constraint) in constraints: - results += self._sload_helper( - copy(global_state), keccak_key, [constraint] - ) - if len(results) > 0: - return results - - return self._sload_helper(global_state, str(index)) + """ + if index not in global_state.environment.active_account.storage.keys(): + for key in global_state.environment.active_account.storage.keys(): + if not isinstance(index, BitVecFunc) or not isinstance(key, BitVecFunc): + global_state.mstate.constraints.append(Bool(key.raw != index.raw)) + continue + key_map = Extract(255, 0, key.input_) + index_map = Extract(255, 0, index.input_) + if simplify(key_map == index_map): + continue + global_state.mstate.constraints.append(key != index) + """ + state.stack.append(global_state.environment.active_account.storage[index]) + return [global_state] @staticmethod def _sload_helper( @@ -1454,59 +1434,21 @@ class Instruction: global keccak_function_manager state = global_state.mstate index, value = state.stack.pop(), state.stack.pop() + """ + if index not in global_state.environment.active_account.storage.keys(): + for key in global_state.environment.active_account.storage.keys(): + if not isinstance(index, BitVecFunc) or not isinstance(key, BitVecFunc): + global_state.mstate.constraints.append(Bool(key.raw != index.raw)) + continue + key_map = Extract(255, 0, key.input_) + index_map = Extract(255, 0, index.input_) + if simplify(key_map == index_map): + continue + global_state.mstate.constraints.append(key != index) + """ log.debug("Write to storage[" + str(index) + "]") - - try: - index = util.get_concrete_int(index) - return self._sstore_helper(global_state, index, value) - except TypeError: - is_keccak = keccak_function_manager.is_keccak(index) - if not is_keccak: - return self._sstore_helper(global_state, str(index), value) - - storage_keys = global_state.environment.active_account.storage.keys() - keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys) - - results = [] # type: List[GlobalState] - new = symbol_factory.Bool(False) - - for keccak_key in keccak_keys: - key_argument = keccak_function_manager.get_argument( - keccak_key - ) # type: Expression - index_argument = keccak_function_manager.get_argument( - index - ) # type: Expression - condition = key_argument == index_argument - condition = ( - condition - if type(condition) == bool - else is_true(simplify(cast(Bool, condition))) - ) - if condition: - return self._sstore_helper( - copy(global_state), - keccak_key, - value, - key_argument == index_argument, - ) - - results += self._sstore_helper( - copy(global_state), - keccak_key, - value, - key_argument == index_argument, - ) - - new = Or(new, cast(Bool, key_argument != index_argument)) - - if len(results) > 0: - results += self._sstore_helper( - copy(global_state), str(index), value, new - ) - return results - - return self._sstore_helper(global_state, str(index), value) + global_state.environment.active_account.storage[index] = value + return [global_state] @staticmethod def _sstore_helper(global_state, index, value, constraint=None): diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index c85726d5..2ca1bf8b 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -3,11 +3,10 @@ This includes classes representing accounts and their storage. """ from copy import deepcopy, copy -from typing import Any, Dict, KeysView, Union +from typing import Any, Dict, Union -from z3 import ExprRef -from mythril.laser.smt import Array, symbol_factory, BitVec +from mythril.laser.smt import Array, K, BitVec, simplify, BitVecFunc, Extract from mythril.disassembler.disassembly import Disassembly from mythril.laser.smt import symbol_factory @@ -15,66 +14,74 @@ from mythril.laser.smt import symbol_factory class Storage: """Storage class represents the storage of an Account.""" - def __init__(self, concrete=False, address=None, dynamic_loader=None) -> None: + def __init__( + self, concrete=False, address=None, dynamic_loader=None, keys=None + ) -> None: """Constructor for Storage. :param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic """ - self._storage = {} # type: Dict[Union[int, str], Any] - self.concrete = concrete + if concrete: + self._standard_storage = K(256, 256, 0) + self._map_storage = {} + else: + self._standard_storage = Array("Storage", 256, 256) + self._map_storage = {} + + self._keys = keys or set() self.dynld = dynamic_loader self.address = address def __getitem__(self, item: Union[str, int]) -> Any: - try: - return self._storage[item] - except KeyError: - if ( - self.address - and self.address.value != 0 - and (self.dynld and self.dynld.storage_loading) - ): - try: - self._storage[item] = symbol_factory.BitVecVal( - int( - self.dynld.read_storage( - contract_address=self.address, index=int(item) - ), - 16, - ), - 256, - ) - return self._storage[item] - except ValueError: - pass - - if self.concrete: - return symbol_factory.BitVecVal(0, 256) - - self._storage[item] = symbol_factory.BitVecSym( - "storage_{}_{}".format(str(item), str(self.address)), 256 - ) - return self._storage[item] - - def __setitem__(self, key: Union[int, str], value: Any) -> None: - self._storage[key] = value - - def keys(self) -> KeysView: - """ + self._keys.add(item) + storage = self._get_corresponding_storage(item) + return simplify(storage[item]) + + @staticmethod + def get_map_index(key): + if not isinstance(key, BitVecFunc) or key.func_name != "keccak256": + return None + index = Extract(255, 0, key.input_) + print(simplify(index), key.input_) + return simplify(index) + + def _get_corresponding_storage(self, key): + index = self.get_map_index(key) + if index is None: + storage = self._standard_storage + else: + try: + storage = self._map_storage[index] + except KeyError: + if isinstance(self._standard_storage, Array): + self._map_storage[index] = Array("Storage", 256, 256) + else: + self._map_storage[index] = K(256, 256, 0) + storage = self._map_storage[index] + return storage - :return: - """ - return self._storage.keys() + def __setitem__(self, key, value: Any) -> None: + self._keys.add(key) + storage = self._get_corresponding_storage(key) + storage[key] = value def __deepcopy__(self, memodict={}): + concrete = isinstance(self._standard_storage, K) storage = Storage( - concrete=self.concrete, address=self.address, dynamic_loader=self.dynld + concrete=concrete, + address=self.address, + dynamic_loader=self.dynld, + keys=deepcopy(self._keys), ) - storage._storage = copy(self._storage) + storage._standard_storage = deepcopy(self._standard_storage) + storage._map_storage = deepcopy(self._map_storage) return storage def __str__(self): - return str(self._storage) + return str(self._standard_storage) + + def keys(self): + return self._keys class Account: @@ -158,13 +165,13 @@ class Account: "storage": self.storage, } - def __deepcopy__(self, memodict={}): + def __copy__(self, memodict={}): new_account = Account( address=self.address, code=self.code, contract_name=self.contract_name, balances=self._balances, ) - new_account.storage = deepcopy(self.storage) + new_account.storage = copy(self.storage) new_account.code = self.code return new_account diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 15e9c43f..73b33516 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -1,7 +1,7 @@ """This module contains the class used to represent state-change constraints in the call graph.""" -from mythril.laser.smt import Solver, Bool, symbol_factory +from mythril.laser.smt import Solver, Bool, symbol_factory, simplify from typing import Iterable, List, Optional, Union from z3 import unsat @@ -54,7 +54,9 @@ class Constraints(list): :param constraint: The constraint to be appended """ - constraint = constraint if isinstance(constraint, Bool) else Bool(constraint) + constraint = ( + simplify(constraint) if isinstance(constraint, Bool) else Bool(constraint) + ) super(Constraints, self).append(constraint) self._is_possible = None diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index e6a13cd3..86364a69 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -61,6 +61,7 @@ class GlobalState: environment = copy(self.environment) mstate = deepcopy(self.mstate) transaction_stack = copy(self.transaction_stack) + environment.active_account = world_state[environment.active_account.address] return GlobalState( world_state, environment, diff --git a/mythril/laser/smt/array.py b/mythril/laser/smt/array.py index c2d658d2..00107df1 100644 --- a/mythril/laser/smt/array.py +++ b/mythril/laser/smt/array.py @@ -8,7 +8,8 @@ default values over a certain range. from typing import cast import z3 -from mythril.laser.smt.bitvec import BitVec +from mythril.laser.smt.bitvec import BitVec, If +from mythril.laser.smt.bool import Bool class BaseArray: @@ -24,6 +25,9 @@ class BaseArray: def __setitem__(self, key: BitVec, value: BitVec) -> None: """Sets an item in the array, key can be symbolic.""" + if isinstance(value, Bool): + value = If(value, 1, 0) + self.raw = z3.Store(self.raw, key.raw, value.raw) # type: ignore diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index f73ef504..cbf60d69 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -205,7 +205,7 @@ class BitVecFunc(BitVec): :return: The resulting Bool """ return _comparison_helper( - self, other, operator.eq, default_value=True, inputs_equal=False + self, other, operator.ne, default_value=True, inputs_equal=False ) def __lshift__(self, other: Union[int, "BitVec"]) -> "BitVec": @@ -223,3 +223,6 @@ class BitVecFunc(BitVec): :return The resulting right shifted output: """ return _arithmetic_helper(self, other, operator.rshift) + + def __hash__(self) -> int: + return self.raw.__hash__() diff --git a/mythril/laser/smt/bool.py b/mythril/laser/smt/bool.py index 1dd1cc76..1859ab43 100644 --- a/mythril/laser/smt/bool.py +++ b/mythril/laser/smt/bool.py @@ -80,6 +80,9 @@ class Bool(Expression[z3.BoolRef]): else: return False + def __hash__(self) -> int: + return self.raw.__hash__() + def And(*args: Union[Bool, bool]) -> Bool: """Create an And expression.""" @@ -90,6 +93,13 @@ def And(*args: Union[Bool, bool]) -> Bool: return Bool(z3.And([a.raw for a in args_list]), union) +def Xor(a: Bool, b: Bool) -> Bool: + """Create an And expression.""" + + union = a.annotations + b.annotations + return Bool(z3.Xor(a.raw, b.raw), union) + + def Or(*args: Union[Bool, bool]) -> Bool: """Create an or expression. diff --git a/mythril/laser/smt/expression.py b/mythril/laser/smt/expression.py index 8e9e697e..ae98cd31 100644 --- a/mythril/laser/smt/expression.py +++ b/mythril/laser/smt/expression.py @@ -45,6 +45,12 @@ class Expression(Generic[T]): def __repr__(self) -> str: return repr(self.raw) + def size(self): + return self.raw.size() + + def __hash__(self) -> int: + return self.raw.__hash__() + G = TypeVar("G", bound=Expression) diff --git a/tests/instructions/codecopy_test.py b/tests/instructions/codecopy_test.py index 9d63efa8..8843199f 100644 --- a/tests/instructions/codecopy_test.py +++ b/tests/instructions/codecopy_test.py @@ -10,9 +10,13 @@ from mythril.laser.ethereum.transaction.transaction_models import MessageCallTra def test_codecopy_concrete(): # Arrange - active_account = Account("0x0", code=Disassembly("60606040")) - environment = Environment(active_account, None, None, None, None, None) - og_state = GlobalState(None, environment, None, MachineState(gas_limit=8000000)) + world_state = WorldState() + account = world_state.create_account(balance=10, address=101) + account.code = Disassembly("60606040") + environment = Environment(account, None, None, None, None, None) + og_state = GlobalState( + world_state, environment, None, MachineState(gas_limit=8000000) + ) og_state.transaction_stack.append( (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) ) diff --git a/tests/instructions/sar_test.py b/tests/instructions/sar_test.py index b618582f..3a23da13 100644 --- a/tests/instructions/sar_test.py +++ b/tests/instructions/sar_test.py @@ -2,6 +2,7 @@ import pytest from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.machine_state import MachineState from mythril.laser.ethereum.state.global_state import GlobalState @@ -12,9 +13,11 @@ from mythril.laser.smt import symbol_factory, simplify def get_state(): - active_account = Account("0x0", code=Disassembly("60606040")) - environment = Environment(active_account, None, None, None, None, None) - state = GlobalState(None, environment, None, MachineState(gas_limit=8000000)) + world_state = WorldState() + account = world_state.create_account(balance=10, address=101) + account.code = Disassembly("60606040") + environment = Environment(account, None, None, None, None, None) + state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000)) state.transaction_stack.append( (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) ) diff --git a/tests/instructions/shl_test.py b/tests/instructions/shl_test.py index 0e36c088..fb1680a5 100644 --- a/tests/instructions/shl_test.py +++ b/tests/instructions/shl_test.py @@ -12,9 +12,11 @@ from mythril.laser.smt import symbol_factory, simplify def get_state(): - active_account = Account("0x0", code=Disassembly("60606040")) - environment = Environment(active_account, None, None, None, None, None) - state = GlobalState(None, environment, None, MachineState(gas_limit=8000000)) + world_state = WorldState() + account = world_state.create_account(balance=10, address=101) + account.code = Disassembly("60606040") + environment = Environment(account, None, None, None, None, None) + state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000)) state.transaction_stack.append( (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) ) diff --git a/tests/instructions/shr_test.py b/tests/instructions/shr_test.py index aaf370e2..f0f66787 100644 --- a/tests/instructions/shr_test.py +++ b/tests/instructions/shr_test.py @@ -12,9 +12,11 @@ from mythril.laser.smt import symbol_factory, simplify, LShR def get_state(): - active_account = Account("0x0", code=Disassembly("60606040")) - environment = Environment(active_account, None, None, None, None, None) - state = GlobalState(None, environment, None, MachineState(gas_limit=8000000)) + world_state = WorldState() + account = world_state.create_account(balance=10, address=101) + account.code = Disassembly("60606040") + environment = Environment(account, None, None, None, None, None) + state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000)) state.transaction_stack.append( (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) ) diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 381438cb..244b5844 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -125,7 +125,8 @@ def test_vmtest( account.code = Disassembly(details["code"][2:]) account.nonce = int(details["nonce"], 16) for key, value in details["storage"].items(): - account.storage[int(key, 16)] = int(value, 16) + key_bitvec = symbol_factory.BitVecVal(int(key, 16), 256) + account.storage[key_bitvec] = symbol_factory.BitVecVal(int(value, 16), 256) world_state.put_account(account) account.set_balance(int(details["balance"], 16)) @@ -175,8 +176,7 @@ def test_vmtest( for index, value in details["storage"].items(): expected = int(value, 16) - actual = account.storage[int(index, 16)] - + actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)] if isinstance(actual, Expression): actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual diff --git a/tests/laser/state/storage_test.py b/tests/laser/state/storage_test.py deleted file mode 100644 index 35e31df3..00000000 --- a/tests/laser/state/storage_test.py +++ /dev/null @@ -1,53 +0,0 @@ -import pytest -from mythril.laser.ethereum.state.account import Storage -from mythril.laser.smt import Expression - -storage_uninitialized_test_data = [({}, 1), ({1: 5}, 2), ({1: 5, 3: 10}, 2)] - - -@pytest.mark.parametrize("initial_storage,key", storage_uninitialized_test_data) -def test_concrete_storage_uninitialized_index(initial_storage, key): - # Arrange - storage = Storage(concrete=True) - storage._storage = initial_storage - - # Act - value = storage[key] - - # Assert - assert value == 0 - - -@pytest.mark.parametrize("initial_storage,key", storage_uninitialized_test_data) -def test_symbolic_storage_uninitialized_index(initial_storage, key): - # Arrange - storage = Storage(concrete=False) - storage._storage = initial_storage - - # Act - value = storage[key] - - # Assert - assert isinstance(value, Expression) - - -def test_storage_set_item(): - # Arrange - storage = Storage() - - # Act - storage[1] = 13 - - # Assert - assert storage[1] == 13 - - -def test_storage_change_item(): - # Arrange - storage = Storage() - storage._storage = {1: 12} - # Act - storage[1] = 14 - - # Assert - assert storage[1] == 14 diff --git a/tests/testdata/outputs_expected/metacoin.sol.o.json b/tests/testdata/outputs_expected/metacoin.sol.o.json index 712f50c1..c95b9c75 100644 --- a/tests/testdata/outputs_expected/metacoin.sol.o.json +++ b/tests/testdata/outputs_expected/metacoin.sol.o.json @@ -1,5 +1,19 @@ { "error": null, - "issues": [], + "issues": [ + { + "address": 498, + "contract": "Unknown", + "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.", + "function": "sendToken(address,uint256)", + "max_gas_used": 52806, + "min_gas_used": 11860, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Overflow", + "tx_sequence": "" + } + ], "success": true } \ No newline at end of file diff --git a/tests/testdata/outputs_expected/metacoin.sol.o.jsonv2 b/tests/testdata/outputs_expected/metacoin.sol.o.jsonv2 index 40de69b4..8a565326 100644 --- a/tests/testdata/outputs_expected/metacoin.sol.o.jsonv2 +++ b/tests/testdata/outputs_expected/metacoin.sol.o.jsonv2 @@ -1,6 +1,25 @@ [ { - "issues": [], + "issues": [ + { + "description": { + "head": "The binary addition can overflow.", + "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion." + }, + "extra": { + "discoveryTime": "", + "testCase": "" + }, + "locations": [ + { + "sourceMap": "498:1:0" + } + ], + "severity": "High", + "swcID": "SWC-101", + "swcTitle": "Integer Overflow and Underflow" + } + ], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": [ diff --git a/tests/testdata/outputs_expected/metacoin.sol.o.markdown b/tests/testdata/outputs_expected/metacoin.sol.o.markdown index 321484fd..1eb30c6a 100644 --- a/tests/testdata/outputs_expected/metacoin.sol.o.markdown +++ b/tests/testdata/outputs_expected/metacoin.sol.o.markdown @@ -1,3 +1,14 @@ -# Analysis results for None +# Analysis results for test-filename.sol -The analysis was completed successfully. No issues were detected. +## Integer Overflow +- SWC ID: 101 +- Severity: High +- Contract: Unknown +- Function name: `sendToken(address,uint256)` +- PC address: 498 +- Estimated Gas Usage: 11860 - 52806 + +### Description + +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. diff --git a/tests/testdata/outputs_expected/metacoin.sol.o.text b/tests/testdata/outputs_expected/metacoin.sol.o.text index 729320d8..412039a2 100644 --- a/tests/testdata/outputs_expected/metacoin.sol.o.text +++ b/tests/testdata/outputs_expected/metacoin.sol.o.text @@ -1 +1,11 @@ -The analysis was completed successfully. No issues were detected. +==== Integer Overflow ==== +SWC ID: 101 +Severity: High +Contract: Unknown +Function name: sendToken(address,uint256) +PC address: 498 +Estimated Gas Usage: 11860 - 52806 +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. +-------------------- +