AwesomeREA.org

Tool

Manticore

Trail of Bits' now-archived symbolic execution tool for Linux ELF binaries on x86, x86-64, AArch64 and ARMv7, Ethereum smart contracts as EVM bytecode, and WebAssembly modules. It runs a program on symbolic inputs to explore the states it can reach, generates concrete inputs that lead to a chosen state and detects crashes and other failures, solving constraints with an external Yices, Z3 or CVC4 solver. The manticore CLI writes generated test cases to an mcore_ workspace, while the Python API adds instruction hooks, event callbacks and custom initial states; manticore-verifier checks contract properties written in the contract's own language.

Requirements & limits

  • Archived and unmaintained: the README states that the project is no longer internally developed and maintained, and GitHub marks the repository archived. The reviewed master commit, from 2026-06-24, only changes that status; the last change under manticore/ dates from 2022-08-07. The latest release is 0.3.7 on GitHub and PyPI (2022-02-17), and PyPI's nightly 0.3.8.dev builds end on 2024-02-27.
  • Requires Python 3.7 or later. pip install manticore covers EVM and WASM, manticore[native] adds the pinned capstone 5.0.0rc2 and unicorn 2.x needed for native binaries, and a trailofbits/manticore Docker image is offered. The README names the latest Ubuntu LTS on GitHub Actions as the supported platform, gives macOS experimental EVM and WASM support but no native-binary support, and recommends a larger stack limit; CI at the reviewed commit still runs Python 3.7 on ubuntu-20.04, and newer Python releases were not checked.
  • Inputs are the user's own ELF binaries, Solidity or Vyper sources or EVM bytecode, or WASM modules. Contract analysis needs solc on PATH and compiles through crytic-compile; the README says EVM Istanbul semantics are not fully implemented, so some opcodes may be unsupported. Whole-program CLI runs are prone to state explosion, which the README suggests limiting by tailoring the initial state through the API.
  • CI runs ethereum, native, WASM, examples and other test suites after downloading Yices 2.6.2 and solc 0.4.24. tests/native/binaries and examples/linux/binaries hold small prebuilt Linux test programs for amd64 and ARMv7, some with their C sources; larger examples, including CTF problems, live in the separate manticore-examples repository, and server/ holds an unpublished gRPC wrapper for the Manticore UI.
  • AGPL-3.0; the README says Trail of Bits can be contacted for an exception to its terms. The ASE 2019 paper (arXiv 1907.03890) describes the tool. The reviewed sources state no REA use, and this collection did not install Manticore or analyze any program.

About this entry

Type
Tool
Category
Binary analysis libraries
Relationship
Foundation tool
Targets
Binary

Sources reviewed

The description was reviewed against primary sources. This does not establish runtime testing, security auditing or verified compatibility.

Report an outdated entry Suggest a translation fix

Primary sources

  1. README.md GitHub · trailofbits/manticore · Revision cdf6c4b
  2. README.md#L225-L236 GitHub · trailofbits/manticore · Revision cdf6c4b
  3. setup.py GitHub · trailofbits/manticore · Revision cdf6c4b
  4. .github/workflows/ci.yml GitHub · trailofbits/manticore · Revision cdf6c4b
  5. tests/native/binaries GitHub · trailofbits/manticore · Revision cdf6c4b
  6. server/README.md GitHub · trailofbits/manticore · Revision cdf6c4b
  7. LICENSE GitHub · trailofbits/manticore · Revision cdf6c4b
  8. https://github.com/trailofbits/manticore/releases/tag/0.3.7
  9. https://pypi.org/project/manticore/0.3.7/
  10. https://arxiv.org/abs/1907.03890

More in Native binaries

All 111 entries in Native binaries