Detectors () (#637)

* 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
This commit is contained in:
feliam
2017-12-12 14:56:39 -03:00
committed by GitHub
parent df9af1fd12
commit 4b79711b92
5 changed files with 318 additions and 31 deletions

99
examples/evm/solidse.py Normal file
View File

@@ -0,0 +1,99 @@
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

View File

@@ -65,10 +65,16 @@ def parse_arguments():
def ethereum_cli(args):
from seth import ManticoreEVM
from seth import ManticoreEVM, IntegerOverflow, UnitializedStorage, UnitializedMemory
m = ManticoreEVM(procs=args.procs)
################ Default? Detectors #######################
m.register_detector(IntegerOverflow())
m.register_detector(UnitializedStorage())
m.register_detector(UnitializedMemory())
with open(args.argv[0]) as f:
source_code = f.read()
@@ -100,6 +106,18 @@ def ethereum_cli(args):
for state in m.all_states:
print str(state.context['last_exception'])
for address, pc, finding in m.global_findings:
output = ''
output += 'Finding: %s\n' % finding
output += '\t Contract: %s\n' % address
output += '\t Program counter: %s\n' % pc
output += '\t Snippet:\n'
src = m.get_metadata(address).get_source_for(pc)
output += '\n'.join(('\t\t'+x for x in src.split('\n')))
output += '\n'
print output
# for state in seth.all_states:
# blockchain = state.platform
# for tx in blockchain.transactions: # external transactions

View File

@@ -297,6 +297,10 @@ class State(Eventful):
from .smtlib import solver
return solver
def can_be_true(self, expr):
return self._solver.can_be_true(self._constraints, expr)
def solve_one(self, expr):
'''
Concretize a symbolic :class:`~manticore.core.smtlib.expression.Expression` into

View File

@@ -505,6 +505,10 @@ class EVMAsm(object):
}
return classes.get(self.opcode>>4, 'Invalid instruction')
@property
def uses_stack(self):
''' True if the instruction reads/writes from/to the stack '''
return self.reads_from_stack or self.writes_to_stack
@property
def reads_from_stack(self):
@@ -566,7 +570,11 @@ class EVMAsm(object):
''' True if the instruction access block information'''
return self.group == 'Block Information'
@property
def is_arithmetic(self):
''' True if the instruction is an arithmetic operation '''
return self.semantics in ('ADD', 'MUL', 'SUB', 'DIV', 'SDIV', 'MOD', 'SMOD', 'ADDMOD', 'MULMOD', 'EXP', 'SIGNEXTEND')
#from http://gavwood.com/paper.pdf
_table = {#opcode: (name, immediate_operand_size, pops, pushes, gas, description)
0x00: ('STOP', 0, 0, 0, 0, 'Halts execution.'),
@@ -1032,7 +1040,12 @@ class EVM(Eventful):
from position 0), and the stack contents. The memory
contents are a series of zeroes of bitsize 256
'''
_published_events = {'read_code', 'decode_instruction', 'execute_instruction', 'concrete_sha3', 'symbolic_sha3'}
_published_events = {'evm_execute_instruction',
'evm_read_storage', 'evm_write_storage',
'evm_read_memory',
'evm_write_memory',
'evm_read_code',
'decode_instruction', 'execute_instruction', 'concrete_sha3', 'symbolic_sha3'}
def __init__(self, constraints, address, origin, price, data, caller, value, code, header, global_storage=None, depth=0, gas=1000000, **kwargs):
'''
Builds a Ethereum Virtual Machine instance
@@ -1154,6 +1167,7 @@ class EVM(Eventful):
#CHECK VALUE IS A 256 BIT INT OR BITVEC
self._allocate(address)
self.memory.write(address, [value])
self._publish('did_evm_write_memory', address, value)
def _load(self, address):
@@ -1162,6 +1176,8 @@ class EVM(Eventful):
value = arithmetic_simplifier(value)
if isinstance(value, Constant) and not value.taint:
value = value.value
self._publish('did_evm_read_memory', address, value)
return value
@staticmethod
@@ -1243,11 +1259,11 @@ class EVM(Eventful):
setstate=setstate,
policy='ALL')
self._publish( 'will_decode_instruction', self.pc)
self._publish('will_decode_instruction', self.pc)
last_pc = self.pc
current = self.instruction
self._publish( 'will_execute_instruction', self.pc, current)
self._publish('will_execute_instruction', self.pc, current)
#Consume some gas
self._consume(current.fee)
@@ -1263,7 +1279,6 @@ class EVM(Eventful):
for _ in range(current.pops):
arguments.append(self._pop())
#simplify stack arguments
for i in range(len(arguments)):
if isinstance(arguments[i], Expression):
@@ -1271,10 +1286,13 @@ class EVM(Eventful):
if isinstance(arguments[i], Constant):
arguments[i] = arguments[i].value
self._publish('will_evm_execute_instruction', current, arguments)
last_pc = self.pc
#Execute
try:
result = implementation(*arguments)
self._publish('did_evm_execute_instruction', current, arguments, result)
except ConcretizeStack as ex:
for arg in reversed(arguments):
self._push(arg)
@@ -1561,7 +1579,7 @@ class EVM(Eventful):
self._store(mem_offset+i, 0)
else:
self._store(mem_offset+i, Operators.ORD(self.bytecode[code_offset+i]))
self._publish( 'did_read_code', code_offset, size)
self._publish( 'did_evm_read_code', code_offset, size)
def GASPRICE(self):
'''Get price of gas in current environment'''
@@ -1643,13 +1661,16 @@ class EVM(Eventful):
def SLOAD(self, offset):
'''Load word from storage'''
return self.global_storage[self.address]['storage'].get(offset,0)
value = self.global_storage[self.address]['storage'].get(offset,0)
self._publish('did_evm_read_storage', offset, value)
return value
def SSTORE(self, offset, value):
'''Save word to storage'''
self.global_storage[self.address]['storage'][offset] = value
if value is 0:
del self.global_storage[self.address]['storage'][offset]
self._publish('did_evm_write_storage', offset, value)
def JUMP(self, dest):
'''Alter the program counter'''
@@ -1832,7 +1853,7 @@ class EVM(Eventful):
################################################################################
################################################################################
class EVMWorld(Platform):
_published_events = {'read_code', 'decode_instruction', 'execute_instruction', 'concrete_sha3', 'symbolic_sha3'}
_published_events = {'evm_read_storage', 'evm_write_storage', 'evm_read_code', 'decode_instruction', 'execute_instruction', 'concrete_sha3', 'symbolic_sha3'}
def __init__(self, constraints, storage=None, **kwargs):
super(EVMWorld, self).__init__(path="NOPATH", **kwargs)
@@ -2255,7 +2276,6 @@ class EVMWorld(Platform):
if self.depth == 0:
tx = self._transactions[-1]
tx.return_data=data
#tx.last_pc = prev_vm.pc
tx.result = 'RETURN'
raise TerminateState("RETURN", testcase=True)
@@ -2279,7 +2299,6 @@ class EVMWorld(Platform):
if self.depth == 0:
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
@@ -2296,7 +2315,6 @@ class EVMWorld(Platform):
if self.depth == 0:
tx = self._transactions[-1]
#tx.last_pc = prev_vm.pc
tx.return_data=None
tx.result = 'THROW'
raise TerminateState("THROW", testcase=True)
@@ -2315,7 +2333,6 @@ class EVMWorld(Platform):
if self.depth == 0:
tx = self._transactions[-1]
tx.return_data=data
#tx.last_pc = prev_vm.pc
tx.result = 'REVERT'
raise TerminateState("REVERT", testcase=True)

View File

@@ -7,7 +7,99 @@ import tempfile
from subprocess import Popen, PIPE
import sha3
import json
import logging
import StringIO
from .core.plugin import Plugin
logger = logging.getLogger(__name__)
################ Detectors ####################
class Detector(Plugin):
@property
def name(self):
return self.__class__.__name__.split('.')[-1]
def get_findings(self, state):
return state.context.setdefault('seth.findings.%s'%self.name,set())
def add_finding(self, state, finding):
address = state.platform.current.address
pc = state.platform.current.pc
self.get_findings(state).add((address, pc, finding))
with self.manticore.locked_context('seth.global_findings', set) as global_findings:
global_findings.add((address, pc, finding))
logger.info(finding)
def _get_src(self, address, pc):
return self.manticore.get_metadata(address).get_source_for(pc)
def report(self, state):
output = ''
for address, pc, finding in self.get_findings(state):
output += 'Finding %s\n' % finding
output += '\t Contract: %s\n' % address
output += '\t Program counter: %s\n' % pc
output += '\t Snippet:\n'
output += '\n'.join(('\t\t'+x for x in self._get_src(address, pc).split('\n')))
output += '\n'
return output
class IntegerOverflow(Detector):
'''
Detects any it overflow on instructions ADD and SUB.
'''
def did_evm_execute_instruction_callback(self, state, instruction, arguments, result):
if instruction.semantics == 'ADD':
if state.can_be_true(result < arguments[0]) or state.can_be_true(result < arguments[1]):
self.add_finding(state, "Integer overflow at ADD instruction")
if instruction.semantics == 'SUB':
if state.can_be_true(arguments[1] > arguments[0]):
src = self._get_src(state)
self.add_finding(state, "Integer underflow at SUB instruction")
class UnitializedMemory(Detector):
'''
detects the use of not initialized memory
'''
def did_evm_read_memory(self, state, offset, value):
if not state.can_be_true(value != 0):
#Not initialized memory should be zero
return
#check if offset is known
cbu = True #Can be unknown
for known_address in state.context['seth.detectors.initialized_memory']:
cbu = Operators.AND(cbu, offset!=known_address)
if state.can_be_true(cbu):
self.add_finding(state, "Potentially reading uninitialized memory at instruction")
def did_evm_write_memory(self, state, offset, value):
#concrete or symbolic write
state.context.setdefault('seth.detectors.initialized_memory',set()).add(offset)
class UnitializedStorage(Detector):
'''
UnitializedStorage: detects the use of not initialized storage
'''
def did_evm_read_storage(self, state, offset, value):
if not state.can_be_true(value != 0):
#Not initialized memory should be zero
return
#check if offset is known
cbu = True #Can be unknown
for known_address in state.context['seth.detectors.initialized_storage']:
cbu = Operators.AND(cbu, offset!=known_address)
if state.can_be_true(cbu):
self.add_finding(state, "Potentially reading uninitialized storage")
def did_evm_write_storage(self, state, offset, value):
#concrete or symbolic write
state.context.setdefault('seth.detectors.initialized_storage',set()).add(offset)
def calculate_coverage(code, seen):
''' '''
@@ -26,14 +118,60 @@ def calculate_coverage(code, seen):
return count*100.0/total
class SolidityMetadata(object):
def __init__(self, name, source_code, init_bytecode, metadata, metadata_runtime, hashes, abi):
def __init__(self, name, source_code, init_bytecode, runtime_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 ])
self.runtime_bytecode = runtime_bytecode
# https://solidity.readthedocs.io/en/develop/miscellaneous.html#source-mappings
self.metadata_runtime = {}
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
asm_offset = 0
asm_pos = 0
md = dict(enumerate(metadata_runtime[asm_pos].split(':')))
s = int(md.get(0,0))
l = int(md.get(1,0))
f = int(md.get(2,0))
j = md.get(3,None)
for i in evm.EVMAsm.disassemble_all(self.runtime_bytecode[:end]):
if len(metadata_runtime[asm_pos]):
md = metadata_runtime[asm_pos]
if len(md):
d = {}
for p, k in enumerate(md.split(':')):
if len(k):
d[p]=k
s = int(d.get(0,s))
l = int(d.get(1,l))
f = int(d.get(2,f))
j = d.get(3,j)
self.metadata_runtime[asm_offset] = (s,l,f,j)
asm_pos += 1
asm_offset += i.size
def get_source_for(self, asm_pos):
''' Solidity source code snippet related to `asm_pos` evm bytecode offset
'''
beg, size, _, _ = self.metadata_runtime[asm_pos]
output = ''
nl = self.source_code.count('\n')
snippet = self.source_code[beg:beg+size]
for l in snippet.split('\n'):
output += ' %s %s\n'%(nl, l)
nl+=1
return output
@property
def signatures(self):
@@ -181,7 +319,7 @@ class ABI(object):
value = -(value & mask) + (value & ~mask)
return value, offset+32
elif ty == u'':
return '', offset
return None, offset
elif ty in (u'bytes', u'string'):
dyn_offset = 4 + get_uint(256,offset)
size = get_uint(256, dyn_offset)
@@ -210,7 +348,10 @@ class ABI(object):
arguments = []
for ty in types:
val, off = ABI._consume_type(ty, data, off)
arguments.append(val)
if val is not None:
arguments.append(val)
else:
break
if is_multiple:
if func_name is not None:
@@ -361,7 +502,7 @@ class ManticoreEVM(Manticore):
with tempfile.NamedTemporaryFile() as temp:
temp.write(source_code)
temp.flush()
p = Popen([solc, '--combined-json', 'abi,srcmap,srcmap-runtime,bin,hashes', temp.name], stdout=PIPE)
p = Popen([solc, '--combined-json', 'abi,srcmap,srcmap-runtime,bin,hashes,bin-runtime', 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]
@@ -371,7 +512,8 @@ class ManticoreEVM(Manticore):
srcmap_runtime = outp['srcmap-runtime'].split(';')
hashes = outp['hashes']
abi = json.loads(outp['abi'])
return name, source_code, bytecode, srcmap, srcmap_runtime, hashes, abi
runtime = outp['bin-runtime'].decode('hex')
return name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi
def __init__(self, procs=1):
''' A manticere EVM manager
@@ -388,7 +530,9 @@ class ManticoreEVM(Manticore):
initial_state.context['tx'] = []
super(ManticoreEVM, self).__init__(initial_state)
self.detectors = {}
self.metadata = {}
#The following should go to manticore.context so we can use multiprocessing
self.context['seth'] = {}
self.context['seth']['_pending_transaction'] = None
@@ -399,7 +543,7 @@ class ManticoreEVM(Manticore):
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('did_read_code', self._did_evm_read_code)
self._executor.subscribe('on_symbolic_sha3', self._symbolic_sha3)
self._executor.subscribe('on_concrete_sha3', self._concrete_sha3)
@@ -498,10 +642,9 @@ class ManticoreEVM(Manticore):
:return: an EVMAccount
'''
name, source_code, init_bytecode, metadata, metadata_runtime, hashes, abi = self._compile(source_code)
self._output.store.save_value('contract.bytecode', init_bytecode)
name, source_code, init_bytecode, runtime_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.metadata[address] = SolidityMetadata(name, source_code, init_bytecode, metadata, metadata_runtime, hashes, abi)
self.metadata[address] = SolidityMetadata(name, source_code, init_bytecode, runtime_bytecode, metadata, metadata_runtime, hashes, abi)
return EVMAccount(address, self, default_caller=owner)
def create_contract(self, owner, balance=0, init=None, address=None):
@@ -630,7 +773,7 @@ class ManticoreEVM(Manticore):
#Get the ID of the single running state
state_id = self.running_state_ids[0]
else:
raise Exception("More than one state running. Do not know which one to choose.")
raise Exception("More than one state running.")
if state_id == -1:
state = self.initial_state
@@ -719,22 +862,28 @@ class ManticoreEVM(Manticore):
''' INTERNAL USE '''
state.context.setdefault('seth.trace',[]).append((state.platform.current.address, pc))
def _did_read_code(self, state, offset, size):
def _did_evm_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 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
return self.metadata.get(address)
def register_detector(self, d):
if not isinstance(d, Detector):
raise Exception("Not a Detector")
self.detectors[d.name] = d
self.register_plugin(d)
@property
def global_findings(self):
with self.locked_context('seth.global_findings', set) as global_findings:
return global_findings
def report(self, state, ty=None):
''' Prints a small report on state. Prints a little something about state :) '''