Slither 与 Manticore 从零到报告：智能合约测试覆盖率避坑记

Slither 与 Manticore 从零到报告：智能合约测试覆盖率避坑记

【免费下载链接】publicationsPublications from Trail of Bits项目地址: https://gitcode.com/GitHub_Trending/pu/publications

2016 年 The DAO 被一个重入漏洞掏空，事后复盘发现那条"再次进入"的分支，测试里一次都没走到过。智能合约测试覆盖率要回答的正是：你的用例到底盖住了多少条真实路径。Trail of Bits 的 publications 仓库里沉淀了 Slither 与 Manticore 的一线演讲和工作坊材料，本文按"装好 → 首扫 → 深扫 → 出报告"的顺序，把整套流程走一遍。

装好 Slither，先扫出静态底稿

第一遍排查建议交给静态分析：快、零配置，还能在代码进评审前就把可疑点标出来。装法和首扫各占一行：

pip install slither-analyzer slither ./contracts/MyToken.sol

它的原理是把 Solidity 先翻译成 SlithIR 中间表示（Slither 自家的 IR，可理解为"合约的中间语言"），再在其上跑污点追踪等分析，命中精度比纯正则匹配高不少。官方材料称内置 20 多个开箱即用的安全检测器，另有若干 gas 优化类检查，想快速上手 Slither，这份 EthCC 演讲是最好的入门材料：Slither 官方演讲（EthCC 2019）

踩过的两个坑，分享给你：

• 误报不用硬扛，在对应代码行上方写// slither-disable-next-line压制单条告警，别图省事整个关掉检测器
• 报告里标红的 public 函数单独记一份清单——它们就是下一轮动态验证的重点对象

静态扫完，动态验证做了吗

静态分析只能说"这里像问题"，能不能真的被触发，得让代码实际跑一遍。Manticore（符号执行工具，白话：不靠猜输入，而是用符号变量把每条分支的条件解出来）负责这一步。装法同上，pip install manticore，最小脚本如下，可以当作 Manticore 符号执行教程的起点：

from manticore.ethereum import ManticoreEVM m = ManticoreEVM() c = m.solidity_create_contract("MyToken.sol") m.run()

跑完它会列出所有可达状态，每个状态附注"什么输入能走到这里"。下图来自仓库内一场讲状态搜索的演讲：


红框表示"value==1"这条路径被判定可达——这类"跑得通但没人测过"的状态，就是覆盖率缺口最直观的样子。两处常见卡点：

• 路径爆炸导致跑不完：给探索深度设个上限，先让主流程收敛，再逐步放开
• 想系统练手：Devcon 4 工作坊目录里带完整练习和 API 讲解，Manticore API 手册 值得通读

出报告：把两份结果合进 CI

工具跑完不算完，结果要能沉淀、能被复查。Slither 支持导出机器可读格式（JSON/SARIF），配合 Manticore 的状态清单，评审时就能指着具体路径讨论。流水线里加三步即可：

- run: pip install slither-analyzer manticore - run: slither . --sarif-out slither.sarif - run: manticore tests/sym_token.py

顺序别反的经验：先静态后符号，静态结果当线索、符号结果当结论，两边对不上的条目优先人工复核。

下一步行动清单：

• 给现有合约跑一遍slither，把检测器报告贴进 PR 描述
• 挑一个 public 资金函数写 Manticore 脚本，记录可达状态数
• 把上面流水线三行合进 CI，让覆盖率缺口在合并前暴露

延伸阅读

• 用 Manticore 与符号执行找合约 Bug 工作坊（Devcon 4）
• 智能合约常见缺陷论文（FC 2020）
• 用 Slither Python API 写自定义检查

【免费下载链接】publicationsPublications from Trail of Bits项目地址: https://gitcode.com/GitHub_Trending/pu/publications