diff --git a/CHANGELOG.md b/CHANGELOG.md index 59664fd..904222d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,7 +11,7 @@ The format is based on [Keep a Changelog](http://keepachangelog.com/). - Command line verbosity: `--verbose` -> `-v` (up to `-vvvv`) ### Fixed -- Linux model fixes: syscalls, ELF loading +- Linux platform fixes: syscalls, ELF loading - x86 and ARM fixes ## 0.1.0 - 2017-04-24 diff --git a/manticore/core/cpu/abstractcpu.py b/manticore/core/cpu/abstractcpu.py index 7265ce7..883eb71 100644 --- a/manticore/core/cpu/abstractcpu.py +++ b/manticore/core/cpu/abstractcpu.py @@ -294,12 +294,12 @@ class SyscallAbi(Abi): raise NotImplementedError ############################################################################ -# Abstract cpu encapsulating common cpu methods used by models and executor. +# Abstract cpu encapsulating common cpu methods used by platforms and executor. class Cpu(object): ''' Base class for all Cpu architectures. Functionality common to all architectures (and expected from users of a Cpu) should be here. Commonly - used by models and py:class:manticore.core.Executor + used by platforms and py:class:manticore.core.Executor The following attributes need to be defined in any derived class diff --git a/manticore/core/executor.py b/manticore/core/executor.py index a24a3c6..f4ee876 100644 --- a/manticore/core/executor.py +++ b/manticore/core/executor.py @@ -263,7 +263,7 @@ class Executor(object): # without loading the file later. receive_size = 0 transmit_size = 0 - for sysname, fd, data in state.model.syscall_trace: + for sysname, fd, data in state.platform.syscall_trace: if sysname in ('_receive', '_read'): receive_size += len(data) if sysname in ('_transmit', '_write'): @@ -288,14 +288,14 @@ class Executor(object): self._states[state.name] = {'received' : receive_size, 'transmited': transmit_size, - 'icount': state.model.current.icount, + 'icount': state.platform.current.icount, 'dicount': len(state.visited), 'proc': last_cpu, 'pc': last_pc, - 'syscount': len(state.model.syscall_trace), - 'smem': len(state.model.current.memory._symbols), + 'syscount': len(state.platform.syscall_trace), + 'smem': len(state.platform.current.memory._symbols), 'symbols': len(str(state.constraints)), - 'nsyscalls': len(state.model.syscall_trace), + 'nsyscalls': len(state.platform.syscall_trace), 'forks': state.forks, 'filesize':filesize, 'branches':state.branches, @@ -452,8 +452,8 @@ class Executor(object): output.write('Status:\n {}\n'.format(message)) output.write('\n') - for cpu in filter(None, state.model.procs): - idx = state.model.procs.index(cpu) + for cpu in filter(None, state.platform.procs): + idx = state.platform.procs.index(cpu) output.write("================ PROC: %02d ================\n"%idx) output.write("Memory:\n") @@ -489,11 +489,11 @@ class Executor(object): buf = solver.get_value(state.constraints, symbol) file(self._getFilename('test_%08x.txt'%test_number),'a').write("%s: %s\n"%(symbol.name, repr(buf))) - file(self._getFilename('test_%08x.syscalls'%test_number),'a').write(repr(state.model.syscall_trace)) + file(self._getFilename('test_%08x.syscalls'%test_number),'a').write(repr(state.platform.syscall_trace)) stdout = '' stderr = '' - for sysname, fd, data in state.model.syscall_trace: + for sysname, fd, data in state.platform.syscall_trace: if sysname in ('_transmit', '_write') and fd == 1: stdout += ''.join(map(str, data)) if sysname in ('_transmit', '_write') and fd == 2: @@ -505,7 +505,7 @@ class Executor(object): stdin_file = 'test_{:08x}.stdin'.format(test_number) with open(self._getFilename(stdin_file), 'wb') as f: try: - for sysname, fd, data in state.model.syscall_trace: + for sysname, fd, data in state.platform.syscall_trace: if sysname not in ('_receive', '_read') or fd != 0: continue for c in data: diff --git a/manticore/core/state.py b/manticore/core/state.py index 804eeb1..07ff3be 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -13,8 +13,8 @@ class State(object): Representation of a unique program state/path. :param ConstraintSet constraints: Initial constraints on state - :param model: Initial constraints on state - :type model: Decree or Linux or Windows + :param platform: Initial constraints on state + :type platform: Platform ''' # Class global counter @@ -28,13 +28,13 @@ class State(object): State._state_count.value += 1 return ret - def __init__(self, constraints, model): - self.model = model + def __init__(self, constraints, platform): + self.platform = platform self.forks = 0 self.co = self.get_new_id() self.constraints = constraints - self.model._constraints = constraints - for proc in self.model.procs: + self.platform._constraints = constraints + for proc in self.platform.procs: proc._constraints = constraints proc.memory._constraints = constraints @@ -46,7 +46,7 @@ class State(object): self._child = None def __reduce__(self): - return (self.__class__, (self.constraints, self.model), + return (self.__class__, (self.constraints, self.platform), {'visited': self.visited, 'last_pc': self.last_pc, 'forks': self.forks, 'co': self.co, 'input_symbols': self.input_symbols, 'branches': self.branches}) @@ -57,11 +57,11 @@ class State(object): @property def cpu(self): - return self.model.current + return self.platform.current @property def mem(self): - return self.model.current.memory + return self.platform.current.memory @property def name(self): @@ -69,7 +69,7 @@ class State(object): def __enter__(self): assert self._child is None - new_state = State(self.constraints.__enter__(), self.model) + new_state = State(self.constraints.__enter__(), self.platform) new_state.visited = set(self.visited) new_state.forks = self.forks + 1 new_state.co = State.get_new_id() @@ -83,13 +83,13 @@ class State(object): self._child = None def execute(self): - trace_item = (self.model._current, self.cpu.PC) + trace_item = (self.platform._current, self.cpu.PC) try: - result = self.model.execute() + result = self.platform.execute() except: trace_item = None raise - assert self.model.constraints is self.constraints + assert self.platform.constraints is self.constraints assert self.mem.constraints is self.constraints self.visited.add(trace_item) self.last_pc = trace_item diff --git a/manticore/manticore.py b/manticore/manticore.py index d1fa96b..ed3fd67 100644 --- a/manticore/manticore.py +++ b/manticore/manticore.py @@ -20,30 +20,30 @@ from .core.state import State, AbandonState from .core.parser import parse from .core.smtlib import solver, Expression, Operators, SolverException, Array, ConstraintSet from core.smtlib import BitVec, Bool -from .models import linux, decree, windows +from .platforms import linux, decree, windows from .utils.helpers import issymbolic logger = logging.getLogger('MANTICORE') def makeDecree(args): constraints = ConstraintSet() - model = decree.SDecree(constraints, ','.join(args.programs)) - initial_state = State(constraints, model) + platform = decree.SDecree(constraints, ','.join(args.programs)) + initial_state = State(constraints, platform) logger.info('Loading program %s', args.programs) #if args.data != '': # logger.info('Starting with concrete input: {}'.format(args.data)) - model.input.transmit(args.data) - model.input.transmit(initial_state.symbolicate_buffer('+'*14, label='RECEIVE')) + platform.input.transmit(args.data) + platform.input.transmit(initial_state.symbolicate_buffer('+'*14, label='RECEIVE')) return initial_state def makeLinux(program, argv, env, concrete_start = ''): logger.info('Loading program %s', program) constraints = ConstraintSet() - model = linux.SLinux(constraints, program, argv=argv, envp=env, + platform = linux.SLinux(constraints, program, argv=argv, envp=env, symbolic_files=('symbolic.txt')) - initial_state = State(constraints, model) + initial_state = State(constraints, platform) if concrete_start != '': logger.info('Starting with concrete input: {}'.format(concrete_start)) @@ -59,12 +59,12 @@ def makeLinux(program, argv, env, concrete_start = ''): # If any of the arguments or environment refer to symbolic values, re- # initialize the stack if any(issymbolic(x) for val in argv + env for x in val): - model.setup_stack([program] + argv, env) + platform.setup_stack([program] + argv, env) - model.input.transmit(concrete_start) + platform.input.transmit(concrete_start) #set stdin input... - model.input.transmit(initial_state.symbolicate_buffer('+'*256, label='STDIN')) + platform.input.transmit(initial_state.symbolicate_buffer('+'*256, label='STDIN')) return initial_state @@ -80,14 +80,14 @@ def makeWindows(args): logger.debug('Additional context loaded with contents {}'.format(additional_context)) #DEBUG constraints = ConstraintSet() - model = windows.SWindows(constraints, args.programs[0], additional_context, snapshot_folder=args.workspace) + platform = windows.SWindows(constraints, args.programs[0], additional_context, snapshot_folder=args.workspace) #This will interpret the buffer specification written in INTEL ASM. (It may dereference pointers) - data_size = parse(args.size, model.current.read_bytes, model.current.read_register) - data_ptr = parse(args.buffer, model.current.read_bytes, model.current.read_register) + data_size = parse(args.size, platform.current.read_bytes, platform.current.read_register) + data_ptr = parse(args.buffer, platform.current.read_bytes, platform.current.read_register) logger.debug('Buffer at %x size %d bytes)', data_ptr, data_size) - buf_str = "".join(model.current.read_bytes(data_ptr, data_size)) + buf_str = "".join(platform.current.read_bytes(data_ptr, data_size)) logger.debug('Original buffer: %s', buf_str.encode('hex')) offset = args.offset @@ -96,20 +96,20 @@ def makeWindows(args): size = min(args.maxsymb, data_size - offset - len(concrete_data)) symb = constraints.new_array(name='RAWMSG', index_max=size) - model.current.write_bytes(data_ptr + offset, concrete_data) - model.current.write_bytes(data_ptr + offset + len(concrete_data), [symb[i] for i in xrange(size)] ) + platform.current.write_bytes(data_ptr + offset, concrete_data) + platform.current.write_bytes(data_ptr + offset + len(concrete_data), [symb[i] for i in xrange(size)] ) logger.debug('First %d bytes are left concrete', offset) logger.debug('followed by %d bytes of concrete start', len(concrete_data)) - hex_head = "".join(model.current.read_bytes(data_ptr, offset+len(concrete_data))) + hex_head = "".join(platform.current.read_bytes(data_ptr, offset+len(concrete_data))) logger.debug('Hexdump head: %s', hex_head.encode('hex')) logger.debug('Total symbolic characters inserted: %d', size) logger.debug('followed by %d bytes of unmodified concrete bytes at end.', (data_size-offset-len(concrete_data))-size ) - hex_tail = "".join(map(chr, model.current.read_bytes(data_ptr+offset+len(concrete_data)+size, data_size-(offset+len(concrete_data)+size)))) + hex_tail = "".join(map(chr, platform.current.read_bytes(data_ptr+offset+len(concrete_data)+size, data_size-(offset+len(concrete_data)+size)))) logger.debug('Hexdump tail: %s', hex_tail.encode('hex')) - logger.info("Starting PC is: {:08x}".format(model.current.PC)) + logger.info("Starting PC is: {:08x}".format(platform.current.PC)) - return State(constraints, model) + return State(constraints, platform) def binary_type(path): ''' @@ -203,7 +203,7 @@ class Manticore(object): logging.basicConfig(format='%(asctime)s: [%(process)d]%(stateid)s %(name)s:%(levelname)s: %(message)s', stream=sys.stdout) - for loggername in ['VISITOR', 'EXECUTOR', 'CPU', 'REGISTERS', 'SMT', 'MEMORY', 'MAIN', 'MODEL']: + for loggername in ['VISITOR', 'EXECUTOR', 'CPU', 'REGISTERS', 'SMT', 'MEMORY', 'MAIN', 'PLATFORM']: logging.getLogger(loggername).addFilter(ctxfilter) logging.getLogger(loggername).setState = types.MethodType(loggerSetState, logging.getLogger(loggername)) @@ -273,10 +273,10 @@ class Manticore(object): def verbosity(self, setting): levels = [[], [('MAIN', logging.INFO), ('EXECUTOR', logging.INFO)], - [('MAIN', logging.INFO), ('EXECUTOR', logging.DEBUG), ('MODEL', logging.DEBUG)], - [('MAIN', logging.INFO), ('EXECUTOR', logging.DEBUG), ('MODEL', logging.DEBUG), ('MEMORY', logging.DEBUG), ('CPU', logging.DEBUG)], - [('MAIN', logging.INFO), ('EXECUTOR', logging.DEBUG), ('MODEL', logging.DEBUG), ('MEMORY', logging.DEBUG), ('CPU', logging.DEBUG), ('REGISTERS', logging.DEBUG)], - [('MAIN', logging.INFO), ('EXECUTOR', logging.DEBUG), ('MODEL', logging.DEBUG), ('MEMORY', logging.DEBUG), ('CPU', logging.DEBUG), ('REGISTERS', logging.DEBUG), ('SMT', logging.DEBUG)]] + [('MAIN', logging.INFO), ('EXECUTOR', logging.DEBUG), ('PLATFORM', logging.DEBUG)], + [('MAIN', logging.INFO), ('EXECUTOR', logging.DEBUG), ('PLATFORM', logging.DEBUG), ('MEMORY', logging.DEBUG), ('CPU', logging.DEBUG)], + [('MAIN', logging.INFO), ('EXECUTOR', logging.DEBUG), ('PLATFORM', logging.DEBUG), ('MEMORY', logging.DEBUG), ('CPU', logging.DEBUG), ('REGISTERS', logging.DEBUG)], + [('MAIN', logging.INFO), ('EXECUTOR', logging.DEBUG), ('PLATFORM', logging.DEBUG), ('MEMORY', logging.DEBUG), ('CPU', logging.DEBUG), ('REGISTERS', logging.DEBUG), ('SMT', logging.DEBUG)]] # Takes a value and ensures it's in a certain range def clamp(val, minimum, maximum): return sorted((minimum, val, maximum))[1] @@ -481,19 +481,19 @@ class Manticore(object): # event code is in place. import core.cpu import importlib - import models + import platforms with open(path, 'r') as fnames: for line in fnames.readlines(): address, cc_name, name = line.strip().split(' ') - fmodel = models + fmodel = platforms name_parts = name.split('.') - importlib.import_module(".models.{}".format(name_parts[0]), 'manticore') + importlib.import_module(".platforms.{}".format(name_parts[0]), 'manticore') for n in name_parts: fmodel = getattr(fmodel,n) - assert fmodel != models + assert fmodel != platforms def cb_function(state): - state.model.invoke_model(fmodel, prefix_args=(state.model,)) + state.platform.invoke_model(fmodel, prefix_args=(state.platform,)) self._model_hooks.setdefault(int(address,0), set()).add(cb_function) def _model_hook_callback(self, state): diff --git a/manticore/models/__init__.py b/manticore/platforms/__init__.py similarity index 100% rename from manticore/models/__init__.py rename to manticore/platforms/__init__.py diff --git a/manticore/models/cgcrandom.py b/manticore/platforms/cgcrandom.py similarity index 100% rename from manticore/models/cgcrandom.py rename to manticore/platforms/cgcrandom.py diff --git a/manticore/models/decree.py b/manticore/platforms/decree.py similarity index 99% rename from manticore/models/decree.py rename to manticore/platforms/decree.py index 9de56fc..2541d82 100644 --- a/manticore/models/decree.py +++ b/manticore/platforms/decree.py @@ -15,7 +15,7 @@ import StringIO import logging import random -logger = logging.getLogger("MODEL") +logger = logging.getLogger("PLATFORM") class SymbolicSyscallArgument(ConcretizeRegister): @@ -73,7 +73,7 @@ class Socket(object): class Decree(object): ''' - A simple Decree Operating System Model. + A simple Decree Operating System Platform. This class emulates the most common Decree system calls ''' CGC_EBADF=1 @@ -88,9 +88,9 @@ class Decree(object): def __init__(self, programs): ''' - Builds a Decree OS model - :param cpus: CPU for this model. - :param mem: memory for this model. + Builds a Decree OS platform + :param cpus: CPU for this platform. + :param mem: memory for this platform. :todo: generalize for more CPUs. :todo: fix deps? ''' @@ -909,14 +909,14 @@ class Decree(object): class SDecree(Decree): ''' - A symbolic extension of a Decree Operating System Model. + A symbolic extension of a Decree Operating System Platform. ''' def __init__(self, constraints, programs, symbolic_random=None): ''' Builds a symbolic extension of a Decree OS :param constraints: a constraint set - :param cpus: CPU for this model - :param mem: memory for this model + :param cpus: CPU for this platform + :param mem: memory for this platform ''' self._constraints = constraints self.random = 0 diff --git a/manticore/models/libc.py b/manticore/platforms/libc.py similarity index 100% rename from manticore/models/libc.py rename to manticore/platforms/libc.py diff --git a/manticore/models/linux.py b/manticore/platforms/linux.py similarity index 99% rename from manticore/models/linux.py rename to manticore/platforms/linux.py index fc37ce1..e7d5996 100644 --- a/manticore/models/linux.py +++ b/manticore/platforms/linux.py @@ -9,13 +9,13 @@ from ..core.cpu.abstractcpu import Interruption, Syscall, ConcretizeRegister from ..core.cpu.cpufactory import CpuFactory from ..core.memory import SMemory32, SMemory64, Memory32, Memory64 from ..core.smtlib import Operators, ConstraintSet -from ..models.platform import Platform +from ..platforms.platform import Platform from elftools.elf.elffile import ELFFile import logging import random from ..core.cpu.arm import * from ..core.executor import SyscallNotImplemented, ProcessExit -logger = logging.getLogger("MODEL") +logger = logging.getLogger("PLATFORM") class RestartSyscall(Exception): @@ -259,13 +259,13 @@ class Socket(object): class Linux(Platform): ''' - A simple Linux Operating System Model. + A simple Linux Operating System Platform. This class emulates the most common Linux system calls ''' def __init__(self, program, argv=None, envp=None): ''' - Builds a Linux OS model + Builds a Linux OS platform :param string program: The path to ELF binary :param list argv: The argv array; not including binary. :param list envp: The ENV variables. @@ -1828,13 +1828,13 @@ class Linux(Platform): class SLinux(Linux): ''' - A symbolic extension of a Decree Operating System Model. + A symbolic extension of a Decree Operating System Platform. ''' def __init__(self, constraints, programs, argv, envp, symbolic_random=None, symbolic_files=()): ''' Builds a symbolic extension of a Decree OS :param constraints: a constraints. - :param mem: memory for this model. + :param mem: memory for this platform. ''' self._constraints = ConstraintSet() self.random = 0 @@ -2036,12 +2036,12 @@ class DecreeEmu(object): RANDOM = 0 @staticmethod - def cgc_initialize_secret_page(model): + def cgc_initialize_secret_page(platform): logger.info("Skipping: cgc_initialize_secret_page()") return 0 @staticmethod - def cgc_random(model, buf, count, rnd_bytes): + def cgc_random(platform, buf, count, rnd_bytes): import cgcrandom if issymbolic(buf): logger.info("Ask to write random bytes to a symbolic buffer") @@ -2061,7 +2061,7 @@ class DecreeEmu(object): data.append(value) DecreeEmu.random += 1 - cpu = model.current + cpu = platform.current cpu.write(buf, data) if rnd_bytes: cpu.store(rnd_bytes, len(data), 32) diff --git a/manticore/models/platform.py b/manticore/platforms/platform.py similarity index 84% rename from manticore/models/platform.py rename to manticore/platforms/platform.py index cfafb31..38e55a8 100644 --- a/manticore/models/platform.py +++ b/manticore/platforms/platform.py @@ -4,7 +4,7 @@ import inspect class Platform(object): ''' - Base class for all operating system models. + Base class for all operating system platforms. ''' def __init__(self, path): self._path = path diff --git a/manticore/models/windows.py b/manticore/platforms/windows.py similarity index 83% rename from manticore/models/windows.py rename to manticore/platforms/windows.py index 3009ecd..01091d7 100644 --- a/manticore/models/windows.py +++ b/manticore/platforms/windows.py @@ -9,7 +9,7 @@ from ..core.cpu.abstractcpu import Interruption, Syscall, \ ConcretizeRegister, ConcretizeArgument, IgnoreAPI from ..core.executor import ForkState, SyscallNotImplemented from ..utils.helpers import issymbolic -from ..models.platform import Platform +from ..platforms.platform import Platform from ..binary.pe import minidump @@ -18,7 +18,7 @@ import StringIO import logging import random from windows_syscalls import syscalls_num -logger = logging.getLogger("MODEL") +logger = logging.getLogger("PLATFORM") class ProcessExit(Exception): def __init__(self, code): @@ -50,7 +50,7 @@ def toStr(state, value): class Windows(Platform): ''' - A simple Windows Operating System Model. + A simple Windows Operating System Platform. This class emulates some Windows system calls ''' @@ -69,7 +69,7 @@ class Windows(Platform): def __init__(self, path, additional_context = None, snapshot_folder=None): ''' - Builds a Windows OS model + Builds a Windows OS platform ''' super(Windows, self).__init__(path) @@ -92,7 +92,7 @@ class Windows(Platform): self.flavor = "Windows10SP%d"%minor else: raise NotImplementedError("Windows version {}.{} not supported".format(major, minor)) - logger.info('Initializing %s model', self.flavor) + logger.info('Initializing %s platform', self.flavor) # Setting up memory maps memory = self._mk_memory() @@ -432,7 +432,7 @@ class Windows(Platform): class SWindows(Windows): ''' - A symbolic extension of a Decree Operating System Model. + A symbolic extension of a Decree Operating System Platform. ''' def __init__(self, constraints, path, additional_context=None, snapshot_folder=None): ''' @@ -516,23 +516,23 @@ def readStringFromPointer(state, cpu, ptr, utf16, max_symbols=8): class ntdll(object): @staticmethod - def NtWriteFile(model, FileHandle, Event, ApcRoutine, ApcContext, IoStatusBlock, Buffer, Length, ByteOffset, Key): - return model.NtWriteFile(FileHandle, Event, ApcRoutine, ApcContext, IoStatusBlock, Buffer, Length, ByteOffset, Key) + def NtWriteFile(platform, FileHandle, Event, ApcRoutine, ApcContext, IoStatusBlock, Buffer, Length, ByteOffset, Key): + return platform.NtWriteFile(FileHandle, Event, ApcRoutine, ApcContext, IoStatusBlock, Buffer, Length, ByteOffset, Key) @staticmethod - def NtReleaseKeyedEvent(model, KeyedEventHandle, Key, Alertable, Timeout): - return model.NtReleaseKeyedEvent(KeyedEventHandle, Key, Alertable, Timeout) + def NtReleaseKeyedEvent(platform, KeyedEventHandle, Key, Alertable, Timeout): + return platform.NtReleaseKeyedEvent(KeyedEventHandle, Key, Alertable, Timeout) @staticmethod - def NtQueryPerformanceCounter(model, PerformanceCounter, PerformanceFrequency): - return model.NtQueryPerformanceCounter(PerformanceCounter, PerformanceFrequency) + def NtQueryPerformanceCounter(platform, PerformanceCounter, PerformanceFrequency): + return platform.NtQueryPerformanceCounter(PerformanceCounter, PerformanceFrequency) @staticmethod - def NtClose(model, Handle): - return model.NtClose(Handle) + def NtClose(platform, Handle): + return platform.NtClose(Handle) @staticmethod - def RtlAllocateHeap(model, handle, flags, size): + def RtlAllocateHeap(platform, handle, flags, size): if issymbolic(size): logger.info("RtlAllcoateHeap({}, {}, SymbolicSize); concretizing size".format(str(handle), str(flags)) ) raise ConcretizeArgument(2) @@ -540,26 +540,26 @@ class ntdll(object): raise IgnoreAPI("RtlAllocateHeap({}, {}, {:08x})".format(str(handle), str(flags), size)) @staticmethod - def RtlpReportHeapFailure(model): + def RtlpReportHeapFailure(platform): raise MemoryException("Heap Failure Detected via RtlpReportHeapFailure!", 0xFFFFFFFF) @staticmethod - def RtlpLogHeapFailure(model): + def RtlpLogHeapFailure(platform): raise MemoryException("Heap Failure Detected via RtlpLogHeapFailure!", 0xFFFFFFFE) class kernel32(object): @staticmethod - def RegOpenKeyExW(model, hKey, lpSubKey, ulOptions, samDesired, phkResult): - return kernel32._RegOpenKeyEx(model, True, hKey, lpSubKey, ulOptions, samDesired, phkResult) + def RegOpenKeyExW(platform, hKey, lpSubKey, ulOptions, samDesired, phkResult): + return kernel32._RegOpenKeyEx(platform, True, hKey, lpSubKey, ulOptions, samDesired, phkResult) @staticmethod - def RegOpenKeyExA(model, hKey, lpSubKey, ulOptions, samDesired, phkResult): - return kernel32._RegOpenKeyEx(model, False, hKey, lpSubKey, ulOptions, samDesired, phkResult) + def RegOpenKeyExA(platform, hKey, lpSubKey, ulOptions, samDesired, phkResult): + return kernel32._RegOpenKeyEx(platform, False, hKey, lpSubKey, ulOptions, samDesired, phkResult) @staticmethod - def _RegOpenKeyEx(model, utf16, hKey, lpSubKey, ulOptions, samDesired, phkResult): + def _RegOpenKeyEx(platform, utf16, hKey, lpSubKey, ulOptions, samDesired, phkResult): """LONG WINAPI RegOpenKeyEx( _In_ HKEY hKey, _In_opt_ LPCTSTR lpSubKey, @@ -569,11 +569,11 @@ class kernel32(object): ); Detect symbolic registry access. Attempt to simulate fake registry opening """ - cpu = model.current + cpu = platform.current myname = "RegOpenKeyEx{}".format(utf16 and "W" or "A") try: - key_str = readStringFromPointer(model, cpu, lpSubKey, utf16) + key_str = readStringFromPointer(platform, cpu, lpSubKey, utf16) except MemoryException as me: raise MemoryException("{}: {}".format(myname, me.cause), 0xFFFFFFFF) except SymbolicAPIArgument: @@ -587,20 +587,20 @@ class kernel32(object): if issymbolic(phkResult): #Check if the symbol has a single solution. - values = solver.get_all_values(model.constraints, phkResult, maxcnt=2, silent=True) + values = solver.get_all_values(platform.constraints, phkResult, maxcnt=2, silent=True) if len(values) == 1: phkResult = values[0] if issymbolic(phkResult): - if solver.can_be_true(model.constraints, phkResult==0): + if solver.can_be_true(platform.constraints, phkResult==0): raise ForkState(phkResult==0) else: - cpu.write_int(phkResult, model._getRegHandle(key_str), 32) + cpu.write_int(phkResult, platform._getRegHandle(key_str), 32) return 0 elif phkResult != 0: - cpu.write_int(phkResult, model._getRegHandle(key_str), 32) + cpu.write_int(phkResult, platform._getRegHandle(key_str), 32) return 0 else: raise IgnoreAPI("{}({}, [{}], {}, {}, {})".format(myname, @@ -608,19 +608,19 @@ class kernel32(object): str(phkResult))) @staticmethod - def RegCreateKeyExW(model, hkey, lpSubKey, Reserved, lpClass, dwOptions, + def RegCreateKeyExW(platform, hkey, lpSubKey, Reserved, lpClass, dwOptions, samDesired, lpSecurityAttributes, phkResult, lpdwDisposition): - return kernel32._RegCreateKeyEx(model, True, hkey, lpSubKey, Reserved, lpClass, dwOptions, + return kernel32._RegCreateKeyEx(platform, True, hkey, lpSubKey, Reserved, lpClass, dwOptions, samDesired, lpSecurityAttributes, phkResult, lpdwDisposition) @staticmethod - def RegCreateKeyExA(model, hkey, lpSubKey, Reserved, lpClass, dwOptions, + def RegCreateKeyExA(platform, hkey, lpSubKey, Reserved, lpClass, dwOptions, samDesired, lpSecurityAttributes, phkResult, lpdwDisposition): - return kernel32._RegCreateKeyEx(model, False, hkey, lpSubKey, Reserved, lpClass, dwOptions, + return kernel32._RegCreateKeyEx(platform, False, hkey, lpSubKey, Reserved, lpClass, dwOptions, samDesired, lpSecurityAttributes, phkResult, lpdwDisposition) @staticmethod - def _RegCreateKeyEx(model, utf16, hKey, lpSubKey, Reserved, lpClass, dwOptions, + def _RegCreateKeyEx(platform, utf16, hKey, lpSubKey, Reserved, lpClass, dwOptions, samDesired, lpSecurityAttributes, phkResult, lpdwDisposition): """ LONG WINAPI RegCreateKeyEx( _In_ HKEY hKey, @@ -633,11 +633,11 @@ class kernel32(object): _Out_ PHKEY phkResult, _Out_opt_ LPDWORD lpdwDisposition );""" - cpu = model.current + cpu = platform.current myname = "RegCreateKeyEx{}".format(utf16 and "W" or "A") try: - key_str = readStringFromPointer(model, cpu, lpSubKey, utf16) + key_str = readStringFromPointer(platform, cpu, lpSubKey, utf16) except MemoryException as me: raise MemoryException("{}: {}".format(myname, me.cause), 0xFFFFFFFF) except SymbolicAPIArgument: @@ -650,20 +650,20 @@ class kernel32(object): if issymbolic(phkResult): #Check if the symbol has a single solution. - values = solver.get_all_values(model.constraints, phkResult, maxcnt=2, silent=True) + values = solver.get_all_values(platform.constraints, phkResult, maxcnt=2, silent=True) if len(values) == 1: phkResult = values[0] if issymbolic(phkResult): - if solver.can_be_true(model.constraints, phkResult==0): + if solver.can_be_true(platform.constraints, phkResult==0): raise ForkState(phkResult==0) else: - cpu.write_int(phkResult, model._getRegHandle(key_str), 32) + cpu.write_int(phkResult, platform._getRegHandle(key_str), 32) return 0 elif phkResult != 0: - cpu.write_int(phkResult, model._getRegHandle(key_str), 32) + cpu.write_int(phkResult, platform._getRegHandle(key_str), 32) return 0 else: raise IgnoreAPI("{}({}, [{}], {}, {}, {}, {}, {}, {}, {})".format(myname, @@ -671,13 +671,13 @@ class kernel32(object): str(lpSecurityAttributes), str(samDesired), str(phkResult), str(lpdwDisposition))) @staticmethod - def HeapAlloc(model, handle, flags, size): - ntdll.RtlAllocateHeap(model, handle, flags, size) + def HeapAlloc(platform, handle, flags, size): + ntdll.RtlAllocateHeap(platform, handle, flags, size) # TODO: move this to Windows class if we ever # implement a real handle table @staticmethod - def GetStdHandle(model, nStdHandle): + def GetStdHandle(platform, nStdHandle): logger.info("GetStdHandle(%x)", nStdHandle) # ignore nStdHandle -- just return a valid value STD_INPUT_HANDLE = -10 @@ -687,7 +687,7 @@ class kernel32(object): if issymbolic(nStdHandle): #Check if the symbol has a single solution. - values = solver.get_all_values(model.constraints, nStdHandle, maxcnt=2, silent=True) + values = solver.get_all_values(platform.constraints, nStdHandle, maxcnt=2, silent=True) if len(values) == 1: nStdHandle = values[0] else: @@ -714,29 +714,29 @@ class kernel32(object): return -1 #INVALID_HANDLE_VALUE @staticmethod - def CloseHandle(model, hObject): + def CloseHandle(platform, hObject): logger.info("CloseHandle(%x)", hObject) - if model.NT_SUCCESS(model.NtClose(hObject)): + if platform.NT_SUCCESS(platform.NtClose(hObject)): return 1 else: return 0 # TODO: possibly implement using NtCreateFile and/or use a handle table @staticmethod - def CreateFileW(model, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile): - return kernel32._CreateFile(model, True, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile) + def CreateFileW(platform, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile): + return kernel32._CreateFile(platform, True, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile) @staticmethod - def CreateFileA(model, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile): - return kernel32._CreateFile(model, False, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile) + def CreateFileA(platform, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile): + return kernel32._CreateFile(platform, False, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile) @staticmethod - def _CreateFile(model, utf16, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile): + def _CreateFile(platform, utf16, lpFileName, dwDesiredAccess, dwShareMode, lpSecurityAttributes, dwCreationDisposition, dwFlagsAndAttributes, hTemplateFile): '''https://msdn.microsoft.com/en-us/library/windows/desktop/aa363858(v=vs.85).aspx''' - cpu = model.current + cpu = platform.current try: - filename = readStringFromPointer(model, cpu, lpFileName, utf16) + filename = readStringFromPointer(platform, cpu, lpFileName, utf16) except MemoryException as me: msg = "CreateFile{}: {}".format(utf16 and "W" or "A", me.cause) raise MemoryException(msg, 0xFFFFFFFF) @@ -754,20 +754,20 @@ class kernel32(object): _In_opt_ HANDLE hTemplateFile: %s );""" % (utf16 and "W" or "A", filename, - toStr(model, dwDesiredAccess), - toStr(model, dwShareMode), - toStr(model, lpSecurityAttributes), - toStr(model, dwCreationDisposition), - toStr(model, dwFlagsAndAttributes), - toStr(model, hTemplateFile),)) + toStr(platform, dwDesiredAccess), + toStr(platform, dwShareMode), + toStr(platform, lpSecurityAttributes), + toStr(platform, dwCreationDisposition), + toStr(platform, dwFlagsAndAttributes), + toStr(platform, hTemplateFile),)) - cpu = model.current + cpu = platform.current - return model._fileHandle(lpFileName) + return platform._fileHandle(lpFileName) #TODO possibly implement via NtWriteFile @staticmethod - def WriteFile(model, hFile, lpBuffer, nNumberOfBytesToWrite, lpNumberOfBytesWritten, lpOverlapped): + def WriteFile(platform, hFile, lpBuffer, nNumberOfBytesToWrite, lpNumberOfBytesWritten, lpOverlapped): '''https://msdn.microsoft.com/en-us/library/windows/desktop/aa365747(v=vs.85).aspx''' logger.info("""WriteFile( _In_ HANDLE hFile: %s, @@ -776,25 +776,25 @@ class kernel32(object): _Out_opt_ LPDWORD lpNumberOfBytesWritten: %s, _Inout_opt_ LPOVERLAPPED lpOverlapped: %s );"""%( - toStr(model, hFile), - toStr(model, lpBuffer), - toStr(model, nNumberOfBytesToWrite), - toStr(model, lpNumberOfBytesWritten), - toStr(model, lpOverlapped)) + toStr(platform, hFile), + toStr(platform, lpBuffer), + toStr(platform, nNumberOfBytesToWrite), + toStr(platform, lpNumberOfBytesWritten), + toStr(platform, lpOverlapped)) ) if issymbolic(lpNumberOfBytesWritten): #Check if the symbol has a single solution. - values = solver.get_all_values(model.constraints, lpNumberOfBytesWritten, maxcnt=2, silent=True) + values = solver.get_all_values(platform.constraints, lpNumberOfBytesWritten, maxcnt=2, silent=True) if len(values) == 1: logger.info("ONE VALUE lpNumberOfBytesWritten: {}".format(lpNumberOfBytesWritten)) lpNumberOfBytesWritten = values[0] - cpu = model.current + cpu = platform.current if issymbolic(lpNumberOfBytesWritten): - if solver.can_be_true(model.constraints, lpNumberOfBytesWritten==0): + if solver.can_be_true(platform.constraints, lpNumberOfBytesWritten==0): raise ForkState(lpNumberOfBytesWritten==0) logger.info("WRITING TO SYMB lpNumberOfBytesWritten: {}".format(lpNumberOfBytesWritten)) @@ -806,23 +806,23 @@ class kernel32(object): return 1 @staticmethod - def CreateProcessW(model, lpApplicationName, lpCommandLine, lpProcessAttributes, + def CreateProcessW(platform, lpApplicationName, lpCommandLine, lpProcessAttributes, lpThreadAttributes, bInheritHandles, dwCreationFlags, lpEnvironment, lpCurrentDirectory, lpStartupInfo, lpProcessInformation): - return kernel32._CreateProcess(model, True, lpApplicationName, lpCommandLine, lpProcessAttributes, + return kernel32._CreateProcess(platform, True, lpApplicationName, lpCommandLine, lpProcessAttributes, lpThreadAttributes, bInheritHandles, dwCreationFlags, lpEnvironment, lpCurrentDirectory, lpStartupInfo, lpProcessInformation) @staticmethod - def CreateProcessA(model, lpApplicationName, lpCommandLine, lpProcessAttributes, + def CreateProcessA(platform, lpApplicationName, lpCommandLine, lpProcessAttributes, lpThreadAttributes, bInheritHandles, dwCreationFlags, lpEnvironment, lpCurrentDirectory, lpStartupInfo, lpProcessInformation): - return kernel32._CreateProcess(model, False, lpApplicationName, lpCommandLine, lpProcessAttributes, + return kernel32._CreateProcess(platform, False, lpApplicationName, lpCommandLine, lpProcessAttributes, lpThreadAttributes, bInheritHandles, dwCreationFlags, lpEnvironment, lpCurrentDirectory, lpStartupInfo, lpProcessInformation) @staticmethod - def _CreateProcess(model, utf16, lpApplicationName, lpCommandLine, lpProcessAttributes, + def _CreateProcess(platform, utf16, lpApplicationName, lpCommandLine, lpProcessAttributes, lpThreadAttributes, bInheritHandles, dwCreationFlags, lpEnvironment, lpCurrentDirectory, lpStartupInfo, lpProcessInformation): """BOOL WINAPI CreateProcess( @@ -839,10 +839,10 @@ class kernel32(object): );""" myname = "CreateProcess{}".format(utf16 and "W" or "A") - cpu = model.current + cpu = platform.current try: - appname = readStringFromPointer(model, cpu, lpApplicationName, utf16) + appname = readStringFromPointer(platform, cpu, lpApplicationName, utf16) except MemoryException as me: msg = "{}: {}".format(myname, me.cause) raise MemoryException(msg, 0xFFFFFFFF) @@ -850,7 +850,7 @@ class kernel32(object): raise ConcretizeArgument(0) try: - cmdline = readStringFromPointer(model, cpu, lpCommandLine, utf16) + cmdline = readStringFromPointer(platform, cpu, lpCommandLine, utf16) except MemoryException as me: msg = "{}: {}".format(myname, me.cause) raise MemoryException(msg, 0xFFFFFFFF) diff --git a/manticore/models/windows_syscalls.py b/manticore/platforms/windows_syscalls.py similarity index 100% rename from manticore/models/windows_syscalls.py rename to manticore/platforms/windows_syscalls.py diff --git a/tests/test_linux.py b/tests/test_linux.py index f87c6c6..d6ed8ca 100644 --- a/tests/test_linux.py +++ b/tests/test_linux.py @@ -1,6 +1,6 @@ import unittest -from manticore.models import linux +from manticore.platforms import linux class LinuxTest(unittest.TestCase): diff --git a/tests/test_state.py b/tests/test_state.py index fe018e9..b638563 100644 --- a/tests/test_state.py +++ b/tests/test_state.py @@ -3,7 +3,7 @@ import unittest from manticore.core.executor import State from manticore.core.smtlib import BitVecVariable from manticore.core.smtlib import ConstraintSet -from manticore.models import linux +from manticore.platforms import linux class FakeMemory(object): def __init__(self): @@ -21,7 +21,7 @@ class FakeCpu(object): def memory(self): return self._memory -class FakeModel(object): +class FakePlatform(object): def __init__(self): self._constraints = None self.procs = [FakeCpu()] @@ -71,7 +71,7 @@ class StateTest(unittest.TestCase): def test_state(self): constraints = ConstraintSet() - initial_state = State(constraints, FakeModel()) + initial_state = State(constraints, FakePlatform()) arr = initial_state.symbolicate_buffer('+'*100, label='SYMBA') initial_state.constrain(arr[0] > 0x41) diff --git a/tests/test_unicorn.py b/tests/test_unicorn.py index c5691e1..3cdad35 100644 --- a/tests/test_unicorn.py +++ b/tests/test_unicorn.py @@ -7,7 +7,7 @@ from manticore.core.cpu.abstractcpu import ConcretizeMemory, ConcretizeRegister from manticore.core.memory import Memory32, SMemory32 from manticore.core.executor import State from manticore.core.smtlib import BitVecVariable, ConstraintSet -from manticore.models import linux +from manticore.platforms import linux from manticore.utils.emulate import UnicornEmulator from capstone.arm import * @@ -1317,9 +1317,9 @@ class UnicornConcretization(unittest.TestCase): def get_state(cls): if cls.cpu is None: constraints = ConstraintSet() - model = linux.SLinux(constraints, '/bin/ls', argv=[], envp=[]) - cls.state = State(constraints, model) - cls.cpu = model._mk_proc('armv7') + platform = linux.SLinux(constraints, '/bin/ls', argv=[], envp=[]) + cls.state = State(constraints, platform) + cls.cpu = platform._mk_proc('armv7') return (cls.cpu, cls.state)