manticore v0.3 releases: Dynamic binary analysis tool
Manticore is a prototyping tool for dynamic binary analysis, with support for symbolic execution, taint analysis, and binary instrumentation.
- Input Generation: automatically generates inputs that trigger unique code paths
- Crash Discovery: discovers inputs that crash programs via memory safety violations
- Execution Tracing: records an instruction-level trace of execution for each generated input
- Programmatic Interface: exposes programmatic access to its analysis engine via a Python API
Manticore supports binaries of the following formats, operating systems, and architectures. It has been primarily used on binaries compiled from C and C++. Examples of practical manticore usage are also on github.
- OS/Formats: Linux ELF, Windows Minidump
- Architectures: x86, x86_64, ARMv7 (partial)
Executor Refactor (#1385)
We’ve completed a major refactor of the core executor that reorganizes Manticore’s state machine to be more amenable toward use with the multiprocesssing module. This refactor introduces some small API changes:
- One must explicitly call the
finalizemethod to dump test cases from a run
will_start_runevent has been renamed to
solvermodule requires explicitly accessing the Z3Solver singleton.
from manticore.core.smtlib import solverbecomes:
manticore.running_stateshas been renamed to
For more information about changes to the state machine, see the diagram in core/manticore.py
We’ve run the
blackautoformatter on the master branch of Manticore, and added a check for compliance to our CI. To ensure your code is properly formatted, run
black -t py36 -l 100 .in your Manticore directory before committing.
Support for statically-linked AArch64 binaries (#1424)
Contractor nkaretnikov spent several months adding support for AArch64 on Linux. As this is a brand new architecture, we’ve left in most of the debugging assertions, which may slow it down slightly.
We look forward to getting feedback on this architecture so we can eventually remove the debugging assertions.
- Added Symbolic EVM Tests for the Frontier fork. Note that we don’t support any other forks (i.e. Constantinople) yet. (#1431, #1441)
- [fixed API] Fixed relative paths for .sol files (#1393)
- [fixed API] Support dynamic parameters in constructors (#1414)
- Fixed detector failure when PC is symbolic (#1395)
- Transfers from etherless contracts no longer report STOP (#1392)
- Added stubs for missing system calls & downgraded most missing calls from exceptions to warnings (#1384)
- Fixed DECREE magic pages (#1413)
- Store x86 registers in a set instead of a list (#1415)
- Fix register boundary check for non-x86 architectures (#1429)
movhpson x86 (#1444)
# Install system dependencies
sudo apt-get update && sudo apt-get install z3 python-pip -y
python -m pip install -U pip
# Install manticore and its dependencies
git clone https://github.com/trailofbits/manticore.git && cd manticore sudo pip install .
# Build the examples
# Use the Manticore CLI
cat mcore_*/*1.stdin | ./basic
cat mcore_*/*2.stdin | ./basic
# Use the Manticore API
python count_instructions.py ../linux/helloworld
$ manticore ./path/to/binary # runs, and creates a mcore_* directory with analysis results
Copyright (C) 2018 trailofbits