一个用于分析智能合约和二进制文件的符号执行工具（貌似不止可以分析以太坊智能合约）

manticore example.sol
# 或
manticore project

'
Ethereum flags:
  --verbose-trace 为每个状态转储一个额外的verbose追踪（默认：False）。
  --txlimit TXLIMIT 运行的最大符号交易数（正整数）（默认：无）。
  --txnocoverage 不使用覆盖率作为停止标准（默认：False）。
  --txnoether 不尝试向合约发送乙醚（默认：False）。
  --txaccount TXACCOUNT 符号交易中用作调用者的账户，可以是 "攻击者 "或 "所有者 "或 "combo1"（同时使用）（默认：攻击者）
  --txpreconstrain 制约人类交易，以避免在合同函数调度器中出现异常（默认：False）。
  --contract CONTRACT 在有多个合同的情况下要分析的合同名称（默认：无）
  --avoid-constant 避免探索人类交易的常量函数（默认：False）。
  --limit-loops 限制循环深度（默认：False）
  --no-testcases 在分析结束后，不为发现的状态生成测试案例（默认为False）
  --only-alive-testcases 分析结束后，不为无效/抛出的状态生成测试案例（默认为False）。
  --thorough-mode 配置Manticore进行更详尽的探索。评估气体，为无效状态生成测试用例，探索常量函数，并运行一套小型的检测器。(默认：False)

Ethereum detectors:
  --list-detectors 列出可用的检测器 (默认: False)
  --exclude DETECTORS_TO_EXCLUDE 逗号分隔的应该被排除的探测器列表（默认： )
  --exclude-all 排除所有探测器（默认为False）。
'

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()  # 启动一个新区块链
user_account = m.create_account(balance=1*10**18)  # 创建账户

# 读取合约源码
with open('example.sol') as f:
    source_code = f.read()

# 部署合约
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()  # 创建符号值
# symbolic_data = m.make_symbolic_buffer(320)  # 创建符号字节数组
contract_account.f(symbolic_var)  # 执行测试

print("Results are in {}".format(m.workspace))  # 测试结果输出到m.workspace
m.finalize() # stop the exploration  # 停止测试

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.9;

contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Untitled

参考