|
|
| 名称 |
mythril-symbolic |
| 描述 |
使用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通过追踪以下内容检测重入漏洞：
==== 外部调用至用户提供地址 ====
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 |
形式化验证 |
慢 |
最深 |
最佳实践
- 从快速扫描开始，根据需要增加深度
- 使用Docker确保环境一致性
- 在CI上运行以实现自动化安全检查
- 与静态分析（Slither）结合使用
- 报告前手动验证发现的问题
- 使用适当的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 文档