本文深入探讨了形式验证在智能合约中的重要性,驳斥了关于形式验证的多种误解,强调其在代码开发过程中及早介入的重要性,以及如何提高智能合约的安全性。形式验证不仅能帮助发现安全漏洞,还能通过清晰的规范来保障代码的正确性。
文章讲述了 Notional Finance 系统中出现的一个漏洞,该漏洞由于不正确的形式化验证不变量导致。原本旨在防止资产重复的错误不变量实际上是空洞的,无法发现漏洞。随后通过更正后的简单不变量成功检测到该漏洞,并提出了改进规范安全性的措施,包括审计规范、漏洞赏金、技术检查和集成测试工具,以提高代码安全性和规范的准确性。
本文介绍了SushiSwap的Trident协议在开发过程中发现的一个漏洞,以及修复这一漏洞的方法。文章详细描述了如何通过确定系统的不变性、使用自动化验证工具查找具体的违规场景,并利用这一场景实施攻击。最终,SushiSwap通过调整计算用户应得代币的方式来修复该漏洞。