Better EVM workspace output (#641)

* 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

* Code review

* Code review

* Code review

* Initial detector plugin. integer overflow and unitialized mem

* Better metadata handling and new events for detectors

* detectors wip

* Better name for internal findings context

* Explicit detector register

* review

* New workspace output

* Fix examples

* wrog merge fix

* Fix examples/new api

* Fix examples/new api/output

* More output

* More doc

* Broken examples deleted

* Debug code removed

* Wrong docstring

* Update evm __main__

* Update evm __main__

* Update evm __main__

* Update evm __main__

* Update evm __main__

* Fix TODO
This commit is contained in:
feliam
2017-12-15 02:17:41 -03:00
committed by GitHub
parent 4b79711b92
commit db80685758
13 changed files with 593 additions and 615 deletions

View File

@@ -1,38 +1,38 @@
from manticore.seth import ManticoreEVM
seth = ManticoreEVM()
seth.verbosity(3)
m = ManticoreEVM()
m.verbosity(3)
#And now make the contract account to analyze
source_code = file('coverage.sol').read()
user_account = seth.create_account(balance=1000)
user_account = m.create_account(balance=1000)
bytecode = seth.compile(source_code)
bytecode = m.compile(source_code)
#Initialize contract
contract_account = seth.create_contract(owner=user_account,
contract_account = m.create_contract(owner=user_account,
balance=0,
init=bytecode)
seth.transaction( caller=user_account,
m.transaction( caller=user_account,
address=contract_account,
value=None,
data=seth.SByte(164),
data=m.SByte(164),
)
#Up to here we get only ~30% coverage.
#We need 2 transactions to fully explore the contract
seth.transaction( caller=user_account,
m.transaction( caller=user_account,
address=contract_account,
value=None,
data=seth.SByte(164),
data=m.SByte(164),
)
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:
print seth.report(state_id)
print "[+] There are %d reverted states now"% len(m.final_state_ids)
print "[+] There are %d alive states now"% len(m.running_state_ids)
for state_id in m.running_state_ids:
print m.report(state_id)
print "[+] Global coverage: %x"% contract_account
print seth.coverage(contract_account)
print m.coverage(contract_account)

View File

@@ -1,39 +1,37 @@
from manticore.seth import ManticoreEVM
seth = ManticoreEVM()
from manticore.seth import ManticoreEVM, IntegerOverflow
m = ManticoreEVM()
m.register_detector(IntegerOverflow())
#And now make the contract account to analyze
source_code = '''
pragma solidity ^0.4.15;
contract Overflow {
uint private sellerBalance=0;
function add(uint value) returns (bool){
function add(uint value) returns (uint){
sellerBalance += value; // complicated math with possible overflow
// possible auditor assert
assert(sellerBalance >= value);
return sellerBalance;
}
}
'''
#Initialize user and contracts
user_account = seth.create_account(balance=1000)
contract_account = seth.solidity_create_contract(source_code, owner=user_account, balance=0)
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)
#First add won't overflow uint256 representation
contract_account.add(seth.SValue)
contract_account.add(m.make_symbolic_value())
#Potential overflow
contract_account.add(seth.SValue)
contract_account.add(m.make_symbolic_value())
#Let seth know we are not sending more transactions so it can output
# info about running states and global statistics
m.finalize()
print "[+] Look for results in %s"% m.workspace
print "[+] There are %d reverted states now"% len(seth.final_state_ids)
for state_id in seth.final_state_ids:
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:
print seth.report(state_id)
print "[+] Global coverage: %x"% contract_account
print seth.coverage(contract_account)

View File

@@ -1,7 +1,7 @@
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
m = ManticoreEVM()
#And now make the contract account to analyze
# cat | solc --bin
source_code = '''
@@ -20,31 +20,22 @@ contract NoDistpatcher {
}
'''
print "[+] Creating a user account"
user_account = seth.create_account(balance=1000)
print "[+] Creating a contract account"
contract_account = seth.solidity_create_contract(source_code, owner=user_account)
user_account = m.create_account(balance=1000)
print "[+] Creating a user account", user_account
contract_account = m.solidity_create_contract(source_code, owner=user_account)
print "[+] Creating a contract account", contract_account
print "[+] Source code:"
print source_code
print "[+] Now the symbolic values"
symbolic_data = seth.SByte(320)
symbolic_data = m.make_symbolic_buffer(320)
symbolic_value = None
seth.transaction(caller=user_account,
m.transaction(caller=user_account,
address=contract_account,
data=symbolic_data,
value=symbolic_value )
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:
print seth.report(state_id)
print "[+] Global coverage:"
print seth.coverage(contract_account)
#Let seth know we are not sending more transactions
m.finalize()
print "[+] Look for results in %s"% m.workspace

View File

@@ -1,8 +1,8 @@
from manticore.seth import ManticoreEVM, ABI
################ Script #######################
seth = ManticoreEVM()
seth.verbosity(0)
m = ManticoreEVM()
m.verbosity(0)
#The contract account to analyze
contract_source_code = '''
pragma solidity ^0.4.15;
@@ -80,31 +80,28 @@ contract GenericReentranceExploit {
#Initialize user and contracts
user_account = seth.create_account(balance=100000000000000000)
attacker_account = seth.create_account(balance=100000000000000000)
user_account = m.create_account(balance=100000000000000000)
attacker_account = m.create_account(balance=100000000000000000)
contract_account = seth.solidity_create_contract(contract_source_code, owner=user_account) #Not payable
seth.world.set_balance(contract_account, 1000000000000000000) #give it some ether
contract_account = m.solidity_create_contract(contract_source_code, owner=user_account) #Not payable
m.world.set_balance(contract_account, 1000000000000000000) #give it some ether
exploit_account = seth.solidity_create_contract(exploit_source_code, owner=attacker_account)
exploit_account = m.solidity_create_contract(exploit_source_code, owner=attacker_account)
print "[+] Setup the exploit"
exploit_account.set_vulnerable_contract(contract_account)
exploit_account.set_reentry_reps(30)
print "\t Setting attack string"
print "[+] Setting attack string"
#'\x9d\x15\xfd\x17'+pack_msb(32)+pack_msb(4)+'\x5f\xd8\xc7\x10',
reentry_string = ABI.make_function_id('withdrawBalance()')
exploit_account.set_reentry_attack_string(reentry_string)
print "[+] Initial world state"
print " attacker_account %x balance: %d"% (attacker_account, seth.get_balance(attacker_account))
print " exploit_account %x balance: %d"% (exploit_account, seth.get_balance(exploit_account))
print " user_account %x balance: %d"% (user_account, seth.get_balance(user_account))
print " contract_account %x balance: %d"% (contract_account, seth.get_balance(contract_account))
print " attacker_account %x balance: %d"% (attacker_account, m.get_balance(attacker_account))
print " exploit_account %x balance: %d"% (exploit_account, m.get_balance(exploit_account))
print " user_account %x balance: %d"% (user_account, m.get_balance(user_account))
print " contract_account %x balance: %d"% (contract_account, m.get_balance(contract_account))
#User deposits all in contract
@@ -115,26 +112,16 @@ contract_account.addToBalance(value=100000000000000000)
print "[+] Let attacker deposit some small amount using exploit"
exploit_account.proxycall(ABI.make_function_id('addToBalance()'), value=100000000000000000)
print "[+] Let attacker extract all using exploit"
print "[+] Let attacker extract all using exploit"
exploit_account.proxycall(ABI.make_function_id('withdrawBalance()'))
print "[+] Let attacker destroy the exploit andprofit"
exploit_account.get_money()
print " attacker_account %x balance: %d"% (attacker_account, seth.get_balance(attacker_account))
print " user_account %x balance: %d"% (user_account, seth.get_balance(user_account))
print " contract_account %x balance: %d"% (contract_account, seth.get_balance(contract_account))
print "[+] There are %d reverted states now"% len(seth.final_state_ids)
for state_id in seth.final_state_ids:
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:
print seth.report(state_id)
print "[+] Global coverage:"
print seth.coverage(contract_account)
exploit_account.get_money()
print " attacker_account %x balance: %d"% (attacker_account, m.get_balance(attacker_account))
print " user_account %x balance: %d"% (user_account, m.get_balance(user_account))
print " contract_account %x balance: %d"% (contract_account, m.get_balance(contract_account))
m.finalize()
print "[+] Look for results in %s"% m.workspace

View File

@@ -1,8 +1,8 @@
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
seth.verbosity(0)
m = ManticoreEVM()
m.verbosity(0)
#The contract account to analyze
contract_source_code = '''
pragma solidity ^0.4.15;
@@ -76,10 +76,10 @@ contract GenericReentranceExploit {
#Initialize user and contracts
user_account = seth.create_account(balance=100000000000000000)
attacker_account = seth.create_account(balance=100000000000000000)
contract_account = seth.solidity_create_contract(contract_source_code, owner=user_account) #Not payable
exploit_account = seth.solidity_create_contract(exploit_source_code, owner=attacker_account)
user_account = m.create_account(balance=100000000000000000)
attacker_account = m.create_account(balance=100000000000000000)
contract_account = m.solidity_create_contract(contract_source_code, owner=user_account) #Not payable
exploit_account = m.solidity_create_contract(exploit_source_code, owner=attacker_account)
#User deposits all in contract
@@ -87,10 +87,10 @@ print "[+] user deposited some."
contract_account.addToBalance(value=100000000000000000)
print "[+] Initial world state"
print " attacker_account %x balance: %d"% (attacker_account, seth.get_balance(attacker_account))
print " exploit_account %x balance: %d"% (exploit_account, seth.get_balance(exploit_account))
print " user_account %x balance: %d"% (user_account, seth.get_balance(user_account))
print " contract_account %x balance: %d"% (contract_account, seth.get_balance(contract_account))
print " attacker_account %x balance: %d"% (attacker_account, m.get_balance(attacker_account))
print " exploit_account %x balance: %d"% (exploit_account, m.get_balance(exploit_account))
print " user_account %x balance: %d"% (user_account, m.get_balance(user_account))
print " contract_account %x balance: %d"% (contract_account, m.get_balance(contract_account))
@@ -101,28 +101,20 @@ print "\t Setting 30 reply reps"
exploit_account.set_reentry_reps(30)
print "\t Setting reply string"
exploit_account.set_reentry_attack_string(seth.SByte(4))
exploit_account.set_reentry_attack_string(m.SByte(4))
#Attacker is
print "[+] Attacker first transaction"
exploit_account.proxycall(seth.SByte(4), value=seth.SValue)
exploit_account.proxycall(m.SByte(4), value=m.SValue)
print "[+] Attacker second transaction"
exploit_account.proxycall(seth.SByte(4))
exploit_account.proxycall(m.SByte(4))
print "[+] The attacker destroys the exploit contract and profit"
exploit_account.get_money()
#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 "[+] There are %d alive states now"% (len(seth.running_state_ids))
for state_id in seth.running_state_ids:
world = seth.get_world(state_id)
print "[+] Global coverage:"
print seth.coverage(contract_account, ty='SUICIDE')
#Let seth know we are not sending more transactions so it can output
# info about running states and global statistics
m.finalize()
print "[+] Look for results in %s"% m.workspace

View File

@@ -1,8 +1,8 @@
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
seth.verbosity(0)
m = ManticoreEVM()
m.verbosity(2)
#And now make the contract account to analyze
# cat | solc --bin
source_code = '''
@@ -21,27 +21,17 @@ contract Test {
}
'''
#Initialize accounts
user_account = seth.create_account(balance=1000)
contract_account = seth.solidity_create_contract(source_code, owner=user_account)
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)
symbolic_data = seth.SByte(4)
symbolic_data = m.make_symbolic_buffer(4)
symbolic_value = None
seth.transaction( caller=user_account,
m.transaction( caller=user_account,
address=contract_account,
value=symbolic_value,
data=symbolic_data
)
print "[+] There are %d reverted states now"% len(seth.final_state_ids)
for state_id in seth.final_state_ids:
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:
print seth.report(state_id)
print "[+] Global coverage:"
print seth.coverage(contract_account)
m.finalize()
print "[+] Look for results in %s"% m.workspace

View File

@@ -1,8 +1,8 @@
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
seth.verbosity(2)
m = ManticoreEVM()
m.verbosity(2)
#And now make the contract account to analyze
# cat | solc --bin
source_code = '''
@@ -30,28 +30,19 @@ contract Test {
}
'''
#Initialize accounts
user_account = seth.create_account(balance=1000)
contract_account = seth.solidity_create_contract(source_code, owner=user_account)
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)
symbolic_data = seth.SByte(64)
symbolic_data = m.SByte(64)
symbolic_value = 0
seth.transaction( caller=user_account,
m.transaction( caller=user_account,
address=contract_account,
value=symbolic_value,
data=symbolic_data
)
print "[+] There are %d reverted states now"% len(seth.final_state_ids)
for state_id in seth.final_state_ids:
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:
print seth.report(state_id)
print "[+] Global coverage:"
print seth.coverage(contract_account)
m.finalize()
print "[+] Look for results in %s"% m.workspace

View File

@@ -1,8 +1,8 @@
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
seth.verbosity(0)
m = ManticoreEVM()
m.verbosity(0)
#And now make the contract account to analyze
# cat | solc --bin
source_code = '''
@@ -22,22 +22,22 @@ contract Test {
}
'''
#Initialize accounts
user_account = seth.create_account(balance=1000)
contract_account = seth.solidity_create_contract(source_code, owner=user_account)
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)
contract_account.target(value=seth.SValue)
contract_account.target(value=m.SValue)
print "[+] There are %d reverted states now"% len(seth.final_state_ids)
for state_id in seth.final_state_ids:
print seth.report(state_id)
print "[+] There are %d reverted states now"% len(m.final_state_ids)
for state_id in m.final_state_ids:
print m.report(state_id)
print "[+] There are %d alive states now"% len(seth.running_state_ids)
for state_id in seth.running_state_ids:
print seth.report(state_id)
print "[+] There are %d alive states now"% len(m.running_state_ids)
for state_id in m.running_state_ids:
print m.report(state_id)
print "[+] Global coverage:"
print seth.coverage(contract_account)
print m.coverage(contract_account)

View File

@@ -1,99 +0,0 @@
from manticore.seth import ManticoreEVM, calculate_coverage, ABI
################ 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:
print "="*20
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
metadata = seth.get_metadata(tx.address)
if tx.sort == 'Call':
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
if tx.result in ('THROW', 'REVERT', 'SELFDESTRUCT'):
if metadata is not None:
address, offset = state.context['seth.trace'][-1]
print metadata.get_source_for(offset)
#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