diff --git a/examples/evm/solidse.py b/examples/evm/solidse.py new file mode 100644 index 0000000..cd9179a --- /dev/null +++ b/examples/evm/solidse.py @@ -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 + + + + + diff --git a/manticore/__main__.py b/manticore/__main__.py index 3ba224d..7f7e0a3 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -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 diff --git a/manticore/core/state.py b/manticore/core/state.py index 2d535b3..77c8c7a 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -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 diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index a7d99ec..34a0dcc 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -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) diff --git a/manticore/seth.py b/manticore/seth.py index 14f2a5b..728b5a6 100644 --- a/manticore/seth.py +++ b/manticore/seth.py @@ -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 :) '''