DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

EVM refactor and simple UI (#629)

Browse Source 
* 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
This commit is contained in:
feliam
2017-12-07 20:19:16 -03:00
committed by GitHub
parent 764151de71
commit ed29a22fce
15 changed files with 594 additions and 136 deletions
Download Patch File Download Diff File Expand all files Collapse all files
examples/evm/coverage.py
+1 -1
View File
@@ -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)
examples/evm/integer_overflow.py
+2 -2
View File
@@ -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)
examples/evm/minimal.py
+1 -2
View File
@@ -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)
examples/evm/reentrancy_concrete.py
+2 -2
View File
@@ -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)
examples/evm/reentrancy_symbolic.py
+1 -1
View File
@@ -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')
examples/evm/simple_functions.py
+2 -2
View File
@@ -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)
examples/evm/simple_mapping.py
+2 -2
View File
@@ -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)
examples/evm/simple_transaction.py
+2 -2
View File
@@ -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)
examples/evm/solidse.py
+92
View File
@@ -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
manticore/core/executor.py
+21 -18
View File
@@ -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():
manticore/core/smtlib/expression.py
+38 -8
View File
@@ -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)
manticore/core/smtlib/solver.py
+9 -2
View File
@@ -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]
manticore/manticore.py
+1 -1
View File
@@ -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 '''
manticore/platforms/evm.py
+128 -29
View File
@@ -27,6 +27,26 @@ def ceil32(x):
def to_signed(i):
return Operators.ITEBV(256, i<TT255, i, i-TT256)
class Transaction(object):
__slots__= 'sort', 'address', 'origin', 'price', 'data', 'caller', 'value', 'return_data', 'result'
def __init__(self, sort, address, origin, price, data, caller, value, return_data, result):
self.sort = sort
self.address = address
self.origin = origin
self.price = price
self.data = data
self.caller = caller
self.value = value
self.return_data = return_data
self.result = result
def __reduce__(self):
''' Implements serialization/pickle '''
return (self.__class__, (self.sort, self.address, self.origin, self.price, self.data, self.caller, self.value, self.return_data, self.result))
class EVMMemory(object):
def __init__(self, constraints, address_size=256, value_size=8, *args, **kwargs):
'''
@@ -1041,7 +1061,7 @@ class EVM(Eventful):
self.value = value
self.depth = depth
self.bytecode = code
self.suicide = set()
self.suicides = set()
self.logs = []
self.gas=gas
#FIXME parse decode and mark invalid instructions
@@ -1087,7 +1107,7 @@ class EVM(Eventful):
state['stack'] = self.stack
state['gas'] = self.gas
state['allocated'] = self.allocated
state['suicide'] = self.suicide
state['suicides'] = self.suicides
state['logs'] = self.logs
return state
@@ -1112,7 +1132,7 @@ class EVM(Eventful):
self.stack = state['stack']
self.gas = state['gas']
self.allocated = state['allocated']
self.suicide = state['suicide']
self.suicides = state['suicides']
super(EVM, self).__setstate__(state)
#Memory related
@@ -1822,6 +1842,7 @@ class EVMWorld(Platform):
self._logs = list()
self._sha3 = {}
self._pending_transaction = None
self._transactions = list()
def __getstate__(self):
state = super(EVMWorld, self).__getstate__()
@@ -1832,6 +1853,8 @@ class EVMWorld(Platform):
state['constraints'] = self._constraints
state['callstack'] = self._callstack
state['deleted_address'] = self._deleted_address
state['transactions'] = self._transactions
return state
def __setstate__(self, state):
@@ -1843,6 +1866,7 @@ class EVMWorld(Platform):
self._constraints = state['constraints']
self._callstack = state['callstack']
self._deleted_address = state['deleted_address']
self._transactions = state['transactions']
self._do_events()
def _do_events(self):
@@ -1871,6 +1895,14 @@ class EVMWorld(Platform):
def constraints(self):
return self._constraints
@property
def transactions(self):
return self._transactions
@property
def last_return_data(self):
return self.transactions[-1].return_data
@constraints.setter
def constraints(self, constraints):
self._constraints = constraints
@@ -1889,11 +1921,28 @@ class EVMWorld(Platform):
return None
@property
def suicide(self):
if self.depth:
return self.current.suicide
else:
return self._suicide
def accounts(self):
return self.storage.keys()
@property
def normal_accounts(self):
accs = []
for address in self.accounts:
if len(self.get_code(address)) == 0:
accs.append(address)
return accs
@property
def contract_accounts(self):
accs = []
for address in self.accounts:
if len(self.get_code(address)) > 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
manticore/seth.py
+292 -64
View File
@@ -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))