From 51c6091b7963edc4f77a76972214b9c6ac8c3b2a Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Sun, 5 Jan 2020 00:19:17 +0000 Subject: [PATCH 001/104] Initial commit of connect-to-eth-node. --- manticore/ethereum/manticore.py | 7 +- manticore/platforms/evm.py | 298 ++++++++++------------- manticore/platforms/evm_world_state.py | 314 +++++++++++++++++++++++++ 3 files changed, 437 insertions(+), 182 deletions(-) create mode 100644 manticore/platforms/evm_world_state.py diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 5827d9dbb..478e112d1 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -37,6 +37,7 @@ from .state import State from ..exceptions import EthereumError, DependencyError, NoAliveStates from ..platforms import evm +from ..platforms.evm_world_state import WorldState from ..utils import config, log from ..utils.deprecated import deprecated from ..utils.helpers import PickleSerializer @@ -386,7 +387,9 @@ def contract_accounts(self): def get_account(self, name): return self._accounts[name] - def __init__(self, workspace_url: str = None, policy: str = "random"): + def __init__( + self, world_state: WorldState = None, workspace_url: str = None, policy: str = "random" + ): """ A Manticore EVM manager :param workspace_url: workspace folder name @@ -395,7 +398,7 @@ def __init__(self, workspace_url: str = None, policy: str = "random"): # Make the constraint store constraints = ConstraintSet() # make the ethereum world state - world = evm.EVMWorld(constraints) + world = evm.EVMWorld(constraints, world_state=world_state) initial_state = State(constraints, world) super().__init__(initial_state, workspace_url=workspace_url, policy=policy) self.subscribe("will_terminate_state", self._terminate_state_callback) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 774171fe6..03f788989 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -7,6 +7,7 @@ import inspect from functools import wraps from typing import List, Set, Tuple, Union +from ..platforms.evm_world_state import * from ..platforms.platform import * from ..core.smtlib import ( Z3Solver, @@ -18,6 +19,7 @@ ArrayVariable, ArrayStore, BitVecConstant, + ConstraintSet, translate_to_smtlib, to_constant, simplify, @@ -933,10 +935,18 @@ def _push(self, value): ITEM2 sp-> {empty} """ - assert isinstance(value, int) or isinstance(value, BitVec) and value.size == 256 + assert ( + isinstance(value, bytes) + or isinstance(value, int) + or isinstance(value, BitVec) + and value.size == 256 + ) if len(self.stack) >= 1024: raise StackOverflow() + if isinstance(value, bytes): + value = int.from_bytes(value, "big") + if isinstance(value, int): value = value & TT256M1 @@ -2255,38 +2265,38 @@ class EVMWorld(Platform): def __init__( self, constraints, - storage=None, + world_state: WorldState = None, blocknumber=None, timestamp=None, - difficulty=0, - gaslimit=0, - coinbase=0, + difficulty=None, + gaslimit=None, + coinbase=None, **kwargs, ): super().__init__(path="NOPATH", **kwargs) - self._world_state = {} if storage is None else storage + self._world_state = OverlayWorldState( + world_state if world_state is not None else DefaultWorldState() + ) self._constraints = constraints - self._callstack: List[ - Tuple[Transaction, List[EVMLog], Set[int], Union[bytearray, ArrayProxy], EVM] - ] = [] - self._deleted_accounts: Set[int] = set() + self._callstack: List[Tuple[Transaction, List[EVMLog], WorldState, EVM]] = [] self._logs: List[EVMLog] = list() self._pending_transaction = None self._transactions: List[Transaction] = list() - if blocknumber is None: - # assume initial byzantium block - blocknumber = 4370000 - self._blocknumber = blocknumber + if blocknumber is not None: + self._world_state.set_blocknumber(blocknumber) + + if timestamp is not None: + self._world_state.set_timestamp(timestamp) + + if difficulty is not None: + self._world_state.set_difficulty(difficulty) - if timestamp is None: - # 1524785992; // Thu Apr 26 23:39:52 UTC 2018 - timestamp = 1524785992 - self._timestamp = timestamp + if gaslimit is not None: + self._world_state.set_gaslimit(gaslimit) - self._difficulty = difficulty - self._gaslimit = gaslimit - self._coinbase = coinbase + if coinbase is not None: + self._world_state.set_coinbase(coinbase) def __getstate__(self): state = super().__getstate__() @@ -2295,13 +2305,7 @@ def __getstate__(self): state["world_state"] = self._world_state state["constraints"] = self._constraints state["callstack"] = self._callstack - state["deleted_accounts"] = self._deleted_accounts state["transactions"] = self._transactions - state["_blocknumber"] = self._blocknumber - state["_timestamp"] = self._timestamp - state["_difficulty"] = self._difficulty - state["_gaslimit"] = self._gaslimit - state["_coinbase"] = self._coinbase return state def __setstate__(self, state): @@ -2309,17 +2313,11 @@ def __setstate__(self, state): self._constraints = state["constraints"] self._pending_transaction = state["pending_transaction"] self._world_state = state["world_state"] - self._deleted_accounts = state["deleted_accounts"] self._logs = state["logs"] self._callstack = state["callstack"] self._transactions = state["transactions"] - self._blocknumber = state["_blocknumber"] - self._timestamp = state["_timestamp"] - self._difficulty = state["_difficulty"] - self._gaslimit = state["_gaslimit"] - self._coinbase = state["_coinbase"] - for _, _, _, _, vm in self._callstack: + for _, _, _, vm in self._callstack: self.forward_events_from(vm) def try_simplify_to_constant(self, data): @@ -2364,7 +2362,7 @@ def PC(self): def __getitem__(self, index): assert isinstance(index, int) - return self._world_state[index] + return self.accounts[index] def __contains__(self, key): assert not issymbolic(key), "Symbolic address not supported" @@ -2421,36 +2419,26 @@ def _open_transaction(self, sort, address, price, bytecode_or_data, caller, valu vm = EVM(self._constraints, address, data, caller, value, bytecode, world=self, gas=gas) self._publish("will_open_transaction", tx) - self._callstack.append( - (tx, self.logs, self.deleted_accounts, copy.copy(self.get_storage(address)), vm) - ) + self._callstack.append((tx, self.logs, copy.copy(self._world_state), vm)) self.forward_events_from(vm) self._publish("did_open_transaction", tx) def _close_transaction(self, result, data=None, rollback=False): self._publish("will_close_transaction", self._callstack[-1][0]) - tx, logs, deleted_accounts, account_storage, vm = self._callstack.pop() + tx, logs, world_state, vm = self._callstack.pop() assert self.constraints == vm.constraints # Keep constraints gathered in the last vm self.constraints = vm.constraints if rollback: - self._set_storage(vm.address, account_storage) + self._world_state = world_state self._logs = logs self.send_funds(tx.address, tx.caller, tx.value) else: - self._deleted_accounts = deleted_accounts - # FIXME: BUG: a CREATE can be successful and still return an empty contract :shrug: - if not issymbolic(tx.caller) and ( - tx.sort == "CREATE" or not self._world_state[tx.caller]["code"] - ): + if not issymbolic(tx.caller) and (tx.sort == "CREATE" or not self.get_code(tx.caller)): # Increment the nonce if this transaction created a contract, or if it was called by a non-contract account self.increase_nonce(tx.caller) - if tx.is_human: - for deleted_account in self._deleted_accounts: - if deleted_account in self._world_state: - del self._world_state[deleted_account] tx.set_result(result, data) self._transactions.append(tx) @@ -2497,7 +2485,7 @@ def last_human_transaction(self): def current_vm(self): """current vm""" try: - _, _, _, _, vm = self._callstack[-1] + _, _, _, vm = self._callstack[-1] return vm except IndexError: return None @@ -2506,7 +2494,7 @@ def current_vm(self): def current_transaction(self): """current tx""" try: - tx, _, _, _, _ = self._callstack[-1] + tx, _, _, _ = self._callstack[-1] if tx.result is not None: # That tx finished. No current tx. return None @@ -2518,7 +2506,7 @@ def current_transaction(self): def current_human_transaction(self): """Current ongoing human transaction""" try: - tx, _, _, _, _ = self._callstack[0] + tx, _, _, _ = self._callstack[0] if tx.result is not None: # That tx finished. No current tx. return None @@ -2529,7 +2517,7 @@ def current_human_transaction(self): @property def accounts(self): - return list(self._world_state.keys()) + return list(self._world_state.accounts()) @property def normal_accounts(self): @@ -2547,133 +2535,99 @@ def contract_accounts(self): accs.append(address) return accs - @property - def deleted_accounts(self): - return self._deleted_accounts - - def delete_account(self, address): - if address in self._world_state: - self._deleted_accounts.add(address) + def delete_account(self, address: int): + self._world_state.delete_account(address) - def get_storage_data(self, storage_address, offset): + def get_storage_data(self, storage_address: int, offset: int) -> Any: """ Read a value from a storage slot on the specified account :param storage_address: an account address :param offset: the storage slot to use. - :type offset: int or BitVec + :type offset: int :return: the value :rtype: int or BitVec """ - value = self._world_state[storage_address]["storage"].get(offset, 0) + value = self._world_state.get_storage_data(storage_address, offset) return simplify(value) - def set_storage_data(self, storage_address, offset, value): + def set_storage_data(self, storage_address: int, offset: int, value: Any): """ Writes a value to a storage slot in specified account :param storage_address: an account address :param offset: the storage slot to use. - :type offset: int or BitVec + :type offset: int :param value: the value to write :type value: int or BitVec """ - self._world_state[storage_address]["storage"][offset] = value + self._world_state.set_storage_data(storage_address, offset, value) - def get_storage_items(self, address): - """ - Gets all items in an account storage - - :param address: account address - :return: all items in account storage. items are tuple of (index, value). value can be symbolic - :rtype: list[(storage_index, storage_value)] - """ - storage = self._world_state[address]["storage"] - items = [] - array = storage.array - while not isinstance(array, ArrayVariable): - items.append((array.index, array.value)) - array = array.array - return items - - def has_storage(self, address): + def has_storage(self, address: int) -> bool: """ True if something has been written to the storage. Note that if a slot has been erased from the storage this function may lose any meaning. """ - storage = self._world_state[address]["storage"] - array = storage.array - while not isinstance(array, ArrayVariable): - if isinstance(array, ArrayStore): - return True - array = array.array - return False - - def get_storage(self, address): - """ - Gets the storage of an account + return len(self._world_state.get_storage(address)) > 0 - :param address: account address - :return: account storage - :rtype: bytearray or ArrayProxy - """ - return self._world_state[address]["storage"] + def _get_storage(self, constraints: ConstraintSet, address: int) -> Array: + """Private auxiliary function to retrieve the storage as an Array""" + array = constraints.new_array( + index_bits=256, + value_bits=256, + name=f"STORAGE_{address:x}", + avoid_collisions=True, + default=0, + ) + storage: Dict[int, Any] = {} + try: + storage = self._world_state.get_storage(address) + except NotImplementedError: + pass + for key, value in storage.items(): + array[key] = value + return array - def _set_storage(self, address, storage): - """Private auxiliary function to replace the storage""" - self._world_state[address]["storage"] = storage + def _set_storage(self, address: int, storage: Dict[int, int]): + """Private auxiliary function to set the storage with a Dict[int, int]""" + for key, value in storage.items(): + self._world_state.set_storage_data(address, key, value) - def get_nonce(self, address): - if issymbolic(address): - raise ValueError(f"Cannot retrieve the nonce of symbolic address {address}") - elif address not in self._world_state: - # assume that the caller is a regular account, so initialize its nonce to zero - ret = 0 - elif "nonce" not in self._world_state[address]: - if self._world_state[address]["code"]: - # this is a contract account, so set the nonce to 1 per EIP 161 - ret = 1 - else: - ret = 0 - else: - ret = self._world_state[address]["nonce"] - return ret + def get_nonce(self, address: int) -> Any: + return self._world_state.get_nonce(address) - def increase_nonce(self, address): - new_nonce = self.get_nonce(address) + 1 - self._world_state[address]["nonce"] = new_nonce + def set_nonce(self, address: int, value: Any): + self._world_state.set_nonce(address, value) + + def increase_nonce(self, address: int) -> Any: + new_nonce = self._world_state.get_nonce(address) + 1 + self._world_state.set_nonce(address, new_nonce) return new_nonce - def set_balance(self, address, value): - self._world_state[int(address)]["balance"] = value + def set_balance(self, address: int, value: Any): + self._world_state.set_balance(address, value) - def get_balance(self, address): - if address not in self._world_state: - return 0 - return self._world_state[address]["balance"] + def get_balance(self, address: int) -> Any: + return self._world_state.get_balance(address) - def add_to_balance(self, address, value): - assert address in self._world_state - self._world_state[address]["balance"] += value + def add_to_balance(self, address: int, value: Any): + new_balance = self._world_state.get_balance(address) + value + self.set_balance(address, new_balance) + return new_balance - def send_funds(self, sender, recipient, value): - self._world_state[sender]["balance"] -= value - self._world_state[recipient]["balance"] += value + def send_funds(self, sender: int, recipient: int, value: Any): + self.add_to_balance(sender, -value) + self.add_to_balance(recipient, value) - def get_code(self, address): - if address not in self._world_state: - return bytes() - return self._world_state[address]["code"] + def get_code(self, address: int) -> Any: + return self._world_state.get_code(address) - def set_code(self, address, data): - assert data is not None and isinstance(data, (bytes, Array)) - if self._world_state[address]["code"]: - raise EVMException("Code already set") - self._world_state[address]["code"] = data + def set_code(self, address: int, data: bytes): + self._world_state.set_code(address, data) - def has_code(self, address): - return len(self._world_state[address]["code"]) > 0 + def has_code(self, address: int) -> bool: + return len(self._world_state.get_code(address)) > 0 def log(self, address, topics, data): self._logs.append(EVMLog(address, data, topics)) @@ -2689,19 +2643,19 @@ def block_prevhash(self): return 0 def block_coinbase(self): - return self._coinbase + return self._world_state.get_coinbase() def block_timestamp(self): - return self._timestamp + return self._world_state.get_timestamp() def block_number(self): - return self._blocknumber + return self._world_state.get_blocknumber() def block_difficulty(self): - return self._difficulty + return self._world_state.get_difficulty() def block_gaslimit(self): - return self._gaslimit + return self._world_state.get_gaslimit() def block_hash(self, block_number=None, force_recent=True): """ @@ -2786,7 +2740,9 @@ def execute(self): except EndTx as ex: self._close_transaction(ex.result, ex.data, rollback=ex.is_rollback()) - def create_account(self, address=None, balance=0, code=None, storage=None, nonce=None): + def create_account( + self, address=None, balance=0, code=None, storage: Dict[int, int] = None, nonce=None + ): """ Low level account creation. No transaction is done. @@ -2819,31 +2775,17 @@ def create_account(self, address=None, balance=0, code=None, storage=None, nonce # selfdestructed address, it can not be reused raise EthereumError("The account already exists") - if storage is None: - # Uninitialized values in a storage are 0 by spec - storage = self.constraints.new_array( - index_bits=256, - value_bits=256, - name=f"STORAGE_{address:x}", - avoid_collisions=True, - default=0, - ) - else: - if isinstance(storage, ArrayProxy): - if storage.index_bits != 256 or storage.value_bits != 256: - raise TypeError("An ArrayProxy 256bits -> 256bits is needed") - else: - if any((k < 0 or k >= 1 << 256 for k, v in storage.items())): - raise TypeError( - "Need a dict like object that maps 256 bits keys to 256 bits values" - ) - # Hopefully here we have a mapping from 256b to 256b + if nonce is not None: + self.set_nonce(address, nonce) + + if balance is not None: + self.set_balance(address, balance) - self._world_state[address] = {} - self._world_state[address]["nonce"] = nonce - self._world_state[address]["balance"] = balance - self._world_state[address]["storage"] = storage - self._world_state[address]["code"] = code + if storage is not None: + self._set_storage(address, storage) + + if code is not None: + self.set_code(address, code) # adds hash of new address data = binascii.unhexlify("{:064x}{:064x}".format(address, 0)) @@ -2996,10 +2938,6 @@ def _process_pending_transaction(self): f"Caller account {hex(caller)} does not exist; valid accounts: {list(map(hex, self.accounts))}" ) - if address not in self.accounts: - # Creating an unaccessible account - self.create_account(address=address) - # Check depth failed = self.depth > 1024 @@ -3043,7 +2981,7 @@ def dump(self, stream, state, mevm, message): stream.write("Message: %s\n" % message) stream.write("Last exception: %s\n" % state.context.get("last_exception", "None")) - if last_tx: + if last_tx and "evm.trace" in state.context: at_runtime = last_tx.sort != "CREATE" address, offset, at_init = state.context["evm.trace"][-1] assert last_tx.result is not None or at_runtime != at_init @@ -3075,7 +3013,7 @@ def dump(self, stream, state, mevm, message): balance = state.solve_one(balance) stream.write("Balance: %d %s\n" % (balance, flagged(is_balance_symbolic))) - storage = blockchain.get_storage(account_address) + storage = blockchain._get_storage(state.constraints, account_address) stream.write("Storage: %s\n" % translate_to_smtlib(storage, use_bindings=False)) all_used_indexes = [] @@ -3083,7 +3021,7 @@ def dump(self, stream, state, mevm, message): # make a free symbolic idex that could address any storage slot index = temp_cs.new_bitvec(256) # get the storage for account_address - storage = blockchain.get_storage(account_address) + storage = blockchain._get_storage(temp_cs, account_address) # we are interested only in used slots temp_cs.add(storage.get(index) != 0) # Query the solver to get all storage indexes with used slots diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py new file mode 100644 index 000000000..c397080d2 --- /dev/null +++ b/manticore/platforms/evm_world_state.py @@ -0,0 +1,314 @@ +import logging +import os +from abc import ABC, abstractmethod +from typing import Any, Dict, Set +from urllib.parse import ParseResult, urlparse +from web3 import Web3 +from ..exceptions import EthereumError + + +logger = logging.getLogger(__name__) + + +class WorldState: + @abstractmethod + def accounts(self) -> Set[int]: + pass + + @abstractmethod + def get_nonce(self, address: int) -> Any: + pass + + @abstractmethod + def get_balance(self, address: int) -> Any: + pass + + @abstractmethod + def get_storage(self, address: int) -> Dict[int, Any]: + pass + + @abstractmethod + def get_storage_data(self, address: int, offset: int) -> Any: + pass + + @abstractmethod + def get_code(self, address: int) -> Any: + pass + + @abstractmethod + def get_blocknumber(self) -> Any: + pass + + @abstractmethod + def get_timestamp(self) -> Any: + pass + + @abstractmethod + def get_difficulty(self) -> Any: + pass + + @abstractmethod + def get_gaslimit(self) -> Any: + pass + + @abstractmethod + def get_coinbase(self) -> Any: + pass + + +class DefaultWorldState(WorldState): + def accounts(self) -> Set[int]: + return set() + + def get_nonce(self, address: int) -> Any: + return 0 + + def get_balance(self, address: int) -> Any: + return 0 + + def get_storage(self, address: int) -> Dict[int, Any]: + return {} + + def get_storage_data(self, address: int, offset: int) -> Any: + return 0 + + def get_code(self, address: int) -> Any: + return bytes() + + def get_blocknumber(self) -> Any: + # assume initial byzantium block + return 4370000 + + def get_timestamp(self) -> Any: + # 1524785992; // Thu Apr 26 23:39:52 UTC 2018 + return 1524785992 + + def get_difficulty(self) -> Any: + return 0 + + def get_gaslimit(self) -> Any: + return 0 + + def get_coinbase(self) -> Any: + return 0 + + +class Endpoint: + def __init__(self, blocknumber: int, warned: bool): + self.blocknumber = blocknumber + self.warned = warned + + +_endpoints: Dict[str, Endpoint] = {} + + +def _web3_address(address: int) -> str: + return Web3.toChecksumAddress("0x%0.40x" % address) + + +# sam.moelius: Notes: +# +# 1. https://github.com/ethereum/wiki/wiki/JSON-RPC lists the kinds of information that an Ethereum +# node can provide over JSON RPC. +# +# 2. The accounts and get_storage methods do not make sense when using JSON RPC. IMHO, we should +# program to the least common denominator. In that sense, we should see whether the accounts and +# get_storage methods could be eliminated. + + +class RemoteWorldState(WorldState): + def __init__(self, url: str): + actual = urlparse(url) + expected = ParseResult(scheme="", netloc="", path=url, params="", query="", fragment="") + if actual != expected: + raise EthereumError("URL must be of the form 'IP:PORT': " + url) + self._url = url + + def _web3(self) -> Web3: + web3 = Web3(Web3.WebsocketProvider("ws://" + self._url)) + blocknumber = web3.eth.blockNumber + if self._url not in _endpoints: + _endpoints[self._url] = Endpoint(blocknumber, False) + logger.info("Connected to %s (blocknumber = %d)", self._url, blocknumber) + if _endpoints[self._url].blocknumber != blocknumber: + if not _endpoints[self._url].warned: + logger.warning( + "%s blocknumber has changed (%d != %d)---someone is using the endpoint" + + " beside us", + self._url, + _endpoints[self._url].blocknumber, + blocknumber, + ) + _endpoints[self._url].warned = True + _endpoints[self._url].blocknumber = blocknumber + return web3 + + def accounts(self) -> Set[int]: + raise NotImplementedError + + def get_nonce(self, address: int) -> Any: + return self._web3().eth.getTransactionCount(_web3_address(address)) + + def get_balance(self, address: int) -> Any: + return self._web3().eth.getBalance(_web3_address(address)) + + def get_storage(self, address) -> Dict[int, Any]: + raise NotImplementedError + + def get_storage_data(self, address: int, offset: int) -> Any: + return self._web3().eth.getStorageAt(_web3_address(address), offset) + + def get_code(self, address: int) -> Any: + return self._web3().eth.getCode(_web3_address(address)) + + def get_blocknumber(self) -> Any: + return self._web3().eth.blockNumber + + def get_timestamp(self) -> Any: + return self._web3().eth.timestamp + + def get_difficulty(self) -> Any: + return self._web3().eth.difficulty + + def get_gaslimit(self) -> Any: + return self._web3().eth.gasLimit + + def get_coinbase(self) -> Any: + return self._web3().eth.coinbase + + +# sam.moelius: If we decide to cache results returned from a RemoteWorldState, then they should NOT be +# cached within an overlay. The reason is that this could affect the results of subsequent operations. +# Consider a call to get_storage_data followed by a call to has_storage. If nothing was written to +# storage within the overlay, then the call to has_storage will throw an exception. But if the result +# of the call to get_storage_data was cached in the overlay, then no exception would be thrown. + + +class OverlayWorldState(WorldState): + def __init__(self, underlay: WorldState): + self._underlay: WorldState = underlay + self._deleted_accounts: Set[int] = set() + self._nonce: Dict[int, Any] = {} + self._balance: Dict[int, Any] = {} + self._storage: Dict[int, Dict[int, Any]] = {} + self._code: Dict[int, Any] = {} + self._blocknumber: Any = None + self._timestamp: Any = None + self._difficulty: Any = None + self._gaslimit: Any = None + self._coinbase: Any = None + + def accounts(self) -> Set[int]: + accounts: Set[int] = set() + try: + accounts = self._underlay.accounts() + except NotImplementedError: + pass + return ( + accounts + | self._nonce.keys() + | self._balance.keys() + | self._storage.keys() + | self._code.keys() + ) - self._deleted_accounts + + def get_nonce(self, address: int) -> Any: + if address in self._nonce: + return self._nonce[address] + else: + return self._underlay.get_nonce(address) + + def get_balance(self, address: int) -> Any: + if address in self._balance: + return self._balance[address] + else: + return self._underlay.get_balance(address) + + def get_storage(self, address: int) -> Dict[int, Any]: + storage: Dict[int, Any] = {} + try: + storage = self._underlay.get_storage(address) + except NotImplementedError: + pass + if address in self._storage: + storage.update(self._storage[address]) + return storage + + def get_storage_data(self, address: int, offset: int) -> Any: + if address in self._storage and offset in self._storage[address]: + return self._storage[address][offset] + else: + return self._underlay.get_storage_data(address, offset) + + def get_code(self, address: int) -> Any: + if address in self._code: + return self._code[address] + else: + return self._underlay.get_code(address) + + def get_blocknumber(self) -> Any: + if self._blocknumber is not None: + return self._blocknumber + else: + return self._underlay.get_blocknumber() + + def get_timestamp(self) -> Any: + if self._timestamp is not None: + return self._timestamp + else: + return self._underlay.get_timestamp() + + def get_difficulty(self) -> Any: + if self._difficulty is not None: + return self._difficulty + else: + return self._underlay.get_difficulty() + + def get_gaslimit(self) -> Any: + if self._gaslimit is not None: + return self._gaslimit + else: + return self._underlay.get_gaslimit() + + def get_coinbase(self) -> Any: + if self._coinbase is not None: + return self._coinbase + else: + return self._underlay.get_coinbase() + + def delete_account(self, address: int): + self._nonce[address] = DefaultWorldState().get_nonce(address) + self._balance[address] = DefaultWorldState().get_balance(address) + self._storage[address] = DefaultWorldState().get_storage(address) + self._code[address] = DefaultWorldState().get_code(address) + self._deleted_accounts.add(address) + + def set_nonce(self, address: int, value: Any): + self._nonce[address] = value + self._deleted_accounts.discard(address) + + def set_balance(self, address: int, value: Any): + self._balance[address] = value + self._deleted_accounts.discard(address) + + def set_storage_data(self, address: int, offset: int, value: Any): + self._storage.setdefault(address, {})[offset] = value + self._deleted_accounts.discard(address) + + def set_code(self, address: int, code: Any): + self._code[address] = code + + def set_blocknumber(self, value: Any): + self._blocknumber = value + + def set_timestamp(self, value: Any): + self._timestamp = value + + def set_difficulty(self, value: Any): + self._difficulty = value + + def set_gaslimit(self, value: Any): + self._gaslimit = value + + def set_coinbase(self, value: Any): + self._coinbase = value From 87e3b4496580b1d40d6d37e4c17c798fe3026830 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Sun, 5 Jan 2020 00:33:43 +0000 Subject: [PATCH 002/104] Add web3 to install_requires. --- setup.py | 1 + 1 file changed, 1 insertion(+) diff --git a/setup.py b/setup.py index 63cbf5a88..cff84a0f7 100644 --- a/setup.py +++ b/setup.py @@ -54,6 +54,7 @@ def rtd_dependent_deps(): "ply", "crytic-compile>=0.1.1", "wasm", + "web3", "dataclasses; python_version < '3.7'", ] + rtd_dependent_deps(), From 56a7bab37d0a9aaf350b65543ceb558e8fb7aadd Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Sun, 5 Jan 2020 00:50:11 +0000 Subject: [PATCH 003/104] Ignore web3 types. --- manticore/platforms/evm_world_state.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index c397080d2..6bbb1416a 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -3,7 +3,7 @@ from abc import ABC, abstractmethod from typing import Any, Dict, Set from urllib.parse import ParseResult, urlparse -from web3 import Web3 +from web3 import Web3 # type: ignore from ..exceptions import EthereumError From b395920f2d0914c2befcd0fbf42e89b10e07bea8 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 6 Jan 2020 19:21:26 +0000 Subject: [PATCH 004/104] Handle symbolic offsets. --- manticore/core/smtlib/expression.py | 2 +- manticore/ethereum/manticore.py | 4 + manticore/platforms/evm.py | 68 +++---- manticore/platforms/evm_world_state.py | 263 +++++++++++++++++-------- 4 files changed, 213 insertions(+), 124 deletions(-) diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index 39ec1b198..1af3f4710 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -642,7 +642,7 @@ def __init__( self, index_bits: int, index_max: Optional[int], value_bits: int, *operands, **kwargs ): assert index_bits in (32, 64, 256) - assert value_bits in (8, 16, 32, 64, 256) + assert value_bits in (1, 8, 16, 32, 64, 256) assert index_max is None or index_max >= 0 and index_max < 2 ** index_bits self._index_bits = index_bits self._index_max = index_max diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 478e112d1..482261611 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -1,3 +1,7 @@ +from typeguard.importhook import install_import_hook + +install_import_hook('manticore') + import copy import itertools import binascii diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 03f788989..ed3ed61a1 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -936,17 +936,13 @@ def _push(self, value): sp-> {empty} """ assert ( - isinstance(value, bytes) - or isinstance(value, int) + isinstance(value, int) or isinstance(value, BitVec) and value.size == 256 ) if len(self.stack) >= 1024: raise StackOverflow() - if isinstance(value, bytes): - value = int.from_bytes(value, "big") - if isinstance(value, int): value = value & TT256M1 @@ -2538,30 +2534,30 @@ def contract_accounts(self): def delete_account(self, address: int): self._world_state.delete_account(address) - def get_storage_data(self, storage_address: int, offset: int) -> Any: + def get_storage_data(self, storage_address: int, offset: int) -> Union[int, BitVec]: """ Read a value from a storage slot on the specified account :param storage_address: an account address :param offset: the storage slot to use. - :type offset: int + :type offset: int or BitVec :return: the value :rtype: int or BitVec """ value = self._world_state.get_storage_data(storage_address, offset) return simplify(value) - def set_storage_data(self, storage_address: int, offset: int, value: Any): + def set_storage_data(self, storage_address: int, offset: Union[int, BitVec], value: Union[int, BitVec]): """ Writes a value to a storage slot in specified account :param storage_address: an account address :param offset: the storage slot to use. - :type offset: int + :type offset: int or BitVec :param value: the value to write :type value: int or BitVec """ - self._world_state.set_storage_data(storage_address, offset, value) + self._world_state.set_storage_data(self.constraints, storage_address, offset, value) def has_storage(self, address: int) -> bool: """ @@ -2569,61 +2565,59 @@ def has_storage(self, address: int) -> bool: Note that if a slot has been erased from the storage this function may lose any meaning. """ - return len(self._world_state.get_storage(address)) > 0 + return self._world_state.has_storage(address) - def _get_storage(self, constraints: ConstraintSet, address: int) -> Array: + def _get_storage(self, constraints: ConstraintSet, address: int) -> Union[Dict[int, int], Array]: """Private auxiliary function to retrieve the storage as an Array""" - array = constraints.new_array( - index_bits=256, - value_bits=256, - name=f"STORAGE_{address:x}", - avoid_collisions=True, - default=0, - ) - storage: Dict[int, Any] = {} - try: - storage = self._world_state.get_storage(address) - except NotImplementedError: - pass - for key, value in storage.items(): - array[key] = value - return array + storage = self._world_state.get_storage(address) + if isinstance(storage, dict): + array = constraints.new_array( + index_bits=256, + value_bits=256, + name=f"STORAGE_DATA_{address:x}", + avoid_collisions=True, + default=0, + ) + for key, value in storage.items(): + array[key] = value + storage = array + return storage def _set_storage(self, address: int, storage: Dict[int, int]): """Private auxiliary function to set the storage with a Dict[int, int]""" for key, value in storage.items(): - self._world_state.set_storage_data(address, key, value) + self._world_state.set_storage_data(self.constraints, address, key, value) - def get_nonce(self, address: int) -> Any: + def get_nonce(self, address: int) -> Union[int, BitVec]: return self._world_state.get_nonce(address) - def set_nonce(self, address: int, value: Any): + def set_nonce(self, address: int, value: Union[int, BitVec]): self._world_state.set_nonce(address, value) - def increase_nonce(self, address: int) -> Any: + def increase_nonce(self, address: int) -> Union[int, BitVec]: new_nonce = self._world_state.get_nonce(address) + 1 self._world_state.set_nonce(address, new_nonce) return new_nonce - def set_balance(self, address: int, value: Any): + def set_balance(self, address: int, value: Union[int, BitVec]): self._world_state.set_balance(address, value) - def get_balance(self, address: int) -> Any: + def get_balance(self, address: int) -> Union[int, BitVec]: return self._world_state.get_balance(address) - def add_to_balance(self, address: int, value: Any): + def add_to_balance(self, address: int, value: Union[int, BitVec]): new_balance = self._world_state.get_balance(address) + value self.set_balance(address, new_balance) return new_balance - def send_funds(self, sender: int, recipient: int, value: Any): + def send_funds(self, sender: int, recipient: int, value: Union[int, BitVec]): self.add_to_balance(sender, -value) self.add_to_balance(recipient, value) - def get_code(self, address: int) -> Any: + def get_code(self, address: int) -> Union[bytes, Array]: return self._world_state.get_code(address) - def set_code(self, address: int, data: bytes): + def set_code(self, address: int, data: Union[bytes, Array]): self._world_state.set_code(address, data) def has_code(self, address: int) -> bool: diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 6bbb1416a..2e6b3f735 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -1,98 +1,121 @@ import logging import os from abc import ABC, abstractmethod -from typing import Any, Dict, Set +from typing import Dict, Optional, Set, Union from urllib.parse import ParseResult, urlparse from web3 import Web3 # type: ignore from ..exceptions import EthereumError - +from ..core.smtlib import ( + Array, + BitVec, + BitVecConstant, + BitVecITE, + BitVecZeroExtend, + ConstraintSet, +) logger = logging.getLogger(__name__) +#################################################################################################### + + class WorldState: @abstractmethod def accounts(self) -> Set[int]: pass @abstractmethod - def get_nonce(self, address: int) -> Any: + def get_nonce(self, address: int) -> Union[int, BitVec]: + pass + + @abstractmethod + def get_balance(self, address: int) -> Union[int, BitVec]: pass @abstractmethod - def get_balance(self, address: int) -> Any: + def has_storage(self, address: int) -> bool: pass @abstractmethod - def get_storage(self, address: int) -> Dict[int, Any]: + def get_storage(self, address: int) -> Union[Dict[int, int], Array]: pass @abstractmethod - def get_storage_data(self, address: int, offset: int) -> Any: + def get_storage_data(self, address: int, offset: int) -> Union[int, BitVec]: pass @abstractmethod - def get_code(self, address: int) -> Any: + def get_code(self, address: int) -> Union[bytes, Array]: pass @abstractmethod - def get_blocknumber(self) -> Any: + def get_blocknumber(self) -> Union[int, BitVec]: pass @abstractmethod - def get_timestamp(self) -> Any: + def get_timestamp(self) -> Union[int, BitVec]: pass @abstractmethod - def get_difficulty(self) -> Any: + def get_difficulty(self) -> Union[int, BitVec]: pass @abstractmethod - def get_gaslimit(self) -> Any: + def get_gaslimit(self) -> Union[int, BitVec]: pass @abstractmethod - def get_coinbase(self) -> Any: + def get_coinbase(self) -> Union[int, BitVec]: pass +#################################################################################################### + + class DefaultWorldState(WorldState): def accounts(self) -> Set[int]: return set() - def get_nonce(self, address: int) -> Any: + def get_nonce(self, address: int) -> int: return 0 - def get_balance(self, address: int) -> Any: + def get_balance(self, address: int) -> int: return 0 - def get_storage(self, address: int) -> Dict[int, Any]: + def has_storage(self, address: int) -> bool: + return False + + def get_storage(self, address: int) -> Dict[int, int]: return {} - def get_storage_data(self, address: int, offset: int) -> Any: + def get_storage_data(self, address: int, offset: int) -> int: return 0 - def get_code(self, address: int) -> Any: + def get_code(self, address: int) -> bytes: return bytes() - def get_blocknumber(self) -> Any: + def get_blocknumber(self) -> int: # assume initial byzantium block return 4370000 - def get_timestamp(self) -> Any: + def get_timestamp(self) -> int: # 1524785992; // Thu Apr 26 23:39:52 UTC 2018 return 1524785992 - def get_difficulty(self) -> Any: + def get_difficulty(self) -> int: return 0 - def get_gaslimit(self) -> Any: + def get_gaslimit(self) -> int: return 0 - def get_coinbase(self) -> Any: + def get_coinbase(self) -> int: return 0 +#################################################################################################### + + class Endpoint: def __init__(self, blocknumber: int, warned: bool): self.blocknumber = blocknumber @@ -127,76 +150,109 @@ def __init__(self, url: str): def _web3(self) -> Web3: web3 = Web3(Web3.WebsocketProvider("ws://" + self._url)) blocknumber = web3.eth.blockNumber - if self._url not in _endpoints: - _endpoints[self._url] = Endpoint(blocknumber, False) + endpoint = _endpoints.get(self._url) + if endpoint is None: + endpoint = Endpoint(blocknumber, False) + _endpoints[self._url] = endpoint logger.info("Connected to %s (blocknumber = %d)", self._url, blocknumber) - if _endpoints[self._url].blocknumber != blocknumber: - if not _endpoints[self._url].warned: + if endpoint.blocknumber != blocknumber: + if not endpoint.warned: logger.warning( - "%s blocknumber has changed (%d != %d)---someone is using the endpoint" + "%s blocknumber has changed: %d != %d---someone is using the endpoint" + " beside us", self._url, - _endpoints[self._url].blocknumber, + endpoint.blocknumber, blocknumber, ) - _endpoints[self._url].warned = True - _endpoints[self._url].blocknumber = blocknumber + endpoint.warned = True + endpoint.blocknumber = blocknumber return web3 def accounts(self) -> Set[int]: raise NotImplementedError - def get_nonce(self, address: int) -> Any: + def get_nonce(self, address: int) -> int: return self._web3().eth.getTransactionCount(_web3_address(address)) - def get_balance(self, address: int) -> Any: + def get_balance(self, address: int) -> int: return self._web3().eth.getBalance(_web3_address(address)) - def get_storage(self, address) -> Dict[int, Any]: + def has_storage(self, address: int) -> bool: + raise NotImplementedError + + def get_storage(self, address) -> Dict[int, int]: raise NotImplementedError - def get_storage_data(self, address: int, offset: int) -> Any: - return self._web3().eth.getStorageAt(_web3_address(address), offset) + def get_storage_data(self, address: int, offset: int) -> int: + return int.from_bytes(self._web3().eth.getStorageAt(_web3_address(address), offset), "big") - def get_code(self, address: int) -> Any: + def get_code(self, address: int) -> bytes: return self._web3().eth.getCode(_web3_address(address)) - def get_blocknumber(self) -> Any: + def get_blocknumber(self) -> int: return self._web3().eth.blockNumber - def get_timestamp(self) -> Any: + def get_timestamp(self) -> int: return self._web3().eth.timestamp - def get_difficulty(self) -> Any: + def get_difficulty(self) -> int: return self._web3().eth.difficulty - def get_gaslimit(self) -> Any: + def get_gaslimit(self) -> int: return self._web3().eth.gasLimit - def get_coinbase(self) -> Any: + def get_coinbase(self) -> int: return self._web3().eth.coinbase -# sam.moelius: If we decide to cache results returned from a RemoteWorldState, then they should NOT be -# cached within an overlay. The reason is that this could affect the results of subsequent operations. -# Consider a call to get_storage_data followed by a call to has_storage. If nothing was written to -# storage within the overlay, then the call to has_storage will throw an exception. But if the result -# of the call to get_storage_data was cached in the overlay, then no exception would be thrown. +#################################################################################################### + + +# sam.moelius: map records which (symbolic) offsets have been written to. data holds the values +# written. + + +class Storage: + def __init__(self, constraints: ConstraintSet, address: int): + self.constraints = constraints + self.map = constraints.new_array( + index_bits=256, + value_bits=1, + name=f"STORAGE_MAP_{address:x}", + avoid_collisions=True, + default=0, + ) + self.data = constraints.new_array( + index_bits=256, + value_bits=256, + name=f"STORAGE_DATA_{address:x}", + avoid_collisions=True, + default=0, + ) + self.dirty = False + + +# sam.moelius: If we decide to cache results returned from a RemoteWorldState, then they should NOT +# be cached within an overlay. The reason is that this could affect the results of subsequent +# operations. Consider a call to get_storage_data followed by a call to has_storage. If nothing +# was written to storage within the overlay, then the call to has_storage will throw an exception. +# But if the result of the call to get_storage_data was cached in the overlay, then no exception +# would be thrown. class OverlayWorldState(WorldState): def __init__(self, underlay: WorldState): self._underlay: WorldState = underlay self._deleted_accounts: Set[int] = set() - self._nonce: Dict[int, Any] = {} - self._balance: Dict[int, Any] = {} - self._storage: Dict[int, Dict[int, Any]] = {} - self._code: Dict[int, Any] = {} - self._blocknumber: Any = None - self._timestamp: Any = None - self._difficulty: Any = None - self._gaslimit: Any = None - self._coinbase: Any = None + self._nonce: Dict[int, Union[int, BitVec]] = {} + self._balance: Dict[int, Union[int, BitVec]] = {} + self._storage: Dict[int, Optional[Storage]] = {} + self._code: Dict[int, Union[bytes, Array]] = {} + self._blocknumber: Optional[Union[int, BitVec]] = None + self._timestamp: Optional[Union[int, BitVec]] = None + self._difficulty: Optional[Union[int, BitVec]] = None + self._gaslimit: Optional[Union[int, BitVec]] = None + self._coinbase: Optional[Union[int, BitVec]] = None def accounts(self) -> Set[int]: accounts: Set[int] = set() @@ -212,65 +268,84 @@ def accounts(self) -> Set[int]: | self._code.keys() ) - self._deleted_accounts - def get_nonce(self, address: int) -> Any: + def get_nonce(self, address: int) -> Union[int, BitVec]: if address in self._nonce: return self._nonce[address] else: return self._underlay.get_nonce(address) - def get_balance(self, address: int) -> Any: + def get_balance(self, address: int) -> Union[int, BitVec]: if address in self._balance: return self._balance[address] else: return self._underlay.get_balance(address) - def get_storage(self, address: int) -> Dict[int, Any]: - storage: Dict[int, Any] = {} + def has_storage(self, address: int) -> bool: + dirty = False try: - storage = self._underlay.get_storage(address) + dirty = self._underlay.has_storage(address) except NotImplementedError: pass - if address in self._storage: - storage.update(self._storage[address]) - return storage - - def get_storage_data(self, address: int, offset: int) -> Any: - if address in self._storage and offset in self._storage[address]: - return self._storage[address][offset] - else: - return self._underlay.get_storage_data(address, offset) + storage = self._storage.get(address) + if storage is not None: + dirty = dirty or storage.dirty + return dirty - def get_code(self, address: int) -> Any: + def get_storage(self, address: int) -> Union[Dict[int, int], Array]: + data: Union[Dict[int, int], Array] = {} + try: + data = self._underlay.get_storage(address) + except NotImplementedError: + pass + storage = self._storage.get(address) + if storage is not None: + # sam.moelius: Merging the overlay's storage into the underlay's storage is not + # currently implemented. + if not isinstance(data, dict) or len(data) > 0: + raise NotImplementedError + data = storage.data + return data + + def get_storage_data(self, address: int, offset: int) -> Union[int, BitVec]: + value = self._underlay.get_storage_data(address, offset) + storage = self._storage.get(address) + if storage is not None: + if not isinstance(value, BitVec): + value = BitVecConstant(256, value) + value = BitVecITE(256, storage.map[offset] != 0, storage.data[offset], value) + return value + + def get_code(self, address: int) -> Union[bytes, Array]: if address in self._code: return self._code[address] else: return self._underlay.get_code(address) - def get_blocknumber(self) -> Any: + def get_blocknumber(self) -> Union[int, BitVec]: if self._blocknumber is not None: return self._blocknumber else: return self._underlay.get_blocknumber() - def get_timestamp(self) -> Any: + def get_timestamp(self) -> Union[int, BitVec]: if self._timestamp is not None: return self._timestamp else: return self._underlay.get_timestamp() - def get_difficulty(self) -> Any: + def get_difficulty(self) -> Union[int, BitVec]: if self._difficulty is not None: return self._difficulty else: return self._underlay.get_difficulty() - def get_gaslimit(self) -> Any: + def get_gaslimit(self) -> Union[int, BitVec]: if self._gaslimit is not None: return self._gaslimit else: return self._underlay.get_gaslimit() - def get_coinbase(self) -> Any: + def get_coinbase(self) -> Union[int, BitVec]: if self._coinbase is not None: return self._coinbase else: @@ -279,36 +354,52 @@ def get_coinbase(self) -> Any: def delete_account(self, address: int): self._nonce[address] = DefaultWorldState().get_nonce(address) self._balance[address] = DefaultWorldState().get_balance(address) - self._storage[address] = DefaultWorldState().get_storage(address) + self._storage[address] = None self._code[address] = DefaultWorldState().get_code(address) self._deleted_accounts.add(address) - def set_nonce(self, address: int, value: Any): + def set_nonce(self, address: int, value: Union[int, BitVec]): self._nonce[address] = value self._deleted_accounts.discard(address) - def set_balance(self, address: int, value: Any): + def set_balance(self, address: int, value: Union[int, BitVec]): self._balance[address] = value self._deleted_accounts.discard(address) - def set_storage_data(self, address: int, offset: int, value: Any): - self._storage.setdefault(address, {})[offset] = value + def set_storage_data( + self, + constraints: ConstraintSet, + address: int, + offset: Union[int, BitVec], + value: Union[int, BitVec], + ): + storage = self._storage.get(address) + if storage is None: + storage = Storage(constraints, address) + self._storage[address] = storage + if storage.constraints != constraints: + logger.warning( + "constraints have changed: %s != %s", storage.constraints, constraints, + ) + storage.map[offset] = 1 + storage.data[offset] = value + storage.dirty = True self._deleted_accounts.discard(address) - def set_code(self, address: int, code: Any): + def set_code(self, address: int, code: Union[bytes, Array]): self._code[address] = code - def set_blocknumber(self, value: Any): + def set_blocknumber(self, value: Union[int, BitVec]): self._blocknumber = value - def set_timestamp(self, value: Any): + def set_timestamp(self, value: Union[int, BitVec]): self._timestamp = value - def set_difficulty(self, value: Any): + def set_difficulty(self, value: Union[int, BitVec]): self._difficulty = value - def set_gaslimit(self, value: Any): + def set_gaslimit(self, value: Union[int, BitVec]): self._gaslimit = value - def set_coinbase(self, value: Any): + def set_coinbase(self, value: Union[int, BitVec]): self._coinbase = value From d16736a7a743d86a335107486f5973dd4cf9a344 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 6 Jan 2020 19:26:56 +0000 Subject: [PATCH 005/104] Add typeguard to install_requires. --- setup.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/setup.py b/setup.py index cff84a0f7..862eea198 100644 --- a/setup.py +++ b/setup.py @@ -47,12 +47,13 @@ def rtd_dependent_deps(): "pyyaml", "wrapt", # evm dependencies - "pysha3", + "crytic-compile>=0.1.1", + "ply", "prettytable", "pyevmasm==0.2.0", + "pysha3", "rlp", - "ply", - "crytic-compile>=0.1.1", + "typeguard", "wasm", "web3", "dataclasses; python_version < '3.7'", From 6df79e69ccde21a517b6aab2d694be1b42932ce0 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 6 Jan 2020 20:06:20 +0000 Subject: [PATCH 006/104] Blacken. --- manticore/ethereum/manticore.py | 2 +- manticore/platforms/evm_world_state.py | 13 ++----------- 2 files changed, 3 insertions(+), 12 deletions(-) diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 482261611..7a9b41723 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -1,6 +1,6 @@ from typeguard.importhook import install_import_hook -install_import_hook('manticore') +install_import_hook("manticore") import copy import itertools diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 2e6b3f735..91ad55353 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -5,14 +5,7 @@ from urllib.parse import ParseResult, urlparse from web3 import Web3 # type: ignore from ..exceptions import EthereumError -from ..core.smtlib import ( - Array, - BitVec, - BitVecConstant, - BitVecITE, - BitVecZeroExtend, - ConstraintSet, -) +from ..core.smtlib import Array, BitVec, BitVecConstant, BitVecITE, BitVecZeroExtend, ConstraintSet logger = logging.getLogger(__name__) @@ -378,9 +371,7 @@ def set_storage_data( storage = Storage(constraints, address) self._storage[address] = storage if storage.constraints != constraints: - logger.warning( - "constraints have changed: %s != %s", storage.constraints, constraints, - ) + logger.warning("constraints have changed: %s != %s", storage.constraints, constraints) storage.map[offset] = 1 storage.data[offset] = value storage.dirty = True From 1b50ce028d461ebea56ee1ed3809b622e5be5ae3 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 6 Jan 2020 20:08:00 +0000 Subject: [PATCH 007/104] Better mypy integration. Thanks, @ekilmer. --- manticore/platforms/evm_world_state.py | 2 +- mypy.ini | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 91ad55353..805ff4203 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -3,7 +3,7 @@ from abc import ABC, abstractmethod from typing import Dict, Optional, Set, Union from urllib.parse import ParseResult, urlparse -from web3 import Web3 # type: ignore +from web3 import Web3 from ..exceptions import EthereumError from ..core.smtlib import Array, BitVec, BitVecConstant, BitVecITE, BitVecZeroExtend, ConstraintSet diff --git a/mypy.ini b/mypy.ini index f4c2c4bc7..15b1f84f6 100644 --- a/mypy.ini +++ b/mypy.ini @@ -42,3 +42,6 @@ ignore_missing_imports = True [mypy-wasm.*] ignore_missing_imports = True + +[mypy-web3.*] +ignore_missing_imports = True From 5afa862ea37e9dc6b85d66908c0f69371e353130 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 6 Jan 2020 20:13:17 +0000 Subject: [PATCH 008/104] More blackening. --- manticore/platforms/evm.py | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index ed3ed61a1..5a5dc7bb7 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -935,11 +935,7 @@ def _push(self, value): ITEM2 sp-> {empty} """ - assert ( - isinstance(value, int) - or isinstance(value, BitVec) - and value.size == 256 - ) + assert isinstance(value, int) or isinstance(value, BitVec) and value.size == 256 if len(self.stack) >= 1024: raise StackOverflow() @@ -2547,7 +2543,9 @@ def get_storage_data(self, storage_address: int, offset: int) -> Union[int, BitV value = self._world_state.get_storage_data(storage_address, offset) return simplify(value) - def set_storage_data(self, storage_address: int, offset: Union[int, BitVec], value: Union[int, BitVec]): + def set_storage_data( + self, storage_address: int, offset: Union[int, BitVec], value: Union[int, BitVec] + ): """ Writes a value to a storage slot in specified account @@ -2567,7 +2565,9 @@ def has_storage(self, address: int) -> bool: """ return self._world_state.has_storage(address) - def _get_storage(self, constraints: ConstraintSet, address: int) -> Union[Dict[int, int], Array]: + def _get_storage( + self, constraints: ConstraintSet, address: int + ) -> Union[Dict[int, int], Array]: """Private auxiliary function to retrieve the storage as an Array""" storage = self._world_state.get_storage(address) if isinstance(storage, dict): From 254c6c85a3e908ec3710fecec20fa9e2a597aa80 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 6 Jan 2020 20:34:59 +0000 Subject: [PATCH 009/104] Limit paths that typeguard checks. --- manticore/ethereum/manticore.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 7a9b41723..1255b2637 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -1,6 +1,7 @@ from typeguard.importhook import install_import_hook -install_import_hook("manticore") +install_import_hook("manticore.platforms.evm") +install_import_hook("manticore.platforms.evm_world_state") import copy import itertools From d58368c5dcdaa6cba9d415b5f654173279b05898 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 6 Jan 2020 22:26:15 +0000 Subject: [PATCH 010/104] Fix broken get_storage_data types. --- manticore/platforms/evm.py | 2 +- manticore/platforms/evm_world_state.py | 16 +++++++++++----- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 5a5dc7bb7..8a4f4be07 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2530,7 +2530,7 @@ def contract_accounts(self): def delete_account(self, address: int): self._world_state.delete_account(address) - def get_storage_data(self, storage_address: int, offset: int) -> Union[int, BitVec]: + def get_storage_data(self, storage_address: int, offset: Union[int, BitVec]) -> Union[int, BitVec]: """ Read a value from a storage slot on the specified account diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 805ff4203..6ce362baa 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -35,7 +35,7 @@ def get_storage(self, address: int) -> Union[Dict[int, int], Array]: pass @abstractmethod - def get_storage_data(self, address: int, offset: int) -> Union[int, BitVec]: + def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> Union[int, BitVec]: pass @abstractmethod @@ -82,7 +82,7 @@ def has_storage(self, address: int) -> bool: def get_storage(self, address: int) -> Dict[int, int]: return {} - def get_storage_data(self, address: int, offset: int) -> int: + def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> int: return 0 def get_code(self, address: int) -> bytes: @@ -176,7 +176,9 @@ def has_storage(self, address: int) -> bool: def get_storage(self, address) -> Dict[int, int]: raise NotImplementedError - def get_storage_data(self, address: int, offset: int) -> int: + def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> int: + if not isinstance(offset, int): + raise NotImplementedError return int.from_bytes(self._web3().eth.getStorageAt(_web3_address(address), offset), "big") def get_code(self, address: int) -> bytes: @@ -299,8 +301,12 @@ def get_storage(self, address: int) -> Union[Dict[int, int], Array]: data = storage.data return data - def get_storage_data(self, address: int, offset: int) -> Union[int, BitVec]: - value = self._underlay.get_storage_data(address, offset) + def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> Union[int, BitVec]: + value: Union[int, BitVec] = 0 + try: + value = self._underlay.get_storage_data(address, offset) + except NotImplementedError: + pass storage = self._storage.get(address) if storage is not None: if not isinstance(value, BitVec): From ffa39b7fa4ded18ca6043190c4242f5a040fdad9 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 6 Jan 2020 22:30:17 +0000 Subject: [PATCH 011/104] Blacken. --- manticore/platforms/evm.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 8a4f4be07..1692670f8 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2530,7 +2530,9 @@ def contract_accounts(self): def delete_account(self, address: int): self._world_state.delete_account(address) - def get_storage_data(self, storage_address: int, offset: Union[int, BitVec]) -> Union[int, BitVec]: + def get_storage_data( + self, storage_address: int, offset: Union[int, BitVec] + ) -> Union[int, BitVec]: """ Read a value from a storage slot on the specified account From 7d654aa52e692b3ff500bcc360f2a3544f6dfa89 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Tue, 7 Jan 2020 15:00:00 +0000 Subject: [PATCH 012/104] Revert some changes related to the callstack. --- manticore/platforms/evm.py | 79 +++++++++-------- manticore/platforms/evm_world_state.py | 113 ++++++++++++++----------- 2 files changed, 110 insertions(+), 82 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 1692670f8..a6841229b 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2270,7 +2270,10 @@ def __init__( world_state if world_state is not None else DefaultWorldState() ) self._constraints = constraints - self._callstack: List[Tuple[Transaction, List[EVMLog], WorldState, EVM]] = [] + self._callstack: List[ + Tuple[Transaction, List[EVMLog], Set[int], Optional[Storage], EVM] + ] = [] + self._deleted_accounts: Set[int] = set() self._logs: List[EVMLog] = list() self._pending_transaction = None self._transactions: List[Transaction] = list() @@ -2297,6 +2300,7 @@ def __getstate__(self): state["world_state"] = self._world_state state["constraints"] = self._constraints state["callstack"] = self._callstack + state["deleted_accounts"] = self._deleted_accounts state["transactions"] = self._transactions return state @@ -2305,11 +2309,12 @@ def __setstate__(self, state): self._constraints = state["constraints"] self._pending_transaction = state["pending_transaction"] self._world_state = state["world_state"] + self._deleted_accounts = state["deleted_accounts"] self._logs = state["logs"] self._callstack = state["callstack"] self._transactions = state["transactions"] - for _, _, _, vm in self._callstack: + for _, _, _, _, vm in self._callstack: self.forward_events_from(vm) def try_simplify_to_constant(self, data): @@ -2411,26 +2416,39 @@ def _open_transaction(self, sort, address, price, bytecode_or_data, caller, valu vm = EVM(self._constraints, address, data, caller, value, bytecode, world=self, gas=gas) self._publish("will_open_transaction", tx) - self._callstack.append((tx, self.logs, copy.copy(self._world_state), vm)) + self._callstack.append( + ( + tx, + self.logs, + self.deleted_accounts, + copy.copy(self._world_state.get_storage(address)), + vm, + ) + ) self.forward_events_from(vm) self._publish("did_open_transaction", tx) def _close_transaction(self, result, data=None, rollback=False): self._publish("will_close_transaction", self._callstack[-1][0]) - tx, logs, world_state, vm = self._callstack.pop() + tx, logs, deleted_accounts, account_storage, vm = self._callstack.pop() assert self.constraints == vm.constraints # Keep constraints gathered in the last vm self.constraints = vm.constraints if rollback: - self._world_state = world_state + self._world_state.set_storage(vm.address, account_storage) self._logs = logs self.send_funds(tx.address, tx.caller, tx.value) else: + self._deleted_accounts = deleted_accounts + # FIXME: BUG: a CREATE can be successful and still return an empty contract :shrug: if not issymbolic(tx.caller) and (tx.sort == "CREATE" or not self.get_code(tx.caller)): # Increment the nonce if this transaction created a contract, or if it was called by a non-contract account self.increase_nonce(tx.caller) + if tx.is_human: + for deleted_account in self._deleted_accounts: + self._world_state.delete_account(deleted_account) tx.set_result(result, data) self._transactions.append(tx) @@ -2477,7 +2495,7 @@ def last_human_transaction(self): def current_vm(self): """current vm""" try: - _, _, _, vm = self._callstack[-1] + _, _, _, _, vm = self._callstack[-1] return vm except IndexError: return None @@ -2486,7 +2504,7 @@ def current_vm(self): def current_transaction(self): """current tx""" try: - tx, _, _, _ = self._callstack[-1] + tx, _, _, _, _ = self._callstack[-1] if tx.result is not None: # That tx finished. No current tx. return None @@ -2498,7 +2516,7 @@ def current_transaction(self): def current_human_transaction(self): """Current ongoing human transaction""" try: - tx, _, _, _ = self._callstack[0] + tx, _, _, _, _ = self._callstack[0] if tx.result is not None: # That tx finished. No current tx. return None @@ -2527,8 +2545,13 @@ def contract_accounts(self): accs.append(address) return accs - def delete_account(self, address: int): - self._world_state.delete_account(address) + @property + def deleted_accounts(self): + return self._deleted_accounts + + def delete_account(self, address): + if address in self._world_state: + self._deleted_accounts.add(address) def get_storage_data( self, storage_address: int, offset: Union[int, BitVec] @@ -2567,28 +2590,18 @@ def has_storage(self, address: int) -> bool: """ return self._world_state.has_storage(address) - def _get_storage( - self, constraints: ConstraintSet, address: int - ) -> Union[Dict[int, int], Array]: - """Private auxiliary function to retrieve the storage as an Array""" + def _get_storage(self, constraints: ConstraintSet, address: int) -> Storage: + """Private auxiliary function to retrieve the storage""" storage = self._world_state.get_storage(address) - if isinstance(storage, dict): - array = constraints.new_array( - index_bits=256, - value_bits=256, - name=f"STORAGE_DATA_{address:x}", - avoid_collisions=True, - default=0, - ) - for key, value in storage.items(): - array[key] = value - storage = array + if storage is None: + storage = Storage(constraints, address) return storage - def _set_storage(self, address: int, storage: Dict[int, int]): - """Private auxiliary function to set the storage with a Dict[int, int]""" - for key, value in storage.items(): - self._world_state.set_storage_data(self.constraints, address, key, value) + def _set_storage(self, address: int, storage: Union[Dict[int, int], Optional[Storage]]): + """Private auxiliary function to replace the storage""" + if isinstance(storage, dict): + storage = Storage.fromDict(self.constraints, address, storage) + self._world_state.set_storage(address, storage) def get_nonce(self, address: int) -> Union[int, BitVec]: return self._world_state.get_nonce(address) @@ -2971,7 +2984,7 @@ def _process_pending_transaction(self): def dump(self, stream, state, mevm, message): from ..ethereum.manticore import calculate_coverage, flagged - blockchain = state.platform + blockchain: EVMWorld = state.platform last_tx = blockchain.last_transaction stream.write("Message: %s\n" % message) @@ -3010,7 +3023,7 @@ def dump(self, stream, state, mevm, message): stream.write("Balance: %d %s\n" % (balance, flagged(is_balance_symbolic))) storage = blockchain._get_storage(state.constraints, account_address) - stream.write("Storage: %s\n" % translate_to_smtlib(storage, use_bindings=False)) + stream.write("Storage: %s\n" % translate_to_smtlib(storage.data, use_bindings=False)) all_used_indexes = [] with state.constraints as temp_cs: @@ -3019,14 +3032,14 @@ def dump(self, stream, state, mevm, message): # get the storage for account_address storage = blockchain._get_storage(temp_cs, account_address) # we are interested only in used slots - temp_cs.add(storage.get(index) != 0) + temp_cs.add(storage.map.get(index) != 0) # Query the solver to get all storage indexes with used slots all_used_indexes = Z3Solver.instance().get_all_values(temp_cs, index) if all_used_indexes: stream.write("Storage:\n") for i in all_used_indexes: - value = storage.get(i) + value = storage.data.get(i) is_storage_symbolic = issymbolic(value) stream.write( "storage[%x] = %x %s\n" diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 6ce362baa..7f7524251 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -10,6 +10,42 @@ logger = logging.getLogger(__name__) +# sam.moelius: map records which (symbolic) offsets have been written to. data holds the values +# written. + + +class Storage: + def __init__(self, constraints: ConstraintSet, address: int): + self.constraints = constraints + self.map = constraints.new_array( + index_bits=256, + value_bits=1, + name=f"STORAGE_MAP_{address:x}", + avoid_collisions=True, + default=0, + ) + self.data = constraints.new_array( + index_bits=256, + value_bits=256, + name=f"STORAGE_DATA_{address:x}", + avoid_collisions=True, + default=0, + ) + self.dirty = False + + def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): + self.map[offset] = 1 + self.data[offset] = value + self.dirty = True + + @staticmethod + def fromDict(constraints: ConstraintSet, address: int, items: Dict[int, int]) -> "Storage": + storage = Storage(constraints, address) + for key, value in items.items(): + storage.set(key, value) + return storage + + #################################################################################################### @@ -31,7 +67,7 @@ def has_storage(self, address: int) -> bool: pass @abstractmethod - def get_storage(self, address: int) -> Union[Dict[int, int], Array]: + def get_storage(self, address: int) -> Optional[Storage]: pass @abstractmethod @@ -79,8 +115,8 @@ def get_balance(self, address: int) -> int: def has_storage(self, address: int) -> bool: return False - def get_storage(self, address: int) -> Dict[int, int]: - return {} + def get_storage(self, address: int) -> Optional[Storage]: + raise NotImplementedError def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> int: return 0 @@ -173,7 +209,7 @@ def get_balance(self, address: int) -> int: def has_storage(self, address: int) -> bool: raise NotImplementedError - def get_storage(self, address) -> Dict[int, int]: + def get_storage(self, address) -> Storage: raise NotImplementedError def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> int: @@ -203,30 +239,6 @@ def get_coinbase(self) -> int: #################################################################################################### -# sam.moelius: map records which (symbolic) offsets have been written to. data holds the values -# written. - - -class Storage: - def __init__(self, constraints: ConstraintSet, address: int): - self.constraints = constraints - self.map = constraints.new_array( - index_bits=256, - value_bits=1, - name=f"STORAGE_MAP_{address:x}", - avoid_collisions=True, - default=0, - ) - self.data = constraints.new_array( - index_bits=256, - value_bits=256, - name=f"STORAGE_DATA_{address:x}", - avoid_collisions=True, - default=0, - ) - self.dirty = False - - # sam.moelius: If we decide to cache results returned from a RemoteWorldState, then they should NOT # be cached within an overlay. The reason is that this could affect the results of subsequent # operations. Consider a call to get_storage_data followed by a call to has_storage. If nothing @@ -241,7 +253,7 @@ def __init__(self, underlay: WorldState): self._deleted_accounts: Set[int] = set() self._nonce: Dict[int, Union[int, BitVec]] = {} self._balance: Dict[int, Union[int, BitVec]] = {} - self._storage: Dict[int, Optional[Storage]] = {} + self._storage: Dict[int, Storage] = {} self._code: Dict[int, Union[bytes, Array]] = {} self._blocknumber: Optional[Union[int, BitVec]] = None self._timestamp: Optional[Union[int, BitVec]] = None @@ -261,7 +273,7 @@ def accounts(self) -> Set[int]: | self._balance.keys() | self._storage.keys() | self._code.keys() - ) - self._deleted_accounts + ) def get_nonce(self, address: int) -> Union[int, BitVec]: if address in self._nonce: @@ -286,27 +298,27 @@ def has_storage(self, address: int) -> bool: dirty = dirty or storage.dirty return dirty - def get_storage(self, address: int) -> Union[Dict[int, int], Array]: - data: Union[Dict[int, int], Array] = {} + def get_storage(self, address: int) -> Optional[Storage]: + storage = None try: - data = self._underlay.get_storage(address) + storage = self._underlay.get_storage(address) except NotImplementedError: pass - storage = self._storage.get(address) + # sam.moelius: Rightfully, the overlay's storage should be merged into the underlay's + # storage. However, this is not currently implemented. if storage is not None: - # sam.moelius: Merging the overlay's storage into the underlay's storage is not - # currently implemented. - if not isinstance(data, dict) or len(data) > 0: - raise NotImplementedError - data = storage.data - return data + raise NotImplementedError + storage = self._storage.get(address) + return storage def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> Union[int, BitVec]: value: Union[int, BitVec] = 0 - try: - value = self._underlay.get_storage_data(address, offset) - except NotImplementedError: - pass + # sam.moelius: If the account was ever deleted, then ignore the underlay's storage. + if not address in self._deleted_accounts: + try: + value = self._underlay.get_storage_data(address, offset) + except NotImplementedError: + pass storage = self._storage.get(address) if storage is not None: if not isinstance(value, BitVec): @@ -350,20 +362,24 @@ def get_coinbase(self) -> Union[int, BitVec]: else: return self._underlay.get_coinbase() - def delete_account(self, address: int): + def delete_account(self, constraints: ConstraintSet, address: int): self._nonce[address] = DefaultWorldState().get_nonce(address) self._balance[address] = DefaultWorldState().get_balance(address) - self._storage[address] = None + self._storage[address] = Storage(constraints, address) self._code[address] = DefaultWorldState().get_code(address) self._deleted_accounts.add(address) def set_nonce(self, address: int, value: Union[int, BitVec]): self._nonce[address] = value - self._deleted_accounts.discard(address) def set_balance(self, address: int, value: Union[int, BitVec]): self._balance[address] = value - self._deleted_accounts.discard(address) + + def set_storage(self, address: int, storage: Optional[Storage]): + if storage is None: + del self._storage[address] + else: + self._storage[address] = storage def set_storage_data( self, @@ -381,7 +397,6 @@ def set_storage_data( storage.map[offset] = 1 storage.data[offset] = value storage.dirty = True - self._deleted_accounts.discard(address) def set_code(self, address: int, code: Union[bytes, Array]): self._code[address] = code From 46f7a3038b3280422d91b0b6a36efd18ec68dfe4 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Tue, 7 Jan 2020 15:14:53 +0000 Subject: [PATCH 013/104] Delete accounts unconditionally. --- manticore/platforms/evm.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index a6841229b..161992afd 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2550,8 +2550,7 @@ def deleted_accounts(self): return self._deleted_accounts def delete_account(self, address): - if address in self._world_state: - self._deleted_accounts.add(address) + self._deleted_accounts.add(address) def get_storage_data( self, storage_address: int, offset: Union[int, BitVec] From b1a82f73006bc47dad2a0c2d13a270a1d4fcc471 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Tue, 7 Jan 2020 16:02:10 +0000 Subject: [PATCH 014/104] Do not throw an exception if deleted account is not in dictionary. --- manticore/platforms/evm_world_state.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 7f7524251..46201b9e4 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -377,7 +377,7 @@ def set_balance(self, address: int, value: Union[int, BitVec]): def set_storage(self, address: int, storage: Optional[Storage]): if storage is None: - del self._storage[address] + self._storage.pop(address, None) else: self._storage[address] = storage From d40d143c56b37f765a28316d68c7ff38259acb60 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 8 Jan 2020 02:54:51 +0000 Subject: [PATCH 015/104] Add constraint argument to delete_account call. --- manticore/platforms/evm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 161992afd..0c8ed6b03 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2448,7 +2448,7 @@ def _close_transaction(self, result, data=None, rollback=False): if tx.is_human: for deleted_account in self._deleted_accounts: - self._world_state.delete_account(deleted_account) + self._world_state.delete_account(self.constraints, deleted_account) tx.set_result(result, data) self._transactions.append(tx) From 043f9c0db60c727966a7ffdde6ddd5a43d2c003f Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 8 Jan 2020 09:59:56 +0000 Subject: [PATCH 016/104] Back out typeguard. --- manticore/ethereum/manticore.py | 5 ----- setup.py | 7 +++---- 2 files changed, 3 insertions(+), 9 deletions(-) diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 1255b2637..478e112d1 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -1,8 +1,3 @@ -from typeguard.importhook import install_import_hook - -install_import_hook("manticore.platforms.evm") -install_import_hook("manticore.platforms.evm_world_state") - import copy import itertools import binascii diff --git a/setup.py b/setup.py index 862eea198..cff84a0f7 100644 --- a/setup.py +++ b/setup.py @@ -47,13 +47,12 @@ def rtd_dependent_deps(): "pyyaml", "wrapt", # evm dependencies - "crytic-compile>=0.1.1", - "ply", + "pysha3", "prettytable", "pyevmasm==0.2.0", - "pysha3", "rlp", - "typeguard", + "ply", + "crytic-compile>=0.1.1", "wasm", "web3", "dataclasses; python_version < '3.7'", From 5a66521feefc6add81999050d39a53b737c232d5 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 8 Jan 2020 10:02:25 +0000 Subject: [PATCH 017/104] Use "not in". --- manticore/platforms/evm_world_state.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 46201b9e4..142fdbaa5 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -314,7 +314,7 @@ def get_storage(self, address: int) -> Optional[Storage]: def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> Union[int, BitVec]: value: Union[int, BitVec] = 0 # sam.moelius: If the account was ever deleted, then ignore the underlay's storage. - if not address in self._deleted_accounts: + if address not in self._deleted_accounts: try: value = self._underlay.get_storage_data(address, offset) except NotImplementedError: From 9eff25486b3731ee03aa27be3aa8b92c041aefd1 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 8 Jan 2020 10:47:05 +0000 Subject: [PATCH 018/104] Fix minor indentation issue in ci.yml. --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 43e836083..2de06c090 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -206,7 +206,7 @@ jobs: run_tests_from_dir $TEST_TYPE RV=$? - echo "Running truffle test" + echo "Running truffle test" install_truffle run_truffle_tests RV=$(($RV + $?)) From 081f4b45753037273a33819da78e5a8a8f2dec86 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 8 Jan 2020 14:21:45 +0000 Subject: [PATCH 019/104] "fromDict" -> "from_dict". --- manticore/platforms/evm.py | 2 +- manticore/platforms/evm_world_state.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 0c8ed6b03..bfd90e446 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2599,7 +2599,7 @@ def _get_storage(self, constraints: ConstraintSet, address: int) -> Storage: def _set_storage(self, address: int, storage: Union[Dict[int, int], Optional[Storage]]): """Private auxiliary function to replace the storage""" if isinstance(storage, dict): - storage = Storage.fromDict(self.constraints, address, storage) + storage = Storage.from_dict(self.constraints, address, storage) self._world_state.set_storage(address, storage) def get_nonce(self, address: int) -> Union[int, BitVec]: diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 142fdbaa5..a1bb68f40 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -39,7 +39,7 @@ def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): self.dirty = True @staticmethod - def fromDict(constraints: ConstraintSet, address: int, items: Dict[int, int]) -> "Storage": + def from_dict(constraints: ConstraintSet, address: int, items: Dict[int, int]) -> "Storage": storage = Storage(constraints, address) for key, value in items.items(): storage.set(key, value) From bc0cb7089e7f7aa6366c66fc15109e2527fa6532 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 9 Jan 2020 13:42:15 +0000 Subject: [PATCH 020/104] Add (failing) test_gas_check. --- tests/ethereum/test_general.py | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index ebf604ef2..385bea356 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -1655,13 +1655,35 @@ def test_delegatecall_env(self): 100000000000000000000000 - 10, ) - # checl delegated call storage was not touch + # check delegated call storage was not touch self.assertFalse(world.has_storage(0x111111111111111111111111111111111111111)) self.assertEqual(world.get_storage_data(0x111111111111111111111111111111111111111, 0), 0) self.assertEqual(world.get_storage_data(0x111111111111111111111111111111111111111, 1), 0) self.assertEqual(world.get_storage_data(0x111111111111111111111111111111111111111, 2), 0) self.assertFalse(world.has_storage(0x333333333333333333333333333333333333333)) + def test_gas_check(self): + constraints = ConstraintSet() + world = evm.EVMWorld(constraints) + asm_acc = """ PUSH1 0x0 + SELFDESTRUCT + """ + world.create_account( + address=0x111111111111111111111111111111111111111, code=EVMAsm.assemble(asm_acc) + ) + world.create_account(address=0x222222222222222222222222222222222222222) + world.transaction( + 0x111111111111111111111111111111111111111, + caller=0x222222222222222222222222222222222222222, + gas=5003, + ) + try: + while True: + world.execute() + except TerminateState as e: + result = str(e) + self.assertEqual(result, "SELFDESTRUCT") + class EthPluginTests(unittest.TestCase): def test_FilterFunctions_fallback_function_matching(self): From 32a19ea5d106078f51cd068d1275cd4e56f5ebfa Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 9 Jan 2020 14:26:25 +0000 Subject: [PATCH 021/104] Fix gas check. --- manticore/platforms/evm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 774171fe6..3ea508701 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -991,7 +991,7 @@ def _consume(self, fee): # gas is faithfully accounted and ogg checked at instruction/BB level. if consts.oog == "pedantic" or self.instruction.is_terminator: # explore both options / fork - constraint = simplify(Operators.UGT(self._gas, fee)) + constraint = simplify(Operators.UGE(self._gas, fee)) # FIXME if gas can be both enough and insufficient this will # reenter here and generate redundant queries From 8b0a5ef504f2dea4d7483c6cc8b3d0e6b2ae9ddb Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 9 Jan 2020 18:37:00 +0000 Subject: [PATCH 022/104] Use Storage.set in set_storage_data. --- manticore/platforms/evm_world_state.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index a1bb68f40..eee3e7cc5 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -394,9 +394,7 @@ def set_storage_data( self._storage[address] = storage if storage.constraints != constraints: logger.warning("constraints have changed: %s != %s", storage.constraints, constraints) - storage.map[offset] = 1 - storage.data[offset] = value - storage.dirty = True + storage.set(offset, value) def set_code(self, address: int, code: Union[bytes, Array]): self._code[address] = code From e18fd7c125cb163080bd183ffa1eaf7c243abad4 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 9 Jan 2020 19:42:28 +0000 Subject: [PATCH 023/104] Consider BitVecConstant not symbolic in dump. --- manticore/platforms/evm.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index d4c0aead8..484ca9cd0 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -3038,8 +3038,10 @@ def dump(self, stream, state, mevm, message): if all_used_indexes: stream.write("Storage:\n") for i in all_used_indexes: - value = storage.data.get(i) - is_storage_symbolic = issymbolic(value) + value = simplify(storage.data.get(i)) + is_storage_symbolic = issymbolic(value) and not isinstance( + value, BitVecConstant + ) stream.write( "storage[%x] = %x %s\n" % (state.solve_one(i), state.solve_one(value), flagged(is_storage_symbolic)) From 912366bd85190c68c08ea22be04c7d3de44402a4 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 9 Jan 2020 20:29:59 +0000 Subject: [PATCH 024/104] Add tests. --- tests/ethereum/test_general.py | 61 ++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 385bea356..9d061590d 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -1,6 +1,7 @@ import binascii import unittest from contextlib import contextmanager +from io import StringIO from pathlib import Path import os @@ -30,6 +31,7 @@ from manticore.ethereum.plugins import FilterFunctions from manticore.ethereum.solidity import SolidityMetadata from manticore.platforms import evm +from manticore.platforms.evm_world_state import * from manticore.platforms.evm import EVMWorld, ConcretizeArgument, concretized_args, Return, Stop from manticore.utils.deprecated import ManticoreDeprecationWarning @@ -1305,6 +1307,62 @@ def test_preconstraints(self): self.assertListEqual(sorted(results), ["STOP"] * 2 + ["TXERROR"]) +class EthWorldStateTests(unittest.TestCase): + class CustomWorldState(WorldState): + pass + + def test_custom_world_state(self): + world_state = EthWorldStateTests.CustomWorldState() + m = ManticoreEVM(world_state=world_state) + self.assertIsInstance(m.world._world_state, OverlayWorldState) + # sam.moelius: You cannot use assertEqual because the world may be have been deserialized. + self.assertIsInstance(m.world._world_state._underlay, EthWorldStateTests.CustomWorldState) + + def test_init_blocknumber(self): + constraints = ConstraintSet() + self.assertEqual(evm.EVMWorld(constraints).block_number(), 4370000) + self.assertEqual(evm.EVMWorld(constraints, blocknumber=4370001).block_number(), 4370001) + + def test_init_timestamp(self): + constraints = ConstraintSet() + self.assertEqual(evm.EVMWorld(constraints).block_timestamp(), 1524785992) + self.assertEqual( + evm.EVMWorld(constraints, timestamp=1524785993).block_timestamp(), 1524785993 + ) + + def test_init_difficulty(self): + constraints = ConstraintSet() + self.assertEqual(evm.EVMWorld(constraints).block_difficulty(), 0) + self.assertEqual(evm.EVMWorld(constraints, difficulty=1).block_difficulty(), 1) + + def test_init_gaslimit(self): + constraints = ConstraintSet() + self.assertEqual(evm.EVMWorld(constraints).block_gaslimit(), 0) + self.assertEqual(evm.EVMWorld(constraints, gaslimit=1).block_gaslimit(), 1) + + def test_init_coinbase(self): + constraints = ConstraintSet() + self.assertEqual(evm.EVMWorld(constraints).block_coinbase(), 0) + self.assertEqual( + evm.EVMWorld( + constraints, coinbase=0x111111111111111111111111111111111111111 + ).block_coinbase(), + 0x111111111111111111111111111111111111111, + ) + + def test_dump(self): + m = ManticoreEVM() + address = int(m.create_account()) + self.assertEqual(len([x for x in m.ready_states]), 1) + for state in m.ready_states: + xx = state.constraints.new_bitvec(256, name="x") + state.constraints.add(xx == 0x20) + m.world.set_storage_data(address, xx, 1) + output = StringIO() + m.world.dump(output, state, m, "") + self.assertIn("storage[20] = 1", output.getvalue()) + + class EthHelpersTest(unittest.TestCase): def setUp(self): self.bv = BitVec(256) @@ -1671,6 +1729,8 @@ def test_gas_check(self): world.create_account( address=0x111111111111111111111111111111111111111, code=EVMAsm.assemble(asm_acc) ) + self.assertIn(0x111111111111111111111111111111111111111, world) + self.assertTrue(world.has_code(0x111111111111111111111111111111111111111)) world.create_account(address=0x222222222222222222222222222222222222222) world.transaction( 0x111111111111111111111111111111111111111, @@ -1683,6 +1743,7 @@ def test_gas_check(self): except TerminateState as e: result = str(e) self.assertEqual(result, "SELFDESTRUCT") + self.assertFalse(world.has_code(0x111111111111111111111111111111111111111)) class EthPluginTests(unittest.TestCase): From eec85f9e41fc4d38fca83c9ac616883f558d0d0c Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 13:31:55 +0000 Subject: [PATCH 025/104] Do not thrown an exception when "evm.trace" is not present. --- manticore/platforms/evm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 484ca9cd0..0d9ac6045 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -3056,7 +3056,7 @@ def dump(self, stream, state, mevm, message): runtime_trace = set( ( pc - for contract, pc, at_init in state.context["evm.trace"] + for contract, pc, at_init in state.context.get("evm.trace", []) if address == contract and not at_init ) ) From 51d4494743a40e2d822f0a39e21718e18cc773b2 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 13:35:13 +0000 Subject: [PATCH 026/104] Reduce Storage warnings. --- manticore/platforms/evm_world_state.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index eee3e7cc5..e7ba8d402 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -17,6 +17,7 @@ class Storage: def __init__(self, constraints: ConstraintSet, address: int): self.constraints = constraints + self.warned = False self.map = constraints.new_array( index_bits=256, value_bits=1, @@ -393,7 +394,9 @@ def set_storage_data( storage = Storage(constraints, address) self._storage[address] = storage if storage.constraints != constraints: - logger.warning("constraints have changed: %s != %s", storage.constraints, constraints) + if not storage.warned: + logger.warning("Constraints have changed") + storage.warned = True storage.set(offset, value) def set_code(self, address: int, code: Union[bytes, Array]): From 566620ee29cefdac2bacb6ede43919830616ad21 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 13:35:53 +0000 Subject: [PATCH 027/104] Address Web3 forking bug. If appears that if a process creates a WebsocketProvider and then forks, the child process does not create a new "thread loop" for its own WebsocketProvider. The present commit addresses this issue. --- manticore/platforms/evm_world_state.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index e7ba8d402..68755b364 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -178,6 +178,9 @@ def __init__(self, url: str): self._url = url def _web3(self) -> Web3: + # sam.moelius: Force WebsocketProvider.__init__ to call _get_threaded_loop. The existing + # "threaded loop" could be leftover from a fork, in which case it will not work. + Web3.WebsocketProvider._loop = None web3 = Web3(Web3.WebsocketProvider("ws://" + self._url)) blocknumber = web3.eth.blockNumber endpoint = _endpoints.get(self._url) From a1d5cddb243eceaa5af3f8e009d2ab590133b81c Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 13:46:31 +0000 Subject: [PATCH 028/104] Use count_ready_states in test_dump. --- tests/ethereum/test_general.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 9d061590d..42d6a7fe1 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -1353,7 +1353,7 @@ def test_init_coinbase(self): def test_dump(self): m = ManticoreEVM() address = int(m.create_account()) - self.assertEqual(len([x for x in m.ready_states]), 1) + self.assertEqual(m.count_ready_states(), 1) for state in m.ready_states: xx = state.constraints.new_bitvec(256, name="x") state.constraints.add(xx == 0x20) From 80c0f1f9875506dd91c8c68a0e3769fa84e5db56 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 13:48:31 +0000 Subject: [PATCH 029/104] Add command line arguments. --- manticore/__main__.py | 9 +++++++++ manticore/ethereum/cli.py | 8 +++++++- manticore/ethereum/manticore.py | 23 +++++++++++++---------- 3 files changed, 29 insertions(+), 11 deletions(-) diff --git a/manticore/__main__.py b/manticore/__main__.py index abb142d26..c65ca0f4b 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -162,6 +162,8 @@ def positive(value): "--txnoether", action="store_true", help="Do not attempt to send ether to contract" ) + eth_flags.add_argument("--txvictim", type=str, help="Address of a deployed contract to attack") + eth_flags.add_argument( "--txaccount", type=str, @@ -180,6 +182,13 @@ def positive(value): "--contract", type=str, help="Contract name to analyze in case of multiple contracts" ) + eth_flags.add_argument( + "--rpc", + type=str, + dest="url", + help="Url of an Ethereum node to connect to. Must be of the form 'IP:PORT'", + ) + eth_detectors = parser.add_argument_group("Ethereum detectors") eth_detectors.add_argument( diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index a064587a9..9974988d3 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -17,6 +17,7 @@ from ..core.plugin import Profiler from .manticore import ManticoreEVM from .plugins import FilterFunctions, LoopDepthLimiter, VerboseTrace, KeepOnlyIfStorageChanges +from ..platforms.evm_world_state import RemoteWorldState from ..utils.nointerrupt import WithKeyboardInterruptAs from ..utils import config @@ -70,7 +71,11 @@ def choose_detectors(args): def ethereum_main(args, logger): - m = ManticoreEVM(workspace_url=args.workspace) + world_state = None + if args.url is not None: + world_state = RemoteWorldState(args.url) + + m = ManticoreEVM(workspace_url=args.workspace, world_state=world_state) if args.quick_mode: args.avoid_constant = True @@ -114,6 +119,7 @@ def ethereum_main(args, logger): tx_limit=args.txlimit, tx_use_coverage=not args.txnocoverage, tx_send_ether=not args.txnoether, + contract_account=int(args.txvictim, base=0), tx_account=args.txaccount, tx_preconstrain=args.txpreconstrain, compile_args=vars(args), # FIXME diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 478e112d1..6fb0991d9 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -993,6 +993,7 @@ def multi_tx_analysis( tx_limit=None, tx_use_coverage=True, tx_send_ether=True, + contract_account: int = None, tx_account="attacker", tx_preconstrain=False, args=None, @@ -1000,16 +1001,18 @@ def multi_tx_analysis( ): owner_account = self.create_account(balance=1000, name="owner") attacker_account = self.create_account(balance=1000, name="attacker") - # Pretty print - logger.info("Starting symbolic create contract") - - contract_account = self.solidity_create_contract( - solidity_filename, - contract_name=contract_name, - owner=owner_account, - args=args, - compile_args=compile_args, - ) + + if contract_account is None: + # Pretty print + logger.info("Starting symbolic create contract") + + contract_account = self.solidity_create_contract( + solidity_filename, + contract_name=contract_name, + owner=owner_account, + args=args, + compile_args=compile_args, + ) if tx_account == "attacker": tx_account = [attacker_account] From ca7d2154c1bf2f9ffc270183fc79a99a7045508f Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 15:42:51 +0000 Subject: [PATCH 030/104] Run truffle tests with ganache-cli as the backend. --- .github/workflows/ci.yml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2de06c090..217a4e1da 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -145,20 +145,26 @@ jobs: cd $DIR } - install_truffle(){ + install_node_packages(){ curl -o- https://raw.githubusercontent.com/creationix/nvm/v0.34.0/install.sh | bash source ~/.nvm/nvm.sh nvm install --lts nvm use --lts - npm install -g truffle + npm install -g ganache-cli truffle } run_truffle_tests(){ mkdir truffle_tests cd truffle_tests truffle unbox metacoin - manticore . --contract MetaCoin --workspace output + ADDITIONAL_ARGS="" + if [ "$1" = "deploy" ]; then + ganache-cli -p 7545 -i 5777 & + ADDRESS="$(truffle deploy | grep '> contract address:.*' | tail -n 1 | grep -o '0x.*$')" + ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txvictim $ADDRESS" + fi + manticore . --contract MetaCoin --workspace output $ADDITIONAL_ARGS ### The original comment says we should get 41 states, but after implementing the shift ### insructions, we get 31. Was the original comment a typo? @@ -207,8 +213,9 @@ jobs: RV=$? echo "Running truffle test" - install_truffle + install_node_packages run_truffle_tests + run_truffle_tests deploy RV=$(($RV + $?)) ;; wasm) From 244554ad732755a82f5af7cc20289f9f3d6d6243 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 17:05:20 +0000 Subject: [PATCH 031/104] Don't try to convert None to an int. --- manticore/ethereum/cli.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index 9974988d3..c677e428f 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -113,13 +113,17 @@ def ethereum_main(args, logger): logger.info("Beginning analysis") with m.kill_timeout(): + contract_account = None + if args.txvictim is not None: + contract_account = int(args.txvictim, base=0) + m.multi_tx_analysis( args.argv[0], contract_name=args.contract, tx_limit=args.txlimit, tx_use_coverage=not args.txnocoverage, tx_send_ether=not args.txnoether, - contract_account=int(args.txvictim, base=0), + contract_account=contract_account, tx_account=args.txaccount, tx_preconstrain=args.txpreconstrain, compile_args=vars(args), # FIXME From 9c871cb974d668bd5b07798a1c1999054430ecc8 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 17:10:52 +0000 Subject: [PATCH 032/104] Separate out truffle tests. --- .github/workflows/ci.yml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 217a4e1da..73fab0d0a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -34,7 +34,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - type: ["examples", "ethereum", "ethereum_bench", "ethereum_vm", "native", "wasm", "wasm_sym", "other"] + type: ["examples", "ethereum", "ethereum_bench", "ethereum_truffle", "ethereum_vm", "native", "wasm", "wasm_sym", "other"] steps: - uses: actions/checkout@v1 - name: Set up Python 3.6 @@ -206,18 +206,20 @@ jobs: # Test type case $TEST_TYPE in - ethereum_vm) - make_vmtests - echo "Running only the tests from 'tests/$TEST_TYPE' directory" - run_tests_from_dir $TEST_TYPE - RV=$? - + ethereum_truffle) echo "Running truffle test" install_node_packages run_truffle_tests + RV=$? run_truffle_tests deploy RV=$(($RV + $?)) ;; + ethereum_vm) + make_vmtests + echo "Running only the tests from 'tests/$TEST_TYPE' directory" + run_tests_from_dir $TEST_TYPE + RV=$? + ;; wasm) make_wasm_tests echo "Running only the tests from 'tests/$TEST_TYPE' directory" @@ -248,6 +250,8 @@ jobs: RV=$(($RV + $?)) run_tests_from_dir ethereum RV=$(($RV + $?)) + run_tests_from_dir ethereum_truffle + RV=$(($RV + $?)) make_vmtests; run_tests_from_dir ethereum_vm RV=$(($RV + $?)) make_wasm_tests; run_tests_from_dir wasm From 468036ee95eefa474b8d5e6ea9c46feadada8757 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 17:34:02 +0000 Subject: [PATCH 033/104] Add '-p' to mkdir, and clean-up properly otherwise. --- .github/workflows/ci.yml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 73fab0d0a..d4edb551e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -155,7 +155,7 @@ jobs: } run_truffle_tests(){ - mkdir truffle_tests + mkdir -p truffle_tests cd truffle_tests truffle unbox metacoin ADDITIONAL_ARGS="" @@ -172,8 +172,11 @@ jobs: # but Manticore fails to explore the paths due to the lack of the 0x1f opcode support # see https://github.com/trailofbits/manticore/issues/1166 # if [ "$(ls output/*tx -l | wc -l)" != "41" ]; then - if [ "$(ls output/*tx -l | wc -l)" != "13" ]; then - echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 13" + N="$(ls output/*tx -l | wc -l)" + rm -rf output + if [ "$N" != "13" ]; then + echo "Truffle test failed: $N != 13" + cd .. return 1 fi echo "Truffle test succeded" @@ -207,7 +210,7 @@ jobs: # Test type case $TEST_TYPE in ethereum_truffle) - echo "Running truffle test" + echo "Running truffle tests" install_node_packages run_truffle_tests RV=$? From 6c1509364239f3f05b78d3d51daef7e6c13e2bb5 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 17:44:22 +0000 Subject: [PATCH 034/104] Don't try to unbox over an already unboxed truffle box. --- .github/workflows/ci.yml | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d4edb551e..be28425c5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -155,9 +155,6 @@ jobs: } run_truffle_tests(){ - mkdir -p truffle_tests - cd truffle_tests - truffle unbox metacoin ADDITIONAL_ARGS="" if [ "$1" = "deploy" ]; then ganache-cli -p 7545 -i 5777 & @@ -176,11 +173,9 @@ jobs: rm -rf output if [ "$N" != "13" ]; then echo "Truffle test failed: $N != 13" - cd .. return 1 fi echo "Truffle test succeded" - cd .. return 0 } @@ -212,10 +207,11 @@ jobs: ethereum_truffle) echo "Running truffle tests" install_node_packages - run_truffle_tests + mkdir truffle_tests + cd truffle_tests + truffle unbox metacoin + run_truffle_tests && run_truffle_tests deploy RV=$? - run_truffle_tests deploy - RV=$(($RV + $?)) ;; ethereum_vm) make_vmtests From 920d28d83e5fd6c430ea4843a08c8c82452adc47 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 19:12:03 +0000 Subject: [PATCH 035/104] Remove unused import in evm_world_state.py. --- manticore/platforms/evm_world_state.py | 1 - 1 file changed, 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 68755b364..4ed037e36 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -1,5 +1,4 @@ import logging -import os from abc import ABC, abstractmethod from typing import Dict, Optional, Set, Union from urllib.parse import ParseResult, urlparse From 3f1574700a3ecc5a7f4926575280d6c44600e2b5 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 19:14:53 +0000 Subject: [PATCH 036/104] Remove unused imports from test_general.py. --- tests/ethereum/test_general.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 42d6a7fe1..d01f9ccf6 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -31,7 +31,7 @@ from manticore.ethereum.plugins import FilterFunctions from manticore.ethereum.solidity import SolidityMetadata from manticore.platforms import evm -from manticore.platforms.evm_world_state import * +from manticore.platforms.evm_world_state import OverlayWorldState, WorldState from manticore.platforms.evm import EVMWorld, ConcretizeArgument, concretized_args, Return, Stop from manticore.utils.deprecated import ManticoreDeprecationWarning From 4944d6748bae8cd1ecec04a51a1d377d7f73392f Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 10 Jan 2020 19:37:07 +0000 Subject: [PATCH 037/104] Simplify ci.yml Remove the "all" option. Make the error message a little more intuitive. --- .github/workflows/ci.yml | 25 +------------------------ 1 file changed, 1 insertion(+), 24 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2de06c090..2179d5b9d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -227,34 +227,11 @@ jobs: run_tests_from_dir $TEST_TYPE RV=$? ;; - examples) run_examples ;; - - all) - echo "Running all tests registered in travis_test.sh: examples, native, ethereum, ethereum_vm, other"; - - # Functions should return 0 on success and 1 on failure - RV=0 - run_tests_from_dir native - RV=$(($RV + $?)) - run_tests_from_dir ethereum - RV=$(($RV + $?)) - make_vmtests; run_tests_from_dir ethereum_vm - RV=$(($RV + $?)) - make_wasm_tests; run_tests_from_dir wasm - RV=$(($RV + $?)) - make_wasm_sym_tests; run_tests_from_dir wasm_sym - RV=$(($RV + $?)) - run_tests_from_dir other - RV=$(($RV + $?)) - run_examples - RV=$(($RV + $?)) - ;; - *) - echo "Usage: $0 [examples|native|ethereum|ethereum_vm|other|all]" + echo "Unknown TEST_TYPE: '$TEST_TYPE'" exit 3; ;; esac From d298c19fab2e22a7c393df0bb214ced457d33dd3 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 13 Jan 2020 00:56:05 +0000 Subject: [PATCH 038/104] Remove unnecessary assignment in _web3. --- manticore/platforms/evm_world_state.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 4ed037e36..bcdbe19b4 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -190,14 +190,12 @@ def _web3(self) -> Web3: if endpoint.blocknumber != blocknumber: if not endpoint.warned: logger.warning( - "%s blocknumber has changed: %d != %d---someone is using the endpoint" - + " beside us", + "%s blocknumber has changed: %d != %d---someone is using the endpoint beside us", self._url, endpoint.blocknumber, blocknumber, ) endpoint.warned = True - endpoint.blocknumber = blocknumber return web3 def accounts(self) -> Set[int]: From 72c95b617eeeab0fe6601668328d0f955aaf8914 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 13 Jan 2020 00:57:19 +0000 Subject: [PATCH 039/104] Do not enable uninitialized storage detector when using RPC. It generates too much noise. --- manticore/ethereum/cli.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index c677e428f..12a306623 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -63,6 +63,9 @@ def choose_detectors(args): f"{e} is not a detector name, must be one of {arguments}. See also `--list-detectors`." ) + if args.url is not None: + exclude.append(DetectUninitializedStorage.ARGUMENT) + for arg, detector_cls in detectors.items(): if arg not in exclude: detectors_to_run.append(detector_cls) From 758e8c77c30c3744419c56e51eec4914da6250f2 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 15 Apr 2020 13:40:52 +0000 Subject: [PATCH 040/104] Typo. --- manticore/platforms/evm_world_state.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index bcdbe19b4..130d3d502 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -190,7 +190,7 @@ def _web3(self) -> Web3: if endpoint.blocknumber != blocknumber: if not endpoint.warned: logger.warning( - "%s blocknumber has changed: %d != %d---someone is using the endpoint beside us", + "%s blocknumber has changed: %d != %d---someone is using the endpoint besides us", self._url, endpoint.blocknumber, blocknumber, From 053b393c34d37d86af8324fd7aed2558624eae36 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 15 Apr 2020 13:43:32 +0000 Subject: [PATCH 041/104] Do not require argv[0] when --rpc and --txvictim are given. --- manticore/__main__.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/manticore/__main__.py b/manticore/__main__.py index c65ca0f4b..582fae765 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -38,7 +38,7 @@ def main(): set_verbosity(args.v) - if args.argv[0].endswith(".sol") or is_supported(args.argv[0]): + if args.url is not None or args.argv[0].endswith(".sol") or is_supported(args.argv[0]): ethereum_main(args, logger) elif args.argv[0].endswith(".wasm") or args.argv[0].endswith(".wat"): wasm_main(args, logger) @@ -248,6 +248,9 @@ def positive(value): parsed = parser.parse_args(sys.argv[1:]) config.process_config_values(parser, parsed) + if parsed.url is not None and parsed.txvictim is not None and not parsed.argv: + parsed.argv = [None] + if not parsed.argv: print(parser.format_usage() + "error: the following arguments are required: argv") sys.exit(1) From 1d0cebd79a509d0fc0a4314232d61504bdb6d37c Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 15 Apr 2020 13:50:37 +0000 Subject: [PATCH 042/104] Add tests. --- .github/workflows/ci.yml | 13 +- tests/ethereum_truffle/__init__.py | 1 + tests/ethereum_truffle/test_truffle.py | 212 ++++++++++++++++++ .../truffle/basic/contracts/Basic.sol | 16 ++ .../truffle/basic/contracts/Migrations.sol | 23 ++ .../basic/migrations/1_initial_migration.js | 5 + .../basic/migrations/2_deploy_contracts.js | 7 + .../truffle/basic/truffle-config.js | 99 ++++++++ .../truffle/maze/contracts/Maze.sol | 52 +++++ .../truffle/maze/contracts/Migrations.sol | 23 ++ .../maze/migrations/1_initial_migration.js | 5 + .../maze/migrations/2_deploy_contracts.js | 10 + .../truffle/maze/truffle-config.js | 99 ++++++++ .../predeployed/contracts/Migrations.sol | 23 ++ .../predeployed/contracts/Predeployed.sol | 10 + .../migrations/1_initial_migration.js | 5 + .../migrations/2_deploy_contracts.js | 7 + .../truffle/predeployed/truffle-config.js | 99 ++++++++ 18 files changed, 703 insertions(+), 6 deletions(-) create mode 100644 tests/ethereum_truffle/__init__.py create mode 100644 tests/ethereum_truffle/test_truffle.py create mode 100644 tests/ethereum_truffle/truffle/basic/contracts/Basic.sol create mode 100644 tests/ethereum_truffle/truffle/basic/contracts/Migrations.sol create mode 100644 tests/ethereum_truffle/truffle/basic/migrations/1_initial_migration.js create mode 100644 tests/ethereum_truffle/truffle/basic/migrations/2_deploy_contracts.js create mode 100644 tests/ethereum_truffle/truffle/basic/truffle-config.js create mode 100644 tests/ethereum_truffle/truffle/maze/contracts/Maze.sol create mode 100644 tests/ethereum_truffle/truffle/maze/contracts/Migrations.sol create mode 100644 tests/ethereum_truffle/truffle/maze/migrations/1_initial_migration.js create mode 100644 tests/ethereum_truffle/truffle/maze/migrations/2_deploy_contracts.js create mode 100644 tests/ethereum_truffle/truffle/maze/truffle-config.js create mode 100644 tests/ethereum_truffle/truffle/predeployed/contracts/Migrations.sol create mode 100644 tests/ethereum_truffle/truffle/predeployed/contracts/Predeployed.sol create mode 100644 tests/ethereum_truffle/truffle/predeployed/migrations/1_initial_migration.js create mode 100644 tests/ethereum_truffle/truffle/predeployed/migrations/2_deploy_contracts.js create mode 100644 tests/ethereum_truffle/truffle/predeployed/truffle-config.js diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fcdfe2b87..66ddbdc2c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -154,10 +154,9 @@ jobs: npm install -g ganache-cli truffle } - run_truffle_tests(){ + run_metacoin_tests(){ ADDITIONAL_ARGS="" if [ "$1" = "deploy" ]; then - ganache-cli -p 7545 -i 5777 & ADDRESS="$(truffle deploy | grep '> contract address:.*' | tail -n 1 | grep -o '0x.*$')" ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txvictim $ADDRESS" fi @@ -207,10 +206,12 @@ jobs: ethereum_truffle) echo "Running truffle tests" install_node_packages - mkdir truffle_tests - cd truffle_tests - truffle unbox metacoin - run_truffle_tests && run_truffle_tests deploy + ganache-cli -p 7545 -i 5777 & + run_tests_from_dir $TEST_TYPE \ + && cd "$(mktemp -d)" \ + && truffle unbox metacoin \ + && run_metacoin_tests \ + && run_metacoin_tests deploy RV=$? ;; ethereum_vm) diff --git a/tests/ethereum_truffle/__init__.py b/tests/ethereum_truffle/__init__.py new file mode 100644 index 000000000..3755e783b --- /dev/null +++ b/tests/ethereum_truffle/__init__.py @@ -0,0 +1 @@ +# DO NOT DELETE diff --git a/tests/ethereum_truffle/test_truffle.py b/tests/ethereum_truffle/test_truffle.py new file mode 100644 index 000000000..817fb271a --- /dev/null +++ b/tests/ethereum_truffle/test_truffle.py @@ -0,0 +1,212 @@ +import os +import re +import shutil +import subprocess +import sys +import tempfile +import unittest + +from manticore.ethereum import ABI + +DIRPATH = os.path.dirname(__file__) + +# TLDR: when we launch `python -m manticore` and one uses PyCharm remote interpreter +# the `python` might not refer to proper interpreter. The `/proc/self/exe` is a workaround +# so one doesn't have to set up virtualenv in a remote interpreter. +PYTHON_BIN = sys.executable + +# sam.moelius: All of these tests assume that an Ethereum node is listening on 127.0.0.1:7545. +URL = "127.0.0.1:7545" + + +class EthTruffleTests(unittest.TestCase): + def setUp(self): + # Create a temporary directory + self.test_dir = tempfile.mkdtemp() + + def tearDown(self): + # Remove the directory after the test + shutil.rmtree(self.test_dir) + + def test_basic(self): + dir = os.path.abspath(os.path.join(DIRPATH, "truffle", "basic")) + workspace = os.path.join(self.test_dir, "workspace") + + os.chdir(dir) + + cmd = ["truffle", "deploy"] + output = subprocess.check_output(cmd).decode() + matches = [x for x in re.finditer(r"> contract address:\s*(0x\S*)", output)] + self.assertEqual(len(matches), 2) + address = matches[1].group(1) + + cmd = [ + PYTHON_BIN, + "-m", + "manticore", + "--workspace", + workspace, + "--no-color", + "--rpc", + URL, + "--txvictim", + address, + "--txlimit", + "1", + ] + subprocess.check_call(cmd) + + # sam.moelius: Manticore should have found a call to guess_x with the value of x, and a call + # to guess_y with the value of y. + cmd = [ + "grep", + "-r", + "--include=*.tx", + "^Data: 0x" + + ABI.function_selector("guess_x(uint256)").hex() + + "%0.64x" % int.from_bytes("constructor".encode(), byteorder="big"), + workspace, + ] + subprocess.check_call(cmd) + + cmd = [ + "grep", + "-r", + "--include=*.tx", + "^Data: 0x" + + ABI.function_selector("guess_y(uint256)").hex() + + "%0.64x" % int.from_bytes("set_y".encode(), byteorder="big"), + workspace, + ] + subprocess.check_call(cmd) + + # sam.moelius: test_predeployed is similar to test_basic. The difference is that + # test_predeployed involves two contracts: one deployed by truffle, and one deployed + # (internally) by Manticore. + def test_predeployed(self): + dir = os.path.abspath(os.path.join(DIRPATH, "truffle", "predeployed")) + workspace = os.path.join(self.test_dir, "workspace") + + os.chdir(dir) + + cmd = ["truffle", "deploy"] + output = subprocess.check_output(cmd).decode() + matches = [x for x in re.finditer(r"> contract address:\s*(0x\S*)", output)] + self.assertEqual(len(matches), 2) + address = matches[1].group(1) + + cmd = [ + PYTHON_BIN, + "-m", + "manticore", + "--workspace", + workspace, + "--no-color", + "--rpc", + URL, + "--txlimit", + "1", + "--contract", + "Guesser", + """ + interface Predeployed { + function x() external returns (uint256); + function y() external returns (uint256); + } + contract Guesser { + function guess_x(uint256 _x) external { + require(Predeployed(%s).x() == _x, "x != _x"); + } + function guess_y(uint256 _y) external { + require(Predeployed(%s).y() == _y, "y != _y"); + } + } + """ % (address, address), + ] + subprocess.check_call(cmd) + + # sam.moelius: Manticore should have found a call to guess_x with the value of x, and a call + # to guess_y with the value of y. + cmd = [ + "grep", + "-r", + "--include=*.tx", + "^Data: 0x" + + ABI.function_selector("guess_x(uint256)").hex() + + "%0.64x" % int.from_bytes("constructor".encode(), byteorder="big"), + workspace, + ] + subprocess.check_call(cmd) + + cmd = [ + "grep", + "-r", + "--include=*.tx", + "^Data: 0x" + + ABI.function_selector("guess_y(uint256)").hex() + + "%0.64x" % int.from_bytes("set_y".encode(), byteorder="big"), + workspace, + ] + subprocess.check_call(cmd) + + # sam.moelius: One purpose of test_maze is to give Manticore a lot of work, so that we can alter + # the blockchain while it is working. + def test_maze(self): + dir = os.path.abspath(os.path.join(DIRPATH, "truffle", "maze")) + workspace = os.path.join(self.test_dir, "workspace") + + os.chdir(dir) + + cmd = ["truffle", "deploy"] + output = subprocess.check_output(cmd).decode() + matches = [x for x in re.finditer(r"> contract address:\s*(0x\S*)", output)] + self.assertEqual(len(matches), 2) + address = matches[1].group(1) + + cmd = [ + PYTHON_BIN, + "-m", + "manticore", + "--workspace", + workspace, + "--no-color", + "--rpc", + URL, + "--txvictim", + address, + "--txnocoverage", + ] + mcore = subprocess.Popen(cmd, stdout=subprocess.PIPE) + + # sam.moelius: Burn some ether just to alter the blockchain. It appears that truffle + # console's stdin must be kept open, or else it will not do what you ask of it. + cmd = ["truffle", "console"] + truffle_console = subprocess.Popen(cmd, stdin=subprocess.PIPE, stdout=subprocess.PIPE) + truffle_console.stdin.write( + b"web3.eth.getCoinbase().then(account => web3.eth.sendTransaction({" + + b' to: "0x0000000000000000000000000000000000000000",' + + b" from: account," + + b' value: web3.utils.toWei("10", "ether")' + + b"}))\n" + ) + truffle_console.stdin.flush() + for line in truffle_console.stdout: + if re.search(r"\btransactionHash\b", line.decode()): + break + truffle_console.stdin.close() + + # sam.moelius: Wait for truffle console to finish. + self.assertEqual(mcore.wait(), 0) + + # sam.moelius: Wait for manticore to finish. + self.assertEqual(mcore.wait(), 0) + + # sam.moelius: Manticore should have complained that the blockchain was altered. + self.assertRegex( + mcore.stdout.read().decode(), + r"\bblocknumber has changed\b.*\bsomeone is using the endpoint besides us\b", + ) + + # sam.moelius: Manticore should have found a path through the maze. + cmd = ["grep", "-r", "--include=*.logs", "You won!", workspace] + subprocess.check_call(cmd) diff --git a/tests/ethereum_truffle/truffle/basic/contracts/Basic.sol b/tests/ethereum_truffle/truffle/basic/contracts/Basic.sol new file mode 100644 index 000000000..9fd87a66d --- /dev/null +++ b/tests/ethereum_truffle/truffle/basic/contracts/Basic.sol @@ -0,0 +1,16 @@ +contract Basic { + uint256 x; + uint256 y; + constructor(uint256 _x) public { + x = _x; + } + function set_y(uint256 _y) external { + y = _y; + } + function guess_x(uint256 _x) external view { + require(x == _x, "x != _x"); + } + function guess_y(uint256 _y) external view { + require(y == _y, "y != _y"); + } +} diff --git a/tests/ethereum_truffle/truffle/basic/contracts/Migrations.sol b/tests/ethereum_truffle/truffle/basic/contracts/Migrations.sol new file mode 100644 index 000000000..51dcdc13c --- /dev/null +++ b/tests/ethereum_truffle/truffle/basic/contracts/Migrations.sol @@ -0,0 +1,23 @@ +pragma solidity >=0.4.21 <0.7.0; + +contract Migrations { + address public owner; + uint public last_completed_migration; + + constructor() public { + owner = msg.sender; + } + + modifier restricted() { + if (msg.sender == owner) _; + } + + function setCompleted(uint completed) public restricted { + last_completed_migration = completed; + } + + function upgrade(address new_address) public restricted { + Migrations upgraded = Migrations(new_address); + upgraded.setCompleted(last_completed_migration); + } +} diff --git a/tests/ethereum_truffle/truffle/basic/migrations/1_initial_migration.js b/tests/ethereum_truffle/truffle/basic/migrations/1_initial_migration.js new file mode 100644 index 000000000..ee2135d29 --- /dev/null +++ b/tests/ethereum_truffle/truffle/basic/migrations/1_initial_migration.js @@ -0,0 +1,5 @@ +const Migrations = artifacts.require("Migrations"); + +module.exports = function(deployer) { + deployer.deploy(Migrations); +}; diff --git a/tests/ethereum_truffle/truffle/basic/migrations/2_deploy_contracts.js b/tests/ethereum_truffle/truffle/basic/migrations/2_deploy_contracts.js new file mode 100644 index 000000000..36194a24b --- /dev/null +++ b/tests/ethereum_truffle/truffle/basic/migrations/2_deploy_contracts.js @@ -0,0 +1,7 @@ +const Basic = artifacts.require("Basic"); + +module.exports = function (deployer) { + deployer.deploy(Basic, "0x" + Buffer.from("constructor").toString("hex")).then(basic => { + basic.set_y("0x" + Buffer.from("set_y").toString("hex")); + }); +}; diff --git a/tests/ethereum_truffle/truffle/basic/truffle-config.js b/tests/ethereum_truffle/truffle/basic/truffle-config.js new file mode 100644 index 000000000..38656904c --- /dev/null +++ b/tests/ethereum_truffle/truffle/basic/truffle-config.js @@ -0,0 +1,99 @@ +/** + * Use this file to configure your truffle project. It's seeded with some + * common settings for different networks and features like migrations, + * compilation and testing. Uncomment the ones you need or modify + * them to suit your project as necessary. + * + * More information about configuration can be found at: + * + * truffleframework.com/docs/advanced/configuration + * + * To deploy via Infura you'll need a wallet provider (like truffle-hdwallet-provider) + * to sign your transactions before they're sent to a remote public node. Infura accounts + * are available for free at: infura.io/register. + * + * You'll also need a mnemonic - the twelve word phrase the wallet uses to generate + * public/private key pairs. If you're publishing your code to GitHub make sure you load this + * phrase from a file you've .gitignored so it doesn't accidentally become public. + * + */ + +// const HDWalletProvider = require('truffle-hdwallet-provider'); +// const infuraKey = "fj4jll3k....."; +// +// const fs = require('fs'); +// const mnemonic = fs.readFileSync(".secret").toString().trim(); + +module.exports = { + /** + * Networks define how you connect to your ethereum client and let you set the + * defaults web3 uses to send transactions. If you don't specify one truffle + * will spin up a development blockchain for you on port 9545 when you + * run `develop` or `test`. You can ask a truffle command to use a specific + * network from the command line, e.g + * + * $ truffle test --network + */ + + networks: { + // Useful for testing. The `development` name is special - truffle uses it by default + // if it's defined here and no other network is specified at the command line. + // You should run a client (like ganache-cli, geth or parity) in a separate terminal + // tab if you use this network and you must also set the `host`, `port` and `network_id` + // options below to some value. + // + // development: { + // host: "127.0.0.1", // Localhost (default: none) + // port: 8545, // Standard Ethereum port (default: none) + // network_id: "*", // Any network (default: none) + // }, + + // Another network with more advanced options... + // advanced: { + // port: 8777, // Custom port + // network_id: 1342, // Custom network + // gas: 8500000, // Gas sent with each transaction (default: ~6700000) + // gasPrice: 20000000000, // 20 gwei (in wei) (default: 100 gwei) + // from:
, // Account to send txs from (default: accounts[0]) + // websockets: true // Enable EventEmitter interface for web3 (default: false) + // }, + + // Useful for deploying to a public network. + // NB: It's important to wrap the provider as a function. + // ropsten: { + // provider: () => new HDWalletProvider(mnemonic, `https://ropsten.infura.io/v3/YOUR-PROJECT-ID`), + // network_id: 3, // Ropsten's id + // gas: 5500000, // Ropsten has a lower block limit than mainnet + // confirmations: 2, // # of confs to wait between deployments. (default: 0) + // timeoutBlocks: 200, // # of blocks before a deployment times out (minimum/default: 50) + // skipDryRun: true // Skip dry run before migrations? (default: false for public nets ) + // }, + + // Useful for private networks + // private: { + // provider: () => new HDWalletProvider(mnemonic, `https://network.io`), + // network_id: 2111, // This network is yours, in the cloud. + // production: true // Treats this network as if it was a public net. (default: false) + // } + }, + + // Set default mocha options here, use special reporters etc. + mocha: { + // timeout: 100000 + }, + + // Configure your compilers + compilers: { + solc: { + // version: "0.5.1", // Fetch exact version from solc-bin (default: truffle's version) + // docker: true, // Use "0.5.1" you've installed locally with docker (default: false) + // settings: { // See the solidity docs for advice about optimization and evmVersion + // optimizer: { + // enabled: false, + // runs: 200 + // }, + // evmVersion: "byzantium" + // } + } + } +} diff --git a/tests/ethereum_truffle/truffle/maze/contracts/Maze.sol b/tests/ethereum_truffle/truffle/maze/contracts/Maze.sol new file mode 100644 index 000000000..bbe9f40dc --- /dev/null +++ b/tests/ethereum_truffle/truffle/maze/contracts/Maze.sol @@ -0,0 +1,52 @@ +contract Maze { + event Log(string); + uint constant size = 4; + uint16[size] maze; + uint8 x = 0; + uint8 y = 0; + constructor(uint16[size] memory _maze) public { + assert(bit(0) != 0); + maze = _maze; + assert(!wall(x, y)); + } + function move(uint256 _dir) external { + require(!win(), "You already won!"); + int128 dx = 0; + int128 dy = 0; + if (_dir == uint8(byte('E'))) { + dx = 1; + } else if (_dir == uint8(byte('N'))) { + dy = -1; + } else if (_dir == uint8(byte('S'))) { + dy = 1; + } else if (_dir == uint8(byte('W'))) { + dx = -1; + } else { + require(false, "Invalid direction."); + } + require(x != 0 || dx >= 0, "At left boundary."); + require(y != 0 || dy >= 0, "At upper boundary."); + require(x != size - 1 || dx <= 0, "At right boundary."); + require(y != size - 1 || dy <= 0, "At lower boundary."); + require(!wall(x + uint8(dx), y + uint8(dy)), "Ouch! You bumped into a wall."); + fill(x, y); + x += uint8(dx); + y += uint8(dy); + if (win()) { + emit Log("You won!"); + } + assert(!wall(x, y)); + } + function wall(uint8 _x, uint8 _y) internal view returns(bool) { + return (maze[_y] & bit(_x)) != 0; + } + function fill(uint8 _x, uint8 _y) internal { + maze[_y] |= bit(_x); + } + function bit(uint8 _x) internal pure returns(uint16) { + return uint16(1 << (4 * ((size - 1) - _x))); + } + function win() internal view returns(bool) { + return x == size - 1 && y == size - 1; + } +} diff --git a/tests/ethereum_truffle/truffle/maze/contracts/Migrations.sol b/tests/ethereum_truffle/truffle/maze/contracts/Migrations.sol new file mode 100644 index 000000000..51dcdc13c --- /dev/null +++ b/tests/ethereum_truffle/truffle/maze/contracts/Migrations.sol @@ -0,0 +1,23 @@ +pragma solidity >=0.4.21 <0.7.0; + +contract Migrations { + address public owner; + uint public last_completed_migration; + + constructor() public { + owner = msg.sender; + } + + modifier restricted() { + if (msg.sender == owner) _; + } + + function setCompleted(uint completed) public restricted { + last_completed_migration = completed; + } + + function upgrade(address new_address) public restricted { + Migrations upgraded = Migrations(new_address); + upgraded.setCompleted(last_completed_migration); + } +} diff --git a/tests/ethereum_truffle/truffle/maze/migrations/1_initial_migration.js b/tests/ethereum_truffle/truffle/maze/migrations/1_initial_migration.js new file mode 100644 index 000000000..ee2135d29 --- /dev/null +++ b/tests/ethereum_truffle/truffle/maze/migrations/1_initial_migration.js @@ -0,0 +1,5 @@ +const Migrations = artifacts.require("Migrations"); + +module.exports = function(deployer) { + deployer.deploy(Migrations); +}; diff --git a/tests/ethereum_truffle/truffle/maze/migrations/2_deploy_contracts.js b/tests/ethereum_truffle/truffle/maze/migrations/2_deploy_contracts.js new file mode 100644 index 000000000..93c1a42ff --- /dev/null +++ b/tests/ethereum_truffle/truffle/maze/migrations/2_deploy_contracts.js @@ -0,0 +1,10 @@ +const Maze = artifacts.require("Maze"); + +module.exports = function (deployer) { + deployer.deploy(Maze, [ + "0x0000", + "0x0101", + "0x0100", + "0x0110", + ]); +}; diff --git a/tests/ethereum_truffle/truffle/maze/truffle-config.js b/tests/ethereum_truffle/truffle/maze/truffle-config.js new file mode 100644 index 000000000..38656904c --- /dev/null +++ b/tests/ethereum_truffle/truffle/maze/truffle-config.js @@ -0,0 +1,99 @@ +/** + * Use this file to configure your truffle project. It's seeded with some + * common settings for different networks and features like migrations, + * compilation and testing. Uncomment the ones you need or modify + * them to suit your project as necessary. + * + * More information about configuration can be found at: + * + * truffleframework.com/docs/advanced/configuration + * + * To deploy via Infura you'll need a wallet provider (like truffle-hdwallet-provider) + * to sign your transactions before they're sent to a remote public node. Infura accounts + * are available for free at: infura.io/register. + * + * You'll also need a mnemonic - the twelve word phrase the wallet uses to generate + * public/private key pairs. If you're publishing your code to GitHub make sure you load this + * phrase from a file you've .gitignored so it doesn't accidentally become public. + * + */ + +// const HDWalletProvider = require('truffle-hdwallet-provider'); +// const infuraKey = "fj4jll3k....."; +// +// const fs = require('fs'); +// const mnemonic = fs.readFileSync(".secret").toString().trim(); + +module.exports = { + /** + * Networks define how you connect to your ethereum client and let you set the + * defaults web3 uses to send transactions. If you don't specify one truffle + * will spin up a development blockchain for you on port 9545 when you + * run `develop` or `test`. You can ask a truffle command to use a specific + * network from the command line, e.g + * + * $ truffle test --network + */ + + networks: { + // Useful for testing. The `development` name is special - truffle uses it by default + // if it's defined here and no other network is specified at the command line. + // You should run a client (like ganache-cli, geth or parity) in a separate terminal + // tab if you use this network and you must also set the `host`, `port` and `network_id` + // options below to some value. + // + // development: { + // host: "127.0.0.1", // Localhost (default: none) + // port: 8545, // Standard Ethereum port (default: none) + // network_id: "*", // Any network (default: none) + // }, + + // Another network with more advanced options... + // advanced: { + // port: 8777, // Custom port + // network_id: 1342, // Custom network + // gas: 8500000, // Gas sent with each transaction (default: ~6700000) + // gasPrice: 20000000000, // 20 gwei (in wei) (default: 100 gwei) + // from:
, // Account to send txs from (default: accounts[0]) + // websockets: true // Enable EventEmitter interface for web3 (default: false) + // }, + + // Useful for deploying to a public network. + // NB: It's important to wrap the provider as a function. + // ropsten: { + // provider: () => new HDWalletProvider(mnemonic, `https://ropsten.infura.io/v3/YOUR-PROJECT-ID`), + // network_id: 3, // Ropsten's id + // gas: 5500000, // Ropsten has a lower block limit than mainnet + // confirmations: 2, // # of confs to wait between deployments. (default: 0) + // timeoutBlocks: 200, // # of blocks before a deployment times out (minimum/default: 50) + // skipDryRun: true // Skip dry run before migrations? (default: false for public nets ) + // }, + + // Useful for private networks + // private: { + // provider: () => new HDWalletProvider(mnemonic, `https://network.io`), + // network_id: 2111, // This network is yours, in the cloud. + // production: true // Treats this network as if it was a public net. (default: false) + // } + }, + + // Set default mocha options here, use special reporters etc. + mocha: { + // timeout: 100000 + }, + + // Configure your compilers + compilers: { + solc: { + // version: "0.5.1", // Fetch exact version from solc-bin (default: truffle's version) + // docker: true, // Use "0.5.1" you've installed locally with docker (default: false) + // settings: { // See the solidity docs for advice about optimization and evmVersion + // optimizer: { + // enabled: false, + // runs: 200 + // }, + // evmVersion: "byzantium" + // } + } + } +} diff --git a/tests/ethereum_truffle/truffle/predeployed/contracts/Migrations.sol b/tests/ethereum_truffle/truffle/predeployed/contracts/Migrations.sol new file mode 100644 index 000000000..51dcdc13c --- /dev/null +++ b/tests/ethereum_truffle/truffle/predeployed/contracts/Migrations.sol @@ -0,0 +1,23 @@ +pragma solidity >=0.4.21 <0.7.0; + +contract Migrations { + address public owner; + uint public last_completed_migration; + + constructor() public { + owner = msg.sender; + } + + modifier restricted() { + if (msg.sender == owner) _; + } + + function setCompleted(uint completed) public restricted { + last_completed_migration = completed; + } + + function upgrade(address new_address) public restricted { + Migrations upgraded = Migrations(new_address); + upgraded.setCompleted(last_completed_migration); + } +} diff --git a/tests/ethereum_truffle/truffle/predeployed/contracts/Predeployed.sol b/tests/ethereum_truffle/truffle/predeployed/contracts/Predeployed.sol new file mode 100644 index 000000000..6680d239c --- /dev/null +++ b/tests/ethereum_truffle/truffle/predeployed/contracts/Predeployed.sol @@ -0,0 +1,10 @@ +contract Predeployed { + uint256 public x; + uint256 public y; + constructor(uint256 _x) public { + x = _x; + } + function set_y(uint256 _y) external { + y = _y; + } +} diff --git a/tests/ethereum_truffle/truffle/predeployed/migrations/1_initial_migration.js b/tests/ethereum_truffle/truffle/predeployed/migrations/1_initial_migration.js new file mode 100644 index 000000000..ee2135d29 --- /dev/null +++ b/tests/ethereum_truffle/truffle/predeployed/migrations/1_initial_migration.js @@ -0,0 +1,5 @@ +const Migrations = artifacts.require("Migrations"); + +module.exports = function(deployer) { + deployer.deploy(Migrations); +}; diff --git a/tests/ethereum_truffle/truffle/predeployed/migrations/2_deploy_contracts.js b/tests/ethereum_truffle/truffle/predeployed/migrations/2_deploy_contracts.js new file mode 100644 index 000000000..ff1cdde82 --- /dev/null +++ b/tests/ethereum_truffle/truffle/predeployed/migrations/2_deploy_contracts.js @@ -0,0 +1,7 @@ +const Predeployed = artifacts.require("Predeployed"); + +module.exports = function (deployer) { + deployer.deploy(Predeployed, "0x" + Buffer.from("constructor").toString("hex")).then(predeployed => { + predeployed.set_y("0x" + Buffer.from("set_y").toString("hex")); + }); +}; diff --git a/tests/ethereum_truffle/truffle/predeployed/truffle-config.js b/tests/ethereum_truffle/truffle/predeployed/truffle-config.js new file mode 100644 index 000000000..38656904c --- /dev/null +++ b/tests/ethereum_truffle/truffle/predeployed/truffle-config.js @@ -0,0 +1,99 @@ +/** + * Use this file to configure your truffle project. It's seeded with some + * common settings for different networks and features like migrations, + * compilation and testing. Uncomment the ones you need or modify + * them to suit your project as necessary. + * + * More information about configuration can be found at: + * + * truffleframework.com/docs/advanced/configuration + * + * To deploy via Infura you'll need a wallet provider (like truffle-hdwallet-provider) + * to sign your transactions before they're sent to a remote public node. Infura accounts + * are available for free at: infura.io/register. + * + * You'll also need a mnemonic - the twelve word phrase the wallet uses to generate + * public/private key pairs. If you're publishing your code to GitHub make sure you load this + * phrase from a file you've .gitignored so it doesn't accidentally become public. + * + */ + +// const HDWalletProvider = require('truffle-hdwallet-provider'); +// const infuraKey = "fj4jll3k....."; +// +// const fs = require('fs'); +// const mnemonic = fs.readFileSync(".secret").toString().trim(); + +module.exports = { + /** + * Networks define how you connect to your ethereum client and let you set the + * defaults web3 uses to send transactions. If you don't specify one truffle + * will spin up a development blockchain for you on port 9545 when you + * run `develop` or `test`. You can ask a truffle command to use a specific + * network from the command line, e.g + * + * $ truffle test --network + */ + + networks: { + // Useful for testing. The `development` name is special - truffle uses it by default + // if it's defined here and no other network is specified at the command line. + // You should run a client (like ganache-cli, geth or parity) in a separate terminal + // tab if you use this network and you must also set the `host`, `port` and `network_id` + // options below to some value. + // + // development: { + // host: "127.0.0.1", // Localhost (default: none) + // port: 8545, // Standard Ethereum port (default: none) + // network_id: "*", // Any network (default: none) + // }, + + // Another network with more advanced options... + // advanced: { + // port: 8777, // Custom port + // network_id: 1342, // Custom network + // gas: 8500000, // Gas sent with each transaction (default: ~6700000) + // gasPrice: 20000000000, // 20 gwei (in wei) (default: 100 gwei) + // from:
, // Account to send txs from (default: accounts[0]) + // websockets: true // Enable EventEmitter interface for web3 (default: false) + // }, + + // Useful for deploying to a public network. + // NB: It's important to wrap the provider as a function. + // ropsten: { + // provider: () => new HDWalletProvider(mnemonic, `https://ropsten.infura.io/v3/YOUR-PROJECT-ID`), + // network_id: 3, // Ropsten's id + // gas: 5500000, // Ropsten has a lower block limit than mainnet + // confirmations: 2, // # of confs to wait between deployments. (default: 0) + // timeoutBlocks: 200, // # of blocks before a deployment times out (minimum/default: 50) + // skipDryRun: true // Skip dry run before migrations? (default: false for public nets ) + // }, + + // Useful for private networks + // private: { + // provider: () => new HDWalletProvider(mnemonic, `https://network.io`), + // network_id: 2111, // This network is yours, in the cloud. + // production: true // Treats this network as if it was a public net. (default: false) + // } + }, + + // Set default mocha options here, use special reporters etc. + mocha: { + // timeout: 100000 + }, + + // Configure your compilers + compilers: { + solc: { + // version: "0.5.1", // Fetch exact version from solc-bin (default: truffle's version) + // docker: true, // Use "0.5.1" you've installed locally with docker (default: false) + // settings: { // See the solidity docs for advice about optimization and evmVersion + // optimizer: { + // enabled: false, + // runs: 200 + // }, + // evmVersion: "byzantium" + // } + } + } +} From abdca9e91b50a96c99bd0ac7da785e20c2d468d6 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 15 Apr 2020 19:05:59 +0000 Subject: [PATCH 043/104] Typo. --- manticore/__main__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/__main__.py b/manticore/__main__.py index 0ea57b99f..71e491248 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -189,7 +189,7 @@ def positive(value): "--rpc", type=str, dest="url", - help="Url of an Ethereum node to connect to. Must be of the form 'IP:PORT'", + help="URL of an Ethereum node to connect to. Must be of the form 'IP:PORT'", ) eth_detectors = parser.add_argument_group("Ethereum detectors") From ef328af8bb2c14ac913d8d0164746aa5eb5d2454 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 16 Apr 2020 00:53:02 +0000 Subject: [PATCH 044/104] Address typing issues. --- manticore/platforms/evm.py | 9 +-------- manticore/platforms/evm_world_state.py | 27 +++++++++++++++++++------- 2 files changed, 21 insertions(+), 15 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 6e8889ff6..e455aa94f 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -3010,14 +3010,7 @@ def dump(self, stream, state, mevm, message): stream.write("Balance: %d %s\n" % (balance, flagged(is_balance_symbolic))) storage = blockchain._get_storage(state.constraints, account_address) - concrete_indexes = set() - for sindex in storage.written: - concrete_indexes.add(state.solve_one(sindex, constrain=True)) - - for index in concrete_indexes: - stream.write( - f"storage[{index:x}] = {state.solve_one(storage[index], constrain=True):x}" - ) + storage.dump(stream, state) stream.write("Storage: %s\n" % translate_to_smtlib(storage.data, use_bindings=False)) if consts.sha3 is consts.sha3.concretize: diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 130d3d502..cced6117c 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -1,10 +1,13 @@ import logging from abc import ABC, abstractmethod +from eth_typing import ChecksumAddress, URI +from io import TextIOBase from typing import Dict, Optional, Set, Union from urllib.parse import ParseResult, urlparse from web3 import Web3 -from ..exceptions import EthereumError from ..core.smtlib import Array, BitVec, BitVecConstant, BitVecITE, BitVecZeroExtend, ConstraintSet +from ..ethereum.state import State +from ..exceptions import EthereumError logger = logging.getLogger(__name__) @@ -38,6 +41,16 @@ def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): self.data[offset] = value self.dirty = True + def dump(self, stream: TextIOBase, state: State): + concrete_indexes = set() + for sindex in self.map.written: + concrete_indexes.add(state.solve_one(sindex, constrain=True)) + + for index in concrete_indexes: + stream.write( + f"storage[{index:x}] = {state.solve_one(self.data[index], constrain=True):x}" + ) + @staticmethod def from_dict(constraints: ConstraintSet, address: int, items: Dict[int, int]) -> "Storage": storage = Storage(constraints, address) @@ -154,7 +167,7 @@ def __init__(self, blocknumber: int, warned: bool): _endpoints: Dict[str, Endpoint] = {} -def _web3_address(address: int) -> str: +def _web3_address(address: int) -> ChecksumAddress: return Web3.toChecksumAddress("0x%0.40x" % address) @@ -180,7 +193,7 @@ def _web3(self) -> Web3: # sam.moelius: Force WebsocketProvider.__init__ to call _get_threaded_loop. The existing # "threaded loop" could be leftover from a fork, in which case it will not work. Web3.WebsocketProvider._loop = None - web3 = Web3(Web3.WebsocketProvider("ws://" + self._url)) + web3 = Web3(Web3.WebsocketProvider(URI("ws://" + self._url))) blocknumber = web3.eth.blockNumber endpoint = _endpoints.get(self._url) if endpoint is None: @@ -225,16 +238,16 @@ def get_blocknumber(self) -> int: return self._web3().eth.blockNumber def get_timestamp(self) -> int: - return self._web3().eth.timestamp + return self._web3().eth.getBlock("latest")["timestamp"] def get_difficulty(self) -> int: - return self._web3().eth.difficulty + return self._web3().eth.getBlock("latest")["difficulty"] def get_gaslimit(self) -> int: - return self._web3().eth.gasLimit + return self._web3().eth.getBlock("latest")["gasLimit"] def get_coinbase(self) -> int: - return self._web3().eth.coinbase + return int(self._web3().eth.coinbase) #################################################################################################### From b0a38fdb27f4bd5de7b965779654948f4a6b0b19 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 16 Apr 2020 00:53:39 +0000 Subject: [PATCH 045/104] Report errors in ci.yml. --- .github/workflows/ci.yml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a1490d2fb..04c60e975 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -180,6 +180,9 @@ jobs: run_tests_from_dir() { DIR=$1 pytest --durations=100 --cov=manticore -n auto "tests/$DIR" + if [ $? -ne 0 ]; then + return 1 + fi coverage xml } @@ -211,19 +214,16 @@ jobs: && truffle unbox metacoin \ && run_metacoin_tests \ && run_metacoin_tests deploy - RV=$? ;; ethereum_vm) make_vmtests echo "Running only the tests from 'tests/$TEST_TYPE' directory" run_tests_from_dir $TEST_TYPE - RV=$? ;; wasm) make_wasm_tests echo "Running only the tests from 'tests/$TEST_TYPE' directory" run_tests_from_dir $TEST_TYPE - RV=$? ;; wasm_sym) make_wasm_sym_tests ;& @@ -233,7 +233,6 @@ jobs: other) echo "Running only the tests from 'tests/$TEST_TYPE' directory" run_tests_from_dir $TEST_TYPE - RV=$? ;; examples) run_examples From 913f31fae4fdaf5f158386de656b0ee693818310 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 16 Apr 2020 01:11:32 +0000 Subject: [PATCH 046/104] Add EXPECTED_TX to ci.yml. --- .github/workflows/ci.yml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 04c60e975..852b7c319 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -155,9 +155,11 @@ jobs: run_metacoin_tests(){ ADDITIONAL_ARGS="" + EXPECTED_TX=34 if [ "$1" = "deploy" ]; then ADDRESS="$(truffle deploy | grep '> contract address:.*' | tail -n 1 | grep -o '0x.*$')" ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txvictim $ADDRESS" + EXPECTED_TX=31 fi manticore . --contract MetaCoin --workspace output $ADDITIONAL_ARGS ### The original comment says we should get 41 states, but after implementing the shift @@ -169,8 +171,8 @@ jobs: # if [ "$(ls output/*tx -l | wc -l)" != "41" ]; then N="$(ls output/*tx -l | wc -l)" rm -rf output - if [ "$N" != "34" ]; then - echo "Truffle test failed: $N != 34" + if [ "$N" != "$EXPECTED_TX" ]; then + echo "Truffle test failed: $N != $EXPECTED_TX" return 1 fi echo "Truffle test succeded" From 2ff301ebedc960ab975468f7615afb4f888876ee Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 16 Apr 2020 10:02:31 +0000 Subject: [PATCH 047/104] Better variable name in ci.yml. --- .github/workflows/ci.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 852b7c319..9ede34771 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -169,10 +169,10 @@ jobs: # but Manticore fails to explore the paths due to the lack of the 0x1f opcode support # see https://github.com/trailofbits/manticore/issues/1166 # if [ "$(ls output/*tx -l | wc -l)" != "41" ]; then - N="$(ls output/*tx -l | wc -l)" + ACTUAL_TX="$(ls output/*tx -l | wc -l)" rm -rf output - if [ "$N" != "$EXPECTED_TX" ]; then - echo "Truffle test failed: $N != $EXPECTED_TX" + if [ "$ACTUAL_TX" != "$EXPECTED_TX" ]; then + echo "Truffle test failed: $ACTUAL_TX != $EXPECTED_TX" return 1 fi echo "Truffle test succeded" From bc5085babff5efbafc11526612a59cd1896deef8 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 23 Apr 2020 15:45:24 +0000 Subject: [PATCH 048/104] Fix types. --- manticore/ethereum/manticore.py | 4 ++-- manticore/platforms/evm.py | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index ea4741724..ba50274a3 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -386,7 +386,7 @@ def get_account(self, name): return self._accounts[name] def __init__( - self, world_state: WorldState = None, workspace_url: str = None, policy: str = "random" + self, world_state: Optional[WorldState] = None, workspace_url: str = None, policy: str = "random" ): """ A Manticore EVM manager @@ -1000,7 +1000,7 @@ def multi_tx_analysis( tx_limit=None, tx_use_coverage=True, tx_send_ether=True, - contract_account: int = None, + contract_account: Optional[int] = None, tx_account="attacker", tx_preconstrain=False, args=None, diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index e455aa94f..4e6d0ec32 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2236,7 +2236,7 @@ class EVMWorld(Platform): def __init__( self, constraints, - world_state: WorldState = None, + world_state: Optional[WorldState] = None, blocknumber=None, timestamp=None, difficulty=None, @@ -2737,7 +2737,7 @@ def execute(self): self._close_transaction(ex.result, ex.data, rollback=ex.is_rollback()) def create_account( - self, address=None, balance=0, code=None, storage: Dict[int, int] = None, nonce=None + self, address=None, balance=0, code=None, storage: Optional[Dict[int, int]] = None, nonce=None ): """ Low level account creation. No transaction is done. From e0c7272a34566f5006343b3ed7d5af4cfcfb327a Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 23 Apr 2020 17:57:51 +0000 Subject: [PATCH 049/104] Create DefaultWorldState only once. --- manticore/platforms/evm_world_state.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index cced6117c..39fac2fde 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -377,10 +377,11 @@ def get_coinbase(self) -> Union[int, BitVec]: return self._underlay.get_coinbase() def delete_account(self, constraints: ConstraintSet, address: int): - self._nonce[address] = DefaultWorldState().get_nonce(address) - self._balance[address] = DefaultWorldState().get_balance(address) + default_world_state = DefaultWorldState() + self._nonce[address] = default_world_state.get_nonce(address) + self._balance[address] = default_world_state.get_balance(address) self._storage[address] = Storage(constraints, address) - self._code[address] = DefaultWorldState().get_code(address) + self._code[address] = default_world_state.get_code(address) self._deleted_accounts.add(address) def set_nonce(self, address: int, value: Union[int, BitVec]): From d15cddf48a271afa7ca6e2988c2e64203fcc83e1 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 23 Apr 2020 18:40:22 +0000 Subject: [PATCH 050/104] "--txvictim" -> "--txtarget". --- .github/workflows/ci.yml | 2 +- manticore/__main__.py | 4 ++-- manticore/ethereum/cli.py | 4 ++-- tests/ethereum_truffle/test_truffle.py | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9ede34771..719f9c38e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -158,7 +158,7 @@ jobs: EXPECTED_TX=34 if [ "$1" = "deploy" ]; then ADDRESS="$(truffle deploy | grep '> contract address:.*' | tail -n 1 | grep -o '0x.*$')" - ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txvictim $ADDRESS" + ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txtarget $ADDRESS" EXPECTED_TX=31 fi manticore . --contract MetaCoin --workspace output $ADDITIONAL_ARGS diff --git a/manticore/__main__.py b/manticore/__main__.py index 71e491248..f1e2af551 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -165,7 +165,7 @@ def positive(value): "--txnoether", action="store_true", help="Do not attempt to send ether to contract" ) - eth_flags.add_argument("--txvictim", type=str, help="Address of a deployed contract to attack") + eth_flags.add_argument("--txtarget", type=str, help="Address of a deployed contract to attack") eth_flags.add_argument( "--txaccount", @@ -251,7 +251,7 @@ def positive(value): parsed = parser.parse_args(sys.argv[1:]) config.process_config_values(parser, parsed) - if parsed.url is not None and parsed.txvictim is not None and not parsed.argv: + if parsed.url is not None and parsed.txtarget is not None and not parsed.argv: parsed.argv = [None] if not parsed.argv: diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index be15786d3..0467a7222 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -139,8 +139,8 @@ def ethereum_main(args, logger): with m.kill_timeout(): contract_account = None - if args.txvictim is not None: - contract_account = int(args.txvictim, base=0) + if args.txtarget is not None: + contract_account = int(args.txtarget, base=0) m.multi_tx_analysis( args.argv[0], diff --git a/tests/ethereum_truffle/test_truffle.py b/tests/ethereum_truffle/test_truffle.py index 817fb271a..927779245 100644 --- a/tests/ethereum_truffle/test_truffle.py +++ b/tests/ethereum_truffle/test_truffle.py @@ -49,7 +49,7 @@ def test_basic(self): "--no-color", "--rpc", URL, - "--txvictim", + "--txtarget", address, "--txlimit", "1", @@ -172,7 +172,7 @@ def test_maze(self): "--no-color", "--rpc", URL, - "--txvictim", + "--txtarget", address, "--txnocoverage", ] From cd3b7e61917ce678002ae81d521858a042f8fab2 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 23 Apr 2020 20:52:13 +0000 Subject: [PATCH 051/104] Create accounts when not using RPC. --- manticore/platforms/evm.py | 4 ++++ manticore/platforms/evm_world_state.py | 13 +++++++++++++ 2 files changed, 17 insertions(+) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 4e6d0ec32..7449d8bed 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2934,6 +2934,10 @@ def _process_pending_transaction(self): f"Caller account {hex(caller)} does not exist; valid accounts: {list(map(hex, self.accounts))}" ) + if not self._world_state.is_remote() and address not in self.accounts: + # Creating an unaccessible account + self.create_account(address=address) + # Check depth failed = self.depth > 1024 diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 39fac2fde..85341867d 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -63,6 +63,10 @@ def from_dict(constraints: ConstraintSet, address: int, items: Dict[int, int]) - class WorldState: + @abstractmethod + def is_remote(self) -> bool: + pass + @abstractmethod def accounts(self) -> Set[int]: pass @@ -116,6 +120,9 @@ def get_coinbase(self) -> Union[int, BitVec]: class DefaultWorldState(WorldState): + def is_remote(self) -> bool: + return False + def accounts(self) -> Set[int]: return set() @@ -211,6 +218,9 @@ def _web3(self) -> Web3: endpoint.warned = True return web3 + def is_remote(self) -> bool: + return True + def accounts(self) -> Set[int]: raise NotImplementedError @@ -275,6 +285,9 @@ def __init__(self, underlay: WorldState): self._gaslimit: Optional[Union[int, BitVec]] = None self._coinbase: Optional[Union[int, BitVec]] = None + def is_remote(self) -> bool: + return self._underlay.is_remote() + def accounts(self) -> Set[int]: accounts: Set[int] = set() try: From 0d3254a112db85847b74bc64d43c0cfd28ed8d39 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 24 Apr 2020 00:28:00 +0000 Subject: [PATCH 052/104] Add bad IP/port tests. --- tests/ethereum_truffle/test_truffle.py | 52 ++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/tests/ethereum_truffle/test_truffle.py b/tests/ethereum_truffle/test_truffle.py index 927779245..fe9c311ea 100644 --- a/tests/ethereum_truffle/test_truffle.py +++ b/tests/ethereum_truffle/test_truffle.py @@ -28,6 +28,58 @@ def tearDown(self): # Remove the directory after the test shutil.rmtree(self.test_dir) + def test_bad_ip(self): + workspace = os.path.join(self.test_dir, "workspace") + + cmd = [ + PYTHON_BIN, + "-m", + "manticore", + "--workspace", + workspace, + "--no-color", + "--rpc", + "127.0.0.2:7545", + "--txtarget", + "0x111111111111111111111111111111111111111", + ] + mcore = subprocess.Popen(cmd, stdout=subprocess.PIPE) + + # sam.moelius: Manticore should have failed to connect. + self.assertRegex( + mcore.stdout.read().decode(), + r"\bConnectionRefusedError\(111, \"Connect call failed \('127.0.0.2', 7545\)\"\)", + ) + + # sam.moelius: Wait for manticore to finish. + self.assertEqual(mcore.wait(), 0) + + def test_bad_port(self): + workspace = os.path.join(self.test_dir, "workspace") + + cmd = [ + PYTHON_BIN, + "-m", + "manticore", + "--workspace", + workspace, + "--no-color", + "--rpc", + "127.0.0.1:7546", + "--txtarget", + "0x111111111111111111111111111111111111111", + ] + mcore = subprocess.Popen(cmd, stdout=subprocess.PIPE) + + # sam.moelius: Manticore should have failed to connect. + self.assertRegex( + mcore.stdout.read().decode(), + r"\bConnectionRefusedError\(111, \"Connect call failed \('127.0.0.1', 7546\)\"\)", + ) + + # sam.moelius: Wait for manticore to finish. + self.assertEqual(mcore.wait(), 0) + def test_basic(self): dir = os.path.abspath(os.path.join(DIRPATH, "truffle", "basic")) workspace = os.path.join(self.test_dir, "workspace") From 06da949259349ed847f213abe23bd56c65d237d5 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 24 Apr 2020 11:31:30 +0000 Subject: [PATCH 053/104] Update option description. --- manticore/__main__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/__main__.py b/manticore/__main__.py index f1e2af551..e820bdbf2 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -165,7 +165,7 @@ def positive(value): "--txnoether", action="store_true", help="Do not attempt to send ether to contract" ) - eth_flags.add_argument("--txtarget", type=str, help="Address of a deployed contract to attack") + eth_flags.add_argument("--txtarget", type=str, help="Address of a deployed contract to target") eth_flags.add_argument( "--txaccount", From 7454fa4a53bbd94853e3ec60ca282c314ad01e2c Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Tue, 28 Apr 2020 12:39:37 +0000 Subject: [PATCH 054/104] Raise EthereumError on connection failure. --- manticore/platforms/evm_world_state.py | 6 +++++- tests/ethereum_truffle/test_truffle.py | 4 ++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 85341867d..0dd715d1a 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -201,7 +201,11 @@ def _web3(self) -> Web3: # "threaded loop" could be leftover from a fork, in which case it will not work. Web3.WebsocketProvider._loop = None web3 = Web3(Web3.WebsocketProvider(URI("ws://" + self._url))) - blocknumber = web3.eth.blockNumber + blocknumber = None + try: + blocknumber = web3.eth.blockNumber + except ConnectionRefusedError as e: + raise EthereumError("Could not connect to %s: %s" % (self._url, e.args[1])) endpoint = _endpoints.get(self._url) if endpoint is None: endpoint = Endpoint(blocknumber, False) diff --git a/tests/ethereum_truffle/test_truffle.py b/tests/ethereum_truffle/test_truffle.py index fe9c311ea..f8183df94 100644 --- a/tests/ethereum_truffle/test_truffle.py +++ b/tests/ethereum_truffle/test_truffle.py @@ -48,7 +48,7 @@ def test_bad_ip(self): # sam.moelius: Manticore should have failed to connect. self.assertRegex( mcore.stdout.read().decode(), - r"\bConnectionRefusedError\(111, \"Connect call failed \('127.0.0.2', 7545\)\"\)", + r"\bEthereumError\(\"Could not connect to 127.0.0.2:7545: Connect call failed \('127.0.0.2', 7545\)\",\)", ) # sam.moelius: Wait for manticore to finish. @@ -74,7 +74,7 @@ def test_bad_port(self): # sam.moelius: Manticore should have failed to connect. self.assertRegex( mcore.stdout.read().decode(), - r"\bConnectionRefusedError\(111, \"Connect call failed \('127.0.0.1', 7546\)\"\)", + r"\bEthereumError\(\"Could not connect to 127.0.0.1:7546: Connect call failed \('127.0.0.1', 7546\)\",\)", ) # sam.moelius: Wait for manticore to finish. From fd562dbf5b0dbf2f2bb9132a734355ca4a8aa808 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Tue, 28 Apr 2020 13:39:02 +0000 Subject: [PATCH 055/104] Move OverlayWorldState comment into docstring. --- manticore/platforms/evm_world_state.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 0dd715d1a..26235f863 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -267,15 +267,15 @@ def get_coinbase(self) -> int: #################################################################################################### -# sam.moelius: If we decide to cache results returned from a RemoteWorldState, then they should NOT -# be cached within an overlay. The reason is that this could affect the results of subsequent -# operations. Consider a call to get_storage_data followed by a call to has_storage. If nothing -# was written to storage within the overlay, then the call to has_storage will throw an exception. -# But if the result of the call to get_storage_data was cached in the overlay, then no exception -# would be thrown. - - class OverlayWorldState(WorldState): + """ + If we decide to cache results returned from a RemoteWorldState, then they should NOT be cached + within an overlay. The reason is that this could affect the results of subsequent operations. + Consider a call to get_storage_data followed by a call to has_storage. If nothing was written + to storage within the overlay, then the call to has_storage will throw an exception. But if the + result of the call to get_storage_data was cached in the overlay, then no exception would be + thrown. + """ def __init__(self, underlay: WorldState): self._underlay: WorldState = underlay self._deleted_accounts: Set[int] = set() From 09879e18d6dae1a24eaba6131bcf2c0055438e7c Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Tue, 28 Apr 2020 14:33:48 +0000 Subject: [PATCH 056/104] Store newly created Storage in world_state. --- manticore/platforms/evm.py | 1 + 1 file changed, 1 insertion(+) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 7449d8bed..2cd78c7a5 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2582,6 +2582,7 @@ def _get_storage(self, constraints: ConstraintSet, address: int) -> Storage: storage = self._world_state.get_storage(address) if storage is None: storage = Storage(constraints, address) + self._world_state.set_storage(address, storage) return storage def _set_storage(self, address: int, storage: Union[Dict[int, int], Optional[Storage]]): From 462982aec7940012dbdc9d6e9f62efaedeb18eb2 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Tue, 28 Apr 2020 15:26:37 +0000 Subject: [PATCH 057/104] Add error message in OverlayWorldState.get_storage. --- manticore/platforms/evm_world_state.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 26235f863..7e6d76660 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -338,7 +338,9 @@ def get_storage(self, address: int) -> Optional[Storage]: # sam.moelius: Rightfully, the overlay's storage should be merged into the underlay's # storage. However, this is not currently implemented. if storage is not None: - raise NotImplementedError + # sam.moelius: At present, the get_storage methods of both DefaultWorldState and + # RemoteWorldState raise NotImplementedError. So this exception should be unreachable. + raise NotImplementedError("Merging of storage is not implemented") storage = self._storage.get(address) return storage From a1b06deec34edca4317660f6194b05946518248f Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 30 Apr 2020 14:05:46 +0000 Subject: [PATCH 058/104] Add constraints parameter to WorldState.get_storage_data. --- manticore/platforms/evm.py | 2 +- manticore/platforms/evm_world_state.py | 20 +++++++++++++++----- 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 2cd78c7a5..793a26ba2 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2552,7 +2552,7 @@ def get_storage_data( :return: the value :rtype: int or BitVec """ - value = self._world_state.get_storage_data(storage_address, offset) + value = self._world_state.get_storage_data(self.constraints, storage_address, offset) return simplify(value) def set_storage_data( diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 7e6d76660..e6ecc2812 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -87,8 +87,12 @@ def has_storage(self, address: int) -> bool: def get_storage(self, address: int) -> Optional[Storage]: pass + # sam.moelius: The addition of the constraints parameter is future-proofing. We might want + # to create a new Storage object in OverlayWorldState when self._storage.get(address) is None. @abstractmethod - def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> Union[int, BitVec]: + def get_storage_data( + self, constraints: ConstraintSet, address: int, offset: Union[int, BitVec] + ) -> Union[int, BitVec]: pass @abstractmethod @@ -138,7 +142,9 @@ def has_storage(self, address: int) -> bool: def get_storage(self, address: int) -> Optional[Storage]: raise NotImplementedError - def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> int: + def get_storage_data( + self, constraints: ConstraintSet, address: int, offset: Union[int, BitVec] + ) -> int: return 0 def get_code(self, address: int) -> bytes: @@ -240,7 +246,9 @@ def has_storage(self, address: int) -> bool: def get_storage(self, address) -> Storage: raise NotImplementedError - def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> int: + def get_storage_data( + self, constraints: ConstraintSet, address: int, offset: Union[int, BitVec] + ) -> int: if not isinstance(offset, int): raise NotImplementedError return int.from_bytes(self._web3().eth.getStorageAt(_web3_address(address), offset), "big") @@ -344,12 +352,14 @@ def get_storage(self, address: int) -> Optional[Storage]: storage = self._storage.get(address) return storage - def get_storage_data(self, address: int, offset: Union[int, BitVec]) -> Union[int, BitVec]: + def get_storage_data( + self, constraints: ConstraintSet, address: int, offset: Union[int, BitVec] + ) -> Union[int, BitVec]: value: Union[int, BitVec] = 0 # sam.moelius: If the account was ever deleted, then ignore the underlay's storage. if address not in self._deleted_accounts: try: - value = self._underlay.get_storage_data(address, offset) + value = self._underlay.get_storage_data(constraints, address, offset) except NotImplementedError: pass storage = self._storage.get(address) From fbebf327bd5a96ed4f7fde8eab898856ffd2fd08 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 30 Apr 2020 14:08:49 +0000 Subject: [PATCH 059/104] Change how Storage objects are allocated. --- manticore/platforms/evm.py | 4 ++-- manticore/platforms/evm_world_state.py | 31 +++++++++++++++++--------- 2 files changed, 23 insertions(+), 12 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 793a26ba2..7af335163 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2581,14 +2581,14 @@ def _get_storage(self, constraints: ConstraintSet, address: int) -> Storage: """Private auxiliary function to retrieve the storage""" storage = self._world_state.get_storage(address) if storage is None: - storage = Storage(constraints, address) + storage = self._world_state.new_storage(constraints, address) self._world_state.set_storage(address, storage) return storage def _set_storage(self, address: int, storage: Union[Dict[int, int], Optional[Storage]]): """Private auxiliary function to replace the storage""" if isinstance(storage, dict): - storage = Storage.from_dict(self.constraints, address, storage) + storage = self._world_state.new_storage(self.constraints, address, storage) self._world_state.set_storage(address, storage) def get_nonce(self, address: int) -> Union[int, BitVec]: diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index e6ecc2812..4e0f12b7d 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -18,6 +18,10 @@ class Storage: def __init__(self, constraints: ConstraintSet, address: int): + """ + :param constraints: the ConstraintSet with which this Storage object is associated + :param address: the address that owns this storage + """ self.constraints = constraints self.warned = False self.map = constraints.new_array( @@ -25,6 +29,9 @@ def __init__(self, constraints: ConstraintSet, address: int): value_bits=1, name=f"STORAGE_MAP_{address:x}", avoid_collisions=True, + # sam.moelius: The use of default here induces a kind of "closed world assumption," + # i.e., the only writes that occur to this storage are those that we observe. See + # ArrayProxy.get in expression.py. default=0, ) self.data = constraints.new_array( @@ -32,7 +39,9 @@ def __init__(self, constraints: ConstraintSet, address: int): value_bits=256, name=f"STORAGE_DATA_{address:x}", avoid_collisions=True, - default=0, + # sam.moelius: The use of default here creates unnecessary if-then-elses. See + # ArrayProxy.get in expression.py. + # default=0, ) self.dirty = False @@ -51,18 +60,20 @@ def dump(self, stream: TextIOBase, state: State): f"storage[{index:x}] = {state.solve_one(self.data[index], constrain=True):x}" ) - @staticmethod - def from_dict(constraints: ConstraintSet, address: int, items: Dict[int, int]) -> "Storage": - storage = Storage(constraints, address) - for key, value in items.items(): - storage.set(key, value) - return storage - #################################################################################################### class WorldState: + def new_storage( + self, constraints: ConstraintSet, address: int, items: Optional[Dict[int, int]] = None + ) -> Storage: + storage = Storage(constraints, address) + if items is not None: + for key, value in items.items(): + storage.set(key, value) + return storage + @abstractmethod def is_remote(self) -> bool: pass @@ -409,7 +420,7 @@ def delete_account(self, constraints: ConstraintSet, address: int): default_world_state = DefaultWorldState() self._nonce[address] = default_world_state.get_nonce(address) self._balance[address] = default_world_state.get_balance(address) - self._storage[address] = Storage(constraints, address) + self._storage[address] = self.new_storage(constraints, address) self._code[address] = default_world_state.get_code(address) self._deleted_accounts.add(address) @@ -434,7 +445,7 @@ def set_storage_data( ): storage = self._storage.get(address) if storage is None: - storage = Storage(constraints, address) + storage = self.new_storage(constraints, address) self._storage[address] = storage if storage.constraints != constraints: if not storage.warned: From ea1b2bd9a8cff3fb46d1b12e4e8c11bdb97ea31a Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 30 Apr 2020 14:10:23 +0000 Subject: [PATCH 060/104] Add EVMWorld.get_storage. --- manticore/platforms/evm.py | 3 +++ manticore/platforms/evm_world_state.py | 12 +++++++++--- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 7af335163..7475d26d3 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2577,6 +2577,9 @@ def has_storage(self, address: int) -> bool: """ return self._world_state.has_storage(address) + def get_storage(self, address: int) -> Storage: + return self._get_storage(self.constraints, address) + def _get_storage(self, constraints: ConstraintSet, address: int) -> Storage: """Private auxiliary function to retrieve the storage""" storage = self._world_state.get_storage(address) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 4e0f12b7d..53aa28ee8 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -45,6 +45,14 @@ def __init__(self, constraints: ConstraintSet, address: int): ) self.dirty = False + def __getitem__(self, offset: Union[int, BitVec]) -> Union[int, BitVec]: + return self.get(offset, 0) + + def get(self, offset: Union[int, BitVec], default: Union[int, BitVec]) -> Union[int, BitVec]: + if not isinstance(default, BitVec): + default = BitVecConstant(256, default) + return BitVecITE(256, self.map[offset] != 0, self.data[offset], default) + def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): self.map[offset] = 1 self.data[offset] = value @@ -375,9 +383,7 @@ def get_storage_data( pass storage = self._storage.get(address) if storage is not None: - if not isinstance(value, BitVec): - value = BitVecConstant(256, value) - value = BitVecITE(256, storage.map[offset] != 0, storage.data[offset], value) + value = storage.get(offset, value) return value def get_code(self, address: int) -> Union[bytes, Array]: From 92a18496f3aec48f2c65e4054fed8e279fff8dc0 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 30 Apr 2020 14:10:58 +0000 Subject: [PATCH 061/104] Add storage tests. --- tests/ethereum/test_storage.py | 268 +++++++++++++++++++++++++++++++++ 1 file changed, 268 insertions(+) create mode 100644 tests/ethereum/test_storage.py diff --git a/tests/ethereum/test_storage.py b/tests/ethereum/test_storage.py new file mode 100644 index 000000000..8ceb80738 --- /dev/null +++ b/tests/ethereum/test_storage.py @@ -0,0 +1,268 @@ +import unittest + +from manticore.core.smtlib import ( + ConstraintSet, + Version, + get_depth, + Operators, + translate_to_smtlib, + simplify, + arithmetic_simplify, + constant_folder, +) +from manticore.core.smtlib.solver import Z3Solver +from manticore.core.smtlib.expression import * +from manticore.platforms.evm_world_state import DefaultWorldState, DefaultWorldState, OverlayWorldState +from manticore.utils.helpers import pickle_dumps + +ADDRESS = 0x111111111111111111111111111111111111111 + +# sam.moelius: These tests were shamelessly copied from test_smtlibv2.py. + +class StorageTest(unittest.TestCase): + _multiprocess_can_split_ = True + + def setUp(self): + self.solver = Z3Solver.instance() + + def assertItemsEqual(self, a, b): + # Required for Python3 compatibility + self.assertEqual(sorted(a), sorted(b)) + + def tearDown(self): + del self.solver + + def testBasicStorage(self): + cs = ConstraintSet() + # make storage + world_state = OverlayWorldState(DefaultWorldState()) + # make free 256bit bitvectors + key = cs.new_bitvec(256) + value = cs.new_bitvec(256) + other_key = cs.new_bitvec(256) + other_value = cs.new_bitvec(256) + # store two symbolic values at symbolic offsets + world_state.set_storage_data(cs, ADDRESS, key, value) + world_state.set_storage_data(cs, ADDRESS, other_key, other_value) + + # assert that the storage is 'A' at key position + cs.add(world_state.get_storage_data(cs, ADDRESS, key) == ord("A")) + + # let's restrict key to be greater than 1000 + cs.add(key.ugt(1000)) + with cs as temp_cs: + # 1001 position of storage can be 'A' + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == ord("A")) + self.assertTrue(self.solver.check(temp_cs)) + + with cs as temp_cs: + # 1001 position of storage can also be 'B' + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == ord("B")) + self.assertTrue(self.solver.check(temp_cs)) + + with cs as temp_cs: + # but if it is 'B' ... + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == ord("B")) + # then key can not be 1001 + temp_cs.add(key == 1001) + self.assertFalse(self.solver.check(temp_cs)) + + with cs as temp_cs: + # If 1001 position is 'B' ... + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == ord("B")) + # then key can be 1000 for ex.. + temp_cs.add(key == 1002) + self.assertTrue(self.solver.check(temp_cs)) + + def testBasicStorage256(self): + cs = ConstraintSet() + # make storage + world_state = OverlayWorldState(DefaultWorldState()) + # make free 256bit bitvectors + key = cs.new_bitvec(256) + value = cs.new_bitvec(256) + other_key = cs.new_bitvec(256) + other_value = cs.new_bitvec(256) + # store two symbolic values at symbolic offsets + world_state.set_storage_data(cs, ADDRESS, key, value) + world_state.set_storage_data(cs, ADDRESS, other_key, other_value) + + # assert that the storage is 111...111 at key position + cs.add(world_state.get_storage_data(cs, ADDRESS, key) == 11111111111111111111111111111111111111111111) + # let's restrict key to be greater than 1000 + cs.add(key.ugt(1000)) + + with cs as temp_cs: + # 1001 position of storage can be 111...111 + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == 11111111111111111111111111111111111111111111) + self.assertTrue(self.solver.check(temp_cs)) + + with cs as temp_cs: + # 1001 position of storage can also be 222...222 + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == 22222222222222222222222222222222222222222222) + self.assertTrue(self.solver.check(temp_cs)) + + with cs as temp_cs: + # but if it is 222...222 ... + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == 22222222222222222222222222222222222222222222) + # then key can not be 1001 + temp_cs.add(key == 1001) + self.assertFalse(self.solver.check(temp_cs)) + + with cs as temp_cs: + # If 1001 position is 222...222 ... + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == 22222222222222222222222222222222222222222222) + # then key can be 1002 for ex.. + temp_cs.add(key == 1002) + self.assertTrue(self.solver.check(temp_cs)) + + def testBasicStorageStore(self): + cs = ConstraintSet() + # make storage + world_state = OverlayWorldState(DefaultWorldState()) + # make free 256bit bitvectors + key = cs.new_bitvec(256) + value = cs.new_bitvec(256) + other_key = cs.new_bitvec(256) + other_value = cs.new_bitvec(256) + # store two symbolic values at symbolic offsets + world_state.set_storage_data(cs, ADDRESS, key, value) + world_state.set_storage_data(cs, ADDRESS, other_key, other_value) + + # assert that the storage is 'A' at key position + world_state.set_storage_data(cs, ADDRESS, key, ord("A")) + # let's restrict key to be greater than 1000 + cs.add(key.ugt(1000)) + + # 1001 position of storage can be 'A' + self.assertTrue(self.solver.can_be_true(cs, world_state.get_storage_data(cs, ADDRESS, 1001) == ord("A"))) + + # 1001 position of storage can be 'B' + self.assertTrue(self.solver.can_be_true(cs, world_state.get_storage_data(cs, ADDRESS, 1001) == ord("B"))) + + with cs as temp_cs: + # but if it is 'B' ... + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == ord("B")) + # then key can not be 1001 + temp_cs.add(key == 1001) + self.assertFalse(self.solver.check(temp_cs)) + + with cs as temp_cs: + # If 1001 position is 'B' ... + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == ord("B")) + # then key can be 1002 for ex.. + temp_cs.add(key != 1002) + self.assertTrue(self.solver.check(temp_cs)) + + def testClosedWorldAssumption(self): + cs = ConstraintSet() + # make storage + world_state = OverlayWorldState(DefaultWorldState()) + # make free 256bit bitvectors + key = cs.new_bitvec(256) + value = cs.new_bitvec(256) + other_key = cs.new_bitvec(256) + other_value = cs.new_bitvec(256) + # store two symbolic values at symbolic offsets + world_state.set_storage_data(cs, ADDRESS, key, value) + world_state.set_storage_data(cs, ADDRESS, other_key, other_value) + + with cs as temp_cs: + # sam.moelius: The value at 1001 can be 'A' and the value at 1002 can be 'B'. + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == ord("A")) + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1002) == ord("B")) + self.assertTrue(self.solver.check(temp_cs)) + + with cs as temp_cs: + # sam.moelius: If the value at 1001 is 'A' and the value at 1002 is 'B', then 'C' + # cannot appear anywhere in storage. + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == ord("A")) + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1002) == ord("B")) + temp_cs.add(world_state.get_storage_data(cs, ADDRESS, key) == ord("C")) + self.assertFalse(self.solver.check(temp_cs)) + + def testBasicStorageSymbIdx(self): + cs = ConstraintSet() + world_state = OverlayWorldState(DefaultWorldState()) + key = cs.new_bitvec(256, name="key") + index = cs.new_bitvec(256, name="index") + + world_state.set_storage_data(cs, ADDRESS, key, 1) # Write 1 to a single location + + cs.add(world_state.get_storage_data(cs, ADDRESS, index) != 0) # Constrain index so it selects that location + + cs.add(index != key) + # key and index are the same there is only one slot in 1 + self.assertFalse(self.solver.check(cs)) + + def testBasicStorageSymbIdx2(self): + cs = ConstraintSet() + world_state = OverlayWorldState(DefaultWorldState()) + key = cs.new_bitvec(256, name="key") + index = cs.new_bitvec(256, name="index") + + world_state.set_storage_data(cs, ADDRESS, key, 1) # Write 1 to a single location + cs.add(world_state.get_storage_data(cs, ADDRESS, index) != 0) # Constrain index so it selects that location + a_index = self.solver.get_value(cs, index) # get a concrete solution for index + cs.add(world_state.get_storage_data(cs, ADDRESS, a_index) != 0) # now storage must have something at that location + cs.add(a_index != index) # remove it from the solutions + + # It should not be another solution for index + self.assertFalse(self.solver.check(cs)) + + def testBasicStorageSymbIdx3(self): + cs = ConstraintSet() + world_state = OverlayWorldState(DefaultWorldState()) + key = cs.new_bitvec(256, name="key") + index = cs.new_bitvec(256, name="index") + + world_state.set_storage_data(cs, ADDRESS, 0, 1) # Write 1 to first location + world_state.set_storage_data(cs, ADDRESS, key, 2) # Write 2 to a symbolic (potentially any (potentially 0))location + + solutions = self.solver.get_all_values(cs, world_state.get_storage_data(cs, ADDRESS, 0)) # get a concrete solution for index + self.assertItemsEqual(solutions, (1, 2)) + + solutions = self.solver.get_all_values( + cs, world_state.get_storage_data(cs, ADDRESS, 0) + ) # get a concrete solution for index 0 + self.assertItemsEqual(solutions, (1, 2)) + + solutions = self.solver.get_all_values( + cs, world_state.get_storage_data(cs, ADDRESS, 1) + ) # get a concrete solution for index 1 + self.assertItemsEqual(solutions, (0, 2)) + + # sam.moelius: Nothing that could be 12345 has been written to storage. + self.assertFalse( + self.solver.can_be_true(cs, world_state.get_storage_data(cs, ADDRESS, 1) == 12345) + ) + + # sam.moelius: Write a symbolic value at symbolic offset key. + value = cs.new_bitvec(256, name="value") + world_state.set_storage_data(cs, ADDRESS, key, value) + + # sam.moelius: Could 12345 appear at offset 1? Yes, because value could be 12345 and key could be 1. + self.assertTrue( + self.solver.can_be_true(cs, world_state.get_storage_data(cs, ADDRESS, 1) == 12345) + ) + + def testBasicPickle(self): + import pickle + + cs = ConstraintSet() + + # make storage + world_state = OverlayWorldState(DefaultWorldState()) + # make free 256bit bitvector + key = cs.new_bitvec(256) + + # assert that the storage is 'A' at key position + world_state.set_storage_data(cs, ADDRESS, key, ord("A")) + # let's restrict key to be greater than 1000 + cs.add(key.ugt(1000)) + cs = pickle.loads(pickle_dumps(cs)) + self.assertTrue(self.solver.check(cs)) + + +if __name__ == "__main__": + unittest.main() From b3089b7208aaeeaea27e9c0aab91de39c4cd12d0 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 30 Apr 2020 14:11:28 +0000 Subject: [PATCH 062/104] Blacken. --- manticore/platforms/evm_world_state.py | 1 + 1 file changed, 1 insertion(+) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 53aa28ee8..ab484ce17 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -303,6 +303,7 @@ class OverlayWorldState(WorldState): result of the call to get_storage_data was cached in the overlay, then no exception would be thrown. """ + def __init__(self, underlay: WorldState): self._underlay: WorldState = underlay self._deleted_accounts: Set[int] = set() From a7d090aef80d99e9321d4ae55d7bc2acdb0b569d Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 30 Apr 2020 17:45:12 +0000 Subject: [PATCH 063/104] Re-add EVMWorld.get_storage docstring. --- manticore/platforms/evm.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 7475d26d3..ec0137e68 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2578,6 +2578,13 @@ def has_storage(self, address: int) -> bool: return self._world_state.has_storage(address) def get_storage(self, address: int) -> Storage: + """ + Gets the storage of an account + + :param address: account address + :return: account storage + :rtype: bytearray or ArrayProxy + """ return self._get_storage(self.constraints, address) def _get_storage(self, constraints: ConstraintSet, address: int) -> Storage: From 954e92f08067745f8d5a004bc97acc770517ddad Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 30 Apr 2020 18:09:47 +0000 Subject: [PATCH 064/104] Correct EVMWorld.get_storage docstring. --- manticore/platforms/evm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index ec0137e68..05c8abeef 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2583,7 +2583,7 @@ def get_storage(self, address: int) -> Storage: :param address: account address :return: account storage - :rtype: bytearray or ArrayProxy + :rtype: Storage """ return self._get_storage(self.constraints, address) From a3e70e24ad653f834bfd318e85b9e5eb55578c17 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 1 May 2020 00:52:34 +0000 Subject: [PATCH 065/104] Add missing newline. --- manticore/platforms/evm_world_state.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index ab484ce17..9f9259c60 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -65,7 +65,7 @@ def dump(self, stream: TextIOBase, state: State): for index in concrete_indexes: stream.write( - f"storage[{index:x}] = {state.solve_one(self.data[index], constrain=True):x}" + f"storage[{index:x}] = {state.solve_one(self.data[index], constrain=True):x}\n" ) From 18bf6486a44fa93057cb85a052b6671ca98097ce Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 1 May 2020 01:15:20 +0000 Subject: [PATCH 066/104] Better error handling/reporting. --- manticore/__main__.py | 9 +++++-- manticore/ethereum/cli.py | 36 +++++++++++++++----------- manticore/ethereum/manticore.py | 2 ++ tests/ethereum_truffle/test_truffle.py | 4 +-- 4 files changed, 32 insertions(+), 19 deletions(-) diff --git a/manticore/__main__.py b/manticore/__main__.py index e820bdbf2..a077e9d7a 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -41,7 +41,12 @@ def main(): resources.check_disk_usage() resources.check_memory_usage() - if args.url is not None or args.argv[0].endswith(".sol") or is_supported(args.argv[0]): + if ( + args.url is not None + or args.txtarget is not None + or args.argv[0].endswith(".sol") + or is_supported(args.argv[0]) + ): ethereum_main(args, logger) elif args.argv[0].endswith(".wasm") or args.argv[0].endswith(".wat"): wasm_main(args, logger) @@ -251,7 +256,7 @@ def positive(value): parsed = parser.parse_args(sys.argv[1:]) config.process_config_values(parser, parsed) - if parsed.url is not None and parsed.txtarget is not None and not parsed.argv: + if parsed.txtarget is not None and not parsed.argv: parsed.argv = [None] if not parsed.argv: diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index 0467a7222..4bc1c1f79 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -15,6 +15,7 @@ DetectManipulableBalance, ) from ..core.plugin import Profiler +from ..exceptions import EthereumError from .manticore import ManticoreEVM from .plugins import ( FilterFunctions, @@ -138,21 +139,26 @@ def ethereum_main(args, logger): logger.info("Beginning analysis") with m.kill_timeout(): - contract_account = None - if args.txtarget is not None: - contract_account = int(args.txtarget, base=0) - - m.multi_tx_analysis( - args.argv[0], - contract_name=args.contract, - tx_limit=args.txlimit, - tx_use_coverage=not args.txnocoverage, - tx_send_ether=not args.txnoether, - contract_account=contract_account, - tx_account=args.txaccount, - tx_preconstrain=args.txpreconstrain, - compile_args=vars(args), # FIXME - ) + try: + contract_account = None + if args.txtarget is not None: + contract_account = int(args.txtarget, base=0) + if world_state is not None and not world_state.get_code(contract_account): + raise EthereumError("Could not get code for target account: " + args.txtarget) + + m.multi_tx_analysis( + args.argv[0], + contract_name=args.contract, + tx_limit=args.txlimit, + tx_use_coverage=not args.txnocoverage, + tx_send_ether=not args.txnoether, + contract_account=contract_account, + tx_account=args.txaccount, + tx_preconstrain=args.txpreconstrain, + compile_args=vars(args), # FIXME + ) + except EthereumError as e: + logger.error("%r", e.args[0]) if not args.no_testcases: m.finalize(only_alive_states=args.only_alive_testcases) diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index ba50274a3..b995e2e6e 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -1025,6 +1025,8 @@ def multi_tx_analysis( compile_args=compile_args, balance=create_value, ) + elif solidity_filename is not None: + raise EthereumError("A target contract and a Solidty filename cannot both be specified") if tx_account == "attacker": tx_account = [attacker_account] diff --git a/tests/ethereum_truffle/test_truffle.py b/tests/ethereum_truffle/test_truffle.py index f8183df94..b64cd77e6 100644 --- a/tests/ethereum_truffle/test_truffle.py +++ b/tests/ethereum_truffle/test_truffle.py @@ -48,7 +48,7 @@ def test_bad_ip(self): # sam.moelius: Manticore should have failed to connect. self.assertRegex( mcore.stdout.read().decode(), - r"\bEthereumError\(\"Could not connect to 127.0.0.2:7545: Connect call failed \('127.0.0.2', 7545\)\",\)", + r"\bm\.main:ERROR: \"Could not connect to 127.0.0.2:7545: Connect call failed \('127.0.0.2', 7545\)\"", ) # sam.moelius: Wait for manticore to finish. @@ -74,7 +74,7 @@ def test_bad_port(self): # sam.moelius: Manticore should have failed to connect. self.assertRegex( mcore.stdout.read().decode(), - r"\bEthereumError\(\"Could not connect to 127.0.0.1:7546: Connect call failed \('127.0.0.1', 7546\)\",\)", + r"\bm\.main:ERROR: \"Could not connect to 127.0.0.1:7546: Connect call failed \('127.0.0.1', 7546\)\"", ) # sam.moelius: Wait for manticore to finish. From ee206c47ceb6508a897c728f9705fe7822cbc9ff Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 1 May 2020 01:36:49 +0000 Subject: [PATCH 067/104] Fix error in ci.yml. --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 719f9c38e..eea5dda2b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -154,14 +154,14 @@ jobs: } run_metacoin_tests(){ - ADDITIONAL_ARGS="" + ADDITIONAL_ARGS=. EXPECTED_TX=34 if [ "$1" = "deploy" ]; then ADDRESS="$(truffle deploy | grep '> contract address:.*' | tail -n 1 | grep -o '0x.*$')" ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txtarget $ADDRESS" EXPECTED_TX=31 fi - manticore . --contract MetaCoin --workspace output $ADDITIONAL_ARGS + manticore --contract MetaCoin --workspace output $ADDITIONAL_ARGS ### The original comment says we should get 41 states, but after implementing the shift ### insructions, we get 31. Was the original comment a typo? From abe52bc4c7a7110ae93e4d4a7ab620a9a875fa9f Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 1 May 2020 09:56:12 +0000 Subject: [PATCH 068/104] Add EVMWorld.get_storage_items. --- manticore/platforms/evm.py | 10 ++++++++++ manticore/platforms/evm_world_state.py | 12 ++++++++++-- 2 files changed, 20 insertions(+), 2 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 05c8abeef..3e46c8085 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2569,6 +2569,16 @@ def set_storage_data( """ self._world_state.set_storage_data(self.constraints, storage_address, offset, value) + def get_storage_items(self, address: int) -> List[Tuple[Union[int, BitVec], Union[int, BitVec]]]: + """ + Gets all items in an account storage + + :param address: account address + :return: all items in account storage. items are tuple of (index, value). value can be symbolic + :rtype: list[(storage_index, storage_value)] + """ + return self.get_storage(address).get_items() + def has_storage(self, address: int) -> bool: """ True if something has been written to the storage. diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 9f9259c60..3e2d78f1d 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -2,10 +2,10 @@ from abc import ABC, abstractmethod from eth_typing import ChecksumAddress, URI from io import TextIOBase -from typing import Dict, Optional, Set, Union +from typing import Dict, List, Optional, Set, Tuple, Union from urllib.parse import ParseResult, urlparse from web3 import Web3 -from ..core.smtlib import Array, BitVec, BitVecConstant, BitVecITE, BitVecZeroExtend, ConstraintSet +from ..core.smtlib import Array, ArrayVariable, BitVec, BitVecConstant, BitVecITE, BitVecZeroExtend, ConstraintSet from ..ethereum.state import State from ..exceptions import EthereumError @@ -58,6 +58,14 @@ def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): self.data[offset] = value self.dirty = True + def get_items(self) -> List[Tuple[Union[int, BitVec], Union[int, BitVec]]]: + items = [] + array = self.data.array + while not isinstance(array, ArrayVariable): + items.append((array.index, array.value)) + array = array.array + return items + def dump(self, stream: TextIOBase, state: State): concrete_indexes = set() for sindex in self.map.written: From 53117d2ffc3048587d19dc2da63d26cca0cdc6d2 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 1 May 2020 18:02:31 +0000 Subject: [PATCH 069/104] Adjust z3 options. --- manticore/core/smtlib/solver.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 78435d199..08a8bb9de 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -164,6 +164,11 @@ def __init__(self): "(set-logic QF_AUFBV)", # The declarations and definitions will be scoped "(set-option :global-decls false)", + # sam.moelius: Option "tactic.solve_eqs.context_solve" was turned on by this commit in z3: + # https://github.com/Z3Prover/z3/commit/3e53b6f2dbbd09380cd11706cabbc7e14b0cc6a2 + # Turning it off greatly improves Manticore's performance on test_integer_overflow_storageinvariant + # in test_consensys_benchmark.py. + "(set-option :tactic.solve_eqs.context_solve false)", ] self._get_value_fmt = (RE_GET_EXPR_VALUE_FMT, 16) From 6ccbd49ce1f2838a691d73304d550fef378d88c1 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 4 May 2020 10:29:13 +0000 Subject: [PATCH 070/104] Experimenting with Storage simplifications. --- manticore/platforms/evm_world_state.py | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 3e2d78f1d..3dfa3c8ed 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -24,16 +24,6 @@ def __init__(self, constraints: ConstraintSet, address: int): """ self.constraints = constraints self.warned = False - self.map = constraints.new_array( - index_bits=256, - value_bits=1, - name=f"STORAGE_MAP_{address:x}", - avoid_collisions=True, - # sam.moelius: The use of default here induces a kind of "closed world assumption," - # i.e., the only writes that occur to this storage are those that we observe. See - # ArrayProxy.get in expression.py. - default=0, - ) self.data = constraints.new_array( index_bits=256, value_bits=256, @@ -51,10 +41,9 @@ def __getitem__(self, offset: Union[int, BitVec]) -> Union[int, BitVec]: def get(self, offset: Union[int, BitVec], default: Union[int, BitVec]) -> Union[int, BitVec]: if not isinstance(default, BitVec): default = BitVecConstant(256, default) - return BitVecITE(256, self.map[offset] != 0, self.data[offset], default) + return self.data.get(offset, default) def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): - self.map[offset] = 1 self.data[offset] = value self.dirty = True @@ -68,7 +57,7 @@ def get_items(self) -> List[Tuple[Union[int, BitVec], Union[int, BitVec]]]: def dump(self, stream: TextIOBase, state: State): concrete_indexes = set() - for sindex in self.map.written: + for sindex in self.data.written: concrete_indexes.add(state.solve_one(sindex, constrain=True)) for index in concrete_indexes: From 88ddfbca9efcaa47f736183bee4fd4c6d3ef9b66 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 4 May 2020 13:11:37 +0000 Subject: [PATCH 071/104] Add nonce checks to test_gas_check. --- tests/ethereum/test_general.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 924dd64bb..d9920cddf 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -1733,6 +1733,7 @@ def test_gas_check(self): ) self.assertIn(0x111111111111111111111111111111111111111, world) self.assertTrue(world.has_code(0x111111111111111111111111111111111111111)) + self.assertEqual(world.get_nonce(0x111111111111111111111111111111111111111), 1) world.create_account(address=0x222222222222222222222222222222222222222) world.transaction( 0x111111111111111111111111111111111111111, @@ -1746,6 +1747,7 @@ def test_gas_check(self): result = str(e) self.assertEqual(result, "SELFDESTRUCT") self.assertFalse(world.has_code(0x111111111111111111111111111111111111111)) + self.assertEqual(world.get_nonce(0x111111111111111111111111111111111111111), 0) class EthPluginTests(unittest.TestCase): From 556a49266c5a2491555b6476bc1e923010764ccf Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 8 May 2020 09:28:45 +0000 Subject: [PATCH 072/104] Remove reference to map. --- manticore/platforms/evm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 3e46c8085..da515ee5d 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -3046,7 +3046,7 @@ def dump(self, stream, state, mevm, message): # get the storage for account_address storage = blockchain._get_storage(temp_cs, account_address) # we are interested only in used slots - temp_cs.add(storage.map.get(index) != 0) + temp_cs.add(storage.data.is_known(index) != 0) # Query the solver to get all storage indexes with used slots all_used_indexes = Z3Solver.instance().get_all_values(temp_cs, index) From 56a38f0c2a8a2c24db81496568aaff80a7566540 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 8 May 2020 14:28:54 +0000 Subject: [PATCH 073/104] Reduce log messages. --- manticore/platforms/evm_world_state.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 3dfa3c8ed..ebbdef50d 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -451,6 +451,8 @@ def set_storage_data( if storage is None: storage = self.new_storage(constraints, address) self._storage[address] = storage + while storage.constraints != constraints and constraints is not None: + constraints = constraints._parent if storage.constraints != constraints: if not storage.warned: logger.warning("Constraints have changed") From a5c2ddc13917e1bbfdf779ef33111f7f6f056b0f Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 8 May 2020 15:24:10 +0000 Subject: [PATCH 074/104] Eliminate ci.yml conflicts. --- .github/workflows/ci.yml | 42 +++++++++++++++++++++------------------- 1 file changed, 22 insertions(+), 20 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index eea5dda2b..686d35da2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -66,13 +66,13 @@ jobs: # concolic assumes presence of ../linux/simpleassert echo "Running concolic.py..." HW=../linux/helloworld - python ./concolic.py + coverage run ./concolic.py if [ $? -ne 0 ]; then return 1 fi echo "Running count_instructions.py..." - python ./count_instructions.py $HW |grep -q Executed + coverage run ./count_instructions.py $HW |grep -q Executed if [ $? -ne 0 ]; then return 1 fi @@ -81,21 +81,21 @@ jobs: gcc -static -g src/state_explore.c -o state_explore ADDRESS=0x$(objdump -S state_explore | grep -A 1 '((value & 0xff) != 0)' | tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:) - python ./introduce_symbolic_bytes.py state_explore $ADDRESS + coverage run ./introduce_symbolic_bytes.py state_explore $ADDRESS if [ $? -ne 0 ]; then return 1 fi echo "Running run_simple.py..." gcc -x c -static -o hello test_run_simple.c - python ./run_simple.py hello + coverage run ./run_simple.py hello if [ $? -ne 0 ]; then return 1 fi echo "Running run_hook.py..." MAIN_ADDR=$(nm $HW|grep 'T main' | awk '{print "0x"$1}') - python ./run_hook.py $HW $MAIN_ADDR + coverage run ./run_hook.py $HW $MAIN_ADDR if [ $? -ne 0 ]; then return 1 fi @@ -105,7 +105,7 @@ jobs: gcc -static -g src/state_explore.c -o state_explore SE_ADDR=0x$(objdump -S state_explore | grep -A 1 'value == 0x41' | tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:) - python ./state_control.py state_explore $SE_ADDR + coverage run ./state_control.py state_explore $SE_ADDR if [ $? -ne 0 ]; then return 1 fi @@ -161,14 +161,9 @@ jobs: ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txtarget $ADDRESS" EXPECTED_TX=31 fi - manticore --contract MetaCoin --workspace output $ADDITIONAL_ARGS - ### The original comment says we should get 41 states, but after implementing the shift - ### insructions, we get 31. Was the original comment a typo? - - # The correct answer should be 41 - # but Manticore fails to explore the paths due to the lack of the 0x1f opcode support - # see https://github.com/trailofbits/manticore/issues/1166 - # if [ "$(ls output/*tx -l | wc -l)" != "41" ]; then + coverage run -m manticore --contract MetaCoin --workspace output $ADDITIONAL_ARGS + # Truffle smoke test. We test if manticore is able to generate states + # from a truffle project. ACTUAL_TX="$(ls output/*tx -l | wc -l)" rm -rf output if [ "$ACTUAL_TX" != "$EXPECTED_TX" ]; then @@ -201,7 +196,9 @@ jobs: launch_examples RESULT=$? echo Ran example scripts + coverage xml popd + cp examples/script/coverage.xml . return $RESULT } @@ -212,28 +209,30 @@ jobs: install_node_packages ganache-cli -p 7545 -i 5777 & run_tests_from_dir $TEST_TYPE \ - && cd "$(mktemp -d)" \ + && mkdir metacoin_tests \ + && cd metacoin_tests \ && truffle unbox metacoin \ && run_metacoin_tests \ - && run_metacoin_tests deploy + && run_metacoin_tests deploy \ + && coverage combine \ + && coverage xml \ + && cd .. \ + && cp metacoin_tests/coverage.xml . ;; ethereum_vm) make_vmtests - echo "Running only the tests from 'tests/$TEST_TYPE' directory" run_tests_from_dir $TEST_TYPE ;; wasm) make_wasm_tests - echo "Running only the tests from 'tests/$TEST_TYPE' directory" run_tests_from_dir $TEST_TYPE ;; wasm_sym) - make_wasm_sym_tests ;& + make_wasm_sym_tests ;& # Fallthrough native) ;& # Fallthrough ethereum) ;& # Fallthrough ethereum_bench) ;& # Fallthrough other) - echo "Running only the tests from 'tests/$TEST_TYPE' directory" run_tests_from_dir $TEST_TYPE ;; examples) @@ -250,3 +249,6 @@ jobs: token: ${{ secrets.CODECOV_TOKEN }} file: ./coverage.xml yml: ./codecov.yml +# Disabled this line because Codecov has been extra flaky lately, and having to re-run the entire +# test suite until every coverage upload step succeeds is more of a hassle than it's worth. +# fail_ci_if_error: true \ No newline at end of file From eecd9b5a67b25e2cabe55ffc783e7a0ea65d7bde Mon Sep 17 00:00:00 2001 From: "Samuel E. Moelius" <35515885+smoelius@users.noreply.github.com> Date: Fri, 8 May 2020 11:45:17 -0400 Subject: [PATCH 075/104] Update ci.yml Add -p to coverage run. --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5ae027ef0..c3ba5f94f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -161,7 +161,7 @@ jobs: ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txtarget $ADDRESS" EXPECTED_TX=31 fi - coverage run -m manticore --contract MetaCoin --workspace output $ADDITIONAL_ARGS + coverage run -p -m manticore --contract MetaCoin --workspace output $ADDITIONAL_ARGS # Truffle smoke test. We test if manticore is able to generate states # from a truffle project. ACTUAL_TX="$(ls output/*tx -l | wc -l)" From 44e6c0a6b106b31c68fd0e3e7cde6b85c062df6c Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 15 May 2020 00:35:38 +0000 Subject: [PATCH 076/104] Do not store constraints in Storage. --- manticore/platforms/evm_world_state.py | 8 -------- 1 file changed, 8 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index ebbdef50d..77769b967 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -22,8 +22,6 @@ def __init__(self, constraints: ConstraintSet, address: int): :param constraints: the ConstraintSet with which this Storage object is associated :param address: the address that owns this storage """ - self.constraints = constraints - self.warned = False self.data = constraints.new_array( index_bits=256, value_bits=256, @@ -451,12 +449,6 @@ def set_storage_data( if storage is None: storage = self.new_storage(constraints, address) self._storage[address] = storage - while storage.constraints != constraints and constraints is not None: - constraints = constraints._parent - if storage.constraints != constraints: - if not storage.warned: - logger.warning("Constraints have changed") - storage.warned = True storage.set(offset, value) def set_code(self, address: int, code: Union[bytes, Array]): From c3ae87fbd143e75bbe269fa70a1556ed063b084c Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 15 May 2020 01:55:59 +0000 Subject: [PATCH 077/104] Eliminate use of dirty. --- manticore/platforms/evm_world_state.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 77769b967..629b2612e 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -31,7 +31,6 @@ def __init__(self, constraints: ConstraintSet, address: int): # ArrayProxy.get in expression.py. # default=0, ) - self.dirty = False def __getitem__(self, offset: Union[int, BitVec]) -> Union[int, BitVec]: return self.get(offset, 0) @@ -43,7 +42,6 @@ def get(self, offset: Union[int, BitVec], default: Union[int, BitVec]) -> Union[ def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): self.data[offset] = value - self.dirty = True def get_items(self) -> List[Tuple[Union[int, BitVec], Union[int, BitVec]]]: items = [] @@ -349,7 +347,7 @@ def has_storage(self, address: int) -> bool: pass storage = self._storage.get(address) if storage is not None: - dirty = dirty or storage.dirty + dirty = dirty or len(storage.data.written) > 0 return dirty def get_storage(self, address: int) -> Optional[Storage]: From 747ad691d77d1c641b23827228b9e7b6fecb4759 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 15 May 2020 11:10:31 +0000 Subject: [PATCH 078/104] Rename Storage.data to Storage._data. --- manticore/platforms/evm.py | 6 +++--- manticore/platforms/evm_world_state.py | 14 +++++++------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index c80b5a97c..b001e4f2f 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -3063,7 +3063,7 @@ def dump(self, stream, state, mevm, message): storage = blockchain._get_storage(state.constraints, account_address) storage.dump(stream, state) - stream.write("Storage: %s\n" % translate_to_smtlib(storage.data, use_bindings=False)) + stream.write("Storage: %s\n" % translate_to_smtlib(storage._data, use_bindings=False)) if consts.sha3 is consts.sha3.concretize: all_used_indexes = [] @@ -3073,14 +3073,14 @@ def dump(self, stream, state, mevm, message): # get the storage for account_address storage = blockchain._get_storage(temp_cs, account_address) # we are interested only in used slots - temp_cs.add(storage.data.is_known(index) != 0) + temp_cs.add(storage._data.is_known(index) != 0) # Query the solver to get all storage indexes with used slots all_used_indexes = Z3Solver.instance().get_all_values(temp_cs, index) if all_used_indexes: stream.write("Storage:\n") for i in all_used_indexes: - value = simplify(storage.data.get(i)) + value = simplify(storage._data.get(i)) is_storage_symbolic = issymbolic(value) and not isinstance( value, BitVecConstant ) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 629b2612e..380183a4d 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -22,7 +22,7 @@ def __init__(self, constraints: ConstraintSet, address: int): :param constraints: the ConstraintSet with which this Storage object is associated :param address: the address that owns this storage """ - self.data = constraints.new_array( + self._data = constraints.new_array( index_bits=256, value_bits=256, name=f"STORAGE_DATA_{address:x}", @@ -38,14 +38,14 @@ def __getitem__(self, offset: Union[int, BitVec]) -> Union[int, BitVec]: def get(self, offset: Union[int, BitVec], default: Union[int, BitVec]) -> Union[int, BitVec]: if not isinstance(default, BitVec): default = BitVecConstant(256, default) - return self.data.get(offset, default) + return self._data.get(offset, default) def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): - self.data[offset] = value + self._data[offset] = value def get_items(self) -> List[Tuple[Union[int, BitVec], Union[int, BitVec]]]: items = [] - array = self.data.array + array = self._data.array while not isinstance(array, ArrayVariable): items.append((array.index, array.value)) array = array.array @@ -53,12 +53,12 @@ def get_items(self) -> List[Tuple[Union[int, BitVec], Union[int, BitVec]]]: def dump(self, stream: TextIOBase, state: State): concrete_indexes = set() - for sindex in self.data.written: + for sindex in self._data.written: concrete_indexes.add(state.solve_one(sindex, constrain=True)) for index in concrete_indexes: stream.write( - f"storage[{index:x}] = {state.solve_one(self.data[index], constrain=True):x}\n" + f"storage[{index:x}] = {state.solve_one(self._data[index], constrain=True):x}\n" ) @@ -347,7 +347,7 @@ def has_storage(self, address: int) -> bool: pass storage = self._storage.get(address) if storage is not None: - dirty = dirty or len(storage.data.written) > 0 + dirty = dirty or len(storage._data.written) > 0 return dirty def get_storage(self, address: int) -> Optional[Storage]: From 235d0b5796324956b332cceb69778f88d74688f2 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Sun, 24 May 2020 12:01:57 +0000 Subject: [PATCH 079/104] Add docstring to Storage.new_storage. --- manticore/platforms/evm_world_state.py | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 380183a4d..0f612ec4c 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -5,7 +5,15 @@ from typing import Dict, List, Optional, Set, Tuple, Union from urllib.parse import ParseResult, urlparse from web3 import Web3 -from ..core.smtlib import Array, ArrayVariable, BitVec, BitVecConstant, BitVecITE, BitVecZeroExtend, ConstraintSet +from ..core.smtlib import ( + Array, + ArrayVariable, + BitVec, + BitVecConstant, + BitVecITE, + BitVecZeroExtend, + ConstraintSet, +) from ..ethereum.state import State from ..exceptions import EthereumError @@ -69,6 +77,12 @@ class WorldState: def new_storage( self, constraints: ConstraintSet, address: int, items: Optional[Dict[int, int]] = None ) -> Storage: + """ + Private auxiliary function to consruct a new storage object + :param constraints: the ConstraintSet with which this Storage object is associated + :param address: the address that owns this storageq + :param items: optional items to populate the storage with + """ storage = Storage(constraints, address) if items is not None: for key, value in items.items(): From 6054033e4687eb6526290cebf859d0f7d4823da2 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Mon, 25 May 2020 15:22:28 +0000 Subject: [PATCH 080/104] Move get_items into ArrayProxy. --- manticore/core/smtlib/expression.py | 10 +++++++++- manticore/platforms/evm_world_state.py | 7 +------ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index 1099031fb..6edfae1c5 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -4,7 +4,7 @@ import re import copy -from typing import Union, Optional, Dict, List +from typing import Union, Optional, Dict, List, Tuple class ExpressionException(SmtlibError): @@ -1179,6 +1179,14 @@ def get(self, index, default=None): default = self.cast_value(default) return BitVecITE(self._array.value_bits, is_known, value, default) + def get_items(self) -> List[Tuple[Union[int, BitVec], Union[int, BitVec]]]: + items = [] + array = self.array + while not isinstance(array, ArrayVariable): + items.append((array.index, array.value)) + array = array.array + return items + class ArraySelect(BitVec): __slots__ = ["_operands"] diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 0f612ec4c..686b457f9 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -52,12 +52,7 @@ def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): self._data[offset] = value def get_items(self) -> List[Tuple[Union[int, BitVec], Union[int, BitVec]]]: - items = [] - array = self._data.array - while not isinstance(array, ArrayVariable): - items.append((array.index, array.value)) - array = array.array - return items + return self._data.get_items() def dump(self, stream: TextIOBase, state: State): concrete_indexes = set() From 45b87b83dc67ebeec1bceaebe8e38b1caa66ea42 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 11:14:39 +0000 Subject: [PATCH 081/104] Correct bitvec width in add_to/sub_from_balance. --- manticore/platforms/evm.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 6d11c4240..845e95956 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2901,10 +2901,14 @@ def get_balance(self, address: int) -> Union[int, BitVec]: return self._world_state.get_balance(address) def add_to_balance(self, address: int, value: Union[int, BitVec]): + if isinstance(value, BitVec): + value = Operators.ZEXTEND(value, 512) new_balance = self.get_balance(address) + value self.set_balance(address, new_balance) def sub_from_balance(self, address: int, value: Union[int, BitVec]): + if isinstance(value, BitVec): + value = Operators.ZEXTEND(value, 512) new_balance = self.get_balance(address) - value self.set_balance(address, new_balance) From 60daa52ed9bf7a5be591db3a77564cb34ec91dd0 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 11:22:04 +0000 Subject: [PATCH 082/104] Blacken. --- manticore/ethereum/cli.py | 4 +- manticore/ethereum/manticore.py | 4 +- tests/ethereum/test_storage.py | 60 ++++++++++++++++++++------ tests/ethereum_truffle/test_truffle.py | 3 +- 4 files changed, 53 insertions(+), 18 deletions(-) diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index 4bc1c1f79..efff534ed 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -144,7 +144,9 @@ def ethereum_main(args, logger): if args.txtarget is not None: contract_account = int(args.txtarget, base=0) if world_state is not None and not world_state.get_code(contract_account): - raise EthereumError("Could not get code for target account: " + args.txtarget) + raise EthereumError( + "Could not get code for target account: " + args.txtarget + ) m.multi_tx_analysis( args.argv[0], diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 2a74b5162..4815746e0 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -391,9 +391,7 @@ def contract_accounts(self): def get_account(self, name): return self._accounts[name] - def __init__( - self, world_state: Optional[WorldState] = None, plugins=None, **kwargs - ): + def __init__(self, world_state: Optional[WorldState] = None, plugins=None, **kwargs): """ A Manticore EVM manager :param plugins: the plugins to register in this manticore manager diff --git a/tests/ethereum/test_storage.py b/tests/ethereum/test_storage.py index 8ceb80738..6df203896 100644 --- a/tests/ethereum/test_storage.py +++ b/tests/ethereum/test_storage.py @@ -12,13 +12,18 @@ ) from manticore.core.smtlib.solver import Z3Solver from manticore.core.smtlib.expression import * -from manticore.platforms.evm_world_state import DefaultWorldState, DefaultWorldState, OverlayWorldState +from manticore.platforms.evm_world_state import ( + DefaultWorldState, + DefaultWorldState, + OverlayWorldState, +) from manticore.utils.helpers import pickle_dumps ADDRESS = 0x111111111111111111111111111111111111111 # sam.moelius: These tests were shamelessly copied from test_smtlibv2.py. + class StorageTest(unittest.TestCase): _multiprocess_can_split_ = True @@ -88,30 +93,45 @@ def testBasicStorage256(self): world_state.set_storage_data(cs, ADDRESS, other_key, other_value) # assert that the storage is 111...111 at key position - cs.add(world_state.get_storage_data(cs, ADDRESS, key) == 11111111111111111111111111111111111111111111) + cs.add( + world_state.get_storage_data(cs, ADDRESS, key) + == 11111111111111111111111111111111111111111111 + ) # let's restrict key to be greater than 1000 cs.add(key.ugt(1000)) with cs as temp_cs: # 1001 position of storage can be 111...111 - temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == 11111111111111111111111111111111111111111111) + temp_cs.add( + world_state.get_storage_data(cs, ADDRESS, 1001) + == 11111111111111111111111111111111111111111111 + ) self.assertTrue(self.solver.check(temp_cs)) with cs as temp_cs: # 1001 position of storage can also be 222...222 - temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == 22222222222222222222222222222222222222222222) + temp_cs.add( + world_state.get_storage_data(cs, ADDRESS, 1001) + == 22222222222222222222222222222222222222222222 + ) self.assertTrue(self.solver.check(temp_cs)) with cs as temp_cs: # but if it is 222...222 ... - temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == 22222222222222222222222222222222222222222222) + temp_cs.add( + world_state.get_storage_data(cs, ADDRESS, 1001) + == 22222222222222222222222222222222222222222222 + ) # then key can not be 1001 temp_cs.add(key == 1001) self.assertFalse(self.solver.check(temp_cs)) with cs as temp_cs: # If 1001 position is 222...222 ... - temp_cs.add(world_state.get_storage_data(cs, ADDRESS, 1001) == 22222222222222222222222222222222222222222222) + temp_cs.add( + world_state.get_storage_data(cs, ADDRESS, 1001) + == 22222222222222222222222222222222222222222222 + ) # then key can be 1002 for ex.. temp_cs.add(key == 1002) self.assertTrue(self.solver.check(temp_cs)) @@ -135,10 +155,14 @@ def testBasicStorageStore(self): cs.add(key.ugt(1000)) # 1001 position of storage can be 'A' - self.assertTrue(self.solver.can_be_true(cs, world_state.get_storage_data(cs, ADDRESS, 1001) == ord("A"))) + self.assertTrue( + self.solver.can_be_true(cs, world_state.get_storage_data(cs, ADDRESS, 1001) == ord("A")) + ) # 1001 position of storage can be 'B' - self.assertTrue(self.solver.can_be_true(cs, world_state.get_storage_data(cs, ADDRESS, 1001) == ord("B"))) + self.assertTrue( + self.solver.can_be_true(cs, world_state.get_storage_data(cs, ADDRESS, 1001) == ord("B")) + ) with cs as temp_cs: # but if it is 'B' ... @@ -189,7 +213,9 @@ def testBasicStorageSymbIdx(self): world_state.set_storage_data(cs, ADDRESS, key, 1) # Write 1 to a single location - cs.add(world_state.get_storage_data(cs, ADDRESS, index) != 0) # Constrain index so it selects that location + cs.add( + world_state.get_storage_data(cs, ADDRESS, index) != 0 + ) # Constrain index so it selects that location cs.add(index != key) # key and index are the same there is only one slot in 1 @@ -202,9 +228,13 @@ def testBasicStorageSymbIdx2(self): index = cs.new_bitvec(256, name="index") world_state.set_storage_data(cs, ADDRESS, key, 1) # Write 1 to a single location - cs.add(world_state.get_storage_data(cs, ADDRESS, index) != 0) # Constrain index so it selects that location + cs.add( + world_state.get_storage_data(cs, ADDRESS, index) != 0 + ) # Constrain index so it selects that location a_index = self.solver.get_value(cs, index) # get a concrete solution for index - cs.add(world_state.get_storage_data(cs, ADDRESS, a_index) != 0) # now storage must have something at that location + cs.add( + world_state.get_storage_data(cs, ADDRESS, a_index) != 0 + ) # now storage must have something at that location cs.add(a_index != index) # remove it from the solutions # It should not be another solution for index @@ -217,9 +247,13 @@ def testBasicStorageSymbIdx3(self): index = cs.new_bitvec(256, name="index") world_state.set_storage_data(cs, ADDRESS, 0, 1) # Write 1 to first location - world_state.set_storage_data(cs, ADDRESS, key, 2) # Write 2 to a symbolic (potentially any (potentially 0))location + world_state.set_storage_data( + cs, ADDRESS, key, 2 + ) # Write 2 to a symbolic (potentially any (potentially 0))location - solutions = self.solver.get_all_values(cs, world_state.get_storage_data(cs, ADDRESS, 0)) # get a concrete solution for index + solutions = self.solver.get_all_values( + cs, world_state.get_storage_data(cs, ADDRESS, 0) + ) # get a concrete solution for index self.assertItemsEqual(solutions, (1, 2)) solutions = self.solver.get_all_values( diff --git a/tests/ethereum_truffle/test_truffle.py b/tests/ethereum_truffle/test_truffle.py index b64cd77e6..a3494e397 100644 --- a/tests/ethereum_truffle/test_truffle.py +++ b/tests/ethereum_truffle/test_truffle.py @@ -173,7 +173,8 @@ def test_predeployed(self): require(Predeployed(%s).y() == _y, "y != _y"); } } - """ % (address, address), + """ + % (address, address), ] subprocess.check_call(cmd) From b8880cf2555ccd94d730dbf0beed68cd70446451 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 11:29:18 +0000 Subject: [PATCH 083/104] Interpret coinbase as hex. --- manticore/platforms/evm_world_state.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 686b457f9..6aedeac6d 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -290,7 +290,7 @@ def get_gaslimit(self) -> int: return self._web3().eth.getBlock("latest")["gasLimit"] def get_coinbase(self) -> int: - return int(self._web3().eth.coinbase) + return int(self._web3().eth.coinbase, 16) #################################################################################################### From c4a0471ddf1c37cdebb785292f97bf95a701b2c6 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 11:41:44 +0000 Subject: [PATCH 084/104] Fiz __getstae__/__setstate__ names. --- manticore/platforms/evm.py | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 845e95956..b860b6686 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2406,25 +2406,25 @@ def __init__( def __getstate__(self): state = super().__getstate__() - state["pending_transaction"] = self._pending_transaction - state["logs"] = self._logs - state["world_state"] = self._world_state - state["constraints"] = self._constraints - state["callstack"] = self._callstack - state["deleted_accounts"] = self._deleted_accounts - state["transactions"] = self._transactions + state["_pending_transaction"] = self._pending_transaction + state["_logs"] = self._logs + state["_world_state"] = self._world_state + state["_constraints"] = self._constraints + state["_callstack"] = self._callstack + state["_deleted_accounts"] = self._deleted_accounts + state["_transactions"] = self._transactions state["_fork"] = self._fork return state def __setstate__(self, state): super().__setstate__(state) - self._constraints = state["constraints"] - self._pending_transaction = state["pending_transaction"] - self._world_state = state["world_state"] - self._deleted_accounts = state["deleted_accounts"] - self._logs = state["logs"] - self._callstack = state["callstack"] - self._transactions = state["transactions"] + self._constraints = state["_constraints"] + self._pending_transaction = state["_pending_transaction"] + self._world_state = state["_world_state"] + self._deleted_accounts = state["_deleted_accounts"] + self._logs = state["_logs"] + self._callstack = state["_callstack"] + self._transactions = state["_transactions"] self._fork = state["_fork"] for _, _, _, _, vm in self._callstack: From 15d5366e288719794ed07cc9d684422cb6cbf405 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 11:46:47 +0000 Subject: [PATCH 085/104] Add comment re disabling uninitialized storage detector. --- manticore/ethereum/cli.py | 1 + 1 file changed, 1 insertion(+) diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index efff534ed..2aa0713de 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -81,6 +81,7 @@ def choose_detectors(args): f"{e} is not a detector name, must be one of {arguments}. See also `--list-detectors`." ) + # sam.moelius: Do not enable uninitialized storage detector when using RPC. It generates too much noise. if args.url is not None: exclude.append(DetectUninitializedStorage.ARGUMENT) From 3a0136067d9aff349f17839872d287f016d17738 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 11:57:51 +0000 Subject: [PATCH 086/104] Set blockheader information. --- manticore/platforms/evm.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index b860b6686..0de6493a3 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2954,6 +2954,12 @@ def start_block( logger.info("Coinbase account does not exists") self.create_account(coinbase) + self._world_state.set_blocknumber(blocknumber) + self._world_state.set_timestamp(timestamp) + self._world_state.set_difficulty(difficulty) + self._world_state.set_gaslimit(gaslimit) + self._world_state.set_coinbase(coinbase) + def end_block(self, block_reward=None): coinbase = self.block_coinbase() if coinbase not in self: From 1de8eba74d337e66136a845ce2c86bea9de86195 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 13:50:03 +0000 Subject: [PATCH 087/104] Use self.get_storage. --- manticore/platforms/evm.py | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 0de6493a3..5b764aa91 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2414,6 +2414,7 @@ def __getstate__(self): state["_deleted_accounts"] = self._deleted_accounts state["_transactions"] = self._transactions state["_fork"] = self._fork + return state def __setstate__(self, state): @@ -2633,13 +2634,7 @@ def _open_transaction(self, sort, address, price, bytecode_or_data, caller, valu vm = self._make_vm_for_tx(tx) self._callstack.append( - ( - tx, - self.logs, - self.deleted_accounts, - copy.copy(self._world_state.get_storage(address)), - vm, - ) + (tx, self.logs, self.deleted_accounts, copy.copy(self.get_storage(address)), vm,) ) self.forward_events_from(vm) self._publish("did_open_transaction", tx) From 91d48ed55bc2efc0ac8285f5b5b574648ee9d456 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 13:53:21 +0000 Subject: [PATCH 088/104] Use self._set_storage. --- manticore/platforms/evm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 5b764aa91..1d0397927 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2651,7 +2651,7 @@ def _close_transaction(self, result, data=None, rollback=False): if data is not None and self.current_vm is not None: self.current_vm._return_data = data if rollback: - self._world_state.set_storage(vm.address, account_storage) + self._set_storage(vm.address, account_storage) self._logs = logs # Return the transaction value self.send_funds(tx.address, tx.caller, tx.value) From 02a540e7e089de85ec06ee4f8b23a85358282dce Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 14:19:44 +0000 Subject: [PATCH 089/104] Nominal changes. --- manticore/platforms/evm_world_state.py | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 6aedeac6d..406c8641e 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -20,10 +20,6 @@ logger = logging.getLogger(__name__) -# sam.moelius: map records which (symbolic) offsets have been written to. data holds the values -# written. - - class Storage: def __init__(self, constraints: ConstraintSet, address: int): """ @@ -33,7 +29,7 @@ def __init__(self, constraints: ConstraintSet, address: int): self._data = constraints.new_array( index_bits=256, value_bits=256, - name=f"STORAGE_DATA_{address:x}", + name=f"STORAGE_{address:x}", avoid_collisions=True, # sam.moelius: The use of default here creates unnecessary if-then-elses. See # ArrayProxy.get in expression.py. From a4c599decb982b01c04397541a4e76924349d712 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 11 Jun 2020 19:42:42 +0000 Subject: [PATCH 090/104] Callstack type has changed. --- manticore/platforms/evm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 1d0397927..8eb91a4bc 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -1956,7 +1956,7 @@ def SSTORE_gas(self, offset, value): # Get the storage from the snapshot took before this call try: original_value = self.world._callstack[-1][-2].get(offset, 0) - except IndexError: + except AttributeError: original_value = 0 current_value = self.world.get_storage_data(storage_address, offset) From 2215ba8707327aa9b5855fa29dbf1b401dc349c3 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 01:12:04 +0000 Subject: [PATCH 091/104] Eliminate unused imports. --- manticore/platforms/evm_world_state.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 406c8641e..6502bbe98 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -1,5 +1,5 @@ import logging -from abc import ABC, abstractmethod +from abc import abstractmethod from eth_typing import ChecksumAddress, URI from io import TextIOBase from typing import Dict, List, Optional, Set, Tuple, Union @@ -7,11 +7,8 @@ from web3 import Web3 from ..core.smtlib import ( Array, - ArrayVariable, BitVec, BitVecConstant, - BitVecITE, - BitVecZeroExtend, ConstraintSet, ) from ..ethereum.state import State From 6b3dbf36833bb0960844f69201cc0d2ba0d73130 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 01:12:31 +0000 Subject: [PATCH 092/104] Simplify Storage.get. --- manticore/platforms/evm_world_state.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 6502bbe98..face8ca12 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -37,8 +37,6 @@ def __getitem__(self, offset: Union[int, BitVec]) -> Union[int, BitVec]: return self.get(offset, 0) def get(self, offset: Union[int, BitVec], default: Union[int, BitVec]) -> Union[int, BitVec]: - if not isinstance(default, BitVec): - default = BitVecConstant(256, default) return self._data.get(offset, default) def set(self, offset: Union[int, BitVec], value: Union[int, BitVec]): From c29a24a204226735a2afd5b835a9d63cbac47e8a Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 01:14:37 +0000 Subject: [PATCH 093/104] Fix bugs introduced by merge. --- manticore/platforms/evm.py | 7 ++----- tests/ethereum/test_general.py | 13 ++++++++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 8eb91a4bc..b59aa7039 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -16,8 +16,6 @@ ArrayProxy, Operators, Constant, - ArrayVariable, - ArrayStore, BitVecConstant, ConstraintSet, translate_to_smtlib, @@ -2402,7 +2400,7 @@ def __init__( self._pending_transaction = None self._transactions: List[Transaction] = list() self._fork = fork - self.start_block() + self.start_block(**kwargs) def __getstate__(self): state = super().__getstate__() @@ -2671,8 +2669,7 @@ def _close_transaction(self, result, data=None, rollback=False): if tx.is_human: for deleted_account in self._deleted_accounts: - if deleted_account in self._world_state: - del self._world_state[deleted_account] + self._world_state.delete_account(self.constraints, deleted_account) unused_fee = unused_gas * tx.price used_fee = used_gas * tx.price self.add_to_balance(tx.caller, unused_fee) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 793769503..1b0de2e0b 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -1352,7 +1352,8 @@ def will_evm_execute_instruction_callback(self, state, i, *args, **kwargs): class EthWorldStateTests(unittest.TestCase): class CustomWorldState(WorldState): - pass + def accounts(self): + raise NotImplementedError def test_custom_world_state(self): world_state = EthWorldStateTests.CustomWorldState() @@ -1375,13 +1376,15 @@ def test_init_timestamp(self): def test_init_difficulty(self): constraints = ConstraintSet() - self.assertEqual(evm.EVMWorld(constraints).block_difficulty(), 0) - self.assertEqual(evm.EVMWorld(constraints, difficulty=1).block_difficulty(), 1) + self.assertEqual(evm.EVMWorld(constraints).block_difficulty(), 0x200) + self.assertEqual(evm.EVMWorld(constraints, difficulty=0x201).block_difficulty(), 0x201) def test_init_gaslimit(self): constraints = ConstraintSet() - self.assertEqual(evm.EVMWorld(constraints).block_gaslimit(), 0) - self.assertEqual(evm.EVMWorld(constraints, gaslimit=1).block_gaslimit(), 1) + self.assertEqual(evm.EVMWorld(constraints).block_gaslimit(), 0x7FFFFFFF) + self.assertEqual( + evm.EVMWorld(constraints, gaslimit=0x80000000).block_gaslimit(), 0x80000000 + ) def test_init_coinbase(self): constraints = ConstraintSet() From f257ec896860e46cb59e96d3082384a95ac3c661 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 02:31:00 +0000 Subject: [PATCH 094/104] More merge bug fixes. --- manticore/platforms/evm.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index b59aa7039..dcb6c0f0e 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -87,7 +87,7 @@ def globalfakesha3(data): description=( "Default behavior for transaction failing because not enough funds." "optimistic: Assume there is always enough funds to pay for value and gas. Wont fork" - "pessimistic: Assume the balance is never enough for paying fo a transaction. Wont fork" + "pessimistic: Assume the balance is never enough for paying for a transaction. Wont fork" "both: Will fork for both options if possible." ), ) @@ -2604,7 +2604,7 @@ def _open_transaction(self, sort, address, price, bytecode_or_data, caller, valu f"Error: contract created from address {hex(caller)} with nonce {self.get_nonce(caller)} was expected to be at address {hex(expected_address)}, but create_contract was called with address={hex(address)}" ) - if address not in self.accounts: + if not self._world_state.is_remote() and address not in self.accounts: logger.info("Address does not exists creating it.") # Creating an unaccessible account self.create_account(address=address, nonce=int(sort != "CREATE")) @@ -2621,7 +2621,7 @@ def _open_transaction(self, sort, address, price, bytecode_or_data, caller, valu self.sub_from_balance(caller, aux_price * aux_gas) self.send_funds(tx.caller, tx.address, tx.value) - if tx.address not in self.accounts: + if not self._world_state.is_remote() and tx.address not in self.accounts: self.create_account(tx.address) # If not a human tx, reset returndata @@ -2942,7 +2942,7 @@ def start_block( gaslimit=0x7FFFFFFF, coinbase=0, ): - if coinbase not in self.accounts and coinbase != 0: + if not self._world_state.is_remote() and coinbase not in self.accounts and coinbase != 0: logger.info("Coinbase account does not exists") self.create_account(coinbase) From 399dd089b06e17d2ae02f3a95c4a5986f86f50f6 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 03:19:09 +0000 Subject: [PATCH 095/104] Handle case where EXP's exponent is a symbolic constant. --- manticore/platforms/evm.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index dcb6c0f0e..c188f3776 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -1526,6 +1526,8 @@ def EXP(self, base, exponent): :param exponent: exponent value, concretized with sampled values :return: BitVec* EXP result """ + if isinstance(exponent, Constant): + exponent = exponent.value if exponent == 0: return 1 From 7a382812d8e457afee5b5c4501588494e9ffa250 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 09:58:04 +0000 Subject: [PATCH 096/104] Turn off detectors in truffle maze test. --- tests/ethereum_truffle/test_truffle.py | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/ethereum_truffle/test_truffle.py b/tests/ethereum_truffle/test_truffle.py index a3494e397..62e3bf5ce 100644 --- a/tests/ethereum_truffle/test_truffle.py +++ b/tests/ethereum_truffle/test_truffle.py @@ -228,6 +228,7 @@ def test_maze(self): "--txtarget", address, "--txnocoverage", + "--exclude-all", ] mcore = subprocess.Popen(cmd, stdout=subprocess.PIPE) From 3446e211bdb87854c0a3cc93f979472392c7cb2d Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 13:05:50 +0000 Subject: [PATCH 097/104] Implement Storage.__copy__. --- manticore/platforms/evm.py | 11 +++++++---- manticore/platforms/evm_world_state.py | 6 ++++++ 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index c188f3776..c833ff1fd 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -1954,10 +1954,13 @@ def SSTORE_gas(self, offset, value): self.fail_if(Operators.ULT(self.gas, SSSTORESENTRYGAS)) # Get the storage from the snapshot took before this call + original_value = 0 try: - original_value = self.world._callstack[-1][-2].get(offset, 0) - except AttributeError: - original_value = 0 + storage = self.world._callstack[-1][-2] + if storage is not None: + original_value = storage.get(offset, 0) + except IndexError: + pass current_value = self.world.get_storage_data(storage_address, offset) @@ -2634,7 +2637,7 @@ def _open_transaction(self, sort, address, price, bytecode_or_data, caller, valu vm = self._make_vm_for_tx(tx) self._callstack.append( - (tx, self.logs, self.deleted_accounts, copy.copy(self.get_storage(address)), vm,) + (tx, self.logs, self.deleted_accounts, copy.copy(self.get_storage(address)), vm) ) self.forward_events_from(vm) self._publish("did_open_transaction", tx) diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index face8ca12..8d538932b 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -1,4 +1,5 @@ import logging +import copy from abc import abstractmethod from eth_typing import ChecksumAddress, URI from io import TextIOBase @@ -33,6 +34,11 @@ def __init__(self, constraints: ConstraintSet, address: int): # default=0, ) + def __copy__(self): + other = Storage.__new__(Storage) + other._data = copy.copy(self._data) + return other + def __getitem__(self, offset: Union[int, BitVec]) -> Union[int, BitVec]: return self.get(offset, 0) From cc97a385f656e20edbb5945a6580114cbb79a06a Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 13:07:06 +0000 Subject: [PATCH 098/104] Convert gas to constant in make_VMTests.py. --- tests/auto_generators/make_VMTests.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/auto_generators/make_VMTests.py b/tests/auto_generators/make_VMTests.py index bd32b30a4..1aa35daf4 100644 --- a/tests/auto_generators/make_VMTests.py +++ b/tests/auto_generators/make_VMTests.py @@ -8,10 +8,10 @@ git clone https://github.com/ethereum/tests --depth=1 ## Get help -python make_VMTest.py --help +python make_VMTests.py --help ## Generate concrete tests: -for i in tests/BlockchainTests/ValidBlocks/VMTests/*/*json; do python make_VMTest.py -i $i --fork Istanbul -o ethereum_vm/VMTests_concrete; done +for i in tests/BlockchainTests/ValidBlocks/VMTests/*/*.json; do python make_VMTests.py -i $i --fork Istanbul -o ethereum_vm/VMTests_concrete; done """ import argparse @@ -66,6 +66,7 @@ def gen_header(testcases): import unittest from binascii import unhexlify from manticore import ManticoreEVM, Plugin +from manticore.core.smtlib import to_constant from manticore.utils import config ''' @@ -214,7 +215,7 @@ def did_close_transaction_callback(self, state, tx): body += f""" for state in m.all_states: world = state.platform - self.assertEqual(used_gas_plugin.used_gas, {blockheader['gasUsed']}) + self.assertEqual(to_constant(used_gas_plugin.used_gas), {blockheader['gasUsed']}) world.end_block()""" From 94055f91c6d02987fd4f9c4cb5805b01b8dfd6c9 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 16:28:35 +0000 Subject: [PATCH 099/104] Coverage fixes in ci.yml. --- .github/workflows/ci.yml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3489cc659..272325e78 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -36,7 +36,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - type: ["ethereum_bench", "examples", "ethereum", "ethereum_truffle", "ethereum_vm", "native", "wasm", "wasm_sym", "other"] + type: ["ethereum_bench", "examples", "ethereum", "ethereum_metacoin", "ethereum_truffle", "ethereum_vm", "native", "wasm", "wasm_sym", "other"] steps: - uses: actions/checkout@v1 - name: Set up Python 3.6 @@ -162,11 +162,10 @@ jobs: run_metacoin_tests(){ COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc ADDITIONAL_ARGS=. - EXPECTED_TX=34 + EXPECTED_TX=26 if [ "$1" = "deploy" ]; then ADDRESS="$(truffle deploy | grep '> contract address:.*' | tail -n 1 | grep -o '0x.*$')" ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txtarget $ADDRESS" - EXPECTED_TX=26 fi coverage run -p -m manticore --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic $ADDITIONAL_ARGS # Truffle smoke test. We test if manticore is able to generate states @@ -174,10 +173,10 @@ jobs: ACTUAL_TX="$(ls output/*tx -l | wc -l)" rm -rf output if [ "$ACTUAL_TX" != "$EXPECTED_TX" ]; then - echo "Truffle test failed: $ACTUAL_TX != $EXPECTED_TX" + echo "MetaCoin test failed: $ACTUAL_TX != $EXPECTED_TX" return 1 fi - echo "Truffle test succeded" + echo "MetaCoin test succeded" return 0 } @@ -213,12 +212,11 @@ jobs: # Test type case $TEST_TYPE in - ethereum_truffle) - echo "Running truffle tests" + ethereum_metacoin) + echo "Running metacoin tests" install_node_packages ganache-cli -p 7545 -i 5777 & - run_tests_from_dir $TEST_TYPE \ - && mkdir metacoin_tests \ + mkdir metacoin_tests \ && cd metacoin_tests \ && truffle unbox metacoin \ && run_metacoin_tests \ @@ -228,6 +226,12 @@ jobs: && cd .. \ && cp metacoin_tests/coverage.xml . ;; + ethereum_truffle) + echo "Running truffle tests" + install_node_packages + ganache-cli -p 7545 -i 5777 & + run_tests_from_dir $TEST_TYPE + ;; ethereum_vm) make_vmtests run_tests_from_dir $TEST_TYPE From 8af686935b49efdba225f11979e19b5be3201287 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 16:55:42 +0000 Subject: [PATCH 100/104] More ci.yml fixes. --- .github/workflows/ci.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 272325e78..678676f85 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -162,10 +162,11 @@ jobs: run_metacoin_tests(){ COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc ADDITIONAL_ARGS=. - EXPECTED_TX=26 + EXPECTED_TX=27 if [ "$1" = "deploy" ]; then ADDRESS="$(truffle deploy | grep '> contract address:.*' | tail -n 1 | grep -o '0x.*$')" ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txtarget $ADDRESS" + EXPECTED_TX=26 fi coverage run -p -m manticore --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic $ADDITIONAL_ARGS # Truffle smoke test. We test if manticore is able to generate states From 4a23d8af71adf6244b1121853334e5e541a83753 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 17:15:44 +0000 Subject: [PATCH 101/104] Up SMT timeout for metacoin tests. --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 678676f85..ae3044ab2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -168,7 +168,7 @@ jobs: ADDITIONAL_ARGS="--rpc 127.0.0.1:7545 --txtarget $ADDRESS" EXPECTED_TX=26 fi - coverage run -p -m manticore --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic $ADDITIONAL_ARGS + coverage run -p -m manticore --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic --smt.timeout 600 $ADDITIONAL_ARGS # Truffle smoke test. We test if manticore is able to generate states # from a truffle project. ACTUAL_TX="$(ls output/*tx -l | wc -l)" From 3fc4264caacdbeef5a408c24c50b60cf798fa582 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 18:22:21 +0000 Subject: [PATCH 102/104] Fix bug concerning balance width. --- manticore/platforms/evm.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index c833ff1fd..fac445a72 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2895,18 +2895,18 @@ def set_balance(self, address: int, value: Union[int, BitVec]): self._world_state.set_balance(address, value) def get_balance(self, address: int) -> Union[int, BitVec]: - return self._world_state.get_balance(address) + return Operators.EXTRACT(self._world_state.get_balance(address), 0, 256) def add_to_balance(self, address: int, value: Union[int, BitVec]): if isinstance(value, BitVec): value = Operators.ZEXTEND(value, 512) - new_balance = self.get_balance(address) + value + new_balance = self._world_state.get_balance(address) + value self.set_balance(address, new_balance) def sub_from_balance(self, address: int, value: Union[int, BitVec]): if isinstance(value, BitVec): value = Operators.ZEXTEND(value, 512) - new_balance = self.get_balance(address) - value + new_balance = self._world_state.get_balance(address) - value self.set_balance(address, new_balance) def send_funds(self, sender: int, recipient: int, value: Union[int, BitVec]): From ebd8cc07da2ed442f608b56a8e969b0a1fee250f Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 18:27:26 +0000 Subject: [PATCH 103/104] Balance width fix was incomplete. --- manticore/platforms/evm.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index fac445a72..180422269 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2901,13 +2901,13 @@ def add_to_balance(self, address: int, value: Union[int, BitVec]): if isinstance(value, BitVec): value = Operators.ZEXTEND(value, 512) new_balance = self._world_state.get_balance(address) + value - self.set_balance(address, new_balance) + self._world_state.set_balance(address, new_balance) def sub_from_balance(self, address: int, value: Union[int, BitVec]): if isinstance(value, BitVec): value = Operators.ZEXTEND(value, 512) new_balance = self._world_state.get_balance(address) - value - self.set_balance(address, new_balance) + self._world_state.set_balance(address, new_balance) def send_funds(self, sender: int, recipient: int, value: Union[int, BitVec]): self.sub_from_balance(sender, value) From cca9dbfc29c0614d56796dbd43730e39702ebe5b Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Fri, 12 Jun 2020 18:56:03 +0000 Subject: [PATCH 104/104] Eliminate new_storage method. --- manticore/platforms/evm.py | 4 ++-- manticore/platforms/evm_world_state.py | 27 +++++++++----------------- 2 files changed, 11 insertions(+), 20 deletions(-) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 180422269..1fd757790 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2862,14 +2862,14 @@ def _get_storage(self, constraints: ConstraintSet, address: int) -> Storage: """Private auxiliary function to retrieve the storage""" storage = self._world_state.get_storage(address) if storage is None: - storage = self._world_state.new_storage(constraints, address) + storage = Storage(constraints, address) self._world_state.set_storage(address, storage) return storage def _set_storage(self, address: int, storage: Union[Dict[int, int], Optional[Storage]]): """Private auxiliary function to replace the storage""" if isinstance(storage, dict): - storage = self._world_state.new_storage(self.constraints, address, storage) + storage = Storage(self.constraints, address, storage) self._world_state.set_storage(address, storage) def get_nonce(self, address: Union[int, BitVec]) -> Union[int, BitVec]: diff --git a/manticore/platforms/evm_world_state.py b/manticore/platforms/evm_world_state.py index 8d538932b..0021a1b4f 100644 --- a/manticore/platforms/evm_world_state.py +++ b/manticore/platforms/evm_world_state.py @@ -19,10 +19,13 @@ class Storage: - def __init__(self, constraints: ConstraintSet, address: int): + def __init__( + self, constraints: ConstraintSet, address: int, items: Optional[Dict[int, int]] = None + ): """ :param constraints: the ConstraintSet with which this Storage object is associated :param address: the address that owns this storage + :param items: optional items to populate the storage with """ self._data = constraints.new_array( index_bits=256, @@ -33,6 +36,9 @@ def __init__(self, constraints: ConstraintSet, address: int): # ArrayProxy.get in expression.py. # default=0, ) + if items is not None: + for key, value in items.items(): + self.set(key, value) def __copy__(self): other = Storage.__new__(Storage) @@ -66,21 +72,6 @@ def dump(self, stream: TextIOBase, state: State): class WorldState: - def new_storage( - self, constraints: ConstraintSet, address: int, items: Optional[Dict[int, int]] = None - ) -> Storage: - """ - Private auxiliary function to consruct a new storage object - :param constraints: the ConstraintSet with which this Storage object is associated - :param address: the address that owns this storageq - :param items: optional items to populate the storage with - """ - storage = Storage(constraints, address) - if items is not None: - for key, value in items.items(): - storage.set(key, value) - return storage - @abstractmethod def is_remote(self) -> bool: pass @@ -426,7 +417,7 @@ def delete_account(self, constraints: ConstraintSet, address: int): default_world_state = DefaultWorldState() self._nonce[address] = default_world_state.get_nonce(address) self._balance[address] = default_world_state.get_balance(address) - self._storage[address] = self.new_storage(constraints, address) + self._storage[address] = Storage(constraints, address) self._code[address] = default_world_state.get_code(address) self._deleted_accounts.add(address) @@ -451,7 +442,7 @@ def set_storage_data( ): storage = self._storage.get(address) if storage is None: - storage = self.new_storage(constraints, address) + storage = Storage(constraints, address) self._storage[address] = storage storage.set(offset, value)