曼图罗斯是一个用于分析二进制文件和智能合约的符号执行工具。
项目描述
曼图罗斯
曼图罗斯是用于分析智能合约和二进制文件的符号执行工具。
功能
- 程序探索： 曼图罗斯可以使用符号输入执行程序并探索它可能达到的所有状态
- 输入生成： 曼图罗斯可以自动生成导致给定程序状态的具体输入
- 错误发现： 曼图罗斯可以检测二进制文件和智能合约中的崩溃和其他失败情况
- 仪器： 曼图罗斯通过事件回调和指令钩子提供对状态探索的精细控制
- 程序接口： 曼图罗斯通过Python API公开对其分析引擎的编程访问
曼图罗斯可以分析以下类型的程序
- Ethereum智能合约（EVM字节码）
- Linux ELF二进制文件（x86、x86_64、aarch64和ARMv7）
- WASM模块
安装
注意：我们建议在虚拟环境中安装曼图罗斯，以防止与其他项目或包发生冲突
选项1：从PyPI安装
pip install manticore
选项2：从PyPI安装，需要额外的依赖项以执行本地二进制文件
pip install "manticore[native]"
选项3：安装夜间开发构建
pip install --pre "manticore[native]"
选项4：从master分支安装
git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"
选项 5：通过 Docker 安装
docker pull trailofbits/manticore
安装完成后，将提供 manticore 命令行工具和 Python API。
对于开发安装，请参阅我们的 wiki。
使用方法
命令行界面
Manticore 具有命令行界面，可以执行二进制或智能合约的基本符号分析。分析结果将放置在以 mcore_ 开头的 workspace 目录中。有关 workspace 的信息，请参阅 wiki。
EVM
如果（例如）合约有 .sol 或 .vy 扩展名，Manticore 命令行界面将自动检测您正在尝试测试合约。请参阅 演示。
点击展开
$ manticore examples/evm/umd_example.sol
[9921] m.main:INFO: Registered plugins: DetectUninitializedMemory, DetectReentrancySimple, DetectExternalCallAndLeak, ...
[9921] m.e.manticore:INFO: Starting symbolic create contract
[9921] m.e.manticore:INFO: Starting symbolic transaction: 0
[9921] m.e.manticore:INFO: 4 alive states, 6 terminated states
[9921] m.e.manticore:INFO: Starting symbolic transaction: 1
[9921] m.e.manticore:INFO: 16 alive states, 22 terminated states
[13761] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
[13754] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
...
[13743] m.c.manticore:INFO: Generated testcase No. 36 - THROW(3 txs)
[13740] m.c.manticore:INFO: Generated testcase No. 37 - THROW(3 txs)
[9921] m.c.manticore:INFO: Results in ~/manticore/mcore_gsncmlgx
Manticore-verifier
提供了一种替代的 CLI 工具，它可以简化合约测试，并允许使用与合约相同的高级语言编写属性方法。查看 manticore-verifier 文档。请参阅 演示
本地
点击展开
$ manticore examples/linux/basic
[9507] m.n.manticore:INFO: Loading program examples/linux/basic
[9507] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Results in ~/manticore/mcore_7u7hgfay
[9507] m.n.manticore:INFO: Total time: 2.8029580116271973
API
Manticore 提供了一个 Python 编程接口，可用于实现强大的自定义分析。
EVM
对于以太坊智能合约，API 可用于对任意合约属性的详细验证。用户可以设置起始条件，执行符号事务，然后审查发现的状态，以确保合约的守恒性。
点击展开
from manticore.ethereum import ManticoreEVM
contract_src="""
contract Adder {
function incremented(uint value) public returns (uint){
if (value == 1)
revert();
return value + 1;
}
}
"""
m = ManticoreEVM()
user_account = m.create_account(balance=10000000)
contract_account = m.solidity_create_contract(contract_src,
owner=user_account,
balance=0)
value = m.make_symbolic_value()
contract_account.incremented(value)
for state in m.ready_states:
print("can value be 1? {}".format(state.can_be_true(value == 1)))
print("can value be 200? {}".format(state.can_be_true(value == 200)))
本地
还可以使用 API 创建用于 Linux 二进制文件的定制分析工具。调整初始状态有助于避免 CLI 使用时常见的状态爆炸问题。
点击展开
# example Manticore script
from manticore.native import Manticore
m = Manticore.linux('./example')
@m.hook(0x400ca0)
def hook(state):
cpu = state.cpu
print('eax', cpu.EAX)
print(cpu.read_int(cpu.ESP))
m.kill() # tell Manticore to stop
m.run()
WASM
Manticore 还可以评估 WebAssembly 函数在符号输入上的属性验证或一般分析。
点击展开
from manticore.wasm import ManticoreWASM
m = ManticoreWASM("collatz.wasm")
def arg_gen(state):
# Generate a symbolic argument to pass to the collatz function.
# Possible values: 4, 6, 8
arg = state.new_symbolic_value(32, "collatz_arg")
state.constrain(arg > 3)
state.constrain(arg < 9)
state.constrain(arg % 2 == 0)
return [arg]
# Run the collatz function with the given argument generator.
m.collatz(arg_gen)
# Manually collect return values
# Prints 2, 3, 8
for idx, val_list in enumerate(m.collect_returns()):
print("State", idx, "::", val_list[0])
要求
- Manticore 需要 Python 3.7 或更高版本
- Manticore 正式支持由 Github Actions 提供的 Ubuntu 最新 LTS 版本
- Manticore 在 MacOS 上对 EVM 和 WASM（但不是本地 Linux 二进制文件）具有实验性支持
- 我们建议增加堆栈大小。可以通过运行
ulimit -s 100000或通过传递--ulimit stack=100000000:100000000到docker run来完成此操作
编译智能合约
- 以太坊智能合约分析需要您的
$PATH中的solc程序。 - Manticore 使用 crytic-compile 构建智能合约。如果您遇到编译问题，请考虑直接在代码上运行
crytic-compile，以便更容易地识别任何问题。 - 我们仍在实施对 EVM 伊斯坦布尔指令语义的完整支持，因此某些 opcodes 可能不受支持。在紧急情况下，您可以尝试使用 Solidity 0.4.x 编译以避免生成这些指令。
使用不同的求解器（Yices，Z3，CVC4）
Manticore 依赖于支持 smtlib2 的外部求解器。目前支持 Z3、Yices 和 CVC4，并且可以通过命令行或配置设置进行选择。如果 Yices 可用，Manticore 将默认使用它。如果没有，它将回退到 Z3 或 CVC4。如果您想手动选择要使用的求解器，可以这样做： manticore --smt.solver Z3
安装 CVC4
有关更多详细信息，请访问 https://cvc4.github.io/。否则只需获取二进制文件并使用它。
sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
sudo chmod +x /usr/bin/cvc4
安装 Yices
Yices 极其快速。更多详细信息请在此处 https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
寻求帮助
请随时访问 Empire Hacking 中的 #manticore slack 频道以寻求使用或扩展 Manticore 的帮助。[Empire Hacking](https://empireslacking.herokuapp.com/)
文档可在多个位置找到
-
维基页面（wiki）包含了关于如何开始使用Manticore和如何贡献信息的说明。
-
API参考文档（API reference）提供了关于我们API的更详细和深入文档。
-
示例目录（examples）包含了一些展示API功能的简单示例。
-
manticore-examples（manticore-examples）仓库包含了一些更复杂的示例，包括一些真实的CTF问题。
如果您想提交错误报告或功能请求，请使用我们的问题页面。
如有疑问或需要澄清，请访问讨论页面。
许可证
Manticore采用AGPLv3许可证进行许可和分发。如果您需要条款例外，请联系我们（开源邮箱）。
出版物
- Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts，作者：Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, Artem Dinaburg - ASE 19
如果您在学术工作中使用了Manticore，请考虑申请Crytic $10k Research Prize。
ASE 2019演示视频
下载文件
下载适合您平台的文件。如果您不确定选择哪个，请了解更多关于安装包的信息。
源分发
构建分发
manticore-0.3.7.tar.gz的哈希值
| 算法 | 哈希摘要 | |
|---|---|---|
| SHA256 | a7588fd2ea9d903b671d45d7cbf47c983031902ff0fdbaec187c588750c7b8fc |
|
| MD5 | 1e03d6206621efdbe7371bcbaefce9b5 |
|
| BLAKE2b-256 | b0729bb5ac53cf0aad3ca27f3ba1388dc99ffa1a63d110236b26da8ac2bb1a35 |
manticore-0.3.7-py3-none-any.whl的哈希值
| 算法 | 哈希摘要 | |
|---|---|---|
| SHA256 | 4b9beb41a9c42f9ec1ebed75e918f17367ca78c84bc9efc5a9e00deb0962264b |
|
| MD5 | a3deca0fa817ebd1f859ac8d43ba471e |
|
| BLAKE2b-256 | 45572895609b89c83ecf544d8f5175199ea1306c0e76d447bc3df79758a0b356 |
