From 3f0441148fa490d4a38de013c8f66bccebca3fc8 Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Fri, 8 Dec 2017 11:15:03 -0500 Subject: [PATCH] Initial eth cli based on solidse.py (#633) * 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 * initially evm cli from solidse.py * rm prints, make import work it's just `import seth` because this file runs from the perspective of being inside the package. `from manticore.seth` doesn't work because manticore.py gets priority over the manticore package, and there is no seth entity inside manticore.py * rm wip cli file * add excess printing as a big comment * print minimal report * require .sol only * rm solidse again * rm fluff --- examples/evm/solidse.py | 92 ---------------------------------- manticore/__main__.py | 106 ++++++++++++++++++++++++++++++++++++++-- 2 files changed, 102 insertions(+), 96 deletions(-) delete mode 100644 examples/evm/solidse.py diff --git a/examples/evm/solidse.py b/examples/evm/solidse.py deleted file mode 100644 index ae1340e..0000000 --- a/examples/evm/solidse.py +++ /dev/null @@ -1,92 +0,0 @@ -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/__main__.py b/manticore/__main__.py index 8067b8b..3ba224d 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -1,7 +1,7 @@ import sys import argparse -import logging -from manticore import Manticore, log, make_initial_state + +from manticore import Manticore sys.setrecursionlimit(10000) @@ -63,13 +63,111 @@ def parse_arguments(): return parsed + +def ethereum_cli(args): + from seth import ManticoreEVM + + m = ManticoreEVM(procs=args.procs) + + with open(args.argv[0]) as f: + source_code = f.read() + + user_account = m.create_account(balance=1000) + contract_account = m.solidity_create_contract(source_code, owner=user_account) + attacker_account = m.create_account(balance=1000) + + last_coverage = None + new_coverage = 0 + tx_count = 0 + while new_coverage != last_coverage and new_coverage < 100: + + symbolic_data = m.make_symbolic_buffer(320) + symbolic_value = m.make_symbolic_value() + + m.transaction(caller=attacker_account, + address=contract_account, + data=symbolic_data, + value=symbolic_value ) + + tx_count += 1 + last_coverage = new_coverage + new_coverage = m.global_coverage(contract_account) + + print "[+] Coverage after %d transactions: %d%%"%(tx_count, new_coverage) + print "[+] There are %d reverted states now"% len(m.terminated_state_ids) + print "[+] There are %d alive states now"% len(m.running_state_ids) + + for state in m.all_states: + print str(state.context['last_exception']) + + # 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 + + def main(): args = parse_arguments() - env = {key:val for key, val in map(lambda env: env[0].split('='), args.env)} - Manticore.verbosity(args.v) + # TODO(mark): Temporarily hack ethereum support into manticore cli + if args.argv[0].endswith('.sol'): + ethereum_cli(args) + return + + env = {key:val for key, val in map(lambda env: env[0].split('='), args.env)} + m = Manticore(args.argv[0], argv=args.argv[1:], env=env, workspace_url=args.workspace, policy=args.policy, disasm=args.disasm) #Fixme(felipe) remove this, move to plugin