manticore
Manticore 0.3.7
该项目不再由内部开发和维护。然而，我们很乐意审查并接受社区编写的小型拉取请求。我们只会考虑错误修复和微小的增强。
任何新的或当前开放的问题和讨论都应得到社区的回答和支持。
Manticore 是一种用于分析智能合约和二进制文件的符号执行工具。
Manticore 可以分析以下类型的程序：
注意：我们建议在虚拟环境中安装 Manticore，以防止与其他项目或包发生冲突
选项 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 CLI 工具和 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.8029580116271973Manticore 提供了一个 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或将--ulimit stack=100000000:100000000传递给docker run来完成$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 问题
如果您想提交错误报告或功能请求，请使用我们的问题页面。
如有疑问和澄清，请访问讨论页面。
Manticore 根据 AGPLv3 许可证进行许可和分发。如果您正在寻找条款的例外情况，请联系我们。
如果您在学术工作中使用 Manticore，请考虑申请 Crytic 10k 美元研究奖。
