Eveneko Blogger


现在市面上出现了一些 Wasm 的符号执行工具,例如 Manticore,我们需要调研并实际部署一下测试一下他们的功能和性能。


  • Install via Docker

    docker run -idt --name=manticore -v ~/Docker/manticore:/data/docker_share --ulimit stack=100000000:100000000 trailofbits/manticore:latest
  • Environment

    • Manticore requires Python 3.7 or greater
    • Manticore officially supports the latest LTS version of Ubuntu(Mac not ok)
    • Manticore is recommended running with increased stack size
    • Manticore is recommended installing Manticore in a virtual environment to prevent conflicts with other projects or packages


  • Program Exploration: Manticore can execute a program with symbolic inputs and explore all the possible states it can reach
  • Input Generation: Manticore can automatically produce concrete inputs that result in a given program state
  • Error Discovery: Manticore can detect crashes and other failure cases in binaries and smart contracts
  • Instrumentation: Manticore provides fine-grained control of state exploration via event callbacks and instruction hooks
  • Programmatic Interface: Manticore exposes programmatic access to its analysis engine via a Python API


  • CLI

    • 可以对二进制或智能合约进行基本的符号分析
    • 分析结果将放置在 mcore_* 文件夹
  • API

    • Manticore 提供了一个 Python 编程接口
  • 分析对象

    • Ethereum smart contracts (EVM bytecode)
    • Linux ELF binaries (x86, x86_64, aarch64, and ARMv7)
    • WASM Modules
      • Manticore 还可以通过符号输入评估 WebAssembly 函数,以进行属性验证或一般分析。
  • Using a different solver

    • Yices
    • Z3
    • CVC4

C library Implementation

Performance Testing



  • Post title:Manticore
  • Post author:Eveneko
  • Create time:2021-09-06 11:01:57
  • Post link:
  • Copyright Notice:All articles in this blog are licensed under BY-NC-SA unless stating additionally.