DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

Refactor platform details out from Manticore (#421)

Browse Source 
* WIP New Policy class

* WIP pubsub

* Update Signal tests

* small fixes from github comments

* Fix event decode_instruction signature

* Good merge

* Good good merge

* WIP manticore refactor

* Fix default old-style initial state

* add -> enqueue

* @m.init

* Fix workspace url

* Some test skipped

* Ad Fixme to platform specific stuff in State

* add -> enqueue

* Enqueue created state

* Fix m.init

Use a messy hack to adhere to the spec (callback func receive 1 state argument)

* Add _coverage_file ivar to Manticore

* Fix symbolic files

* remove extra enqueue

* Fixing __main__

* comments

* Refactor CLI, and Manticore high level interfaces (#498)

* Refactor main,

- classmethod for linux
- refactor manticore ctor - compat with old linux behavior
- changed verbosity API (to allow for this use case: what if you want to set verbosity for the stuff manticore does in its ctor?)

* rm old verbosity

* small

* Add decree classmethod

* Rm checks ; they are redundant anyway

* Misc

* Move add_symbolic_file to linux platform

* rm redundant checks

* Rm explicit args for deprecated interface

* Fix cli bug

* Allow for both linux and decree from cli

* Add back argv positional param for deprecated api compat
This commit is contained in:
feliam
2017-09-13 18:37:42 -03:00
committed by GitHub
parent f6fea10376
commit 23c2585316
7 changed files with 333 additions and 468 deletions
Download Patch File Download Diff File Expand all files Collapse all files
manticore/__main__.py
+12 -45
View File
@@ -1,8 +1,7 @@
import sys
import argparse
import logging
from manticore import Manticore
from manticore import Manticore, log, make_initial_state
sys.setrecursionlimit(10000)
@@ -24,20 +23,10 @@ def parse_arguments():
disas = ['capstone', 'binja-il']
parser.add_argument('--disasm', type=str, default='capstone', choices=disas,
help=argparse.SUPPRESS)
parser.add_argument('--dumpafter', type=int, default=0,
help='Dump state after every N instructions; 0 to disable')
parser.add_argument('--env', type=str, nargs=1, default=[], action='append',
help='Specify symbolic environment variable VARNAME=++++++')
parser.add_argument('--errorfile', type=str, default=None,
help='where to write the memory error locations')
parser.add_argument('--file', type=str, action='append', dest='files',
parser.add_argument('--file', type=str, default=[], action='append', dest='files',
help='Specify symbolic input file, \'+\' marks symbolic bytes')
parser.add_argument('--maxstorage', type=int, default=0,
help='Storage use cap in megabytes.')
parser.add_argument('--maxstates', type=int, default=0,
help='Maximun number of states to mantain at the same time')
parser.add_argument('--maxsymb', type=int, default=512,
help='Maximun number of symbolic bytes to inject')
parser.add_argument('--names', type=str, default=None,
help=("File with function addresses to replace "
"with known models"))
@@ -79,51 +68,29 @@ def parse_arguments():
def main():
args = parse_arguments()
m = Manticore(args.argv[0], args.argv[1:], disasm=args.disasm)
m.policy = args.policy
m.args = args
if args.data:
m.concrete_data = args.data
env = {key:val for key, val in map(lambda env: env[0].split('='), args.env)}
if args.workspace:
m.workspace = args.workspace
Manticore.verbosity(args.v)
if args.profile:
m.should_profile = args.profile
m = Manticore(args.argv[0], argv=args.argv[1:], env=env, workspace_url=args.workspace, policy=args.policy, disasm=args.disasm)
if args.dumpafter != 0:
m.dumpafter = args.dumpafter
if args.maxstorage != 0:
m.maxstorage = args.maxstorage
if args.maxstates != 0:
m.maxstates = args.maxstates
if args.coverage:
m.coverage_file = args.coverage
#Fixme(felipe) remove this, move to plugin
m.coverage_file = args.coverage
if args.names is not None:
m.apply_model_hooks(args.names)
if args.env:
for entry in args.env:
name, val = entry[0].split('=')
m.env_add(name, val)
if args.files:
for file in args.files:
m.add_symbolic_file(file)
if args.assertions:
m.load_assertions(args.assertions)
m.verbosity = args.v
@m.init
def init(initial_state):
for file in args.files:
initial_state.platform.add_symbolic_file(file)
m.run(args.procs, args.timeout)
#m.dump_stats()
m.run(procs=args.procs, timeout=args.timeout, should_profile=args.profile)
if __name__ == '__main__':
main()
manticore/core/executor.py
+11 -7
View File
@@ -203,6 +203,9 @@ class Executor(Eventful):
if self.load_workspace():
if initial is not None:
logger.error("Ignoring initial state")
else:
if initial is not None:
self.add(initial)
@contextmanager
def locked_context(self, key=None, default=dict):
@@ -270,12 +273,12 @@ class Executor(Eventful):
###############################################
# Synchronization helpers
@sync
def _start_run(self):
def _notify_start_run(self):
#notify siblings we are about to start a run()
self._running.value += 1
@sync
def _stop_run(self):
def _notify_stop_run(self):
#notify siblings we are about to stop this run()
self._running.value -= 1
if self._running.value < 0:
@@ -415,7 +418,7 @@ class Executor(Eventful):
with WithKeyboardInterruptAs(self.shutdown):
#notify siblings we are about to start a run
self._start_run()
self._notify_start_run()
logger.debug("Starting Manticore Symbolic Emulator Worker (pid %d).",os.getpid())
@@ -426,7 +429,7 @@ class Executor(Eventful):
if current_state is None:
with self._lock:
#notify siblings we are about to stop this run
self._stop_run()
self._notify_stop_run()
#Select a single state_id
current_state_id = self.get()
#load selected state from secondary storage
@@ -435,8 +438,8 @@ class Executor(Eventful):
self.forward_events_from(current_state, True)
logger.info("load state %r", current_state_id)
self.publish('will_load_state', current_state, current_state_id)
#notify siblings we have a state to play with
self._start_run()
#notify siblings we have a state to play with
self._notify_start_run()
#If current_state is still None. We are done.
if current_state is None:
@@ -491,6 +494,7 @@ class Executor(Eventful):
except (Exception, AssertionError) as e:
import traceback
trace = traceback.format_exc()
print str(e), trace
logger.error("Exception: %s\n%s", str(e), trace)
#Notify this worker is done
self.publish('will_terminate_state', current_state, current_state_id, 'Exception')
@@ -500,7 +504,7 @@ class Executor(Eventful):
assert current_state is None
#notify siblings we are about to stop this run
self._stop_run()
self._notify_stop_run()
#Notify this worker is done (not sure it's needed)
self.publish('will_finish_run')
manticore/core/state.py
+10 -8
View File
@@ -81,14 +81,6 @@ class State(Eventful):
# Events are lost in serialization and fork !!
self.forward_events_from(platform)
def record_branch(self, target):
branches = self.context['branches']
branch = (self.cpu._last_pc, target)
if branch in branches:
branches[branch] += 1
else:
branches[branch] = 1
def __getstate__(self):
state = super(State, self).__getstate__()
state['platform'] = self._platform
@@ -362,9 +354,19 @@ class State(Eventful):
def mem(self):
return self._platform.current.memory
#FIXME(felipe) Remove this
def _init_context(self):
self.context['branches'] = dict()
#FIXME(felipe) Remove this
def record_branch(self, target):
branches = self.context['branches']
branch = (self.cpu._last_pc, target)
if branch in branches:
branches[branch] += 1
else:
branches[branch] = 1
def generate_testcase(self, name, message='State generated testcase'):
"""
Generate a testcase for this state and place in the analysis workspace.
manticore/manticore.py
+284 -406
View File
@@ -2,7 +2,6 @@ import os
import sys
import time
import types
import logging
import binascii
import functools
import cProfile
@@ -13,6 +12,7 @@ from contextlib import contextmanager
from threading import Timer
import elftools
from elftools.elf.elffile import ELFFile
from elftools.elf.sections import SymbolTableSection
@@ -24,11 +24,24 @@ from .core.workspace import ManticoreOutput, Workspace
from .platforms import linux, decree, windows
from .utils.helpers import issymbolic, is_binja_disassembler
from .utils.nointerrupt import WithKeyboardInterruptAs
import logging
from .utils import log
log.init_logging()
logger = logging.getLogger('MANTICORE')
def makeBinja(program, disasm, argv, env, symbolic_files, concrete_start=''):
def make_binja(program, disasm, argv, env, symbolic_files, concrete_start=''):
def _check_disassembler_present(disasm):
if is_binja_disassembler(disasm):
try:
import binaryninja
except ImportError:
err = ("BinaryNinja not found! You MUST own a BinaryNinja version"
" that supports GUI-less processing for this option"
" to work. Please configure your PYTHONPATH appropriately or"
" select a different disassembler")
raise SystemExit(err)
_check_disassembler_present(disasm)
constraints = ConstraintSet()
logger.info('Loading binary ninja IL from %s', program)
platform = linux.SLinux(program,
@@ -39,7 +52,8 @@ def makeBinja(program, disasm, argv, env, symbolic_files, concrete_start=''):
initial_state = State(constraints, platform)
return initial_state
def makeDecree(program, concrete_data=''):
def make_decree(program, concrete_data='', **kwargs):
constraints = ConstraintSet()
platform = decree.SDecree(constraints, program)
initial_state = State(constraints, platform)
@@ -51,16 +65,17 @@ def makeDecree(program, concrete_data=''):
platform.input.transmit(initial_state.symbolicate_buffer('+'*14, label='RECEIVE'))
return initial_state
def makeLinux(program, disasm, argv, env, symbolic_files, concrete_start=''):
logger.info('Loading program %s (platform: Linux)', program)
def make_linux(program, argv=None, env=None, symbolic_files=None, concrete_start = ''):
env = {} if env is None else env
argv = [] if argv is None else argv
env = ['%s=%s'%(k,v) for k,v in env.items()]
logger.info('Loading program %s', program)
constraints = ConstraintSet()
platform = linux.SLinux(program, argv=argv, envp=env,
symbolic_files=symbolic_files)
platform = linux.SLinux(program,
argv=argv,
envp=env,
symbolic_files=symbolic_files,
disasm=disasm)
initial_state = State(constraints, platform)
if concrete_start != '':
@@ -82,11 +97,10 @@ def makeLinux(program, disasm, argv, env, symbolic_files, concrete_start=''):
#set stdin input...
platform.input.write(initial_state.symbolicate_buffer('+' * 256,
label='STDIN'))
return initial_state
def makeWindows(args):
def make_windows(args, programs, context, data, offset, maxsymb, workspace, size=None, buffer=None, **kwargs):
assert args.size is not None, "Need to specify buffer size"
assert args.buffer is not None, "Need to specify buffer base address"
logger.debug('Loading program %s (platform: Windows)', args.argv)
@@ -128,82 +142,54 @@ def makeWindows(args):
return State(constraints, platform)
def binary_type(path):
'''
Given a path to a binary, return a string representation of its type.
i.e. ELF, PE, DECREE, QNX
'''
magic = None
with open(path) as f:
magic = f.read(4)
def make_initial_state(binary_path, **kwargs):
if 'disasm' in kwargs:
if kwargs.get('disasm') == "binja-il":
return make_binja(binary_path, **kwargs)
else:
del kwargs['disasm']
magic = file(binary_path).read(4)
if magic == '\x7fELF':
return 'ELF'
elif magic == 'MDMP':
return 'PE'
# Linux
state = make_linux(binary_path, **kwargs)
elif magic == '\x7fCGC':
return 'DECREE'
# Decree
state = make_decree(binary_path, **kwargs)
else:
raise NotImplementedError("Binary {} not supported. Magic bytes: 0x{}".format(path, binascii.hexlify(magic)))
raise NotImplementedError("Binary {} not supported.".format(binary_path))
return state
class Manticore(object):
'''
The central analysis object.
:param path_or_state: Path to a binary to analyze or `State` object
:param path_or_state: Path to a binary to analyze (deprecated) or `State` object
:type path_or_state: str or State
:param args: Arguments to provide to binary
:type args: list[str]
:param argv: Arguments to provide to binary (deprecated)
:type argv: list[str]
:ivar dict context: Global context for arbitrary data storage
'''
def __init__(self, path_or_state, args=None, disasm='capstone'):
args = [] if args is None else args
def __init__(self, path_or_state, argv=None, workspace_url=None, policy='random', **kwargs):
if isinstance(path_or_state, str):
assert os.path.isfile(path_or_state)
self._binary = path_or_state
self._initial_state_type = binary_type(self._binary)
if isinstance(workspace_url, str):
if ':' not in workspace_url:
ws_path = 'fs:' + workspace_url
else:
ws_path = workspace_url
else:
assert isinstance(path_or_state, State), "Manticore must be intialized with either a state or a path to a binary"
self._binary = None
self._initial_state_type = 'MCORE'
self._check_disassembler_present(disasm)
self._disasm = disasm
# yan's comment
self._argv = args
self._env = {}
# Will be set to a temporary directory if not set before running start()
self._policy = 'random'
ws_path = None
self._output = ManticoreOutput(ws_path)
self._context = {}
self._coverage_file = None
self._memory_errors = None
self._should_profile = False
self._workers = []
# XXX(yan) '_args' will be removed soon; exists currently to ease porting
self._args = args
self._time_started = 0
self._begun_trace = False
self._assertions = {}
self._model_hooks = {}
#sugar for 'will_execute_instruction"
self._hooks = {}
self._running = False
self._arch = None
self._concrete_data = ''
self._dumpafter = 0
self._maxstates = 0
self._maxstorage = 0
self._workspace = getattr(args, 'workspace', None)
self._symbolic_files = [] # list of string
if isinstance(self._workspace, str):
if ':' not in self._workspace:
self._workspace = 'fs:' + self._workspace
self._output = ManticoreOutput(self._workspace)
self._executor = Executor(workspace=self._output.descriptor)
self._symbolic_files = []
self._executor = Executor(workspace=ws_path, policy=policy)
self._workers = []
#Link Executor events to default callbacks in manticore object
self._executor.subscribe('did_read_register', self._read_register_callback)
self._executor.subscribe('will_write_register', self._write_register_callback)
@@ -215,21 +201,42 @@ class Manticore(object):
self._executor.subscribe('forking_state', self._forking_state_callback)
self._executor.subscribe('will_terminate_state', self._terminate_state_callback)
self._executor.subscribe('will_generate_testcase', self._generate_testcase_callback)
self._executor.subscribe('did_finish_run', self._finish_run_callback)
#Executor wide shared context
self._context = {}
# XXX(yan) This is a bit obtuse; once PE support is updated this should
# be refactored out
if self._initial_state_type == 'ELF':
self._binary_obj = ELFFile(file(self._binary))
if isinstance(path_or_state, str):
assert os.path.isfile(path_or_state)
self._initial_state = make_initial_state(path_or_state, argv=argv, **kwargs)
elif isinstance(path_or_state, State):
self._initial_state = path_or_state
else:
raise TypeError("Manticore must be intialized with either a State or a path to a binary")
log.init_logging()
#Move the folowwing into a plugin
self._assertions = {}
@classmethod
def linux(cls, path, argv=None, envp=None, symbolic_files=None, concrete_start='', **kwargs):
try:
return cls(make_linux(path, argv, envp, symbolic_files, concrete_start), **kwargs)
except elftools.common.exceptions.ELFError:
raise Exception('Invalid binary: {}'.format(path))
@classmethod
def decree(cls, path, concrete_data='', **kwargs):
try:
return cls(make_decree(path, concrete_data), **kwargs)
except KeyError: # FIXME(mark) magic parsing for DECREE should raise better error
raise Exception('Invalid binary: {}'.format(path))
@property
def initial_state(self):
return self._initial_state
@property
def context(self):
''' Convenient access to shared context '''
if self._executor is None:
if not self.running:
return self._context
else:
logger.warning("Using shared context without a lock")
@@ -263,7 +270,7 @@ class Manticore(object):
@contextmanager
def _real_context():
if self._executor is None:
if not self.running :
yield self._context
else:
with self._executor.locked_context() as context:
@@ -278,81 +285,74 @@ class Manticore(object):
yield ctx
context[key] = ctx
# XXX(yan): args is a temporary hack to include while we continue moving
# non-Linux platforms to new-style arg handling.
@property
def args(self):
return self._args
@args.setter
def args(self, args):
self._args = args
@property
def should_profile(self):
return self._should_profile
@should_profile.setter
def should_profile(self, enable_profiling):
self._should_profile = enable_profiling
@property
def concrete_data(self):
return self._concrete_data
@concrete_data.setter
def concrete_data(self, data):
self._concrete_data = data
@property
def maxstates(self):
return self._maxstates
@maxstates.setter
def maxstates(self, max_states):
self._maxstates = max_states
@property
def dumpafter(self):
return self._dumpafter
@dumpafter.setter
def dumpafter(self, dump_after):
self._dumpafter = dump_after
@property
def maxstorage(self):
return self._maxstorage
@property
def verbosity(self):
@staticmethod
def verbosity(level):
"""Convenience interface for setting logging verbosity to one of
several predefined logging presets. Valid values: 0-5.
"""
return log.manticore_verbosity
@verbosity.setter
def verbosity(self, setting):
"""A call used to modify the level of output verbosity
:param int setting: the level of verbosity to be used
"""
log.set_verbosity(setting)
@maxstorage.setter
def maxstorage(self, max_storage):
self._maxstorage = max_storage
log.set_verbosity(level)
@property
def workspace(self):
return self._workspace
def running(self):
return self._executor._running.value
@workspace.setter
def workspace(self, ws):
assert not self._running, "Can't set workspace if Manticore is running."
if ':' not in ws:
ws = "fs:" + ws
self._output = ManticoreOutput(ws)
self._executor._workspace = Workspace(self._executor._lock, self._output._descriptor)
def enqueue(self, state):
''' Dynamically enqueue states. Users should typically not need to do this '''
assert not self.running, "Can't add state where running. Can we?"
self._executor.add(state)
###########################################################################
# Workers #
###########################################################################
def _start_workers(self, num_processes, profiling=False):
assert num_processes > 0, "Must have more than 0 worker processes"
logger.info("Starting %d processes.", num_processes)
if profiling:
def profile_this(func):
@functools.wraps(func)
def wrapper(*args, **kwargs):
profile = cProfile.Profile()
profile.enable()
result = func(*args, **kwargs)
profile.disable()
profile.create_stats()
with self.locked_context('profiling_stats', list) as profiling_stats:
profiling_stats.append(profile.stats.items())
return result
return wrapper
target = profile_this(self._executor.run)
else:
target = self._executor.run
if num_processes == 1:
target()
else:
for _ in range(num_processes):
p = Process(target=target, args=())
self._workers.append(p)
p.start()
def _join_workers(self):
with WithKeyboardInterruptAs(self._executor.shutdown):
while len(self._workers) > 0:
w = self._workers.pop().join()
############################################################################
# Common hooks + callback
############################################################################
def init(self, f):
'''
A decorator used to register a hook function to run before analysis begins. Hook
function takes one :class:`~manticore.core.state.State` argument.
'''
def callback(manticore_obj, state):
f(state)
self._executor.subscribe('will_start_run', types.MethodType(callback, self))
return f
def hook(self, pc):
'''
@@ -381,160 +381,26 @@ class Manticore(object):
raise TypeError("pc must be either an int or None, not {}".format(pc.__class__.__name__))
else:
self._hooks.setdefault(pc, set()).add(callback)
if self._hooks:
self._executor.subscribe('will_execute_instruction', self._hook_callback)
def add_symbolic_file(self, symbolic_file):
'''
Add a symbolic file. Each '+' in the file will be considered
as symbolic, other char are concretized.
Symbolic files must have been defined before the call to `run()`.
def _hook_callback(self, state, instruction):
pc = state.cpu.PC
'Invoke all registered generic hooks'
:param str symbolic_file: the name of the symbolic file
'''
self._symbolic_files.append(symbolic_file)
# Ignore symbolic pc.
# TODO(yan): Should we ask the solver if any of the hooks are possible,
# and execute those that are?
if not isinstance(pc, (int, long)):
return
def _get_symbol_address(self, symbol):
'''
Return the address of |symbol| within the binary
'''
if self._binary_obj is None:
return NotImplementedError("Symbols aren't supported")
for section in self._binary_obj.iter_sections():
if not isinstance(section, SymbolTableSection):
continue
symbols = section.get_symbol_by_name(symbol)
if len(symbols) == 0:
continue
return symbols[0].entry['st_value']
def _make_state(self, path):
if self._initial_state_type == 'BinaryNinjaIL' or self._disasm == "binja-il":
# Binary Ninja
env = ['%s=%s' % (k, v) for k, v in self._env.items()]
state = makeBinja(self._binary, self._disasm, self._argv, env,
self._symbolic_files, self._concrete_data)
elif self._initial_state_type == 'ELF':
# Linux
env = ['%s=%s' % (k, v) for k, v in self._env.items()]
state = makeLinux(self._binary, self._disasm, self._argv, env,
self._symbolic_files, self._concrete_data)
elif self._initial_state_type == 'PE':
# Windows
state = makeWindows(self._args)
elif self._initial_state_type == 'DECREE':
# Decree
state = makeDecree(self._binary, self._concrete_data)
elif self._initial_state_type == 'MCORE':
state = path_or_state
else:
raise NotImplementedError("Binary {} not supported.".format(path))
return state
@property
def policy(self):
return self._policy
@policy.setter
def policy(self, policy):
assert not self._running, "Can't set policy if Manticore is running."
self._policy = policy
@property
def coverage_file(self):
return self._coverage_file
@coverage_file.setter
def coverage_file(self, path):
assert not self._running, "Can't set coverage file if Manticore is running."
self._coverage_file = path
@property
def memory_errors_file(self):
return self._memory_errors
@memory_errors_file.setter
def memory_errors_file(self, path):
assert not self._running, "Can't set memory errors if Manticore is running."
self._memory_errors = path
@property
def env(self):
return self._env
@env.setter
def env(self, env):
'''
Update environment variables from |env|. Use repeated '+' chars for
symbolic values.
'''
assert isinstance(env, dict)
assert not self._running, "Can't set process env if Manticore is running."
self._env.update(env)
return self._env
def env_add(self, key, value, overwrite=True):
if key in self._env:
if overwrite:
self._env[key] = value
else:
self._env[key] = value
@property
def arch(self):
assert self._binary is not None
if self._arch is not None:
return self._arch
arch = self._binary_obj.get_machine_arch()
if arch == 'x86': self._arch = 'i386'
elif arch == 'x64': self._arch = 'x86_64'
elif arch == 'ARM': self._arch = 'arm'
else: raise "Unsupported architecture: %s"%(arch, )
return self._arch
def _start_workers(self, num_processes, profiling=False):
assert num_processes > 0, "Must have more than 0 worker processes"
logger.info("Starting %d processes.", num_processes)
if profiling:
def profile_this(func):
@functools.wraps(func)
def wrapper(*args, **kwargs):
profile = cProfile.Profile()
profile.enable()
result = func(*args, **kwargs)
profile.disable()
profile.create_stats()
with self.locked_context('profiling_stats', list) as profiling_stats:
profiling_stats.append(profile.stats.items())
return result
return wrapper
target = profile_this(self._executor.run)
else:
target = self._executor.run
if self._disasm == 'binja-il':
target()
else:
for _ in range(num_processes):
p = Process(target=target, args=())
self._workers.append(p)
p.start()
def _join_workers(self):
with WithKeyboardInterruptAs(self._executor.shutdown):
while len(self._workers) > 0:
w = self._workers.pop().join()
# Invoke all pc-specific hooks
for cb in self._hooks.get(pc, []):
cb(state)
# Invoke all pc-agnostic hooks
for cb in self._hooks.get(None, []):
cb(state)
############################################################################
# Model hooks + callback
@@ -561,6 +427,8 @@ class Manticore(object):
def cb_function(state):
state.platform.invoke_model(fmodel, prefix_args=(state.platform,))
self._model_hooks.setdefault(int(address,0), set()).add(cb_function)
self._executor.subscribe('will_execute_instruction', self._model_hook_callback)
def _model_hook_callback(self, state, instruction):
pc = state.cpu.PC
@@ -582,6 +450,34 @@ class Manticore(object):
if pc in self._assertions:
logger.debug("Repeated PC in assertions file %s", path)
self._assertions[pc] = ' '.join(line.split(' ')[1:])
self._executor.subscribe('will_execute_instruction', self._assertions_callback)
def _assertions_callback(self, state, instruction):
pc = state.cpu.PC
if pc not in self._assertions:
return
from core.parser import parse
program = self._assertions[pc]
#This will interpret the buffer specification written in INTEL ASM.
# (It may dereference pointers)
assertion = parse(program, state.cpu.read_int, state.cpu.read_register)
if not solver.can_be_true(state.constraints, assertion):
logger.info(str(state.cpu))
logger.info("Assertion %x -> {%s} does not hold. Aborting state.",
state.cpu.pc, program)
raise TerminateState()
#Everything is good add it.
state.constraints.add(assertion)
##########################################################################
#Some are Place holders Remove
#Any platform specific callback should go to a plugin
def _terminate_state_callback(self, state, state_id, ex):
#aggregates state statistics into exceutor statistics. FIXME split
@@ -675,14 +571,101 @@ class Manticore(object):
import marshal
marshal.dump(ps.stats, s)
def _start_run(self):
assert not self.running
#FIXME this will be self.publish
self._executor.publish('will_start_run', self._initial_state)
self.enqueue(self._initial_state)
self._initial_state = None
def finish_run(self):
if self.should_profile:
#Copy the local main context to the shared conext
self._executor._shared_context.update(self._context)
def _finish_run(self, profiling=False):
assert not self.running
#Copy back the shared context
self._context = dict(self._executor._shared_context)
if profiling:
self._produce_profiling_data()
#FIXME this will be self.publish
self._executor.publish('did_finish_run')
def run(self, procs=1, timeout=0, should_profile=False):
'''
Runs analysis.
:param int procs: Number of parallel worker processes
:param timeout: Analysis timeout, in seconds
'''
assert not self.running, "Manticore is already running."
self._start_run()
self._time_started = time.time()
if timeout > 0:
t = Timer(timeout, self.terminate)
t.start()
try:
self._start_workers(procs, profiling=should_profile)
self._join_workers()
finally:
if timeout > 0:
t.cancel()
self._finish_run(profiling=should_profile)
def terminate(self):
'''
Gracefully terminate the currently-executing run. Typically called from within
a :func:`~hook`.
'''
self._executor.shutdown()
#############################################################################
#############################################################################
#############################################################################
# Move all the following elsewhere Not all manticores have this
def _get_symbol_address(self, symbol):
'''
Return the address of |symbol| within the binary
'''
# XXX(yan) This is a bit obtuse; once PE support is updated this should
# be refactored out
if self._binary_type == 'ELF':
self._binary_obj = ELFFile(file(self._binary))
if self._binary_obj is None:
return NotImplementedError("Symbols aren't supported")
for section in self._binary_obj.iter_sections():
if not isinstance(section, SymbolTableSection):
continue
symbols = section.get_symbol_by_name(symbol)
if len(symbols) == 0:
continue
return symbols[0].entry['st_value']
@property
def coverage_file(self):
return self._coverage_file
@coverage_file.setter
def coverage_file(self, path):
assert not self.running, "Can't set coverage file if Manticore is running."
self._coverage_file = path
def _finish_run_callback(self):
_shared_context = self.context
executor_visited = _shared_context.get('visited', set())
#Fixme this is duplicated?
if self.coverage_file is not None:
with self._output.save_stream(self.coverage_file) as f:
@@ -707,108 +690,3 @@ class Manticore(object):
logger.info('IPS: %d', instructions_count/elapsed)
def run(self, procs=1, timeout=0):
'''
Runs analysis.
:param int procs: Number of parallel worker processes
:param timeout: Analysis timeout, in seconds
'''
assert not self._running, "Manticore is already running."
args = self._args
replay = None
if hasattr(args, 'replay') and args.replay is not None:
with open(args.replay, 'r') as freplay:
replay = map(lambda x: int(x, 16), freplay.readlines())
initial_state = self._make_state(self._binary)
self._executor.policy = self.policy
self._executor.add(initial_state)
if self._hooks:
self._executor.subscribe('will_execute_instruction', self._hook_callback)
if self._model_hooks:
self._executor.subscribe('will_execute_instruction', self._model_hook_callback)
if self._assertions:
self._executor.subscribe('will_execute_instruction', self._assertions_callback)
self._time_started = time.time()
self._running = True
if timeout > 0:
t = Timer(timeout, self.terminate)
t.start()
try:
self._start_workers(procs, profiling=self.should_profile)
self._join_workers()
finally:
self._running = False
if timeout > 0:
t.cancel()
#Copy back the shared conext
self._context = dict(self._executor._shared_context)
self._executor = None
self.finish_run()
def terminate(self):
'''
Gracefully terminate the currently-executing run. Typically called from within
a :func:`~hook`.
'''
self._executor.shutdown()
def _assertions_callback(self, state, instruction):
pc = state.cpu.PC
if pc not in self._assertions:
return
from core.parser import parse
program = self._assertions[pc]
#This will interpret the buffer specification written in INTEL ASM.
# (It may dereference pointers)
assertion = parse(program, state.cpu.read_int, state.cpu.read_register)
if not solver.can_be_true(state.constraints, assertion):
logger.info(str(state.cpu))
logger.info("Assertion %x -> {%s} does not hold. Aborting state.",
state.cpu.pc, program)
raise TerminateState()
#Everything is good add it.
state.constraints.add(assertion)
def _hook_callback(self, state, instruction):
pc = state.cpu.PC
'Invoke all registered generic hooks'
# Ignore symbolic pc.
# TODO(yan): Should we ask the solver if any of the hooks are possible,
# and execute those that are?
if not isinstance(pc, (int, long)):
return
# Invoke all pc-specific hooks
for cb in self._hooks.get(pc, []):
cb(state)
# Invoke all pc-agnostic hooks
for cb in self._hooks.get(None, []):
cb(state)
def _check_disassembler_present(self, disasm):
if is_binja_disassembler(disasm):
try:
import binaryninja
except ImportError:
err = ("BinaryNinja not found! You MUST own a BinaryNinja version"
" that supports GUI-less processing for this option"
" to work. Please configure your PYTHONPATH appropriately or"
" select a different disassembler")
raise SystemExit(err)
manticore/platforms/linux.py
+10
View File
@@ -2279,6 +2279,16 @@ class SLinux(Linux):
cpu = CpuFactory.get_cpu(mem, arch)
return cpu
def add_symbolic_file(self, symbolic_file):
'''
Add a symbolic file. Each '+' in the file will be considered
as symbolic, other char are concretized.
Symbolic files must have been defined before the call to `run()`.
:param str symbolic_file: the name of the symbolic file
'''
self.symbolic_files.append(symbolic_file)
@property
def constraints(self):
return self._constraints
manticore/utils/event.py
+2 -2
View File
@@ -47,9 +47,9 @@ class Eventful(object):
return self._signals.setdefault(name, dict())
# The underscore _name is to avoid naming collisions with callback params
def publish(self, _name, *args, **kwargs):
def publish(self, _name, *args, **kwargs):
bucket = self._get_signal_bucket(_name)
for robj, methods in bucket.items():
for robj, methods in bucket.iteritems():
for callback in methods:
callback(robj(), *args, **kwargs)
tests/test_memdumps.py
+4
View File
@@ -84,12 +84,15 @@ class IntegrationTest(unittest.TestCase):
self.assertGreaterEqual(actual, expected)
@unittest.skip('Windows temporarily unmaintained')
def testSimpleParse(self):
self._runManticore("simple_parse")
@unittest.skip('Windows temporarily unmaintained')
def testSimpleDeref(self):
self._runManticore("simple_bad_deref")
@unittest.skip('Windows temporarily unmaintained')
def testSimpleBufferOverflow(self):
self._runManticore("simple_buffer_overflow")
@@ -102,6 +105,7 @@ class IntegrationTest(unittest.TestCase):
def testWin32API(self):
self._runManticore("win32_api_test")
@unittest.skip('Windows temporarily unmaintained')
def testAPIInterception(self):
self._runManticore("api_interception")