diff --git a/manticore/core/cpu/abstractcpu.py b/manticore/core/cpu/abstractcpu.py index a5d2bd7..65ea4be 100644 --- a/manticore/core/cpu/abstractcpu.py +++ b/manticore/core/cpu/abstractcpu.py @@ -777,7 +777,7 @@ class Cpu(Eventful): ''' self._icount += 1 self._publish('did_execute_instruction', self._last_pc, self.PC, insn) - + def emulate(self, insn): ''' If we could not handle emulating an instruction, use Unicorn to emulate diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py index 6ba1b04..8007daa 100644 --- a/manticore/core/plugin.py +++ b/manticore/core/plugin.py @@ -1,12 +1,32 @@ import logging + +from capstone import CS_GRP_JUMP + from ..utils.helpers import issymbolic -from ..utils.event import Eventful logger = logging.getLogger('MANTICORE') class Plugin(object): def __init__(self): self.manticore = None + self.last_reg_state = {} + +def _dict_diff(d1, d2): + ''' + Produce a dict that includes all the keys in d2 that represent different values in d1, as well as values that + aren't in d1. + + :param dict d1: First dict + :param dict d2: Dict to compare with + :rtype: dict + ''' + d = {} + for key in set(d1).intersection(set(d2)): + if d2[key] != d1[key]: + d[key] = d2[key] + for key in set(d2).difference(set(d1)): + d[key] = d2[key] + return d class Tracer(Plugin): def will_start_run_callback(self, state): @@ -15,6 +35,69 @@ class Tracer(Plugin): def did_execute_instruction_callback(self, state, pc, target_pc, instruction): state.context['trace'].append(pc) +class ExtendedTracer(Plugin): + def __init__(self): + ''' + Record a detailed execution trace + ''' + super(ExtendedTracer, self).__init__() + self.last_dict = {} + self.current_pc = None + self.context_key = 'e_trace' + + def will_start_run_callback(self, state): + state.context[self.context_key] = [] + + def register_state_to_dict(self, cpu): + d = {} + for reg in cpu.canonical_registers: + val = cpu.read_register(reg) + d[reg] = val if not issymbolic(val) else '' + return d + + def will_execute_instruction_callback(self, state, pc, instruction): + self.current_pc = pc + + def did_execute_instruction_callback(self, state, pc, target_pc, instruction): + reg_state = self.register_state_to_dict(state.cpu) + entry = { + 'type': 'regs', + 'values': _dict_diff(self.last_dict, reg_state) + } + self.last_dict = reg_state + state.context[self.context_key].append(entry) + + def will_read_memory_callback(self, state, where, size): + if self.current_pc == where: + return + + #print 'will_read_memory %x %r, current_pc %x'%(where, size, self.current_pc) + + def did_read_memory_callback(self, state, where, value, size): + if self.current_pc == where: + return + + #print 'did_read_memory %x %r %r, current_pc %x'%(where, value, size, self.current_pc) + + def will_write_memory_callback(self, state, where, value, size): + if self.current_pc == where: + return + + #print 'will_write_memory %x %r %r, current_pc %x'%(where, value, size, self.current_pc) + + def did_write_memory_callback(self, state, where, value, size): + if self.current_pc == where: + raise Exception + return + + entry = { + 'type': 'mem_write', + 'where': where, + 'value': value, + 'size': size + } + state.context[self.context_key].append(entry) + class RecordSymbolicBranches(Plugin): def will_start_run_callback(self, state): state.context['branches'] = {} @@ -91,7 +174,6 @@ class Visited(Plugin): logger.info('Coverage: %d different instructions executed', len(executor_visited)) - #TODO document all callbacks class ExamplePlugin(Plugin): def will_decode_instruction_callback(self, state, pc): diff --git a/manticore/core/workspace.py b/manticore/core/workspace.py index 86d3d08..badcb3a 100644 --- a/manticore/core/workspace.py +++ b/manticore/core/workspace.py @@ -65,17 +65,17 @@ class Store(object): @classmethod def fromdescriptor(cls, desc): - """ - Create a :class:`~manticore.core.workspace.Store` instance depending on the descriptor. + """ + Create a :class:`~manticore.core.workspace.Store` instance depending on the descriptor. - Valid descriptors: - * fs: - * redis:: - * mem: + Valid descriptors: + * fs: + * redis:: + * mem: - :param str desc: Store descriptor - :return: Store instance - """ + :param str desc: Store descriptor + :return: Store instance + """ type_, uri = ('fs', None) if desc is None else desc.split(':', 1) for subclass in cls.__subclasses__(): if subclass.store_type == type_: @@ -517,8 +517,8 @@ class ManticoreOutput(object): with self._named_stream('trace') as f: if 'trace' not in state.context: return - for pc in state.context['trace']: - f.write('0x{:08x}\n'.format(pc)) + for entry in state.context['trace']: + f.write('0x{:x}'.format(entry)) def save_constraints(self, state): # XXX(yan): We want to conditionally enable this check diff --git a/manticore/manticore.py b/manticore/manticore.py index 6a03729..3ef416c 100644 --- a/manticore/manticore.py +++ b/manticore/manticore.py @@ -181,6 +181,7 @@ class Manticore(Eventful): #Move the folowing into a plugin self._assertions = {} self._coverage_file = None + self.trace = None #FIXME move the folowing to aplugin self.subscribe('will_generate_testcase', self._generate_testcase_callback) diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index ad1b9cc..f853faf 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -1238,7 +1238,7 @@ class Linux(Platform): def pad(s): return s +'\x00'*(65-len(s)) - now = datetime.now().strftime("%a %b %d %H:%M:%S ART %Y") + now = datetime(2017, 8, 01).strftime("%a %b %d %H:%M:%S ART %Y") info = (('sysname', 'Linux'), ('nodename', 'ubuntu'), ('release', '4.4.0-77-generic'), diff --git a/scripts/follow_trace.py b/scripts/follow_trace.py new file mode 100755 index 0000000..33d167d --- /dev/null +++ b/scripts/follow_trace.py @@ -0,0 +1,118 @@ +#!/usr/bin/env python + +''' +A simple trace following execution driver script. Only supports passing symbolic arguments via argv. + +''' + +import sys +import time +import argparse +import itertools + +from manticore import Manticore, issymbolic +from manticore.core.plugin import ExtendedTracer, Plugin + +def _partition(pred, iterable): + t1, t2 = itertools.tee(iterable) + return (list(itertools.ifilterfalse(pred, t1)), filter(pred, t2)) + + +class TraceReceiver(Plugin): + def __init__(self, tracer): + self._trace = None + self._tracer = tracer + super(self.__class__, self).__init__() + + @property + def trace(self): + return self._trace + + def will_generate_testcase_callback(self, state, test_id, msg): + self._trace = state.context[self._tracer.context_key] + + instructions, writes = _partition(lambda x: x['type'] == 'regs', self._trace) + total = len(self._trace) + print 'Recorded concrete trace: {}/{} instructions, {}/{} writes'.format( + len(instructions), total, len(writes), total) + + +class Follower(Plugin): + def __init__(self, trace): + self.index = 0 + self.trace = trace + self.last_instruction = None + self.symbolic_ranges = [] + self.active = True + super(self.__class__, self).__init__() + + def add_symbolic_range(self, pc_start, pc_end): + self.symbolic_ranges.append((pc_start,pc_end)) + + def get_next(self, type): + event = self.trace[self.index] + assert event['type'] == type + self.index += 1 + return event + + def did_write_memory_callback(self, state, where, value, size): + if not self.active: + return + write = self.get_next('mem_write') + + if not issymbolic(value): + return + + assert write['where'] == where and write['size'] == size + state.constrain(value == write['value']) + + def did_execute_instruction_callback(self, state, last_pc, pc, insn): + if not self.active: + return + event = self.get_next('regs') + self.last_instruction = event['values'] + if issymbolic(pc): + state.constrain(state.cpu.RIP == self.last_instruction['RIP']) + else: + for start, stop in self.symbolic_ranges: + if start <= pc <= stop: + self.active = False + + +def main(): + parser = argparse.ArgumentParser(description='Follow a concrete trace') + parser.add_argument('-f', '--explore_from', help='Value of PC from which to explore symbolically', type=str) + parser.add_argument('-t', '--explore_to', type=str, default=sys.maxint, + help="Value of PC until which to explore symbolically. (Probably don't want this set)") + parser.add_argument('--verbose', '-v', action='count', help='Increase verbosity') + parser.add_argument('cmd', type=str, nargs='+', + help='Program and arguments. Use "--" to separate script arguments from target arguments') + args = parser.parse_args(sys.argv[1:]) + + range = None + if args.explore_from: + range = (args.explore_from, args.explore_to) + + # Create a concrete Manticore and record it + m1 = Manticore.linux(args.cmd[0], args.cmd[1:]) + t = ExtendedTracer() + r = TraceReceiver(t) + m1.verbosity(args.verbose) + m1.register_plugin(t) + m1.register_plugin(r) + m1.run(procs=1) + + time.sleep(3) + + # Create a symbolic Manticore and follow last trace + symbolic_args = ['+'*len(arg) for arg in args.cmd[1:]] + m2 = Manticore.linux(args.cmd[0], symbolic_args) + f = Follower(r.trace) + if range: + f.add_symbolic_range(*range) + m2.verbosity(args.verbose) + m2.register_plugin(f) + m2.run() + +if __name__=='__main__': + main()