利用形式验证在更短时间内捕获棘手的漏洞

在智能合约开发日新月异的领域，确保代码安全至关重要。然而，衡量安全增强或安全服务的有效性仍然是一项难以捉摸的挑战。形式验证（Formal Verification，FV）竞赛提供了一种可测量且有效的方法，通过将形式验证的深度与社区的广度相结合，来提高代码安全性。

代码安全信心的核心

任何安全服务的主要目标都是简单明了的：增强智能合约的安全性。然而，复杂性在于量化这种安全性。传统的安全审查可能不会识别任何问题，这可能导致对安全的错误感知。这种安全感建立在审计人员始终提供一致结果的信念上，而忽视了可变性和错误的人为因素。我们需要一种定量的方法来衡量特定安全服务的有效性。虽然这对于像安全审查这样手动和人的服务来说很困难，但对于编程方法（如测试、模糊测试和形式验证）来说则相对简单。

覆盖率

量化安全服务（如形式验证）有效性的一个关键方面是覆盖率的测量。覆盖率是一种众所周知的指标，通常用于评估测试的有效性，是量化安全服务影响的重要组成部分。在智能合约安全的上下文中，覆盖率帮助确定代码库经过全面测试和验证的程度，为人们提供有关合约安全性信心水平的洞察。

传统方法通常侧重于测试是否触及代码的某个部分，这并不一定保证测试能够捕捉到潜在的漏洞。为了解决这一不足，我们采用替代的方法来更有效地测量覆盖率。变异测试（Mutation testing） 是评估形式规范的主要方法，它直接回答了“如果这里有个漏洞，我们会发现吗？”这个问题。自动化方法使用开源工具如 Gambit 向代码中引入小的变更（变异体）。变异测试还可以通过手动添加复杂的漏洞，例如新增函数或对代码的较大更改来进一步提升，这样可以更全面地测试规范。通过这样做，我们能够更好地了解覆盖率并获得更强的保障。这种变异测试的方法特别适合与一些从更高层次或抽象角度查看代码的测试方法（如不变模糊测试和形式验证）结合使用。

尽管模糊测试和形式验证存在显著差异，但最关键的差别在于它们的方法。模糊测试从无到有，通过各种函数调用逐步构建一个通用环境。相比之下，形式验证则从一个任意状态开始，专注于将其细化到现实场景。这种差异使得形式验证更兼容于高级的变异测试。形式验证采取的更通用的方法允许更大的概括性，这意味着一个性质更有可能捕捉到复杂的变异体或多个相似的变异体。例如，检测代币供应量保存性质的属性可能会同时捕捉多个试图以不同方式操纵供应的变异体或者增加一种新的改变供应的方式的变异体。这种利用单一性质捕获更广泛漏洞的能力导致更有意义的测试，因为捕获变异体意味着类似的其他漏洞也会被捕获。

形式验证还支持各种附加的覆盖率测量方法。目前正在开发的一种特别有趣的方法是能够检查证明属性所需的代码部分，从而提供更深入的覆盖视角。此功能可能在未来的竞赛中使用。

持续形式验证努力的优势

虽然手动代码审查在智能合约安全生态系统中占有一席之地，但长期坚持形式验证的努力在长远中可能产生更大的影响。这是由于两个关键因素：能够测量进展和通过明确表述所有假设持续吸引安全研究人员的参与。

形式验证的一个显著优势是能够通过覆盖率指标量化测量进展。正如谚语所说，如果你不能衡量它，你就不能改善它。形式验证覆盖率是安全性最好的测量指标之一，因为它直接评估规范在捕捉潜在漏洞方面的有效性。这种可量化的方面允许团队随着时间的推移跟踪进展，识别需要更多关注的领域，并最终在智能合约的安全性上达到更高的信心水平。

此外，形式验证迫使所有隐含假设被明确表述，从而保持安全研究人员的参与。在手动代码审查中，研究人员通常依赖直觉和经验来识别潜在问题。然而，如果某些假设未被明确考虑，这种方法可能导致漏洞被忽视。而形式验证则要求研究人员明确规定他们的假设。如果有任何假设保持隐含，反例将在验证过程中出现，促使研究人员完善他们的规范。

这种明确假设的过程也迫使验证过程更加彻底。例如，考虑有趣的输入（例如，发送者是合约还是不假设变量之间的关系），研究人员被迫更彻底地检查这些代码部分。这种增加的审查使他们更有可能捕捉到在手动审查中可能被忽视的漏洞。

总之，长期的形式验证努力可以通过利用覆盖率指标和持续吸引安全研究人员而产生巨大的影响。通过利用这些优势，团队可以在智能合约中实现更高水平的安全性，并在时间内维持这一安全性。然而，我们的目标不是在几个月内确保代码安全；我们需要在几周内完成。这就是社区的力量和形式验证竞赛效率发挥作用的地方。

在不降低质量的情况下压缩时间

形式验证竞赛提供了一种强有力的方法，能够在不降低结果质量的情况下压缩彻底验证代码所需的时间。通过利用社区的集体知识和创造力，这些竞赛通过可测量的方式实现代码安全的快速提升。

典型的竞赛以基本设置开始，包括 Prover 工具 的配置和一些示例属性。参与者在他们的私有代码库中工作，以验证代码，并在比赛结束时与评委分享。竞赛结束时，向代码库引入未知的变异，代表潜在的漏洞。这些变异作为评估参与者验证工作有效性的方式，最难发现的漏洞被赋予最高价值。一旦所有评估完成，最佳规范将用于设置 CI/CD 以便持续验证最强的属性。

竞赛格式鼓励参与者进行创造性思考和从不同角度接触代码。通过迫使参与者明确表述和验证他们的假设，并考虑广泛的潜在漏洞，形式验证竞赛有助于发现稀有的漏洞并增加代码安全性的信心。

为了确保最高质量的结果，表现优秀的参与者被称为 FV 英雄，他们将在竞赛结束时被邀请验证所有变异体是否被强属性捕获。这一额外环节增加了一层审查并帮助维护验证过程的完整性。有关 FV 英雄计划的更多细节将在即将发布的文章中介绍。

结论

通过形式验证实现的高代码覆盖率，结合变异测试和其他先进方法，这是量化和提高代码安全性的一种重要方式。通过在短时间内提供可测量的代码安全性提升，FV 竞赛成为协议智能合约安全工具包中的战略补充。这种方法符合众包解决方案的日益增长趋势，利用社区的集体智慧和效率，实现曾经认为只有通过漫长的独立努力才能实现的目标。FV 竞赛不仅仅是为了更快地发现漏洞；它们的目的是为代码安全建立强大的信心。

• 原文链接： certora.com/blog/communi...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～