智能合约安全工具指南
solidity智能合同安全性
中级我们将使用三种独特的测试和程序分析技术:
- 使用 Slither 进行静态分析。通过不同的程序演示(例如控制流程图),同时对程序的所有路径进行模拟和分析。
- 使用 Echidna 进行模糊测试。 代码是通过伪随机生成的交易来执行的, 模糊器将尝试找到一个违反某个给定的合约特性的交易序列。
- 使用 Manticore 进行符号执行。 一种正式的验证技术,它将每个路径转换为数学公式,在此基础上可对最重要的约束加以检查。
每种技术都有优缺点,在特定情况下会很有用:
技术 | 工具 | 使用方法 | 速度 | 错误遗漏 | 误报 |
---|---|---|---|---|---|
静态分析 | Slither | CLI 和脚本 | 秒 | 中度 | 低 |
模糊测试 | Echidna | Solidity 属性 | 分钟 | 低 | 无 |
符号执行 | Manticore | Solidity 属性和脚本 | 小时 | 无* | 无 |
* 如果在没有超时情况下遍历所有路径
Slither 可以在几秒钟内分析合同,但是静态分析可能会导致误报,不太适合复杂的检查(例如算术检查)。 通过用于按钮访问内置检测器的 API 或用于用户自定义检查的 API 运行 Slither。
Echidna 需要运行几分钟,并且只会产生真阳性的测试结果。 Echidna 会检查用户提供的用 Solidity 编写的安全属性。 由于它的随机侦测的特性,它也许会错失一些 漏洞。
Manticore 进行的是“最大权重”分析。 像 Echidna 一样,Manticore 会验证用户提供的特性。 它需要更多的时间来运行,但它可以证明某个特性的有效性,并且不会报告误报。
推荐工作流程
从 Slither 的内置检测器开始,确保现在没有或以后不会引入简单的漏洞。 使用 Slither 检查与继承、变量依赖关系和结构问题相关的属性。 随着代码库的增大,可以使用 Echidna 来测试状态机更复杂的特性。 再次使用 Slither 开发专门用于那些 Solidity 不提供保护的自定义检查,比如防止某个函数被覆盖。 最后,使用 Manticore 对关键安全属性进行有针对性的验证,例如算术运算。