使用形式化验证在更短的时间内捕获棘手的错误

在智能合约开发这个不断发展的领域中，保护代码至关重要。然而，衡量安全性增强或安全服务的有效性仍然是一个难以捉摸的挑战。形式化验证（FV）竞赛提供了一种可衡量且有效的方法，通过结合形式化验证的深度和社区的广度来提高代码安全性。

代码安全信心的核心

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

覆盖率

量化形式化验证等安全服务有效性的一个关键方面是覆盖率的 measurement。覆盖率是一种众所周知的指标，通常用于评估测试的有效性，也是量化安全服务影响的关键组成部分。在智能合约安全的上下文中，覆盖率有助于确定代码库经过彻底测试和验证的程度，从而深入了解人们对合约安全性的信心水平。

传统方法通常侧重于测试是否触及代码的某个部分，这并不一定保证测试能够发现错误（如果存在）。为了解决这个缺点，我们采用替代方法来更有效地测量覆盖率。Mutation testing 是用于评估形式规范的主要方法，它直接解决了“如果这里存在错误，我们会发现它吗？”这个问题。自动方法使用开源工具（如 Gambit）在代码中引入小的更改（mutants）。通过手动添加复杂错误（例如，新函数或对代码的更大更改）可以进一步进行 Mutation testing，从而更稳健地测试规范。通过这样做，我们可以更好地了解覆盖率并获得更强的保证。这种 Mutation testing 方法与测试方法相结合特别有用，这些测试方法受益于采用代码的高级或抽象视图，例如不变性模糊测试和形式化验证。

虽然模糊测试和形式化验证有明显的区别，但最关键的区别在于它们的方法。模糊测试从一个空白状态开始，并通过各种函数调用逐步构建一个通用环境。相比之下，形式化验证从任意状态开始，并侧重于将其细化为现实场景。这种差异使得形式化验证与高级 Mutation testing 更兼容。形式化验证采用的更通用的方法允许更大的泛化，这意味着一个属性更有可能捕获复杂的 mutants 或多个类似的 mutants。例如，检查 Token 供应守恒的属性可能会捕获试图以不同方式操纵供应的多个 mutants，或者捕获添加一种更改供应的新方法的 mutant。这种用单个属性捕获更广泛的错误的能力会导致更有意义的测试，因为捕获 mutant 意味着也会捕获类似于它的其他错误。

形式化验证还支持各种额外的覆盖率测量方法。目前正在开发的一种特别有趣的方法是能够检查代码的哪些部分对于证明属性是必要的，从而提供更深入的覆盖率视图。此功能可能会在未来的竞赛中使用。

持续的形式化验证工作的优势

虽然手动代码审查在智能合约安全生态系统中占有一席之地，但从长远来看，在形式化验证方面的持续努力可能更具影响力。这是由于两个关键因素：衡量进度的能力以及通过明确声明所有假设来持续吸引安全研究人员。

形式化验证最显著的优势之一是能够通过覆盖率指标定量衡量进度。正如谚语所说，“如果你无法衡量它，你就无法改进它”。形式化验证覆盖率是对安全性最好的测量方法之一，因为它直接评估了规范在捕获潜在错误方面的有效性。这种可量化的方面使团队能够跟踪他们随时间的进展，识别需要更多关注的领域，并最终对智能合约的安全性更有信心。

此外，形式化验证通过强制明确声明所有隐式假设来保持安全研究人员的参与。在手动代码审查中，研究人员通常依靠他们的直觉和经验来识别潜在问题。但是，如果未明确考虑某些假设，此方法可能会导致忽略漏洞。另一方面，形式化验证要求研究人员指定他们的假设。如果任何假设保持隐含，则在验证过程中会出现反例，促使研究人员改进他们的规范。

这种明确声明假设也强制了验证过程的彻底性。例如，通过考虑有趣的输入（例如，发送者是合约或不假设变量之间的关系），研究人员被迫更彻底地检查代码的这些部分。这种增加的审查使他们更有可能发现可能在手动审查中被忽略的错误。

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

在不影响质量的情况下压缩时间

形式化验证竞赛提供了一种强大的方法，可以在不影响结果质量的情况下压缩彻底代码验证所需的时间。通过利用社区的集体知识和创造力，这些竞赛可以通过可衡量的方式快速提高代码安全性。

一个典型的竞赛从一个基本的设置开始，包括 Prover 工具 的配置和一些示例属性。参与者在其私有存储库中验证代码，并在比赛结束时与评委分享。在比赛结束时，未知的 mutations（代表潜在的错误）会被引入到代码库中。这些 mutations 用于评估参与者验证工作的有效性，其中最难找到的错误最有价值。一旦完成所有评估，就可以使用最佳规范来设置 CI/CD，以持续验证最强的属性。

竞赛形式鼓励参与者创造性地思考并从不同的角度处理代码。通过强制参与者明确声明和验证他们的假设，并考虑各种潜在的漏洞，形式化验证竞赛有助于发现罕见的错误并增强对代码安全性的信心。

为了确保最高质量的结果，在竞赛结束时会召集表现最佳的参与者，即 FV Heroes，以验证所有 mutants 是否都被强大的属性捕获。这个额外的阶段增加了一层审查，并有助于维护验证过程的完整性。在即将发布的文章中将提供有关 FV Hero 计划的更多详细信息。

结论

通过形式化验证实现的高代码覆盖率，通过 Mutation testing 和其他高级方法进行测量，是量化和提高代码安全性的主要方法之一。通过在很短的时间内提供可衡量的代码安全性增长，FV 竞赛是对协议智能合约安全工具包的战略补充。这种方法与众包解决方案的日益增长的趋势相一致，利用社区的集体智慧和效率来实现曾经被认为只有通过长期、孤独的努力才能实现的目标。FV 竞赛不仅仅是更快地发现错误；它们还在于在代码安全性方面建立强大的信心。

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