DeFi 安全 101 - 从模糊测试到形式化验证

视频 AI 总结： 该视频主要讲解了如何从模糊测试（Fuzzing）过渡到形式化验证（Formal Verification），并对比了两者的异同。核心观点是，模糊测试和形式化验证都是发现智能合约漏洞的工具，但形式化验证能提供更强的保证。视频通过一个计算二进制数中“1”的个数（pop count）的例子，以及一个简单的 Vault 合约的例子，演示了如何使用 Certora 的工具进行形式化验证，并强调了在智能合约开发中尽早同时使用这两种方法的重要性。

视频中提出的关键信息：

• 模糊测试 (Fuzzing)：通过生成大量随机输入来测试代码，寻找违反预设属性的情况。虽然易于上手，但覆盖范围有限，只能提供概率性的保证。
• 形式化验证 (Formal Verification)：通过数学证明来验证代码是否完全符合规范。可以覆盖所有可能的输入，提供更强的保证，但学习曲线较陡峭。
• 不变性 (Invariants)：在合约的所有状态下都必须保持为真的属性。形式化验证可以用来证明不变性在合约的任何状态下都成立。
• Certora Prover：Certora 的形式化验证工具，可以将代码和规范编译成逻辑公式，并使用求解器来验证公式的有效性。
• CVL (Certora Verification Language)：Certora 的验证语言，用于编写形式化规范。
• Solvency：一种重要的 Vault 合约属性，指总的 shares 数量小于等于总的 tokens 数量。
• 尽早使用：建议在智能合约开发的早期阶段就开始使用模糊测试和形式化验证，以便尽早发现并修复漏洞。