DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

EVM api refactor (#589)

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
This commit is contained in:
feliam
2017-11-29 19:00:49 -03:00
committed by GitHub
parent 3a63402ae5
commit 9c777e6d2b
11 changed files with 403 additions and 270 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/api.rst
+4
View File
@@ -40,6 +40,10 @@ Models
EVM
---
.. automodule:: manticore.platforms.evm
.. automodule:: manticore.seth
:members:
EVM Assembler
---------
.. autoclass:: manticore.platforms.evm::EVMAsm.Instruction
:members:
.. autoclass:: manticore.platforms.evm.EVMAsm
examples/evm/coverage.py
+1 -1
View File
@@ -1,4 +1,4 @@
from seth import *
from manticore.seth import ManticoreEVM
seth = ManticoreEVM()
seth.verbosity(3)
examples/evm/integer_overflow.py
+2 -3
View File
@@ -1,10 +1,9 @@
from seth import *
from manticore.seth import ManticoreEVM
seth = ManticoreEVM()
#And now make the contract account to analyze
source_code = '''
pragma solidity ^0.4.15;
contract Overflow {
event Log(string);
uint private sellerBalance=0;
function add(uint value) returns (bool){
@@ -19,7 +18,7 @@ contract Overflow {
user_account = seth.create_account(balance=1000)
contract_account = seth.solidity_create_contract(source_code, owner=user_account, balance=0)
#First add wont owerflow uint256 representation
#First add won't overflow uint256 representation
contract_account.add(seth.SValue)
#Potential overflow
examples/evm/minimal.py
+2 -2
View File
@@ -1,4 +1,4 @@
from seth import ManticoreEVM
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
@@ -9,7 +9,7 @@ source_code = '''
pragma solidity ^0.4.13;
contract NoDistpatcher {
event Log(string);
function address(){}
function() payable {
if (msg.data[0] == 'A') {
Log("Got an A");
examples/evm/reentrancy_concrete.py
+7 -13
View File
@@ -1,4 +1,4 @@
from seth import ManticoreEVM
from manticore.seth import ManticoreEVM, ABI
################ Script #######################
seth = ManticoreEVM()
@@ -58,13 +58,13 @@ contract GenericReentranceExploit {
reentry_reps = reps;
}
function delegate(bytes data) payable{
function proxycall(bytes data) payable{
// call addToBalance with msg.value ethers
vulnerable_contract.call.value(msg.value)(data);
}
function get_money(){
suicide(owner);
selfdestruct(owner);
}
function () payable{
@@ -76,12 +76,6 @@ contract GenericReentranceExploit {
}
}
}
//Function signatures:
//0ccfac9e: delegate(bytes)
//b8029269: get_money()
//9d15fd17: set_reentry_attack_string(bytes)
//0d4b1aca: set_reentry_reps(int256)
//beac44e7: set_vulnerable_contract(address)
'''
@@ -90,7 +84,7 @@ 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
seth.world[int(contract_account)]['balance']=1000000000000000000 #give it some ether
seth.world.set_balance(contract_account, 1000000000000000000) #give it some ether
exploit_account = seth.solidity_create_contract(exploit_source_code, owner=attacker_account)
@@ -102,7 +96,7 @@ exploit_account.set_reentry_reps(30)
print "\t Setting attack string"
#'\x9d\x15\xfd\x17'+pack_msb(32)+pack_msb(4)+'\x5f\xd8\xc7\x10',
reentry_string = seth.make_function_id('withdrawBalance()')
reentry_string = ABI.make_function_id('withdrawBalance()')
exploit_account.set_reentry_attack_string(reentry_string)
@@ -119,10 +113,10 @@ contract_account.addToBalance(value=100000000000000000)
print "[+] Let attacker deposit some small amount using exploit"
exploit_account.delegate(seth.make_function_id('addToBalance()'), value=100000000000000000)
exploit_account.proxycall(ABI.make_function_id('addToBalance()'), value=100000000000000000)
print "[+] Let attacker extract all using exploit"
exploit_account.delegate(seth.make_function_id('withdrawBalance()'))
exploit_account.proxycall(ABI.make_function_id('withdrawBalance()'))
print "[+] Let attacker destroy the exploit andprofit"
exploit_account.get_money()
examples/evm/reentrancy_symbolic.py
+4 -14
View File
@@ -1,4 +1,4 @@
from seth import ManticoreEVM
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
@@ -27,10 +27,6 @@ contract Reentrance {
userBalance[msg.sender] = 0;
}
}
//Function signatures:
//c0e317fb: addToBalance()
//f8b2cb4f: getBalance(address)
//5fd8c710: withdrawBalance()
'''
exploit_source_code = '''
@@ -58,7 +54,7 @@ contract GenericReentranceExploit {
reentry_reps = reps;
}
function delegate(bytes data) payable{
function proxycall(bytes data) payable{
// call addToBalance with msg.value ethers
vulnerable_contract.call.value(msg.value)(data);
}
@@ -76,12 +72,6 @@ contract GenericReentranceExploit {
}
}
}
//Function signatures:
//0ccfac9e: delegate(bytes)
//b8029269: get_money()
//9d15fd17: set_reentry_attack_string(bytes)
//0d4b1aca: set_reentry_reps(int256)
//beac44e7: set_vulnerable_contract(address)
'''
@@ -115,10 +105,10 @@ exploit_account.set_reentry_attack_string(seth.SByte(4))
#Attacker is
print "[+] Attacker first transaction"
exploit_account.delegate(seth.SByte(4), value=seth.SValue)
exploit_account.proxycall(seth.SByte(4), value=seth.SValue)
print "[+] Attacker second transaction"
exploit_account.delegate(seth.SByte(4))
exploit_account.proxycall(seth.SByte(4))
print "[+] The attacker destroys the exploit contract and profit"
exploit_account.get_money()
examples/evm/simple_functions.py
+1 -2
View File
@@ -1,4 +1,4 @@
from seth import *
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
@@ -24,7 +24,6 @@ contract Test {
user_account = seth.create_account(balance=1000)
contract_account = seth.solidity_create_contract(source_code, owner=user_account)
symbolic_data = seth.SByte(4)
symbolic_value = None
seth.transaction( caller=user_account,
examples/evm/simple_mapping.py
+1 -1
View File
@@ -1,4 +1,4 @@
from seth import *
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
examples/evm/simple_transaction.py
+1 -1
View File
@@ -1,4 +1,4 @@
from seth import *
from manticore.seth import ManticoreEVM
################ Script #######################
seth = ManticoreEVM()
manticore/platforms/evm.py
+66 -48
View File
@@ -699,7 +699,7 @@ class EVMAsm(object):
mnemonic = name
if name == 'PUSH':
mnemonic = '%s%d'%(name, (opcode&0x1f) + 1)
elif name in ('SWAP', 'LOG'):
elif name in ('SWAP', 'LOG', 'DUP'):
mnemonic = '%s%d'%(name, (opcode&0xf) + 1)
reverse_table[mnemonic] = opcode, name, immediate_operand_size, pops, pushes, gas, description
@@ -732,7 +732,7 @@ class EVMAsm(object):
return EVMAsm.Instruction(opcode, name, operand_size, pops, pushes, gas, description, operand=operand, offset=offset)
except:
raise Exception("Something wron at offset %d"%offset)
raise Exception("Something wrong at offset %d"%offset)
@staticmethod
def assemble_all(assembler, offset=0):
@@ -1902,14 +1902,53 @@ class EVMWorld(Platform):
else:
return self._global_storage
@storage.setter
def storage(self, value):
if self.depth:
self.current.global_storage = value
else:
self._global_storage = value
def set_storage_data(self, address, offset, value):
self.storage[address]['storage'][offset] = value
def _push(self, vm):
def get_storage_data(self, address, offset):
return self.storage[address]['storage'].get(offset)
def set_balance(self, address, value):
self.storage[int(address)]['balance'] = value
def get_balance(self, address):
return self.storage[address]['balance']
def add_to_balance(self, address, value):
self.storage[address]['balance'] += value
def send_ether(self, src, dst, value):
src_balance = self.get_balance(src)
dst_balance = self.get_balance(dst)
#discarding absurd amount of ether
self.constraints.add(src_balance + value >= src_balance)
if issymbolic(src_balance) or issymbolic(value):
res = solver.get_all_values(self._constraints, src_balance < value)
if set(res) == set([True, False]):
raise Concretize('Forking on available funds',
expression = src_balance < value,
setstate=lambda a,b: None,
policy='ALL')
if set(res) == set([True]):
self._pending_transaction = None
raise TerminateState("Not Enough Funds for transaction", testcase=True)
else:
if src_balance < value:
self._pending_transaction = None
raise TerminateState("Not Enough Funds for transaction", testcase=True)
self.storage[dst]['balance'] += value
self.storage[src]['balance'] -= value
def get_code(self, address):
return self.storage[address]['code']
def set_code(self, address, data):
self.storage[address]['code'] = data
def _push_vm(self, vm):
#Storage address -> account(value, local_storage)
vm.global_storage = self.storage
vm.global_storage[vm.address]['storage'] = copy.copy(self.storage[vm.address]['storage'])
@@ -1926,13 +1965,17 @@ class EVMWorld(Platform):
self._pop(rollback=True)
raise TerminateState("Maximum call depth limit is reached", testcase=True)
def _pop(self, rollback=False):
def _pop_vm(self, rollback=False):
vm = self._callstack.pop()
assert self.constraints == vm.constraints
if self.current:
self.current.constraints = vm.constraints
if not rollback:
self.storage = vm.global_storage
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:
@@ -2073,14 +2116,14 @@ class EVMWorld(Platform):
for i in range(len(data)):
data_symb[i] = Operators.ORD(data[i])
data = data_symb
bytecode = self.storage[address]['code']
bytecode = self.get_code(address)
self._pending_transaction = ('Call', address, origin, price, data, caller, value, bytecode, header)
if run:
assert self.depth == 0
assert not issymbolic(caller)
assert not issymbolic(address)
assert self.storage[caller]['balance'] >= value
assert self.get_balance(caller) >= value
#run contract
#Assert everything is concrete?
try:
@@ -2095,34 +2138,10 @@ class EVMWorld(Platform):
assert self.current is None or self.current.last_exception is not None
ty, address, origin, price, data, caller, value, bytecode, header = self._pending_transaction
if issymbolic(self.storage[caller]['balance']) or issymbolic(value):
res = solver.get_all_values(self._constraints, self.storage[caller]['balance'] < value)
if set(res) == set([True, False]):
raise Concretize('Forking on available funds',
expression = self.storage[caller]['balance'] < value,
setstate=lambda a,b: None,
policy='ALL')
if set(res) == set([True]):
self._pending_transaction = None
raise TerminateState("Not Enough Funds for transaction", testcase=True)
else:
if self.storage[caller]['balance'] < value:
self._pending_transaction = None
raise TerminateState("Not Enough Funds for transaction", testcase=True)
self._pending_transaction = None
#discarding absurd amount of ether
self.constraints.add(self.storage[address]['balance'] + value >= self.storage[address]['balance'])
self.storage[caller]['balance'] -= value
self.storage[address]['balance'] += value
self.send_ether(caller, address, value)
self._pending_transaction=None
new_vm = EVM(self._constraints, address, origin, price, data, caller, value, bytecode, header, global_storage=self.storage)
self._push(new_vm)
self._push_vm(new_vm)
if self.depth == 1:
#handle human transactions
if ty == 'Create':
@@ -2137,14 +2156,14 @@ class EVMWorld(Platform):
caller = self.current.address
price = self.current.price
depth = self.depth + 1
bytecode = self.storage[to]['code']
bytecode = self.get_code(to)
header = {'timestamp' :1}
self.transaction(address, origin, price, data, caller, value, header)
self._process_pending_transaction()
def RETURN(self, data):
prev_vm = self._pop() #current VM changed!
prev_vm = self._pop_vm() #current VM changed!
if self.depth == 0:
self.last_return=data
self.last_pc = prev_vm.pc
@@ -2157,8 +2176,7 @@ class EVMWorld(Platform):
if isinstance(last_ex, Create):
self.current._push(prev_vm.address)
self.storage[prev_vm.address]['code'] = data
self.set_code(prev_vm.address, data)
else:
size = min(last_ex.out_size, len(data))
self.current.write_buffer(last_ex.out_offset, data[:size])
@@ -2167,7 +2185,7 @@ class EVMWorld(Platform):
self.current.pc += self.current.instruction.size
def STOP(self):
prev_vm = self._pop(rollback=False)
prev_vm = self._pop_vm(rollback=False)
if self.depth == 0:
self.last_pc = prev_vm.pc
raise TerminateState("STOP", testcase=True)
@@ -2178,7 +2196,7 @@ class EVMWorld(Platform):
self.current.pc += self.current.instruction.size
def THROW(self):
prev_vm = self._pop(rollback=True)
prev_vm = self._pop_vm(rollback=True)
#revert balance on CALL fail
self.storage[prev_vm.caller]['balance'] += prev_vm.value
self.storage[prev_vm.address]['balance'] -= prev_vm.value
@@ -2193,7 +2211,7 @@ class EVMWorld(Platform):
self.current.pc += self.current.instruction.size
def REVERT(self, data):
prev_vm = self._pop(rollback=True)
prev_vm = self._pop_vm(rollback=True)
#revert balance on CALL fail
self.storage[prev_vm.caller]['balance'] += prev_vm.value
self.storage[prev_vm.address]['balance'] -= prev_vm.value
@@ -2216,7 +2234,7 @@ class EVMWorld(Platform):
self.storage[recipient]['balance'] += self.storage[address]['balance']
self.storage[address]['balance'] = 0
self.suicide.add(address)
prev_vm = self._pop(rollback=False)
prev_vm = self._pop_vm(rollback=False)
if self.depth == 0:
self.last_pc = prev_vm.pc
raise TerminateState("SELFDESTRUCT", testcase=True)
examples/evm/seth.py → manticore/seth.py
+314 -185
View File
@@ -1,97 +1,52 @@
from manticore import Manticore
from manticore.core.smtlib import ConstraintSet, Operators, solver, issymbolic, Array, Expression, Constant
from manticore.core.smtlib.visitors import arithmetic_simplifier
from manticore.platforms import evm
from manticore.core.state import State
from . import Manticore
from .core.smtlib import ConstraintSet, Operators, solver, issymbolic, Array, Expression, Constant
from .core.smtlib.visitors import arithmetic_simplifier
from .platforms import evm
from .core.state import State
import tempfile
from subprocess import Popen, PIPE
import sha3
import json
import StringIO
class EVMContract(object):
class ABI(object):
'''
This class contains methods to handle the ABI.
The Application Binary Interface is the standard way to interact with
contracts in the Ethereum ecosystem, both from outside the blockchain
and for contract-to-contract interaction.
def __init__(self, address, seth=None, default_caller=None):
self._default_caller = default_caller
self._seth=seth
self._address=address
self._hashes = {}
self._caller = None
self._value = 0
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]
def __int__(self):
return self._address
@property
def address(self):
return self._address
def value(self, value):
self._value = value
return self
def caller(self, caller):
self._caller = caller
return self
def __getattribute__(self, name):
if not name.startswith('_') and name in self._hashes.keys():
def f(*args, **kwargs):
caller = kwargs.get('caller', self._caller)
value = kwargs.get('value', self._value)
tx_data = self._seth.make_function_call(str(self._hashes[name][0]),*args)
if caller is not None:
caller = int(caller)
else:
caller = self._default_caller
self._seth.transaction(caller=caller,
address=self._address,
value=value,
data=tx_data
)
self._caller = None
self._value = 0
return f
else:
return object.__getattribute__(self, name)
class ManticoreEVM(Manticore):
'''
class SByte():
''' Unconstrained symbolic byte, not asociated with any constraint set '''
def __init__(self, size=1):
self.size=size
def __mul__(self, reps):
return Symbol(self.size*reps)
SCHAR = SByte(1)
SUINT = SByte(32)
SValue = None
@staticmethod
def pack_msb(value):
return ''.join(ManticoreEVM.serialize_uint(value))
@staticmethod
def serialize(value):
''' Translates a python object to its EVM ABI serialization.
It supports s '''
if isinstance(value, (str,tuple)):
return ManticoreEVM.serialize_string(value)
return ABI.serialize_string(value)
if isinstance(value, (list)):
return ManticoreEVM.serialize_array(value)
return ABI.serialize_array(value)
if isinstance(value, (int, long)):
return ManticoreEVM.serialize_uint(value)
if isinstance(value, ManticoreEVM.SByte):
return ManticoreEVM.serialize_uint(value.size) + (None,)*value.size + (('\x00',)*(32-(value.size%32)))
return ABI.serialize_uint(value)
if isinstance(value, ABI.SByte):
return ABI.serialize_uint(value.size) + (None,)*value.size + (('\x00',)*(32-(value.size%32)))
if value is None:
return (None,)*32
@staticmethod
def serialize_uint(value, size=32):
'''takes an int and packs it into a 32 byte string, msb first'''
'''Translates a python int into a 32 byte string, msb first'''
assert size >=1
bytes = []
for position in range(size):
@@ -101,15 +56,16 @@ class ManticoreEVM(Manticore):
@staticmethod
def serialize_string(value):
'''Translates a string or a tuple of chars its EVM ABI serialization'''
assert isinstance(value, (str,tuple))
return ManticoreEVM.serialize_uint(len(value)) + tuple(value) + tuple('\x00'*(32-(len(value)%32)))
return ABI.serialize_uint(len(value)) + tuple(value) + tuple('\x00'*(32-(len(value)%32)))
@staticmethod
def serialize_array(value):
assert isinstance(value, list)
serialized = [ManticoreEVM.serialize_uint(len(value))]
serialized = [ABI.serialize_uint(len(value))]
for item in value:
serialized.append(ManticoreEVM.serialize(item))
serialized.append(ABI.serialize(item))
return reduce(lambda x,y: x+y, serialized)
@staticmethod
@@ -125,20 +81,20 @@ class ManticoreEVM(Manticore):
return ()
args = list(args)
for i in range(len(args)):
if isinstance(args[i], EVMContract):
if isinstance(args[i], EVMAccount):
args[i] = int(args[i])
result = []
dynamic_args = []
dynamic_offset = 32*len(args)
for arg in args:
if isinstance(arg, (list, tuple, str, ManticoreEVM.SByte)):
result.append(ManticoreEVM.serialize(dynamic_offset))
serialized_arg = ManticoreEVM.serialize(arg)
result.append(ABI.serialize(dynamic_offset))
serialized_arg = ABI.serialize(arg)
dynamic_args.append(serialized_arg)
assert len(serialized_arg)%32 ==0
dynamic_offset += len(serialized_arg)
else:
result.append(ManticoreEVM.serialize(arg))
result.append(ABI.serialize(arg))
for arg in dynamic_args:
result.append(arg)
@@ -147,20 +103,114 @@ class ManticoreEVM(Manticore):
@staticmethod
def make_function_call(method_name, *args):
function_id = ManticoreEVM.make_function_id(method_name)
function_id = ABI.make_function_id(method_name)
def check_bitsize(value, size):
if isinstance(value, BitVec):
return value.size==size
return (value & ~((1<<size)-1)) == 0
assert len(function_id) == 4
result = [tuple(function_id)]
result.append(ManticoreEVM.make_function_arguments(*args))
result.append(ABI.make_function_arguments(*args))
return reduce(lambda x,y: x+y, result)
class EVMAccount(object):
''' An EVM account '''
def __init__(self, address, seth=None, default_caller=None):
''' Encapsulates an account.
:param address: the address of this account
:type address: 160 bit long integer
:param seth: the controlling manticore
:param default_caller: the default caller address for any transaction
'''
self._default_caller = default_caller
self._seth=seth
self._address=address
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]
def __int__(self):
return 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.
Example use::
#call funtion `add` on contract_account with argument `1000`
contract_account.add(1000)
'''
if not name.startswith('_') and name in self._hashes.keys():
def f(*args, **kwargs):
caller = kwargs.get('caller', None)
value = kwargs.get('value', 0)
tx_data = ABI.make_function_call(str(self._hashes[name][0]), *args)
if caller is not None:
caller = int(caller)
else:
caller = self._default_caller
self._seth.transaction(caller=caller,
address=self._address,
value=value,
data=tx_data
)
self._caller = None
self._value = 0
return f
else:
return object.__getattribute__(self, name)
class ManticoreEVM(Manticore):
''' Manticore EVM manager
Usage Ex::
from manticore.seth import ManticoreEVM, ABI
seth = ManticoreEVM()
#And now make the contract account to analyze
source_code = """
pragma solidity ^0.4.15;
contract AnInt {
uint private i=0;
function set(uint value){
i=value
}
}
"""
#Initialize user and contracts
user_account = seth.create_account(balance=1000)
contract_account = seth.solidity_create_contract(source_code, owner=user_account, balance=0)
contract_account.set(12345, value=100)
seth.report()
print seth.coverage(contract_account)
'''
SByte=ABI.SByte
SValue=ABI.SValue
@staticmethod
def compile(source_code):
"""
Compile a solidity source code
name, source_code, bytecode, srcmap, srcmap_runtime, hashes = ManticoreEVM._compile(source_code)
return bytecode
@staticmethod
def _compile(source_code):
""" Compile a solidity contract, used internally
:param source_code: a solidity source code
:return: name, source_code, bytecode, srcmap, srcmap_runtime, hashes
"""
solc = "solc"
with tempfile.NamedTemporaryFile() as temp:
@@ -178,7 +228,6 @@ class ManticoreEVM(Manticore):
return name, source_code, bytecode, srcmap, srcmap_runtime, hashes
def __init__(self):
#Make the constraint store
constraints = ConstraintSet()
#make the ethereum world state
@@ -196,22 +245,22 @@ class ManticoreEVM(Manticore):
self.context['seth']['_saved_states'] = []
self.context['seth']['_final_states'] = []
self._executor.subscribe('did_load_state', self.load_state_callback)
self._executor.subscribe('will_terminate_state', self.terminate_state_callback)
self._executor.subscribe('will_execute_instruction', self.will_execute_instruction_callback)
self._executor.subscribe('did_execute_instruction', self.did_execute_instruction_callback)
self._executor.subscribe('did_read_code', self.did_read_code)
self._executor.subscribe('on_symbolic_sha3', self.symbolic_sha3)
self._executor.subscribe('on_concrete_sha3', self.concrete_sha3)
self._executor.subscribe('did_load_state', self._load_state_callback)
self._executor.subscribe('will_terminate_state', self._terminate_state_callback)
self._executor.subscribe('will_execute_instruction', self._will_execute_instruction_callback)
self._executor.subscribe('did_execute_instruction', self._did_execute_instruction_callback)
self._executor.subscribe('did_read_code', self._did_read_code)
self._executor.subscribe('on_symbolic_sha3', self._symbolic_sha3)
self._executor.subscribe('on_concrete_sha3', self._concrete_sha3)
@property
def world(self):
if self.initial_state is None:
return None
return self.initial_state.platform
''' The world instance or None if there is more than one state '''
return self.get_world(None)
@property
def running_state_ids(self):
''' IDs of the running states'''
with self.locked_context('seth') as context:
if self.initial_state is not None:
return context['_saved_states'] + [-1]
@@ -220,29 +269,69 @@ class ManticoreEVM(Manticore):
@property
def final_state_ids(self):
''' IDs of the terminated states '''
with self.locked_context('seth') as context:
return context['_final_states']
def get_world(self, state_id=-1):
if state_id == -1:
return self.initial_state.platform
def get_world(self, state_id=None):
''' Returns the evm world of `state_id` state. '''
state = self.load(state_id)
if state is None:
return None
else:
return state.platform
state = self._executor._workspace.load_state(state_id, delete=False)
return state.platform
def get_balance(self, address):
if isinstance(address, EVMContract):
def get_balance(self, address, state_id=None):
''' Balance for account `address` on state `state_id` '''
if isinstance(address, EVMAccount):
address = int(address)
return self.get_world().storage[address]['balance']
return self.get_world(state_id).storage[address]['balance']
def get_storage(self, address, offset, state_id=None):
''' Storage data for `offset` on account `address` on state `state_id` '''
if isinstance(address, EVMAccount):
address = int(address)
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` '''
state = self.load(state_id)
return state.world.last_return
def solidity_create_contract(self, source_code, owner, balance=0, address=None, args=()):
name, source_code, init_bytecode, metadata, metadata_runtime, hashes = self.compile(source_code)
address = self.create_contract(owner=owner, address=address, balance=balance, init=tuple(init_bytecode)+tuple(ManticoreEVM.make_function_arguments(*args)))
''' Creates a solidity contract
:param source_code: solidity source code
:type source_code: str
:param owner: owner account (will be default caller in any transactions)
:type owner: int or EVMAccount
: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
:param args: constructor arguments
:type args: tuple
:return: an EVMAccount
'''
name, source_code, init_bytecode, metadata, metadata_runtime, hashes = 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
return EVMContract(address, self, default_caller=owner)
return EVMAccount(address, self, default_caller=owner)
def create_contract(self, owner, balance=0, init=None, address=None):
''' Only available when there is a single state of the world'''
''' Creates a contract
:param init: initializing evm bytecode and arguments
:type init: str
:param owner: owner account (will be default caller in any transactions)
:type owner: int or EVMAccount
: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
'''
with self.locked_context('seth') as context:
assert context['_pending_transaction'] is None
assert init is not None
@@ -255,15 +344,32 @@ class ManticoreEVM(Manticore):
return address
def create_account(self, balance=0, address=None, code=''):
''' Only available when there is a single state of the world'''
''' Creates a normal account
: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
'''
with self.locked_context('seth') as context:
assert context['_pending_transaction'] is None
return self.world.create_account( address, balance, code=code, storage=None)
def transaction(self, caller, address, value, data):
if isinstance(address, EVMContract):
''' Issue a transaction
:param caller: the address of the account sending the transaction
:type caller: int or EVMAccount
:param value: balance to be transfered on creation
:type value: int or SValue
:param address: the address of the contract to call
:type address: int or EVMAccount
:return: an EVMAccount
'''
if isinstance(address, EVMAccount):
address = int(address)
if isinstance(caller, EVMContract):
if isinstance(caller, EVMAccount):
caller = int(caller)
@@ -274,6 +380,8 @@ class ManticoreEVM(Manticore):
return self.run(procs=10)
def run(self, **kwargs):
''' Run any pending transaction on any running state '''
#Check if there is a pending transaction
with self.locked_context('seth') as context:
assert context['_pending_transaction'] is not None
@@ -302,6 +410,13 @@ class ManticoreEVM(Manticore):
return result
def save(self, state, final=False):
''' Save a state in secondary storage and add it to running or final lists
:param state: A manticore State
:param final: True if state is final
:returns: a state id
'''
#save the state to secondary storage
state_id = self._executor._workspace.save_state(state)
@@ -314,8 +429,33 @@ class ManticoreEVM(Manticore):
context['_saved_states'].append(state_id)
return state_id
def load(self, state_id=None):
''' Load one of the running or final states.
:param state_id: If None it assumes there is a single running state
:type state_id: int or None
'''
state = None
if state_id is None:
#a single state was assumed
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.")
if state_id == -1:
state = self.initial_state
else:
state = self._executor._workspace.load_state(state_id, delete=False)
return state
#Callbacks
def terminate_state_callback(self, state, state_id, e):
def _terminate_state_callback(self, state, state_id, e):
''' INTERNAL USE
Every time a state finishes executing last transaction we save it in
our private list
@@ -339,7 +479,7 @@ class ManticoreEVM(Manticore):
#Callbacks
def load_state_callback(self, state, state_id):
def _load_state_callback(self, state, state_id):
''' INTERNAL USE
When a state was just loaded from stoage we do the pending transaction
'''
@@ -370,31 +510,28 @@ class ManticoreEVM(Manticore):
assert ty == 'CREATE_CONTRACT'
world.create_contract(caller=caller, address=address, balance=value, init=data)
def will_execute_instruction_callback(self, state, pc, instruction):
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
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):
def _did_execute_instruction_callback(self, state, prev_pc, pc, instruction):
''' INTERNAL USE '''
state.context.setdefault('seth.trace',[]).append((state.platform.current.address, pc))
def did_read_code(self, state, offset, size):
def _did_read_code(self, state, offset, size):
''' INTERNAL USE '''
with self.locked_context('code_data', set) as code_data:
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 '''
output = StringIO.StringIO()
def last_return(self, state_id=-1):
if state_id == -1:
state = self.initial_state
else:
state = self._executor._workspace.load_state(state_id, delete=False)
return state.world.last_return
def report(self, state_id, ty=None):
def compare_buffers(a, b):
if len(a) != len(b):
return False
@@ -405,21 +542,18 @@ class ManticoreEVM(Manticore):
return False
return cond
if state_id == -1:
state = self.initial_state
else:
state = self._executor._workspace.load_state(state_id, delete=False)
state = self.load(state_id)
world = state.platform
trace = state.context['seth.trace']
last_pc = trace[-1][1]
last_address = trace[-1][0]
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]
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
# try to get the runtime bytecode from the account
try:
runtime_bytecode = world.storage[last_address]['code']
except:
@@ -429,8 +563,8 @@ class ManticoreEVM(Manticore):
if ty is not None:
if str(e) != ty:
return
print "="*20
print "REPORT:", e,
output.write("REPORT:" + str(e))
try:
# Magic number comes from here:
@@ -449,16 +583,16 @@ class ManticoreEVM(Manticore):
beg, size = map(int, source_pos.split(':'))
print " at:"
output.write( " at:" )
nl = md_source_code.count('\n')
snippet = md_source_code[beg:beg+size]
for l in snippet.split('\n'):
print ' ',nl,' ', l
output.write(' %s %s\n'%(nl, l))
nl+=1
except:
print
output.write('\n')
print "BALANCES"
output.write("BALANCES\n")
for address, account in world.storage.items():
if isinstance(account['balance'], Constant):
account['balance'] = account['balance'].value
@@ -466,38 +600,38 @@ class ManticoreEVM(Manticore):
if issymbolic(account['balance']):
m, M = solver.minmax(world.constraints, arithmetic_simplifier(account['balance']))
if m == M:
print "\t", hex(address), M
output.write('\t%x %r\n'%(address, M))
else:
print "\t", hex(address), "range:[%x, %x]"%(m,M)
output.write('\t%x range:[%x, %x]\n'%(address, m, M))
else:
print "\t", hex(address), account['balance'],"wei"
output.write('\t%x %d wei\n'%(address, account['balance']))
if state.platform.logs:
print "LOGS:"
for address, memlog, topics in state.platform.logs:
try:
res = memlog
if isinstance(memlog, Expression):
res = state.solve_one(memlog)
if isinstance(memlog, Array):
state.constrain(compare_buffers(memlog, res))
else:
state.constrain(memlog== res)
output.write('LOGS:\n')
for address, memlog, topics in state.platform.logs:
try:
res = memlog
if isinstance(memlog, Expression):
res = state.solve_one(memlog)
if isinstance(memlog, Array):
state.constrain(compare_buffers(memlog, res))
else:
state.constrain(memlog== res)
res1 = address
if isinstance(address, Expression):
res = state.solve_one(address)
if isinstance(address, Array):
state.constrain(compare_buffers(address, res))
else:
state.constrain(address == res)
res1 = address
if isinstance(address, Expression):
res = state.solve_one(address)
if isinstance(address, Array):
state.constrain(compare_buffers(address, res))
else:
state.constrain(address == res)
print "\t %s: %r %s" %( hex(res1), ''.join(map(chr,res)), topics)
except Exception,e:
print e
print "\t", address, repr(memlog), topics
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))
print "INPUT SYMBOLS"
output.write('INPUT SYMBOLS\n')
for expr in state.input_symbols:
res = state.solve_one(expr)
if isinstance(expr, Array):
@@ -506,9 +640,9 @@ class ManticoreEVM(Manticore):
state.constrain(expr== res)
try:
print "\t %s: %s"%( expr.name, res.encode('hex'))
output.write('\t %s: %s\n'%( expr.name, res.encode('hex')))
except:
print "\t", expr.name+':', res
output.write('\t %s: %s'% (expr.name, res))
#print "Constraints:"
#print state.constraints
@@ -545,47 +679,42 @@ class ManticoreEVM(Manticore):
size = int('0x'+data[dyn_offset:dyn_offset+64],16)
return data[dyn_offset+64:dyn_offset+64+size*2],offset+8
else:
print "<",ty,">"
raise NotImplemented
raise NotImplemented(ty)
print "TRANSACTION ", tx_num, '-', ty
output.write('TRANSACTION %d - %s' % (tx_num, ty))
try:
md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes= self.context['seth']['metadata'][address]
except:
md_name, md_source_code, md_init_bytecode, md_metadata, md_metadata_runtime, md_hashes = None,None,None,None,None,None
print '\t From: 0x%x'%x(caller)
print '\t To: 0x%x'%x(address)
print '\t Value: %d wei'%x(value)
output.write('\t From: 0x%x\n'% x(caller) )
output.write('\t To: 0x%x\n'%x(address))
output.write('\t Value: %d wei\n'%x(value))
xdata = x(data).encode('hex')
print '\t Data:', xdata
output.write('\t Data: %s\n'% xdata)
if ty == 'CALL':
print '\t Function: ',
done = False
rhashes = dict((hsh, signature) for signature, hsh in md_hashes.iteritems())
try:
rhashes = dict((hsh, signature) for signature, hsh in md_hashes.iteritems())
signature = rhashes.get(xdata[:8], '{fallback}()')
done = True
func_name = signature.split('(')[0]
print func_name,'(',
output.write('\t Function: %s(' % func_name)
types = signature.split('(')[1][:-1].split(',')
off = 8
for ty in types:
if off != 8:
print ',',
val, off = consume_type(ty, xdata, off)
print val,
print ')'
output.write('%s'%val)
output.write(')\n')
except Exception,e:
print e, xdata
output.write('%s %s\n'%(e, xdata))
return output.getvalue()
def 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
@@ -613,7 +742,7 @@ class ManticoreEVM(Manticore):
offset = 0
count = 0
total = 0
for i in evm.EVMDecoder.decode_all(runtime_bytecode[:end]) :
for i in evm.EVMAsm.disassemble_all(runtime_bytecode[:end]) :
if (account_address, offset) in seen:
output += bcolors.OKGREEN
@@ -629,16 +758,16 @@ class ManticoreEVM(Manticore):
output += "Total assembler lines: %d\n"% total
output += "Total assembler lines visited: %d\n"% count
output += "Coverage: %2.2f%%\n"% (count*100.0/total)
return output
def _symbolic_sha3(self, state, data, known_hashes):
''' INTERNAL USE '''
def symbolic_sha3(self, state, data, known_hashes):
with self.locked_context('known_sha3', set) as known_sha3:
state.platform._sha3.update(known_sha3)
def concrete_sha3(self, state, buf, value):
def _concrete_sha3(self, state, buf, value):
''' INTERNAL USE '''
with self.locked_context('known_sha3', set) as known_sha3:
known_sha3.add((buf,value))