From b3bf6fbcde2b5749f946c16d0a113263bdfbd733 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 14 Jun 2019 10:55:18 +0530 Subject: [PATCH 1/2] Fix Storage and calldata --- mythril/laser/ethereum/instructions.py | 70 +++++++++++-------- mythril/laser/ethereum/state/account.py | 16 ++++- tests/laser/evm_testsuite/evm_test.py | 4 +- tests/laser/state/storage_test.py | 12 ++-- .../metacoin.sol.o.graph.html | 6 +- .../outputs_expected/metacoin.sol.o.json | 16 ++++- .../outputs_expected/metacoin.sol.o.jsonv2 | 20 +++++- .../outputs_expected/metacoin.sol.o.markdown | 15 +++- .../outputs_expected/metacoin.sol.o.text | 12 +++- 9 files changed, 124 insertions(+), 47 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index e1903c42..8ab3b5a3 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -768,18 +768,10 @@ class Instruction: size_sym = True if size_sym: - state.mem_extend(mstart, 1) - state.memory[mstart] = global_state.new_bitvec( - "calldata_" - + str(environment.active_account.contract_name) - + "[" - + str(dstart) - + ": + " - + str(size) - + "]", - 8, - ) - return [global_state] + size = ( + 320 + ) # This excess stuff will get overwritten as memory is dynamically sized + size = cast(int, size) if size > 0: try: @@ -1389,7 +1381,15 @@ class Instruction: 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)) + keys = filter(keccak_function_manager.is_keccak, storage_keys) + addr = global_state.get_current_instruction()["address"] + keccak_keys = [ + key + for key in keys + if global_state.environment.active_account.storage.potential_func( + key, addr + ) + ] results = [] # type: List[GlobalState] constraints = [] @@ -1427,11 +1427,16 @@ class Instruction: :param constraints: :return: """ + address = global_state.get_current_instruction()["address"] try: - data = global_state.environment.active_account.storage[index] + data = global_state.environment.active_account.storage.get( + index, addr=address + ) except KeyError: data = global_state.new_bitvec("storage_" + str(index), 256) - global_state.environment.active_account.storage[index] = data + global_state.environment.active_account.storage.put( + key=index, value=data, addr=address + ) if constraints is not None: global_state.mstate.constraints += constraints @@ -1475,7 +1480,15 @@ class Instruction: 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) + keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys)) + addr = global_state.get_current_instruction()["address"] + keccak_keys = [ + key + for key in keccak_keys + if global_state.environment.active_account.storage.potential_func( + key, addr + ) + ] results = [] # type: List[GlobalState] new = symbol_factory.Bool(False) @@ -1528,19 +1541,18 @@ class Instruction: :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") + 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 + address = global_state.get_current_instruction()["address"] + global_state.environment.active_account.storage.put( + key=index, + value=value if not isinstance(value, Expression) else simplify(value), + addr=address, + ) if constraint is not None: global_state.mstate.constraints.append(constraint) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index e806a71e..93b03831 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -24,8 +24,12 @@ class Storage: self.concrete = concrete self.dynld = dynamic_loader self.address = address + self._storage_opcodes = {} # type: Dict - def __getitem__(self, item: Union[str, int]) -> Any: + def get(self, item: Union[str, int], addr: int) -> Any: + if item not in self._storage_opcodes: + self._storage_opcodes[item] = set() + self._storage_opcodes[item].add(addr) try: return self._storage[item] except KeyError: @@ -56,9 +60,17 @@ class Storage: ) return self._storage[item] - def __setitem__(self, key: Union[int, str], value: Any) -> None: + def put(self, key: Union[int, str], value: Any, addr) -> None: + if key not in self._storage_opcodes: + self._storage_opcodes[key] = set() + self._storage_opcodes[key].add(addr) self._storage[key] = value + def potential_func(self, key, opcode) -> bool: + if key not in self._storage_opcodes: + return False + return opcode in self._storage_opcodes[key] + def keys(self) -> KeysView: """ diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 381438cb..93e927ed 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -125,7 +125,7 @@ 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) + account.storage.put(int(key, 16), int(value, 16), 10) world_state.put_account(account) account.set_balance(int(details["balance"], 16)) @@ -175,7 +175,7 @@ def test_vmtest( for index, value in details["storage"].items(): expected = int(value, 16) - actual = account.storage[int(index, 16)] + actual = account.storage.get(int(index, 16), 0) if isinstance(actual, Expression): actual = actual.value diff --git a/tests/laser/state/storage_test.py b/tests/laser/state/storage_test.py index 35e31df3..5fa6078f 100644 --- a/tests/laser/state/storage_test.py +++ b/tests/laser/state/storage_test.py @@ -12,7 +12,7 @@ def test_concrete_storage_uninitialized_index(initial_storage, key): storage._storage = initial_storage # Act - value = storage[key] + value = storage.get(key, 0) # Assert assert value == 0 @@ -25,7 +25,7 @@ def test_symbolic_storage_uninitialized_index(initial_storage, key): storage._storage = initial_storage # Act - value = storage[key] + value = storage.get(key, 0) # Assert assert isinstance(value, Expression) @@ -36,10 +36,10 @@ def test_storage_set_item(): storage = Storage() # Act - storage[1] = 13 + storage.put(key=1, value=13, addr=10) # Assert - assert storage[1] == 13 + assert storage.put(key=1, value=13, addr=10) def test_storage_change_item(): @@ -47,7 +47,7 @@ def test_storage_change_item(): storage = Storage() storage._storage = {1: 12} # Act - storage[1] = 14 + storage.put(key=1, value=14, addr=10) # Assert - assert storage[1] == 14 + assert storage.get(item=1, addr=10) == 14 diff --git a/tests/testdata/outputs_expected/metacoin.sol.o.graph.html b/tests/testdata/outputs_expected/metacoin.sol.o.graph.html index 6ee81b9c..64169495 100644 --- a/tests/testdata/outputs_expected/metacoin.sol.o.graph.html +++ b/tests/testdata/outputs_expected/metacoin.sol.o.graph.html @@ -24,8 +24,8 @@ @@ -59,4 +59,4 @@ }); - + \ No newline at end of file diff --git a/tests/testdata/outputs_expected/metacoin.sol.o.json b/tests/testdata/outputs_expected/metacoin.sol.o.json index 712f50c1..2dd384d1 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", + "debug": "", + "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" + } + ], "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..9c96d9d3 100644 --- a/tests/testdata/outputs_expected/metacoin.sol.o.jsonv2 +++ b/tests/testdata/outputs_expected/metacoin.sol.o.jsonv2 @@ -1,6 +1,24 @@ [ { - "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": "" + }, + "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 bedbc7d287c1b2dd686d1884935f28569ca79764 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 14 Jun 2019 11:57:41 +0530 Subject: [PATCH 2/2] Fix storage tests --- tests/laser/state/storage_test.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/laser/state/storage_test.py b/tests/laser/state/storage_test.py index 5fa6078f..a0da2c94 100644 --- a/tests/laser/state/storage_test.py +++ b/tests/laser/state/storage_test.py @@ -39,7 +39,7 @@ def test_storage_set_item(): storage.put(key=1, value=13, addr=10) # Assert - assert storage.put(key=1, value=13, addr=10) + assert storage.get(item=1, addr=10) == 13 def test_storage_change_item():