Update README.md (#33)
* Update README.md * Add quick start * Update README.md * Update README.md * Update README.md
This commit is contained in:
parent
ca158dd5b4
commit
a6b81c0464
81
README.md
81
README.md
@ -2,27 +2,19 @@
|
||||
|
||||
[](https://travis-ci.com/trailofbits/manticore)
|
||||
|
||||
Manticore is a symbolic execution engine for binary analysis, usable as a
|
||||
command line tool or Python Library (pre-alpha).
|
||||
|
||||
It executes multiple paths of a program simultaneously by replacing input data
|
||||
with a set of constraints representing all possible values of that data,
|
||||
allowing it to thoroughly discover numerous paths as the program executes
|
||||
control flow. By solving the constraints with a theorem prover, Manticore
|
||||
generates concrete inputs to trigger discovered paths.
|
||||
Manticore is a prototyping tool for dynamic binary analysis, with support for
|
||||
symbolic execution, taint analysis, and binary instrumentation.
|
||||
|
||||
## features
|
||||
|
||||
- **Input Generation**: Manticore automatically generates inputs that trigger
|
||||
unique code paths.
|
||||
- **Defect Discovery**: Manticore discovers program defects enabling memory
|
||||
safety violations and generates inputs to trigger them.
|
||||
- **Crash Discovery**: Manticore discovers inputs that crash programs via
|
||||
memory safety violations.
|
||||
- **Execution Tracing**: Manticore records an instruction-level trace of the
|
||||
program's execution for each generated input.
|
||||
- **Concolic Execution**: Manticore loads memory dumps of running Windows
|
||||
programs to allow deep state space exploration.
|
||||
- **Programmatic Interface** (pre-alpha): Manticore exposes programmatic access
|
||||
to its symbolic execution engine via a Python API.
|
||||
- **Programmatic Interface** (beta): Manticore exposes programmatic access
|
||||
to its analysis engine via a Python API.
|
||||
|
||||
## scope
|
||||
|
||||
@ -30,25 +22,56 @@ Manticore supports binaries of the following formats, operating systems, and
|
||||
architectures. It has been primarily used on binaries compiled from C and C++.
|
||||
|
||||
- OS/Formats: Linux ELF, Windows Minidump
|
||||
- Architectures: x86, x86_64, ARMv7
|
||||
- Architectures: x86, x86_64, ARMv7 (partial)
|
||||
|
||||
## requirements
|
||||
|
||||
Manticore is officially supported on Linux and uses Python 2.7.
|
||||
|
||||
### required dependencies
|
||||
## installation
|
||||
|
||||
- Python Dependencies: Run `pip install -r requirements.txt`
|
||||
- Z3 Theorem Prover: Download the latest release for your platform from https://github.com/Z3Prover/z3/releases/latest, and place the enclosed `z3` binary in your `$PATH`.
|
||||
From the root of the Manticore repository, run:
|
||||
|
||||
### development dependencies
|
||||
```
|
||||
pip install .
|
||||
````
|
||||
|
||||
- keystone: Used in unit tests
|
||||
or, if you would like to do a user install:
|
||||
|
||||
```
|
||||
pip install --user .
|
||||
```
|
||||
|
||||
This installs the Manticore CLI tool (`manticore`) and the Python API.
|
||||
|
||||
Then, install the Z3 Theorem Prover. Download the latest release for your
|
||||
platform from https://github.com/Z3Prover/z3/releases/latest, and place the
|
||||
enclosed `z3` binary in your `$PATH`.
|
||||
|
||||
> Note: Due to a known [issue](https://github.com/aquynh/capstone/issues/445),
|
||||
Capstone may not install correctly. If you get this error message,
|
||||
"ImportError: ERROR: fail to load the dynamic library.", or another related
|
||||
to Capstone, try reinstalling via `pip install -I --no-binary capstone`
|
||||
|
||||
## quick start
|
||||
|
||||
After installing Manticore, here is some basic usage you can try.
|
||||
|
||||
```
|
||||
cd examples/linux
|
||||
make
|
||||
manticore basic # a mcore_* directory is created
|
||||
cat mcore_*/*1.stdin | ./basic
|
||||
cat mcore_*/*2.stdin | ./basic
|
||||
|
||||
cd ../script
|
||||
python count_instructions.py ../linux/helloworld
|
||||
```
|
||||
|
||||
## usage
|
||||
|
||||
```
|
||||
python main.py ./path/to/binary # runs, and creates a directory with analysis results
|
||||
$ manticore ./path/to/binary # runs, and creates a directory with analysis results
|
||||
```
|
||||
|
||||
or
|
||||
@ -71,3 +94,19 @@ def hook(state):
|
||||
|
||||
m.run()
|
||||
```
|
||||
|
||||
## FAQ
|
||||
|
||||
### How does Manticore compare to [angr](http://angr.io)?
|
||||
|
||||
In short, Manticore is simpler. Manticore is a smaller codebase, and has fewer
|
||||
dependencies and features. Accordingly, Manticore may also be slower,
|
||||
for example, due to having less symbolic execution optimizations and techniques
|
||||
implemented.
|
||||
|
||||
Generally speaking, a subset of the analyses that can be implemented with angr,
|
||||
can be implemented with Manticore, however if you’ve used neither, you may find
|
||||
Manticore to have a slightly less steep learning curve. Additionally, if you
|
||||
come from a reverse engineering or exploitation background, you may find
|
||||
Manticore intuitive due to its lack of intermediate representation and overall
|
||||
emphasis on staying close to machine abstractions.
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user