双接口设计 · 多样应用场景

Manticore提供两种使用方式：

1. 命令行工具：快速生成程序测试用例（样本输入），每个用例对应独特执行结果（如正常退出或崩溃）
2. Python API：支持定制化分析与应用优化，可解决以下问题：
   • 执行到X点时变量Y是否可能为特定值？
   • 程序能否在运行时到达某段代码？
   • 如何构造触发特定代码执行的输入？
   • 用户输入是否被用作libc函数参数？
   • 函数执行次数统计
   • 给定输入下的指令执行计数

API核心功能还包括：

• 丢弃无关执行状态
• 在任意执行点运行自定义分析函数
• 具体化符号内存
• 内省和修改模拟机器状态

早期应用实例

• DARPA网络大挑战：作为符号执行漏洞挖掘基础组件
• CTF实战案例：
  • Eric Hennenfent：通过二进制插桩/符号执行双解法完成逆向挑战
  • Yan与Mark：用污点符号值追踪用户输入影响范围
  • Josselin Feist：纯API实现漏洞利用（定位崩溃点+符号执行构造约束）
  • Cory Duplantis：解决Google CTF 2016逆向题（演示CTF解题标准化流程）

快速入门指南

环境准备（Ubuntu 16.04）：

1
2
3
4
5
6
7

# 安装系统依赖
sudo apt-get update && sudo apt-get install z3 python-pip -y
python -m pip install -U pip

# 安装Manticore
git clone https://github.com/trailofbits/manticore.git && cd manticore
sudo pip install --no-binary capstone .

基础使用演示：

1. 命令行发现测试用例：

1
2
3
4

cd examples/linux
make
manticore basic
cat mcore_*/*1.stdin | ./basic

2. API统计指令数：

1
2

cd ../script
python count_instructions.py ../linux/helloworld

（正文完）