此项目不再进行内部开发和维护。
Manticore 是一款用于分析智能合约和二进制文件的符号执行工具。
Manticore 可以分析以下类型的程序：
注意：我们建议在虚拟环境中安装 Manticore，以避免与其他项目或包发生冲突。
选项 1：从 PyPI 安装：
pip install manticore
选项 2：从 PyPI 安装，包含执行原生二进制文件所需的额外依赖：
pip install "manticore[native]"
选项 3：安装 nightly 开发构建版本：
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_ 开头的工作目录中。有关工作目录的信息，请参阅 wiki。
如果合约文件扩展名为 .sol 或 .vy（例如），Manticore CLI 会自动检测您正在测试合约。查看演示。
$ 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
提供了另一个 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
Manticore 提供 Python 编程接口，可用于实现强大的自定义分析。
对于以太坊智能合约，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()
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])
ulimit -s 100000 或向 docker run 传递 --ulimit stack=100000000:100000000 来实现$PATH 中包含 solc 程序。crytic-compile，以便更容易地识别问题。Manticore 依赖支持 smtlib2 的外部求解器。目前支持 Z3、Yices 和 CVC4，可通过命令行或配置设置进行选择。如果 Yices 可用，Manticore 将默认使用它。否则，将回退到 Z3 或 CVC4。如果您想手动选择使用哪个求解器，可以这样操作：
manticore --smt.solver Z3
更多详情请访问 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 速度极快。更多详情请访问 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 的帮助。
文档在以下位置提供：
wiki 包含关于入门 Manticore 和贡献的信息
API 参考 提供了更详尽深入的 API 文档
示例 目录包含一些展示 API 功能的小示例
manticore-examples 仓库包含一些更复杂的示例，包括一些真实的 CTF 题目
如果您想提交错误报告或功能请求，请使用我们的 issues 页面。
如需提问和澄清，请访问 讨论 页面。
Manticore 根据 AGPLv3 许可证授权和分发。如果您需要条款的例外情况，请联系我们。
如果您在学术工作中使用 Manticore，请考虑申请 Crytic 10,000 美元研究奖。
