trailofbits / manticore Goto Github PK

we only support reg operands right now

This is in solver.py. We currently let the OSError bubble up from the Popen.

Provide the ability to add arbitrary data that an analyst would like to keep track of to the State structure. For instance, dereferencing count, heap information, and other data that you'd like to use to guide exploration. (cc @montyly)

Something that ties us to Linux right now is fetching libc and the dynamic linker, for example, directly from the filesystem on the machine. To allow mcore to run on more platforms like OS X, add a way to specify directories for mcore to look in for things like ld-linux.so, so you could analyze a dynamically linked ELF on OS X.

Users should ideally have the ability to gain insight on manticore's performance via a simple script. Implementing this probably has two major components:

• Choose/create a workload to benchmark on that effectively emulates "real life" workloads

• Add an option to manticore to save performance information (e.g. time spent in the solver, time spent saving/recovering states, etc.)

Then, our script simply runs manticore on the aforementioned workload and displays the performance information.

Current tests do not cover some behavior of the executor. We also lack integration tests.

So we can lessen our Z3 requirements and make it easier to install

State.symbolicate_buffer uses the label parameter to tag symbolic values, where as State.new_symbolic_buffer uses name.

Specifically in error messages

use case: analyzing a function in a .so

You know what to answer

this is an arm specific function for handling kernel user mode helpers for linux arm, and shouldn't be in the general linux class

write a quick opinionated install.sh script for installing manticore

• checks if in venv and does --user install or not based on that? (http://stackoverflow.com/questions/15454174/how-can-a-shell-function-know-if-it-is-running-within-a-virtualenv)
• does the pip install command
• installs z3
• basic checks that install worked

When a dynamic binary is run on my machine, mcore doesn't even reach main, but errors a message to stderr.

^C2017-04-21 10:29:34,425: [20040][4048] EXECUTOR:ERROR: Interrupted!
2017-04-21 10:29:34,503: [20038][4068] EXECUTOR:ERROR: Interrupted!
2017-04-21 10:29:34,513: [20036][4041] EXECUTOR:ERROR: Interrupted!
2017-04-21 10:29:34,528: [20037][4043] EXECUTOR:ERROR: Interrupted!
^C

^[[B^CTraceback (most recent call last):
File "/usr/bin/manticore", line 9, in
load_entry_point('Manticore', 'console_scripts', 'manticore')()
File "/Projects/manticore/manticore/main.py", line 117, in main
m.run(args.timeout)
File "/Projects/manticore/manticore/manticore.py", line 567, in run
# and execute those that are?
File "/Projects/manticore/manticore/manticore.py", line 464, in _join_workers
def _model_hook_callback(self, state, pc):
File "/Projects/manticore/manticore/core/executor.py", line 98, in shutdown
with self._lock:
File "/usr/lib64/python2.7/multiprocessing/managers.py", line 991, in enter
return self._callmethod('acquire')
File "/usr/lib64/python2.7/multiprocessing/managers.py", line 759, in _callmethod
kind, result = conn.recv()
KeyboardInterrupt
Process Process-3:
Process Process-4:
Traceback (most recent call last):
Traceback (most recent call last):
File "/usr/lib64/python2.7/multiprocessing/process.py", line 258, in _bootstrap
File "/usr/lib64/python2.7/multiprocessing/process.py", line 258, in _bootstrap
Process Process-5:
Traceback (most recent call last):
File "/usr/lib64/python2.7/multiprocessing/process.py", line 258, in _bootstrap
self.run()
self.run()
File "/usr/lib64/python2.7/multiprocessing/process.py", line 114, in run
File "/usr/lib64/python2.7/multiprocessing/process.py", line 114, in run
self.run()
self._target(*self._args, **self._kwargs)
self._target(*self._args, **self._kwargs)
File "/usr/lib64/python2.7/multiprocessing/process.py", line 114, in run
File "/Projects/manticore/manticore/core/executor.py", line 837, in run
File "/Projects/manticore/manticore/core/executor.py", line 837, in run
self._target(*self._args, **self._kwargs)
File "/Projects/manticore/manticore/core/executor.py", line 837, in run
self._stats.append(self._profile.stats.items())
self._stats.append(self._profile.stats.items())
File "/Projects/manticore/manticore/utils/nointerrupt.py", line 17, in exit
File "/Projects/manticore/manticore/utils/nointerrupt.py", line 17, in exit
self._stats.append(self._profile.stats.items())
File "/Projects/manticore/manticore/utils/nointerrupt.py", line 17, in exit
self.old_handler(*self.signal_received)
self.old_handler(*self.signal_received)
self.old_handler(*self.signal_received)
KeyboardInterrupt
KeyboardInterrupt
KeyboardInterrupt

There is at least 1 bug in our handling of dynamically linked binaries, and loading them into the emulated address space. Function: Linux.load.

We should either remove the argument, or initialize constraint set correctly

relevant: #50 #51

enabling this test seems to break following z3 related tests, possibly crashing z3

• do all tests talk to the same instance of z3?
• do we need to have a reset somewhere in between each test?

This helps in situations where we encounter a binary with an instruction we don't support yet.

This issue was automatically created by Allstar and refers to trailofbits/manticore.

Security Policy Violation
Project is out of compliance with Binary Artifacts policy: binaries present in source code

Rule Description
Binary Artifacts are an increased security risk in your repository. Binary artifacts cannot be reviewed, allowing the introduction of possibly obsolete or maliciously subverted executables. For more information see the Security Scorecards Documentation for Binary Artifacts.

Remediation Steps
To remediate, remove the generated executable artifacts from the repository.

First 10 Artifacts Found

• examples/linux/binaries/corruption
• examples/linux/binaries/multiple-styles
• examples/script/aarch64/basic
• examples/script/aarch64/hello42
• tests/native/binaries/arguments
• tests/native/binaries/arguments_linux_amd64
• tests/native/binaries/arguments_linux_armv7
• tests/native/binaries/basic_linux_amd64
• tests/native/binaries/basic_linux_armv7
• tests/native/binaries/basic_state_merging
• Run a Scorecards scan to see full list.

Additional Information
This policy is drawn from Security Scorecards, which is a tool that scores a project's adherence to security best practices. You may wish to run a Scorecards scan directly on this repository for more details.

⚠️ There is an updated version of this policy result! Click here to see the latest update

This issue will auto resolve when the policy is in compliance.

Issue created by Allstar. See https://github.com/ossf/allstar/ for more information. For questions specific to the repository, please contact the owner or maintainer.

Some of them are broken and don't work (--timeout, --env). Need to verify that all advertised functionality in --help works

It resides in executor.py right now, which can make it hard to read the code.

Currently, ARM intrinsics support is done via handling InvalidPCException. This is how it's done in qemu for performance reasons. This complicates our code for both the Linux model and for the Unicorn emulation.

We should do it the way it's done in hardware: Map an extra code of page (which we have) when loading an ARM binary. We won't even need to add atomic support because we're guaranteed to never get hardware interrupts.

use case: analyzing just a particular function, or even just a few instructions of a program

argv is symbolicated accurately, but the resulting expression isn’t written back into the address space

https://github.com/trailofbits/manticore/blob/master/manticore.py#L53

we've gotten a few requests from users to be able to have Manticore run on OS X. this shouldn't be too hard as nothing we do inherently ties us to linux. we'd need to

• eliminate all uses of /dev (i think there are a few)
• make sure all python stdlib calls we make work uniformly on linux/osx
• make sure python dependencies work on both
• add features to allow users to specify locations for ld.so and libraries (#93)

Centralize spawning of z3 subprocess and checking of z3 validity in a single function, rather than having the check in the ctor, and spawn elsewhere.

It would be useful to be able to drop into pdb inside a hook, especially for a new user. Right now, we get an error. It's related to our use of multiprocessing somehow.

2017-03-06 12:02:25,464: [94843][0] EXECUTOR:ERROR: THIS SHOULD NOT REACHABLE! Exception in user code:
Traceback (most recent call last):
  File "/mnt/hgfs/code/manticore/manticore/core/executor.py", line 875, in run
    self.will_execute_pc(current_state, current_state.cpu.PC)
  File "/mnt/hgfs/code/manticore/manticore/utils/event.py", line 31, in __call__
    return self.emit(*args, **kwargs)
  File "/mnt/hgfs/code/manticore/manticore/utils/event.py", line 48, in emit
    results.append(f(obj, *args, **kwargs))
  File "/mnt/hgfs/code/manticore/manticore/manticore.py", line 617, in _hook_callback
    cb(state)
  File "statemachine_eval.py", line 35, in check_tainted_cmp
    insn = state.cpu.instruction
  File "statemachine_eval.py", line 35, in check_tainted_cmp
    insn = state.cpu.instruction
  File "/usr/lib/python2.7/bdb.py", line 49, in trace_dispatch
    return self.dispatch_line(frame)
  File "/usr/lib/python2.7/bdb.py", line 68, in dispatch_line
    if self.quitting: raise BdbQuit
BdbQuit

Right now many of the command line flags have no usage examples or thorough explanation of their functionality, this can make it hard for users to effectively use them

• multiple installation sections are confusing
• directly put --no-binary stuff into commands to run
• add keystone engine to dev install command

Installation feedback

• --no-binary is not available commonly it seems. maybe we should have people use the old no-use-wheel arg?

If they accidentally pass in a str (if they forgot to convert sys.argv[1] to an int for example) it's bad UX because their hook inexplicably won't run. This because how we look up the hooks in _hook_callback

There is a lot of shared code between the models (decree/linux/windows) right now, that could be made more manageable with a parent abstract model.

(manticore) root@kali:~/CTF/HackTheVote/pwn# manticore ./irs 
2017-03-13 16:17:59,590: [48618] MAIN:INFO: Loading program: ['./irs']
2017-03-13 16:17:59,591: [48618] MAIN:INFO: Workspace: ./mcore_LV0KP1
2017-03-13 16:18:01,437: [48668] CPU:ERROR: CPUID with EAX=d not implemented @ f7ff4826
 
2017-03-13 16:22:56,061: [48668] SMT:WARNING: Found an unknown core, probably a solver timeout
2017-03-13 16:24:29,324: [48668] MEMORY:INFO: Reading 4 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7f4a32aed750>
2017-03-13 16:25:00,200: [48668] SMT:WARNING: Found an unknown core, probably a solver timeout
2017-03-13 16:25:35,299: [48668] SMT:WARNING: Found an unknown core, probably a solver timeout
2017-03-13 16:26:07,874: [48668] SMT:WARNING: Found an unknown core, probably a solver timeout
2017-03-13 16:26:40,069: [48668] EXECUTOR:ERROR: Failed an internal assertion: 
Traceback (most recent call last):
  File "/root/.envs/manticore/local/lib/python2.7/site-packages/manticore/core/executor.py", line 923, in run
    assert se.message == 'Max number of different solutions hit'
AssertionError

2017-03-13 16:26:40,100: [48668] EXECUTOR:ERROR: Traceback (most recent call last):
2017-03-13 16:26:40,100: [48668] EXECUTOR:ERROR:   File "/root/.envs/manticore/local/lib/python2.7/site-packages/manticore/core/executor.py", line 923, in run
2017-03-13 16:26:40,101: [48668] EXECUTOR:ERROR:     assert se.message == 'Max number of different solutions hit'
2017-03-13 16:26:40,101: [48668] EXECUTOR:ERROR: AssertionError
Process Process-3:
Traceback (most recent call last):
  File "/usr/lib/python2.7/multiprocessing/process.py", line 258, in _bootstrap
    self.run()
  File "/usr/lib/python2.7/multiprocessing/process.py", line 114, in run
    self._target(*self._args, **self._kwargs)
  File "/root/.envs/manticore/local/lib/python2.7/site-packages/manticore/core/executor.py", line 1018, in run
    if solver.check(current_state.constraints):
  File "/root/.envs/manticore/local/lib/python2.7/site-packages/manticore/core/smtlib/solver.py", line 58, in check
    return self.can_be_true(constraints, True)
  File "/root/.envs/manticore/local/lib/python2.7/site-packages/manticore/core/smtlib/solver.py", line 319, in can_be_true
    self._reset(temp_cs.related_to(expression))
  File "/root/.envs/manticore/local/lib/python2.7/site-packages/manticore/core/smtlib/solver.py", line 206, in _reset
    self._stop_proc()
  File "/root/.envs/manticore/local/lib/python2.7/site-packages/manticore/core/smtlib/solver.py", line 172, in _stop_proc
    self._send("(exit)")
  File "/root/.envs/manticore/local/lib/python2.7/site-packages/manticore/core/smtlib/solver.py", line 222, in _send
    raise SolverException(e)
SolverException: [Errno 32] Broken pipe

And attached is the binary
ultrababy.zip

Note: This is using the dev-fix-cpuid branch

Since these are the three main analysis types we advertise support for