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
This commit is contained in:
Mark Mossberg 2017-12-08 11:15:03 -05:00 committed by GitHub
parent ed29a22fce
commit 3f0441148f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 102 additions and 96 deletions

View File

@ -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

View File

@ -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