⚡

Mythril符号执行分析工具Skill mythril-symbolic

Mythril 符号执行技能是一个用于智能合约安全审计的自动化工具。它通过符号执行技术深度扫描以太坊虚拟机（EVM）字节码，自动检测重入攻击、整数溢出、无保护自毁等关键安全漏洞。该工具支持配置交易深度、超时设置，并能生成概念验证（PoC）利用代码，帮助开发者和安全工程师在部署前发现并修复合约漏洞。关键词：智能合约安全，符号执行，漏洞检测，Mythril，以太坊安全，重入攻击，整数溢出，安全审计，区块链安全，EVM字节码分析。

智能合约 0 次安装 1 次浏览 更新于 2/23/2026

name: mythril-symbolic description: 使用Mythril进行符号执行分析，深度检测智能合约中的漏洞。支持配置交易深度、超时设置和生成概念验证利用代码。 allowed-tools: Read, Grep, Write, Bash, Edit, Glob, WebFetch

Mythril 符号执行技能

通过符号执行进行深度漏洞检测，使用Mythril——一个针对EVM字节码的安全分析工具。

功能

  • 符号执行：配置并运行符号执行分析
  • 交易深度控制：为复杂的交互设置合适的深度
  • 追踪分析：解释符号执行追踪
  • 整数问题：检测溢出/下溢路径（Solidity 0.8之前版本）
  • 状态分析：通过状态变更分析发现重入漏洞
  • 断言检测：识别断言失败和边界情况
  • PoC生成：生成概念验证利用输入

安装

# 通过pip安装
pip install mythril

# 或使用Docker（推荐）
docker pull mythril/myth

# 验证安装
myth version

基础用法

分析源代码

# 分析单个文件
myth analyze Contract.sol

# 指定Solidity版本分析
myth analyze Contract.sol --solv 0.8.20

# 分析特定合约
myth analyze Contract.sol:MyContract

分析字节码

# 分析已部署的合约
myth analyze -a 0x<地址> --rpc <rpc_url>

# 分析字节码文件
myth analyze --bin-runtime contract.bin

配置选项

交易深度

# 默认深度 (2)
myth analyze Contract.sol

# 为复杂交互增加深度
myth analyze Contract.sol --execution-timeout 300 -t 3

# 深度分析（较慢）
myth analyze Contract.sol --execution-timeout 600 -t 4

超时设置

# 设置执行超时（秒）
myth analyze Contract.sol --execution-timeout 300

# 设置求解器超时
myth analyze Contract.sol --solver-timeout 10000

# 快速扫描
myth analyze Contract.sol --execution-timeout 60 -t 2

模块选择

# 运行特定模块
myth analyze Contract.sol --modules ether_thief,suicide

# 可用模块
# - ether_thief
# - suicide
# - integer_overflow/underflow
# - delegatecall
# - arbitrary_write
# - state_change_external_call

输出格式

标准输出

myth analyze Contract.sol

JSON输出

myth analyze Contract.sol -o json > report.json

Markdown输出

myth analyze Contract.sol -o markdown > report.md

JSONV2（详细）

myth analyze Contract.sol -o jsonv2 > detailed.json

漏洞检测

重入检测

Mythril通过追踪以下内容检测重入漏洞：

  • 外部调用
  • 调用后的状态变更
  • ETH转账
==== 外部调用至用户提供地址 ====
SWC ID: 107
严重性: 低
合约: Vulnerable
函数名: withdraw()
PC地址: 1234
预估Gas用量: 2500 - 10000
类型: 信息性
...

整数溢出/下溢

==== 整数溢出 ====
SWC ID: 101
严重性: 高
合约: Token
函数名: transfer(address,uint256)
PC地址: 567
预估Gas用量: 3000 - 5000
函数中可能存在整数溢出...

无保护的自毁

==== 无保护的自毁 ====
SWC ID: 106
严重性: 高
合约: Vulnerable
函数名: kill()
任何发送者都可能触发自毁...

高级用法

混合执行（Concolic Execution）

# 尽可能使用具体值
myth analyze Contract.sol --strategy dfs --execution-timeout 300

自定义约束

# 使用约束文件进行分析
myth analyze Contract.sol --constraints constraints.json

状态空间剪枝

# 限制状态爆炸
myth analyze Contract.sol --max-depth 30 --call-depth-limit 3

CI/CD集成

GitHub Actions

name: Mythril分析
on: [push]

jobs:
  mythril:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3

      - name: 运行Mythril
        uses: docker://mythril/myth
        with:
          args: analyze /github/workspace/contracts/*.sol --solv 0.8.20

自定义脚本

#!/bin/bash
for file in contracts/*.sol; do
    myth analyze "$file" --solv 0.8.20 -o json > "reports/$(basename $file .sol).json"
done

结果解读

严重性等级

等级 描述 行动建议
高 关键漏洞 立即修复
中 潜在问题 调查核实
低 次要问题 考虑修复
信息性 代码质量 可选修复

SWC注册表

SWC ID 名称 描述
SWC-101 整数溢出 算术溢出
SWC-104 未检查的返回值 忽略返回值
SWC-106 无保护的自毁 可访问的自毁
SWC-107 重入 调用后状态变更
SWC-110 断言违规 可达断言
SWC-116 时间戳依赖 区块时间戳使用

流程集成

流程 目的
smart-contract-security-audit.js 深度漏洞分析
smart-contract-fuzzing.js 与模糊测试互补
invariant-testing.js 属性验证

与其他工具对比

工具 技术 速度 深度
Mythril 符号执行 慢 深
Slither 静态分析 快 表面
Echidna 模糊测试 中等 中等
Certora 形式化验证 慢 最深

最佳实践

  1. 从快速扫描开始，根据需要增加深度
  2. 使用Docker确保环境一致性
  3. 在CI上运行以实现自动化安全检查
  4. 与静态分析（Slither）结合使用
  5. 报告前手动验证发现的问题
  6. 使用适当的Solidity版本标志

故障排除

内存不足

# 增加超时，减少深度
myth analyze Contract.sol --execution-timeout 600 -t 2

求解器超时

# 增加求解器超时
myth analyze Contract.sol --solver-timeout 30000

编译错误

# 指定Solidity版本
myth analyze Contract.sol --solv 0.8.20

# 使用特定编译器
myth analyze Contract.sol --solc-json solc.json

另请参阅

  • skills/slither-analysis/SKILL.md - 静态分析
  • skills/echidna-fuzzer/SKILL.md - 基于属性的模糊测试
  • agents/solidity-auditor/AGENT.md - 安全审计员
  • Mythril 文档