From ed29a22fceb0c187e1ee97ae230f5d9524bd0b48 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 7 Dec 2017 20:19:16 -0300 Subject: [PATCH] EVM refactor and simple UI (#629) * Fixes symbolic reentrancy example * Fix coverage Issue# 527 * Remove debug unused code * New solidity biased API and reporting * Updated examples to new api WIP * simple_mapping FIXED. new api * Simple transaction example added. msg.value can be symbolic now * Reentrancy symbolic now updated to new API + bugfixes * Doc and cleanups in evm assembler * EVMInstruction -> Instruction * cleanups * typo * deepcopy in Constant * Better EVM-asm api and doc * some docs * More evm asm docs * Initial seth in place refactor * Fix import * * typo * newline between text and param * similar phrasing to all the other flags * typo * typo * fix function name in comment * sphinx newline * documentation fixes * documentation fixes * refactors * EVMAssembler to EVMAsm * Fix evm @hook signature * EVMAsm * WIP seth doc * WIP move seth * seth moved to manticore module * Fixed DUP and typo * Slightly better evm reporting * review * review * Removed unfinished refactor * Various refactors. Auxiliar for calculating % coverage * Change report in examples * Detailed transactions and reporting accessible to the user2 * Fix on Expression Array * Some documentation * Get full ABI from solc compiler * evm/examples -> bugfixes * Clarify try/except blocks * Code review * Code review --- examples/evm/coverage.py | 2 +- examples/evm/integer_overflow.py | 4 +- examples/evm/minimal.py | 3 +- examples/evm/reentrancy_concrete.py | 4 +- examples/evm/reentrancy_symbolic.py | 2 +- examples/evm/simple_functions.py | 4 +- examples/evm/simple_mapping.py | 4 +- examples/evm/simple_transaction.py | 4 +- examples/evm/solidse.py | 92 +++++++ manticore/core/executor.py | 39 +-- manticore/core/smtlib/expression.py | 46 +++- manticore/core/smtlib/solver.py | 11 +- manticore/manticore.py | 2 +- manticore/platforms/evm.py | 157 +++++++++--- manticore/seth.py | 356 +++++++++++++++++++++++----- 15 files changed, 594 insertions(+), 136 deletions(-) create mode 100644 examples/evm/solidse.py diff --git a/examples/evm/coverage.py b/examples/evm/coverage.py index 6cb9761..31722c7 100644 --- a/examples/evm/coverage.py +++ b/examples/evm/coverage.py @@ -30,7 +30,7 @@ seth.transaction( caller=user_account, print "[+] There are %d reverted states now"% len(seth.final_state_ids) print "[+] There are %d alive states now"% len(seth.running_state_ids) for state_id in seth.running_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] Global coverage: %x"% contract_account print seth.coverage(contract_account) diff --git a/examples/evm/integer_overflow.py b/examples/evm/integer_overflow.py index 680edae..b3ff1ce 100644 --- a/examples/evm/integer_overflow.py +++ b/examples/evm/integer_overflow.py @@ -27,11 +27,11 @@ contract_account.add(seth.SValue) print "[+] There are %d reverted states now"% len(seth.final_state_ids) for state_id in seth.final_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] There are %d alive states now"% len(seth.running_state_ids) for state_id in seth.running_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] Global coverage: %x"% contract_account print seth.coverage(contract_account) diff --git a/examples/evm/minimal.py b/examples/evm/minimal.py index c4aca60..7cfa02d 100644 --- a/examples/evm/minimal.py +++ b/examples/evm/minimal.py @@ -2,7 +2,6 @@ from manticore.seth import ManticoreEVM ################ Script ####################### seth = ManticoreEVM() -seth.verbosity(0) #And now make the contract account to analyze # cat | solc --bin source_code = ''' @@ -42,7 +41,7 @@ print "[+] There are %d reverted states now"% len(seth.final_state_ids) print "[+] There are %d alive states now"% len(seth.running_state_ids) for state_id in seth.running_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] Global coverage:" print seth.coverage(contract_account) diff --git a/examples/evm/reentrancy_concrete.py b/examples/evm/reentrancy_concrete.py index edf0c0f..92f004d 100644 --- a/examples/evm/reentrancy_concrete.py +++ b/examples/evm/reentrancy_concrete.py @@ -127,11 +127,11 @@ print " contract_account %x balance: %d"% (contract_account, seth.get_balance(c print "[+] There are %d reverted states now"% len(seth.final_state_ids) for state_id in seth.final_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] There are %d alive states now"% (len(seth.running_state_ids)) for state_id in seth.running_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] Global coverage:" print seth.coverage(contract_account) diff --git a/examples/evm/reentrancy_symbolic.py b/examples/evm/reentrancy_symbolic.py index ee3b3b9..9edfe62 100644 --- a/examples/evm/reentrancy_symbolic.py +++ b/examples/evm/reentrancy_symbolic.py @@ -119,7 +119,7 @@ exploit_account.get_money() print "[+] There are %d alive states now"% (len(seth.running_state_ids)) for state_id in seth.running_state_ids: - seth.report(state_id) + world = seth.get_world(state_id) print "[+] Global coverage:" print seth.coverage(contract_account, ty='SUICIDE') diff --git a/examples/evm/simple_functions.py b/examples/evm/simple_functions.py index bd678eb..5ac115e 100644 --- a/examples/evm/simple_functions.py +++ b/examples/evm/simple_functions.py @@ -35,11 +35,11 @@ seth.transaction( caller=user_account, print "[+] There are %d reverted states now"% len(seth.final_state_ids) for state_id in seth.final_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] There are %d alive states now"% len(seth.running_state_ids) for state_id in seth.running_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] Global coverage:" print seth.coverage(contract_account) diff --git a/examples/evm/simple_mapping.py b/examples/evm/simple_mapping.py index 78f14d9..6c96c51 100644 --- a/examples/evm/simple_mapping.py +++ b/examples/evm/simple_mapping.py @@ -45,11 +45,11 @@ seth.transaction( caller=user_account, print "[+] There are %d reverted states now"% len(seth.final_state_ids) for state_id in seth.final_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] There are %d alive states now"% len(seth.running_state_ids) for state_id in seth.running_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] Global coverage:" print seth.coverage(contract_account) diff --git a/examples/evm/simple_transaction.py b/examples/evm/simple_transaction.py index 0957e2e..b2b1193 100644 --- a/examples/evm/simple_transaction.py +++ b/examples/evm/simple_transaction.py @@ -31,11 +31,11 @@ contract_account.target(value=seth.SValue) print "[+] There are %d reverted states now"% len(seth.final_state_ids) for state_id in seth.final_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] There are %d alive states now"% len(seth.running_state_ids) for state_id in seth.running_state_ids: - seth.report(state_id) + print seth.report(state_id) print "[+] Global coverage:" print seth.coverage(contract_account) diff --git a/examples/evm/solidse.py b/examples/evm/solidse.py new file mode 100644 index 0000000..ae1340e --- /dev/null +++ b/examples/evm/solidse.py @@ -0,0 +1,92 @@ +from manticore.seth import ManticoreEVM, calculate_coverage, ABI +import sys +################ Script ####################### +seth = ManticoreEVM(procs=8) +seth.verbosity(0) +#And now make the contract account to analyze +# cat | solc --bin +source_code = file(sys.argv[1],'rb').read() + +user_account = seth.create_account(balance=1000) +print "[+] Creating a user account", user_account + + +contract_account = seth.solidity_create_contract(source_code, owner=user_account) +print "[+] Creating a contract account", contract_account + +attacker_account = seth.create_account(balance=1000) +print "[+] Creating a attacker account", attacker_account + + +last_coverage = None +new_coverage = 0 +tx_count = 0 +while new_coverage != last_coverage and new_coverage < 100: + + symbolic_data = seth.make_symbolic_buffer(320) + symbolic_value = seth.make_symbolic_value() + + seth.transaction(caller=attacker_account, + address=contract_account, + data=symbolic_data, + value=symbolic_value ) + + tx_count += 1 + last_coverage = new_coverage + new_coverage = seth.global_coverage(contract_account) + + print "[+] Coverage after %d transactions: %d%%"%(tx_count, new_coverage) + print "[+] There are %d reverted states now"% len(seth.terminated_state_ids) + print "[+] There are %d alive states now"% len(seth.running_state_ids) + +for state in seth.all_states: + blockchain = state.platform + for tx in blockchain.transactions: #external transactions + print "Transaction:" + print "\tsort %s" % tx.sort #Last instruction or type? TBD + print "\tcaller 0x%x" % state.solve_one(tx.caller) #The caller as by the yellow paper + print "\taddress 0x%x" % state.solve_one(tx.address) #The address as by the yellow paper + print "\tvalue: %d" % state.solve_one(tx.value) #The value as by the yellow paper + print "\tcalldata: %r" % state.solve_one(tx.data) + print "\tresult: %s" % tx.result #The result if any RETURN or REVERT + print "\treturn_data: %r" % state.solve_one(tx.return_data) #The returned data if RETURN or REVERT + + if tx.sort == 'Call': + metadata = seth.get_metadata(tx.address) + if metadata is not None: + function_id = tx.data[:4] #hope there is enough data + function_id = state.solve_one(function_id).encode('hex') + signature = metadata.get_func_signature(function_id) + print "\tparsed calldata", ABI.parse(signature, tx.data) #func_id, *function arguments + if tx.result == 'RETURN': + ret_types = metadata.get_func_return_types(function_id) + print '\tparsed return_data', ABI.parse(ret_types, tx.return_data) #function return + + #the logs + for log_item in blockchain.logs: + print "log address", log_item.address + print "memlog", log_item.memlog + for topic in log_item.topics: + print "topic", topic + + for address in blockchain.deleted_addresses: + print "deleted address", address #selfdestructed address + + #accounts alive in this state + for address in blockchain.contract_accounts: + code = blockchain.get_code(address) + balance = blockchain.get_balance(address) + trace = set(( offset for address_i, offset in state.context['seth.trace'] if address == address_i)) + print calculate_coverage(code, trace) #coverage % for address in this state + +# All accounts ever created by the script +# (may not all be alife in all states) +# (accounts created by contract code are not in this list ) +print "[+] Global coverage:" +for address in seth.contract_accounts: + print address, seth.global_coverage(address) #coverage % for address in this state + + + + + diff --git a/manticore/core/executor.py b/manticore/core/executor.py index 1fe1e27..5795ed9 100644 --- a/manticore/core/executor.py +++ b/manticore/core/executor.py @@ -427,23 +427,26 @@ class Executor(Eventful): while not self.is_shutdown(): - try: - #select a suitable state to analyze - if current_state is None: - with self._lock: - #notify siblings we are about to stop this run - self._notify_stop_run() - #Select a single state_id - current_state_id = self.get() - #load selected state from secondary storage - if current_state_id is not None: - self._publish('will_load_state', current_state_id) - current_state = self._workspace.load_state(current_state_id) - self.forward_events_from(current_state, True) - self._publish('did_load_state', current_state, current_state_id) - logger.info("load state %r", current_state_id) - #notify siblings we have a state to play with - self._notify_start_run() + try: # handle fatal errors: exceptions in Manticore + try: # handle external (e.g. solver) errors, and executor control exceptions + #select a suitable state to analyze + if current_state is None: + with self._lock: + #notify siblings we are about to stop this run + self._notify_stop_run() + try: + #Select a single state_id + current_state_id = self.get() + #load selected state from secondary storage + if current_state_id is not None: + self._publish('will_load_state', current_state_id) + current_state = self._workspace.load_state(current_state_id) + self.forward_events_from(current_state, True) + self._publish('did_load_state', current_state, current_state_id) + logger.info("load state %r", current_state_id) + #notify siblings we have a state to play with + finally: + self._notify_start_run() #If current_state is still None. We are done. if current_state is None: @@ -453,7 +456,7 @@ class Executor(Eventful): assert current_state is not None assert current_state.constraints is current_state.platform.constraints - try: + # Allows to terminate manticore worker on user request while not self.is_shutdown(): diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index b7d22a2..35aa845 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -10,6 +10,8 @@ class Expression(object): super(Expression, self).__init__() self._taint = frozenset(taint) + def __repr__(self): + return "<%s at %x>" % (type(self).__name__, id(self)) @property def is_tainted(self): return len(self._taint) != 0 @@ -536,7 +538,7 @@ class Array(Expression): def __init__(self, index_bits, index_max, *operands, **kwargs): assert index_bits in (32, 64, 256) assert index_max is None or isinstance(index_max, (int, long)) - assert index_max is None or index_max > 0 and index_max < 2 ** index_bits + 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 super(Array, self).__init__(*operands, **kwargs) @@ -619,10 +621,22 @@ class ArrayProxy(Array): self._array = array self.name = array.name + + def __len__(self): + return len(self._array) + @property def operands(self): return self._array.operands + + @property + def index_bits(self): + return self._array.index_bits + @property + def index_max(self): + return self._array.index_max + @property def taint(self): return self._array.taint @@ -635,8 +649,17 @@ class ArrayProxy(Array): self._array = auxiliar return auxiliar + def _fix_index(self, index): + stop, start = index.stop, index.start + if start is None: + start = 0 + if stop is None: + stop = len(self) + return start, stop + def _get_size(self, index): - size = index.stop - index.start + start, stop = self._fix_index(index) + size = stop - start if isinstance(size, BitVec): import visitors from manticore.core.smtlib.visitors import arithmetic_simplifier @@ -648,23 +671,30 @@ class ArrayProxy(Array): def __getitem__(self, index): if isinstance(index, slice): + start, stop = self._fix_index(index) size = self._get_size(index) - result = [] + new_array = ArrayVariable(self.index_bits, size, name='%s_b%d_e%d'%(self.name, start, stop), taint=self.taint) + new_array = ArrayProxy(new_array) for i in xrange(size): - if self.index_max is not None and not isinstance(i+index.start, Expression) and i+index.start >= self.index_max: - result.append(0) + if self.index_max is not None and not isinstance(i+start, Expression) and i+start >= self.index_max: + new_array[i] = 0 else: - result.append(self._array.select(index.start+i)) - return result + new_array[i] = self._array.select(start+i) + return new_array else: + if self.index_max is not None : + if not isinstance(index, Expression) and index >= self.index_max: + raise IndexError return self._array.select(index) def __setitem__(self, index, value): + if isinstance(index, slice): + start, stop = self._fix_index(index) size = self._get_size(index) assert len(value) == size for i in xrange(size): - self.store(index.start+i, value[i]) + self.store(start+i, value[i]) else: self.store(index, value) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index d6027e1..0379c63 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -447,9 +447,16 @@ class Z3Solver(Solver): The current set of assertions must be sat. :param val: an expression or symbol ''' if not issymbolic(expression): + if expression is None: + return if isinstance(expression, str): - expression = ord(expression) - if isinstance(expression, list): + if len(expression) == 1: + expression = ord(expression) + else: + expression = map(ord, expression) + if isinstance(expression, (list, tuple)): + if len(expression) == 0: + return expression arr = constraints.new_array(index_max=len(expression)) for i in range(len(expression)): arr[i] = expression[i] diff --git a/manticore/manticore.py b/manticore/manticore.py index 3ef416c..3e6234b 100644 --- a/manticore/manticore.py +++ b/manticore/manticore.py @@ -394,7 +394,7 @@ class Manticore(Eventful): @property def running(self): - return self._executor._running.value + return self._executor.running def enqueue(self, state): ''' Dynamically enqueue states. Users should typically not need to do this ''' diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index bfd600a..bd5480a 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -27,6 +27,26 @@ def ceil32(x): def to_signed(i): return Operators.ITEBV(256, i 0: + accs.append(address) + return accs + + @property + def deleted_addresses(self): + return self._deleted_address @property def storage(self): @@ -1948,6 +1997,41 @@ class EVMWorld(Platform): self.storage[address]['code'] = data + def log(self, address, topic, data): + self.logs.append((address, data, topics)) + logger.info('LOG %r %r', memlog, topics) + + def log_storage(self, addr): + pass + + def add_refund(self, value): + pass + + def block_prevhash(self): + return 0 + + def block_coinbase(self): + return 0 + + def block_timestamp(self): + return 0 + + def block_number(self): + return 0 + + def block_difficulty(self): + return 0 + + def block_gas_limit(self): + return 0 + + def tx_origin(self): + return self.current_vm.origin + + def tx_gasprice(self): + return 0 + + #CALLSTACK def _push_vm(self, vm): #Storage address -> account(value, local_storage) vm.global_storage = self.storage @@ -1970,15 +2054,14 @@ class EVMWorld(Platform): assert self.constraints == vm.constraints if self.current: self.current.constraints = vm.constraints + if not rollback: if self.depth: self.current.global_storage = vm.global_storage else: self._global_storage = vm.global_storage - - self._deleted_address = self._deleted_address.union(vm.suicide) - self._logs += vm.logs - if not self.depth: + self._deleted_address = self._deleted_address.union(vm.suicides) + self._logs += vm.logs for address in self._deleted_address: del self.storage[address] return vm @@ -2027,11 +2110,6 @@ class EVMWorld(Platform): except TerminateState as e: if self.depth == 0 and e.message == 'RETURN': return self.last_return - '''import traceback - print "Exception in user code:" - print '-'*60 - traceback.print_exc(file=sys.stdout) - print '-'*60''' raise e def create_account(self, address=None, balance=0, code='', storage=None): @@ -2108,11 +2186,15 @@ class EVMWorld(Platform): if origin is None and caller is not None: origin = caller + if address not in self.accounts or\ + caller not in self.accounts or \ + origin != caller and origin not in self.accounts: + raise TerminateState('Account does not exist %x'%address, testcase=True) + if header is None: header = {'timestamp':1} if any([ isinstance(data[i], Expression) for i in range(len(data))]): data_symb = self._constraints.new_array(index_bits=256, index_max=len(data)) - #data_symb = EVMMemory(self.constraints, 256, 8) for i in range(len(data)): data_symb[i] = Operators.ORD(data[i]) data = data_symb @@ -2143,12 +2225,17 @@ class EVMWorld(Platform): new_vm = EVM(self._constraints, address, origin, price, data, caller, value, bytecode, header, global_storage=self.storage) self._push_vm(new_vm) if self.depth == 1: + #handle human transactions if ty == 'Create': self.current.last_exception = Create(None, None, None) + data = bytecode elif ty == 'Call': self.current.last_exception = Call(None, None, None, None) + tx = Transaction(ty, address, origin, price, data, caller, value, None, None) + self._transactions.append(tx) + def CALL(self, gas, to, value, data): address = to @@ -2165,8 +2252,10 @@ class EVMWorld(Platform): def RETURN(self, data): prev_vm = self._pop_vm() #current VM changed! if self.depth == 0: - self.last_return=data - self.last_pc = prev_vm.pc + tx = self._transactions[-1] + tx.return_data=data + #tx.last_pc = prev_vm.pc + tx.result = 'RETURN' raise TerminateState("RETURN", testcase=True) @@ -2187,7 +2276,10 @@ class EVMWorld(Platform): def STOP(self): prev_vm = self._pop_vm(rollback=False) if self.depth == 0: - self.last_pc = prev_vm.pc + tx = self._transactions[-1] + tx.return_data=None + #tx.last_pc = prev_vm.pc + tx.result = 'STOP' raise TerminateState("STOP", testcase=True) self.current.last_exception = None self.current._push(1) @@ -2202,7 +2294,10 @@ class EVMWorld(Platform): self.storage[prev_vm.address]['balance'] -= prev_vm.value if self.depth == 0: - self.last_pc = prev_vm.pc + tx = self._transactions[-1] + #tx.last_pc = prev_vm.pc + tx.return_data=None + tx.result = 'THROW' raise TerminateState("THROW", testcase=True) self.current.last_exception = None @@ -2217,8 +2312,10 @@ class EVMWorld(Platform): self.storage[prev_vm.address]['balance'] -= prev_vm.value if self.depth == 0: - self.last_return=data - self.last_pc = prev_vm.pc + tx = self._transactions[-1] + tx.return_data=data + #tx.last_pc = prev_vm.pc + tx.result = 'REVERT' raise TerminateState("REVERT", testcase=True) self.current.last_exception = None @@ -2233,12 +2330,14 @@ class EVMWorld(Platform): self.create_account(address=recipient, balance=0, code='', storage=None) self.storage[recipient]['balance'] += self.storage[address]['balance'] self.storage[address]['balance'] = 0 - self.suicide.add(address) + self.current.suicides.add(address) prev_vm = self._pop_vm(rollback=False) - if self.depth == 0: - self.last_pc = prev_vm.pc - raise TerminateState("SELFDESTRUCT", testcase=True) + if self.depth == 0: + tx = self._transactions[-1] + tx.result = 'SELFDESTRUCT' + raise TerminateState("SELFDESTRUCT", testcase=True) + def HASH(self, data): def compare_buffers(a, b): @@ -2255,7 +2354,7 @@ class EVMWorld(Platform): logger.info("SHA3 Searching over %d known hashes", len(self._sha3)) logger.info("SHA3 TODO save this state for future explorations with more known hashes") #Broadcast the signal - self._publish( 'on_symbolic_sha3', data, self._sha3.items()) + self._publish('on_symbolic_sha3', data, self._sha3.items()) results = [] known_hashes = False diff --git a/manticore/seth.py b/manticore/seth.py index 982eaf1..b5f69b5 100644 --- a/manticore/seth.py +++ b/manticore/seth.py @@ -9,6 +9,54 @@ import sha3 import json import StringIO +def calculate_coverage(code, seen): + ''' ''' + runtime_bytecode = code + end = None + if ''.join(runtime_bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \ + and ''.join(runtime_bytecode[-2:]) =='\x00\x29': + end = -9-33-2 #Size of metadata at the end of most contracts + + count, total = 0, 0 + for i in evm.EVMAsm.disassemble_all(runtime_bytecode[:end]) : + if i.offset in seen: + count += 1 + total += 1 + + return count*100.0/total + +class SolidityMetadata(object): + def __init__(self, name, source_code, init_bytecode, metadata, metadata_runtime, hashes, abi): + self.name = name + self.source_code = source_code + self.init_bytecode = init_bytecode + self.metadata = metadata + self.metadata_runtime = metadata_runtime + self.hashes = hashes + self.abi = dict( [(item.get('name', '{fallback}'), item) for item in abi ]) + + @property + def signatures(self): + return dict(( (b,a) for (a,b) in self.hashes.items() )) + + def get_abi(self, hsh): + func_name = self.get_func_name(hsh) + return self.abi[func_name] + + def get_func_argument_types(self, hsh): + abi = self.get_abi(hsh) + return '('+','.join(x['type'] for x in abi['inputs']) +')' + + def get_func_return_types(self, hsh): + abi = self.get_abi(hsh) + return '('+','.join(x['type'] for x in abi['outputs']) +')' + + def get_func_name(self, hsh): + signature = self.signatures.get(hsh,'{fallback}()') + return signature.split('(')[0] + + def get_func_signature(self, hsh): + return self.signatures.get(hsh, '{fallback}()') class ABI(object): ''' @@ -114,6 +162,66 @@ class ABI(object): return reduce(lambda x,y: x+y, result) + + @staticmethod + def _consume_type(ty, data, offset): + def get_uint(size, offset): + byte_size = size/8 + padding = 32 - byte_size # for 160 + return Operators.CONCAT(size, *map(Operators.ORD, data[offset+padding:offset+padding+byte_size])) + if ty == u'uint256': + return get_uint(256, offset), offset+32 + if ty == u'bool': + return get_uint(8, offset), offset+32 + elif ty == u'address': + return get_uint(160, offset), offset+32 + elif ty == u'int256': + value = get_uint(256, offset) + mask = 2**(256 - 1) + value = -(value & mask) + (value & ~mask) + return value, offset+32 + elif ty == u'': + return '', offset + elif ty in (u'bytes', u'string'): + dyn_offset = 4 + get_uint(256,offset) + size = get_uint(256, dyn_offset) + return data[dyn_offset+32:dyn_offset+32+size], offset+4 + else: + print "<",ty,">" + raise NotImplemented(ty) + + @staticmethod + def parse(signature, data): + is_multiple = '(' in signature + + if is_multiple: + func_name = signature.split('(')[0] + types = signature.split('(')[1][:-1].split(',') + if len(func_name) > 0: + off = 4 + else: + func_name = None + off = 0 + else: + func_name = None + types = (signature,) + off = 0 + + arguments = [] + for ty in types: + val, off = ABI._consume_type(ty, data, off) + arguments.append(val) + + if is_multiple: + if func_name is not None: + return func_name, tuple(arguments) + else: + return tuple(arguments) + else: + return arguments[0] + + + class EVMAccount(object): ''' An EVM account ''' def __init__(self, address, seth=None, default_caller=None): @@ -131,14 +239,18 @@ class EVMAccount(object): self._hashes = {} if self._seth: - name, source_code, init_bytecode, metadata, metadata_runtime, hashes = self._seth.context['seth']['metadata'][address] - for signature in hashes.keys(): - func_name = str(signature.split('(')[0]) - self._hashes[func_name] = signature, hashes[signature] + md = self._seth.get_metadata(address) + if md is not None: + for signature, func_id in md.hashes.items(): + func_name = str(signature.split('(')[0]) + self._hashes[func_name] = signature, func_id def __int__(self): return self._address + def __str__(self): + return str(self._address) + def __getattribute__(self, name): ''' If this is a contract account of which we know the functions hashes this will build the transaction for the function call. @@ -199,9 +311,42 @@ class ManticoreEVM(Manticore): SByte=ABI.SByte SValue=ABI.SValue + def make_symbolic_buffer(self, size): + ''' Creates a symbolic buffer of size bytes to be used in transactions. + You can not operate on it. It is intended as a place holder for the + real expression. + + Example use:: + + symbolic_data = seth.make_symbolic_buffer(320) + seth.transaction(caller=attacker_account, + address=contract_account, + data=symbolic_data, + value=100000 ) + + + ''' + return ABI.SByte(size) + + def make_symbolic_value(self): + ''' Creates a symbolic value, normally a uint256, to be used in transactions. + You can not operate on it. It is intended as a place holder for the + real expression. + + Example use:: + + symbolic_value = seth.make_symbolic_value() + seth.transaction(caller=attacker_account, + address=contract_account, + data=data, + value=symbolic_data ) + + ''' + return ABI.SValue @staticmethod def compile(source_code): + ''' Get initialization bytecode from a solidity source code ''' name, source_code, bytecode, srcmap, srcmap_runtime, hashes = ManticoreEVM._compile(source_code) return bytecode @@ -216,7 +361,7 @@ class ManticoreEVM(Manticore): with tempfile.NamedTemporaryFile() as temp: temp.write(source_code) temp.flush() - p = Popen([solc, '--combined-json', 'srcmap,srcmap-runtime,bin,hashes', temp.name], stdout=PIPE) + p = Popen([solc, '--combined-json', 'abi,srcmap,srcmap-runtime,bin,hashes', temp.name], stdout=PIPE) outp = json.loads(p.stdout.read()) assert len(outp['contracts']), "Only one contract by file supported" name, outp = outp['contracts'].items()[0] @@ -225,9 +370,16 @@ class ManticoreEVM(Manticore): srcmap = outp['srcmap'].split(';') srcmap_runtime = outp['srcmap-runtime'].split(';') hashes = outp['hashes'] - return name, source_code, bytecode, srcmap, srcmap_runtime, hashes + abi = json.loads(outp['abi']) + return name, source_code, bytecode, srcmap, srcmap_runtime, hashes, abi - def __init__(self): + def __init__(self, procs=1): + ''' A manticere EVM manager + :param procs: number of workers to use in the exploration + ''' + self.normal_accounts = set() + self.contract_accounts = set() + self._config_procs=procs #Make the constraint store constraints = ConstraintSet() #make the ethereum world state @@ -236,11 +388,9 @@ class ManticoreEVM(Manticore): initial_state.context['tx'] = [] super(ManticoreEVM, self).__init__(initial_state) - + self.metadata = {} #The following should go to manticore.context so we can use multiprocessing self.context['seth'] = {} - self.context['seth']['trace'] = [] - self.context['seth']['metadata'] = {} self.context['seth']['_pending_transaction'] = None self.context['seth']['_saved_states'] = [] self.context['seth']['_final_states'] = [] @@ -267,12 +417,41 @@ class ManticoreEVM(Manticore): else: return context['_saved_states'] + @property - def final_state_ids(self): + def all_state_ids(self): + ''' IDs of the all states ''' + return self.running_state_ids + self.terminated_state_ids + + @property + def terminated_state_ids(self): ''' IDs of the terminated states ''' with self.locked_context('seth') as context: return context['_final_states'] + @property + def running_states(self): + ''' Iterates over the running states''' + for state_id in self.running_state_ids: + state = self.load(state_id) + yield state + + @property + def terminated_states(self): + ''' Iterates over the terminated states''' + for state_id in self.terminated_state_ids: + state = self.load(state_id) + yield state + + @property + def all_states(self): + ''' Iterates over the all states (terminated and alive)''' + for state_id in self.terminated_state_ids + self.running_state_ids: + state = self.load(state_id) + yield state + + + #deprecate this 5 in favor of for sta in seth.all_states: do stuff? def get_world(self, state_id=None): ''' Returns the evm world of `state_id` state. ''' state = self.load(state_id) @@ -294,9 +473,14 @@ class ManticoreEVM(Manticore): return self.get_world(state_id).storage[address]['storage'].get(offset) def last_return(self, state_id=None): - ''' last returned buffer for state `state_id` ''' + ''' Last returned buffer for state `state_id` ''' state = self.load(state_id) - return state.world.last_return + return state.platform.last_return + + def transactions(self, state_id=None): + ''' Transactions list for state `state_id` ''' + state = self.load(state_id) + return state.platform.transactions def solidity_create_contract(self, source_code, owner, balance=0, address=None, args=()): ''' Creates a solidity contract @@ -314,9 +498,9 @@ class ManticoreEVM(Manticore): :return: an EVMAccount ''' - name, source_code, init_bytecode, metadata, metadata_runtime, hashes = self._compile(source_code) + name, source_code, init_bytecode, metadata, metadata_runtime, hashes, abi = self._compile(source_code) address = self.create_contract(owner=owner, address=address, balance=balance, init=tuple(init_bytecode)+tuple(ABI.make_function_arguments(*args))) - self.context['seth']['metadata'][address] = name, source_code, init_bytecode, metadata, metadata_runtime, hashes + self.metadata[address] = SolidityMetadata(name, source_code, init_bytecode, metadata, metadata_runtime, hashes, abi) return EVMAccount(address, self, default_caller=owner) def create_contract(self, owner, balance=0, init=None, address=None): @@ -329,9 +513,10 @@ class ManticoreEVM(Manticore): :param balance: balance to be transfered on creation :type balance: int or SValue :param address: the address for the new contract (optional) - :type address: int or EVMAccount - :return: an EVMAccount address (long) + :type address: int + :return: an EVMAccount ''' + assert len(self.running_state_ids) == 1, "No forking yet" with self.locked_context('seth') as context: assert context['_pending_transaction'] is None assert init is not None @@ -339,8 +524,9 @@ class ManticoreEVM(Manticore): address = self.world._new_address() self.context['seth']['_pending_transaction'] = ('CREATE_CONTRACT', owner, address, balance, init) - self.run() + self.run(procs=self._config_procs) + self.contract_accounts.add(address) return address def create_account(self, balance=0, address=None, code=''): @@ -349,12 +535,15 @@ class ManticoreEVM(Manticore): :param balance: balance to be transfered on creation :type balance: int or SValue :param address: the address for the new contract (optional) - :type address: int or EVMAccount - :return: an EVMAccount address (long) + :type address: int + :return: an EVMAccount ''' + assert len(self.running_state_ids) == 1, "No forking yet" with self.locked_context('seth') as context: assert context['_pending_transaction'] is None - return self.world.create_account( address, balance, code=code, storage=None) + address = self.world.create_account( address, balance, code=code, storage=None) + self.normal_accounts.add(address) + return address def transaction(self, caller, address, value, data): ''' Issue a transaction @@ -371,13 +560,12 @@ class ManticoreEVM(Manticore): address = int(address) if isinstance(caller, EVMAccount): caller = int(caller) - - + if isinstance(data, self.SByte): data = (None,)*data.size with self.locked_context('seth') as context: context['_pending_transaction'] = ('CALL', caller, address, value, data) - return self.run(procs=10) + return self.run(procs=self._config_procs) def run(self, **kwargs): ''' Run any pending transaction on any running state ''' @@ -387,13 +575,11 @@ class ManticoreEVM(Manticore): assert context['_pending_transaction'] is not None #there is at least one states in seth saved states assert context['_saved_states'] or self.initial_state - #there is no states added to the executor queue assert len(self._executor.list()) == 0 for state_id in context['_saved_states']: self._executor.put(state_id) - context['_saved_states'] = [] #A callback will use _pending_transaction and issue the transaction @@ -404,6 +590,7 @@ class ManticoreEVM(Manticore): if len(context['_saved_states'])==1: self._initial_state = self._executor._workspace.load_state(context['_saved_states'][0], delete=True) context['_saved_states'] = [] + assert self.running_state_ids == [-1] #clear pending transcations. We are done. context['_pending_transaction'] = None @@ -441,12 +628,9 @@ class ManticoreEVM(Manticore): if len(self.running_state_ids) == 1: #Get the ID of the single running state state_id = self.running_state_ids[0] - if state_id != -1: - #if there is a single running state with id != 1. We consider it is a new initial_state - assert self.initial_state is None - state = self.initial_state = self._executor._workspace.load_state(state_id, delete=True) else: - raise Exception("More than one state running. Do not know which to choose.") + raise Exception("More than one state running. Do not know which one to choose.") + if state_id == -1: state = self.initial_state else: @@ -455,6 +639,17 @@ class ManticoreEVM(Manticore): return state #Callbacks + def _symbolic_sha3(self, state, data, known_hashes): + ''' INTERNAL USE ''' + + with self.locked_context('known_sha3', set) as known_sha3: + state.platform._sha3.update(known_sha3) + + def _concrete_sha3(self, state, buf, value): + ''' INTERNAL USE ''' + with self.locked_context('known_sha3', set) as known_sha3: + known_sha3.add((buf,value)) + def _terminate_state_callback(self, state, state_id, e): ''' INTERNAL USE Every time a state finishes executing last transaction we save it in @@ -469,7 +664,7 @@ class ManticoreEVM(Manticore): ty, caller, address, value, data = context['_pending_transaction'] if ty == 'CREATE_CONTRACT': world = state.platform - world.storage[address]['code'] = world.last_return + world.storage[address]['code'] = world.last_return_data self.save(state) e.testcase = False #Do not generate a testcase file @@ -483,14 +678,15 @@ class ManticoreEVM(Manticore): ''' INTERNAL USE When a state was just loaded from stoage we do the pending transaction ''' - if state.context.get('processed', False): return world = state.platform state.context['processed'] = True with self.locked_context('seth') as context: + #take current global transaction we need to apply to all running states ty, caller, address, value, data = context['_pending_transaction'] txnum = len(state.context['tx']) + #Replace any none by symbolic values if value is None: value = state.new_symbolic_value(256, label='tx%d_value'%txnum) @@ -501,23 +697,21 @@ class ManticoreEVM(Manticore): if data[i] is not None: symbolic_data[i] = data[i] data = symbolic_data - state.context['tx'].append((ty, caller, address, value, data)) - - if ty == 'CALL': world.transaction(address=address, caller=caller, data=data, value=value) else: assert ty == 'CREATE_CONTRACT' world.create_contract(caller=caller, address=address, balance=value, init=data) + state.context['tx'].append((ty, caller, address, value, data)) def _will_execute_instruction_callback(self, state, pc, instruction): ''' INTERNAL USE ''' assert state.constraints == state.platform.constraints assert state.platform.constraints == state.platform.current.constraints - + #print state.platform.current with self.locked_context('coverage', set) as coverage: coverage.add((state.platform.current.address, state.platform.current.pc)) - + def _did_execute_instruction_callback(self, state, prev_pc, pc, instruction): ''' INTERNAL USE ''' state.context.setdefault('seth.trace',[]).append((state.platform.current.address, pc)) @@ -528,8 +722,21 @@ class ManticoreEVM(Manticore): for i in range(offset, offset+size): code_data.add((state.platform.current.address, i)) - def report(self, state_id=None, ty=None): - ''' Prints a small report on state id ''' + + def get_metadata(self, address): + ''' Gets the solidity metadata for address. + This is available only if address is a contract created from solidity + ''' + try: + md = self.metadata[address] + except: + md = SolidityMetadata(None, None, None, None, None, None) + return md + + def report(self, state, ty=None): + ''' Prints a small report on state. Prints a little something about state :) ''' + world = state.platform + output = StringIO.StringIO() def compare_buffers(a, b): @@ -542,16 +749,13 @@ class ManticoreEVM(Manticore): return False return cond - state = self.load(state_id) - world = state.platform trace = state.context['seth.trace'] - last_address, last_pc = trace[-1] - + last_address, last_pc = trace[-1] #Try to recover metadata from solidity based contracts try: md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes = self.context['seth']['metadata'][last_address] except: - md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes = None,None,None,None,None,None + md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes = None, None, None, None, None, None # try to get the runtime bytecode from the account try: @@ -569,7 +773,7 @@ class ManticoreEVM(Manticore): try: # Magic number comes from here: # http://solidity.readthedocs.io/en/develop/metadata.html#encoding-of-the-metadata-hash-in-the-bytecode - asm = list(evm.EVMDecoder.decode_all(runtime_bytecode[:-9-33-2])) + asm = list(evm.EVMAsm.disassemble_all(runtime_bytecode[:-9-33-2])) asm_offset = 0 pos = 0 source_pos = md_metadata_runtime[pos] @@ -589,7 +793,7 @@ class ManticoreEVM(Manticore): for l in snippet.split('\n'): output.write(' %s %s\n'%(nl, l)) nl+=1 - except: + except Exception as e: output.write('\n') output.write("BALANCES\n") @@ -606,9 +810,9 @@ class ManticoreEVM(Manticore): else: output.write('\t%x %d wei\n'%(address, account['balance'])) - if state.platform.logs: + if world.logs: output.write('LOGS:\n') - for address, memlog, topics in state.platform.logs: + for address, memlog, topics in world.logs: try: res = memlog if isinstance(memlog, Expression): @@ -628,7 +832,6 @@ class ManticoreEVM(Manticore): output.write('\t %s: %r %s\n' %( hex(res1), ''.join(map(chr,res)), topics)) except Exception,e: - print e output.write('\t %r %r %r\n' % (address, repr(memlog), topics)) output.write('INPUT SYMBOLS\n') @@ -642,7 +845,7 @@ class ManticoreEVM(Manticore): try: output.write('\t %s: %s\n'%( expr.name, res.encode('hex'))) except: - output.write('\t %s: %s'% (expr.name, res)) + output.write('\t %s: %s\n'% (expr.name, res)) #print "Constraints:" #print state.constraints @@ -713,12 +916,48 @@ class ManticoreEVM(Manticore): output.write('%s %s\n'%(e, xdata)) return output.getvalue() - def coverage(self, account_address): + def global_coverage(self, account_address): + ''' Returns code coverage for the contract on `account_address`. + This sums up all the visited code lines from any of the explored + states. + ''' + account_address = int(account_address) + + #Search one state in which the account_address exists + world=None + for state_id in self.all_state_ids: + world = self.get_world(state_id) + if account_address in world.storage: + break + + seen = self.context['coverage'] #.union( self.context.get('code_data', set())) + runtime_bytecode = world.storage[account_address]['code'] + + end = None + if ''.join(runtime_bytecode[-44: -34]) =='\x00\xa1\x65\x62\x7a\x7a\x72\x30\x58\x20' \ + and ''.join(runtime_bytecode[-2:]) =='\x00\x29': + end = -9-33-2 #Size of metadata at the end of most contracts + + count, total = 0, 0 + for i in evm.EVMAsm.disassemble_all(runtime_bytecode[:end]) : + if (account_address, i.offset) in seen: + count += 1 + total += 1 + + return count*100.0/total + + def report_coverage(self, account_address): ''' Output a code coverage report for contract account_address ''' account_address = int(account_address) #This will just pick one of the running states. #This assumes the code and the accounts are the same in all versions of the world - world = self.get_world(self.running_state_ids[0]) + #Search one state in which the account_address exists + world=None + for state_id in self.all_state_ids: + world = self.get_world(state_id) + if account_address in world.storage: + break + seen = self.context['coverage'] #.union( self.context.get('code_data', set())) runtime_bytecode = world.storage[account_address]['code'] class bcolors: @@ -760,14 +999,3 @@ class ManticoreEVM(Manticore): output += "Coverage: %2.2f%%\n"% (count*100.0/total) return output - def _symbolic_sha3(self, state, data, known_hashes): - ''' INTERNAL USE ''' - - with self.locked_context('known_sha3', set) as known_sha3: - state.platform._sha3.update(known_sha3) - - def _concrete_sha3(self, state, buf, value): - ''' INTERNAL USE ''' - with self.locked_context('known_sha3', set) as known_sha3: - known_sha3.add((buf,value)) -