DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

Rename os model terminology from "models" to "platforms" (#243)

Browse Source 
* Rename

* rename in manticore.py

* rename in executor.py

* big rename

* big rename

* update changelog
This commit is contained in:
Mark Mossberg
2017-05-09 19:25:32 -04:00
committed by GitHub
parent b8991e0c64
commit e4a4916597
16 changed files with 159 additions and 159 deletions
Download Patch File Download Diff File Expand all files Collapse all files
CHANGELOG.md
+1 -1
View File
@@ -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
manticore/core/cpu/abstractcpu.py
+2 -2
View File
@@ -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
manticore/core/executor.py
+10 -10
View File
@@ -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:
manticore/core/state.py
+13 -13
View File
@@ -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
manticore/manticore.py
+30 -30
View File
@@ -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):
manticore/models/__init__.py → manticore/platforms/__init__.py
View File
manticore/models/cgcrandom.py → manticore/platforms/cgcrandom.py
View File
manticore/models/decree.py → manticore/platforms/decree.py
+8 -8
View File
@@ -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
manticore/models/libc.py → manticore/platforms/libc.py
View File
manticore/models/linux.py → manticore/platforms/linux.py
+9 -9
View File
@@ -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)
manticore/models/platform.py → manticore/platforms/platform.py
+1 -1
View File
@@ -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
manticore/models/windows.py → manticore/platforms/windows.py
+77 -77
View File
@@ -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)
manticore/models/windows_syscalls.py → manticore/platforms/windows_syscalls.py
View File
tests/test_linux.py
+1 -1
View File
@@ -1,6 +1,6 @@
import unittest
from manticore.models import linux
from manticore.platforms import linux
class LinuxTest(unittest.TestCase):
tests/test_state.py
+3 -3
View File
@@ -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)
tests/test_unicorn.py
+4 -4
View File
@@ -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)