From dd7b255fc97b53dfc7504759e79719d97e7122b9 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 21 Jun 2019 22:26:46 +0530 Subject: [PATCH 01/11] Fix storage --- mythril/laser/ethereum/instructions.py | 118 +++++------------- mythril/laser/ethereum/state/account.py | 105 ++++++++-------- mythril/laser/ethereum/state/constraints.py | 6 +- mythril/laser/ethereum/state/global_state.py | 1 + mythril/laser/smt/array.py | 6 +- mythril/laser/smt/bitvecfunc.py | 5 +- mythril/laser/smt/bool.py | 10 ++ mythril/laser/smt/expression.py | 6 + tests/instructions/codecopy_test.py | 10 +- tests/instructions/sar_test.py | 9 +- tests/instructions/shl_test.py | 8 +- tests/instructions/shr_test.py | 8 +- tests/laser/evm_testsuite/evm_test.py | 6 +- tests/laser/state/storage_test.py | 53 -------- .../outputs_expected/metacoin.sol.o.json | 16 ++- .../outputs_expected/metacoin.sol.o.jsonv2 | 21 +++- .../outputs_expected/metacoin.sol.o.markdown | 15 ++- .../outputs_expected/metacoin.sol.o.text | 12 +- 18 files changed, 201 insertions(+), 214 deletions(-) delete mode 100644 tests/laser/state/storage_test.py 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. +-------------------- + From efd7c95f86bcc4e0e763414537ec0bb801bf8da9 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 25 Jun 2019 17:31:58 +0530 Subject: [PATCH 02/11] Use different SMT array for each map --- mythril/analysis/modules/integer.py | 3 - mythril/analysis/solver.py | 2 +- mythril/laser/ethereum/instructions.py | 104 +----------------------- mythril/laser/ethereum/keccak.py | 38 --------- mythril/laser/ethereum/state/account.py | 20 +---- 5 files changed, 6 insertions(+), 161 deletions(-) delete mode 100644 mythril/laser/ethereum/keccak.py diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index cbaf144d..b2e58ca8 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -230,7 +230,6 @@ class IntegerOverflowUnderflowModule(DetectionModule): or annotation.overflowing_state in state_annotation.ostates_seen ): continue - state_annotation.overflowing_state_annotations.append(annotation) state_annotation.ostates_seen.add(annotation.overflowing_state) @@ -248,7 +247,6 @@ class IntegerOverflowUnderflowModule(DetectionModule): or annotation.overflowing_state in state_annotation.ostates_seen ): continue - state_annotation.overflowing_state_annotations.append(annotation) state_annotation.ostates_seen.add(annotation.overflowing_state) @@ -311,7 +309,6 @@ class IntegerOverflowUnderflowModule(DetectionModule): try: constraints = state.mstate.constraints + [annotation.constraint] - transaction_sequence = solver.get_transaction_sequence( state, constraints ) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 16a74eae..ed401369 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -28,7 +28,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True :return: """ s = Optimize() - timeout = 100000 + timeout = 200000 if enforce_execution_time: timeout = min(timeout, time_handler.time_remaining() - 500) if timeout <= 0: diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 5bb3e10e..0285bdb6 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -18,15 +18,11 @@ from mythril.laser.smt import ( ULT, UGT, BitVec, - is_true, - Bool, - BitVecFunc, is_false, URem, SRem, If, Bool, - Or, Not, LShR, ) @@ -43,7 +39,6 @@ from mythril.laser.ethereum.evm_exceptions import ( OutOfGasException, ) from mythril.laser.ethereum.gas import OPCODE_GAS -from mythril.laser.ethereum.keccak import KeccakFunctionManager from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction import ( MessageCallTransaction, @@ -58,8 +53,6 @@ log = logging.getLogger(__name__) TT256 = 2 ** 256 TT256M1 = 2 ** 256 - 1 -keccak_function_manager = KeccakFunctionManager() - class StateTransition(object): """Decorator that handles global state copy and original return. @@ -195,7 +188,6 @@ class Instruction: if not post else getattr(self, op + "_" + "post", None) ) - if instruction_mutator is None: raise NotImplementedError @@ -419,6 +411,7 @@ class Instruction: * helper.pop_bitvec(global_state.mstate) ) ) + return [global_state] @StateTransition() @@ -895,7 +888,6 @@ class Instruction: :param global_state: :return: """ - global keccak_function_manager state = global_state.mstate op0, op1 = state.stack.pop(), state.stack.pop() @@ -950,7 +942,6 @@ class Instruction: ) log.debug("Created BitVecFunc hash.") - keccak_function_manager.add_keccak(result, state.memory[index]) else: keccak = utils.sha3(data.value.to_bytes(length, byteorder="big")) result = symbol_factory.BitVecFuncVal( @@ -1366,64 +1357,13 @@ class Instruction: :param global_state: :return: """ - global keccak_function_manager state = global_state.mstate index = state.stack.pop() log.debug("Storage access at index " + 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( - global_state: GlobalState, index: Union[str, int], constraints=None - ): - """ - - :param global_state: - :param index: - :param constraints: - :return: - """ - try: - data = global_state.environment.active_account.storage[index] - except KeyError: - data = global_state.new_bitvec("storage_" + str(index), 256) - global_state.environment.active_account.storage[index] = data - - if constraints is not None: - global_state.mstate.constraints += constraints - - global_state.mstate.stack.append(data) - return [global_state] - - @staticmethod - def _get_constraints(keccak_keys, this_key, argument): - """ - - :param keccak_keys: - :param this_key: - :param argument: - """ - global keccak_function_manager - for keccak_key in keccak_keys: - if keccak_key == this_key: - continue - keccak_argument = keccak_function_manager.get_argument(keccak_key) - yield keccak_argument != argument - @StateTransition() def sstore_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1431,54 +1371,12 @@ class Instruction: :param global_state: :return: """ - 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) + "]") global_state.environment.active_account.storage[index] = value return [global_state] - @staticmethod - def _sstore_helper(global_state, index, value, constraint=None): - """ - - :param global_state: - :param index: - :param value: - :param constraint: - :return: - """ - try: - global_state.environment.active_account = deepcopy( - global_state.environment.active_account - ) - global_state.accounts[ - global_state.environment.active_account.address.value - ] = global_state.environment.active_account - - global_state.environment.active_account.storage[index] = ( - value if not isinstance(value, Expression) else simplify(value) - ) - except KeyError: - log.debug("Error writing to storage: Invalid index") - - if constraint is not None: - global_state.mstate.constraints.append(constraint) - - return [global_state] - @StateTransition(increment_pc=False, enable_gas=False) def jump_(self, global_state: GlobalState) -> List[GlobalState]: """ diff --git a/mythril/laser/ethereum/keccak.py b/mythril/laser/ethereum/keccak.py deleted file mode 100644 index 47a39ed1..00000000 --- a/mythril/laser/ethereum/keccak.py +++ /dev/null @@ -1,38 +0,0 @@ -"""This module contains a function manager to deal with symbolic Keccak -values.""" -from mythril.laser.smt import Expression - - -class KeccakFunctionManager: - """A keccak function manager for symbolic expressions.""" - - def __init__(self): - """""" - self.keccak_expression_mapping = {} - - def is_keccak(self, expression: Expression) -> bool: - """ - - :param expression: - :return: - """ - return str(expression) in self.keccak_expression_mapping.keys() - - def get_argument(self, expression: Expression) -> Expression: - """ - - :param expression: - :return: - """ - if not self.is_keccak(expression): - raise ValueError("Expression is not a recognized keccac result") - return self.keccak_expression_mapping[str(expression)][1] - - def add_keccak(self, expression: Expression, argument: Expression) -> None: - """ - - :param expression: - :param argument: - """ - index = str(expression) - self.keccak_expression_mapping[index] = (expression, argument) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 2ca1bf8b..327fcc82 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -2,7 +2,7 @@ This includes classes representing accounts and their storage. """ -from copy import deepcopy, copy +from copy import deepcopy from typing import Any, Dict, Union @@ -14,9 +14,7 @@ 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, keys=None - ) -> None: + def __init__(self, concrete=False, address=None, dynamic_loader=None) -> None: """Constructor for Storage. :param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic @@ -28,12 +26,10 @@ class Storage: 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: - self._keys.add(item) storage = self._get_corresponding_storage(item) return simplify(storage[item]) @@ -42,7 +38,6 @@ class Storage: 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): @@ -61,17 +56,13 @@ class Storage: return storage 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=concrete, - address=self.address, - dynamic_loader=self.dynld, - keys=deepcopy(self._keys), + concrete=concrete, address=self.address, dynamic_loader=self.dynld ) storage._standard_storage = deepcopy(self._standard_storage) storage._map_storage = deepcopy(self._map_storage) @@ -80,9 +71,6 @@ class Storage: def __str__(self): return str(self._standard_storage) - def keys(self): - return self._keys - class Account: """Account class representing ethereum accounts.""" @@ -172,6 +160,6 @@ class Account: contract_name=self.contract_name, balances=self._balances, ) - new_account.storage = copy(self.storage) + new_account.storage = deepcopy(self.storage) new_account.code = self.code return new_account From edb906d391b8b84d21ecb0b70afeb6dadd3ebd94 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 25 Jun 2019 17:38:16 +0530 Subject: [PATCH 03/11] revert the timeout to normal --- mythril/analysis/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index ed401369..16a74eae 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -28,7 +28,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True :return: """ s = Optimize() - timeout = 200000 + timeout = 100000 if enforce_execution_time: timeout = min(timeout, time_handler.time_remaining() - 500) if timeout <= 0: From ecac6e8b77099bdcf8dd2f7b49dfabf5fe4e42fb Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 25 Jun 2019 17:54:13 +0530 Subject: [PATCH 04/11] Fix type hints --- mythril/laser/ethereum/state/account.py | 20 ++++++++++++-------- mythril/laser/smt/__init__.py | 8 ++++---- mythril/laser/smt/bitvecfunc.py | 2 +- 3 files changed, 17 insertions(+), 13 deletions(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 327fcc82..9ec82f05 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -6,7 +6,7 @@ from copy import deepcopy from typing import Any, Dict, Union -from mythril.laser.smt import Array, K, BitVec, simplify, BitVecFunc, Extract +from mythril.laser.smt import Array, K, BitVec, simplify, BitVecFunc, Extract, BaseArray from mythril.disassembler.disassembly import Disassembly from mythril.laser.smt import symbol_factory @@ -20,8 +20,8 @@ class Storage: :param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic """ if concrete: - self._standard_storage = K(256, 256, 0) - self._map_storage = {} + self._standard_storage = K(256, 256, 0) # type: BaseArray + self._map_storage = {} # type: Dict[BitVec, BaseArray] else: self._standard_storage = Array("Storage", 256, 256) self._map_storage = {} @@ -29,18 +29,22 @@ class Storage: self.dynld = dynamic_loader self.address = address - def __getitem__(self, item: Union[str, int]) -> Any: + def __getitem__(self, item: BitVec) -> Any: 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": + def get_map_index(key: BitVec) -> BitVec: + if ( + not isinstance(key, BitVecFunc) + or key.func_name != "keccak256" + or key.input_ is None + ): return None index = Extract(255, 0, key.input_) return simplify(index) - def _get_corresponding_storage(self, key): + def _get_corresponding_storage(self, key: BitVec) -> BaseArray: index = self.get_map_index(key) if index is None: storage = self._standard_storage @@ -68,7 +72,7 @@ class Storage: storage._map_storage = deepcopy(self._map_storage) return storage - def __str__(self): + def __str__(self) -> str: return str(self._standard_storage) diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index d849d0c4..5a3f1ca1 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -72,7 +72,7 @@ class SymbolFactory(Generic[T, U]): func_name: str, size: int, annotations: Annotations = None, - input_: Union[int, "BitVec"] = None, + input_: "BitVec" = None, ) -> BitVecFunc: """Creates a new bit vector function with a symbolic value. @@ -91,7 +91,7 @@ class SymbolFactory(Generic[T, U]): func_name: str, size: int, annotations: Annotations = None, - input_: Union[int, "BitVec"] = None, + input_: "BitVec" = None, ) -> BitVecFunc: """Creates a new bit vector function with a symbolic value. @@ -140,7 +140,7 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]): func_name: str, size: int, annotations: Annotations = None, - input_: Union[int, "BitVec"] = None, + input_: "BitVec" = None, ) -> BitVecFunc: """Creates a new bit vector function with a concrete value.""" raw = z3.BitVecVal(value, size) @@ -152,7 +152,7 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]): func_name: str, size: int, annotations: Annotations = None, - input_: Union[int, "BitVec"] = None, + input_: "BitVec" = None, ) -> BitVecFunc: """Creates a new bit vector function with a symbolic value.""" raw = z3.BitVec(name, size) diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index cbf60d69..257d2b46 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -79,7 +79,7 @@ class BitVecFunc(BitVec): self, raw: z3.BitVecRef, func_name: Optional[str], - input_: Union[int, "BitVec"] = None, + input_: "BitVec" = None, annotations: Optional[Annotations] = None, ): """ From 7f2a598f70ac45af00395faa64e91e51de0cab47 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 25 Jun 2019 18:09:57 +0530 Subject: [PATCH 05/11] Update storage tests --- tests/laser/state/storage_test.py | 58 +++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 tests/laser/state/storage_test.py diff --git a/tests/laser/state/storage_test.py b/tests/laser/state/storage_test.py new file mode 100644 index 00000000..2e8aa4f9 --- /dev/null +++ b/tests/laser/state/storage_test.py @@ -0,0 +1,58 @@ +import pytest +from mythril.laser.smt import symbol_factory +from mythril.laser.ethereum.state.account import Storage +from mythril.laser.smt import Expression + +BVV = symbol_factory.BitVecVal + +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) + for k, val in initial_storage.items(): + storage[BVV(k, 256)] = BVV(val, 256) + + # Act + value = storage[BVV(key, 256)] + + # 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) + for k, val in initial_storage.items(): + storage[BVV(k, 256)] = BVV(val, 256) + + # Act + value = storage[BVV(key, 256)] + + # Assert + assert isinstance(value, Expression) + + +def test_storage_set_item(): + # Arrange + storage = Storage() + + # Act + storage[BVV(1, 256)] = BVV(13, 256) + + # Assert + assert storage[BVV(1, 256)] == BVV(13, 256) + + +def test_storage_change_item(): + # Arrange + storage = Storage() + storage[BVV(1, 256)] = BVV(12, 256) + # Act + storage[BVV(1, 256)] = BVV(14, 256) + + # Assert + assert storage[BVV(1, 256)] == BVV(14, 256) From 7c0c4d3c7b4efc2f6fabfe06fc78d1b95e6d27d3 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 25 Jun 2019 22:51:18 +0530 Subject: [PATCH 06/11] Fix deepcopy issue --- mythril/laser/ethereum/state/account.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index cfa63c21..696f7016 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -2,7 +2,7 @@ This includes classes representing accounts and their storage. """ -from copy import deepcopy +from copy import copy, deepcopy from typing import Any, Dict, Union @@ -26,6 +26,8 @@ class Storage: self._standard_storage = Array("Storage", 256, 256) self._map_storage = {} + self.print_storage = {} # type: Dict[BitVec, BitVec] + self.dynld = dynamic_loader self.address = address @@ -50,6 +52,7 @@ class Storage: ), 256, ) + self.print_storage[item] = storage[item] return storage[item] except ValueError: pass @@ -84,6 +87,7 @@ class Storage: def __setitem__(self, key, value: Any) -> None: storage = self._get_corresponding_storage(key) + self.print_storage[key] = value storage[key] = value def __deepcopy__(self, memodict={}): @@ -93,10 +97,12 @@ class Storage: ) storage._standard_storage = deepcopy(self._standard_storage) storage._map_storage = deepcopy(self._map_storage) + storage.print_storage = copy(self.print_storage) return storage def __str__(self) -> str: - return str(self._standard_storage) + # TODO: Do something better here + return str(self.print_storage) class Account: From 4f257422b8391609138da6b5f2c30b062e81098e Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 25 Jun 2019 23:00:19 +0530 Subject: [PATCH 07/11] Rename print_storage variable --- mythril/laser/ethereum/state/account.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 696f7016..bd594e8d 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -26,7 +26,7 @@ class Storage: self._standard_storage = Array("Storage", 256, 256) self._map_storage = {} - self.print_storage = {} # type: Dict[BitVec, BitVec] + self.printable_storage = {} # type: Dict[BitVec, BitVec] self.dynld = dynamic_loader self.address = address @@ -52,7 +52,7 @@ class Storage: ), 256, ) - self.print_storage[item] = storage[item] + self.printable_storage[item] = storage[item] return storage[item] except ValueError: pass @@ -87,7 +87,7 @@ class Storage: def __setitem__(self, key, value: Any) -> None: storage = self._get_corresponding_storage(key) - self.print_storage[key] = value + self.printable_storage[key] = value storage[key] = value def __deepcopy__(self, memodict={}): @@ -97,12 +97,12 @@ class Storage: ) storage._standard_storage = deepcopy(self._standard_storage) storage._map_storage = deepcopy(self._map_storage) - storage.print_storage = copy(self.print_storage) + storage.print_storage = copy(self.printable_storage) return storage def __str__(self) -> str: # TODO: Do something better here - return str(self.print_storage) + return str(self.printable_storage) class Account: From 952699010d1b356696b3d50bcd949699792d9d0b Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 26 Jun 2019 20:59:01 +0530 Subject: [PATCH 08/11] Add an extra map --- mythril/laser/ethereum/state/account.py | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index bd594e8d..2b465706 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -21,10 +21,10 @@ class Storage: """ if concrete: self._standard_storage = K(256, 256, 0) # type: BaseArray - self._map_storage = {} # type: Dict[BitVec, BaseArray] else: self._standard_storage = Array("Storage", 256, 256) - self._map_storage = {} + self._map_storage = {} + self._keccak_map_storage = {} # type: Dict[BitVec, BaseArray] self.printable_storage = {} # type: Dict[BitVec, BitVec] @@ -74,9 +74,14 @@ class Storage: index = self.get_map_index(key) if index is None: storage = self._standard_storage + else: + if isinstance(key, BitVecFunc) and key.func_name == "keccak256": + storage_map = self._keccak_map_storage + else: + storage_map = self._map_storage try: - storage = self._map_storage[index] + storage = storage_map[index] except KeyError: if isinstance(self._standard_storage, Array): self._map_storage[index] = Array("Storage", 256, 256) From 01e7c579cf300410541db0f03e98d1acfbfbbcf5 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 26 Jun 2019 21:00:04 +0530 Subject: [PATCH 09/11] Fix type hints --- mythril/laser/ethereum/state/account.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 2b465706..7141a919 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -23,7 +23,7 @@ class Storage: self._standard_storage = K(256, 256, 0) # type: BaseArray else: self._standard_storage = Array("Storage", 256, 256) - self._map_storage = {} + self._map_storage = {} # type: Dict[BitVec, BaseArray] self._keccak_map_storage = {} # type: Dict[BitVec, BaseArray] self.printable_storage = {} # type: Dict[BitVec, BitVec] From 49791f3f2589396bfcadbd93046e2e48ac033193 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 26 Jun 2019 21:04:04 +0530 Subject: [PATCH 10/11] Fix black --- mythril/laser/ethereum/state/account.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 7141a919..f48db48f 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -23,7 +23,7 @@ class Storage: self._standard_storage = K(256, 256, 0) # type: BaseArray else: self._standard_storage = Array("Storage", 256, 256) - self._map_storage = {} # type: Dict[BitVec, BaseArray] + self._map_storage = {} # type: Dict[BitVec, BaseArray] self._keccak_map_storage = {} # type: Dict[BitVec, BaseArray] self.printable_storage = {} # type: Dict[BitVec, BitVec] From 584b7c88b80155b08d01b5e5cfdf133c3b239c53 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Thu, 27 Jun 2019 12:50:34 +0530 Subject: [PATCH 11/11] Use proper keccak inputs for maps --- mythril/laser/ethereum/state/account.py | 55 +++++++++++++++++-------- 1 file changed, 37 insertions(+), 18 deletions(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index f48db48f..d3e6f876 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -3,10 +3,19 @@ This includes classes representing accounts and their storage. """ from copy import copy, deepcopy -from typing import Any, Dict, Union - - -from mythril.laser.smt import Array, K, BitVec, simplify, BitVecFunc, Extract, BaseArray +from typing import Any, Dict, Union, Tuple, cast + + +from mythril.laser.smt import ( + Array, + K, + BitVec, + simplify, + BitVecFunc, + Extract, + BaseArray, + Concat, +) from mythril.disassembler.disassembly import Disassembly from mythril.laser.smt import symbol_factory @@ -24,15 +33,25 @@ class Storage: else: self._standard_storage = Array("Storage", 256, 256) self._map_storage = {} # type: Dict[BitVec, BaseArray] - self._keccak_map_storage = {} # type: Dict[BitVec, BaseArray] self.printable_storage = {} # type: Dict[BitVec, BitVec] self.dynld = dynamic_loader self.address = address - def __getitem__(self, item: BitVec) -> Any: - storage = self._get_corresponding_storage(item) + @staticmethod + def _sanitize(input_: BitVec) -> BitVec: + if input_.size() == 512: + return input_ + if input_.size() > 512: + return Extract(511, 0, input_) + else: + return Concat(symbol_factory.BitVecVal(0, 512 - input_.size()), input_) + + def __getitem__(self, item: BitVec) -> BitVec: + storage, is_keccak_storage = self._get_corresponding_storage(item) + if is_keccak_storage: + item = self._sanitize(cast(BitVecFunc, item).input_) value = storage[item] if ( value.value == 0 @@ -70,29 +89,29 @@ class Storage: index = Extract(255, 0, key.input_) return simplify(index) - def _get_corresponding_storage(self, key: BitVec) -> BaseArray: + def _get_corresponding_storage(self, key: BitVec) -> Tuple[BaseArray, bool]: index = self.get_map_index(key) if index is None: storage = self._standard_storage - + is_keccak_storage = False else: - if isinstance(key, BitVecFunc) and key.func_name == "keccak256": - storage_map = self._keccak_map_storage - else: - storage_map = self._map_storage + storage_map = self._map_storage try: storage = storage_map[index] except KeyError: if isinstance(self._standard_storage, Array): - self._map_storage[index] = Array("Storage", 256, 256) + storage_map[index] = Array("Storage", 512, 256) else: - self._map_storage[index] = K(256, 256, 0) - storage = self._map_storage[index] - return storage + storage_map[index] = K(512, 256, 0) + storage = storage_map[index] + is_keccak_storage = True + return storage, is_keccak_storage def __setitem__(self, key, value: Any) -> None: - storage = self._get_corresponding_storage(key) + storage, is_keccak_storage = self._get_corresponding_storage(key) self.printable_storage[key] = value + if is_keccak_storage: + key = self._sanitize(key.input_) storage[key] = value def __deepcopy__(self, memodict={}):