学习不变量测试 第一天

• 原文链接：https://getrecon.substack.com/p/first-day-at-invariant-school
• 译者：AI翻译官，校对：翻译小组
• 本文永久链接：learnblockchain.cn/article…

从 0 到 1 开始不变量测试

模糊测试领域概览

随着使用不变量测试通过模糊测试和形式化验证来发现 Solidity 合约中隐藏 bug 的方法越来越流行,许多人渴望开始但不知从何下手。在这篇文章中,我们将看到评估不变量只是另一种形式的测试,需要一些额外的设置。

要开始不变量测试,你需要了解两个独特的关键细节:

1. 搭建脚手架（Scaffolding）

2. 定义不变量

搭建脚手架是添加必要的函数和系统设置的过程,允许模糊器在你的合约上执行随机调用序列。使用这个设置,我们定义不变量,这些是关于系统应该始终为真的陈述。

模糊器将使用你的脚手架来寻找一个具有特定参数的调用序列,使得你定义的任何不变量不成立。如果模糊器找到这样的序列,那么你很可能存在 bug。

在这篇文章中,我们将看到如何为一个仓库搭建脚手架,并通过评估我们定义的不变量来体验模糊测试的威力。

让我们开始模糊吧。

要建造房子你需要脚手架

在我们实际执行不变量测试之前,我们需要一些东西让它们站立起来,一种让它们钩入我们的系统并操纵其状态的方法。

这是过程中最不迷人和最重复的部分,这就是为什么我们在 Recon 构建的第一个工具可以帮助解决这个问题。我们的 Builder 为你提供了一种自动化的方法,可以将系统合约中所有公开可见的函数添加到脚手架中。你还可以获得所有必要的辅助合约,以使用标准化格式保持测试套件的组织性和易维护性。

Echidna、Medusa 和 Foundry 在设置不变量测试的要求上各不相同。这意味着我们需要一个标准接口来允许我们使用这三种工具,这就是我们从 Chimera 框架 获得的,Builder 会自动将其添加到我们的设置中。

理论上,上述每个不变量测试工具的工作原理是用随机值调用合约函数,并验证定义的不变量是否成立。然而在实践中,由于用随机值调用函数的过程计算密集,为了更好地分配有限的计算资源,选择实际修改状态变量值的特定入口点(非 view 函数)至关重要。

构建测试脚手架

现在我们将介绍如何使用 Builder 为 这个简化的仓库 中的现有 Foundry 项目附加不变量测试脚手架(harness)。

在我们的示例中,我们将使用 Trail of Bits 的 Echidna 模糊器,因为它经过实战检验并被广泛采用。但我们从 Builder 获得的设置也适用于 Medusa 和 Foundry 不变量测试。

要使用 Builder,我们只需要在 Add Repos 标签页的表单中粘贴 GitHub 仓库的链接,然后点击 Start Job。

Add Repos 页面上添加公共仓库的表单。

在创建的Job中,Recon Builder 将抓取仓库中所有合约的 ABI,并查找公共的非 view 函数。

这一步应该适用于大多数公共 Foundry 仓库,但如果你正在使用自己的仓库并且难以构建,请检查它是否属于 这篇文章 中描述的非标准仓库类别,并按照其中描述的后续步骤进行构建。如果你仍然遇到困难,请在 我们的 discord 上联系我们的团队

Job 完成后,我们的仓库将出现在 Build Your Handlers 标签页中,在那里我们选择我们想要允许模糊器用作系统入口点的函数。

Build Your Handlers 页面上的切换按钮让我们选择要添加到 TargetFunctions 合约中的合约和函数。

对于我们的示例,我们将选择 Counter 合约中唯一两个公开的、改变状态的函数(increment 和 setNumber),这给我们一个如下所示的 TargetFunctions 合约:

因为这是一个简化的示例,我们不需要担心这些目标函数的覆盖率(达到所有代码路径),因为我们的合约逻辑很简单,模糊器使用完全随机的输入就可以轻松达到所有路径。

要在我们的仓库中使用目标函数,我们需要使用 Download all files 按钮从 Build Your Handlers 页面下载上述合约以及其他辅助文件。

Build Your Handlers 页面顶部的按钮。

我们下载的其他文件处理了所有必要的测试设置和继承。

现在剩下的就是按照 Installation Help 页面上的步骤添加和管理必要的依赖项。

点击 Download all files 后,按照这些步骤将下载的文件和依赖项添加到你的仓库中。

按照这些步骤后,我们可以使用 forge build 编译我们的仓库,以确保所有步骤都正确执行。如果你的仓库无法编译,请尝试重复上述步骤或查看 这篇文章 的常见构建问题部分。

现在我们已经完成了测试不变量的一半工作!

定义不变量

有了目标函数的脚手架,我们就拥有了模糊器开始调用我们系统所需的一切,这样它就可以像用户或攻击者一样改变状态。

定义不变量的更有趣的部分是我们在代码中对系统做出断言,并允许模糊器验证该陈述是否对多个测试用例成立。

我们使用文档和注释等方式来定义系统的不变量,这些不变量概述了系统的预期行为,然后我们将其与系统的实际行为进行比较。

在我们的例子中,看一下系统中唯一的合约(Counter):

示例仓库中 Counter 合约的实现。

从 setNumber 函数上方的 NatSpec 注释中,我们可以看到有一个隐含的假设:"number 变量永远不能被设置为 0"。

知道不变量是一个关于系统的陈述,它应该始终为真,通常定义了应该始终发生或永远不应发生的行为,我们可以使用这个简单的英语陈述作为我们第一个系统不变量的定义。

我们在使用 Recon Builder 时为我们创建的 Properties 合约中定义了这个不变量:

为我们的 Counter 合约定义的不变量的代码实现。

这个不变量被定义为一个 Echidna 布尔属性;查看这个 readme 以了解更多关于 Echidna 支持的测试模式以及如何定义它们。

Echidna/Medusa 将在每次调用我们的 TargetFunctions 合约中定义的函数之后测试这个不变量,方法是检查函数的返回值。如果 crytic_counter_never_zero 函数返回 true,则意味着该不变量对于给定的调用成立,如果返回 false,则意味着模糊测试器已经找到了一个打破不变量的调用序列, 并将随后通过控制台中的日志显示这一点。

因为模糊测试器可以使用不同的测试模式,我们需要打开正确的模式,以便模糊测试器专门检查布尔属性。对于 Echidna 来说,只需要将 testMode 更改为 "property",如 echidna.yaml 配置文件中所示:

Recon Builder 生成的配置文件,测试模式已切换为 "property"。

开始运行

我们现在拥有了让模糊测试器通过尝试使用随机输入调用我们的 TargetFunctions 来测试我们定义的不变量是否成立所需的一切。这是一次模糊测试运行或作业,也是模糊测试魔法发生的地方。

在运行之前,值得注意的是,Recon Builder 创建的合约的继承结构将使我们所有的目标函数看起来都是在 CryticTester 合约的实例上调用的,但这个合约实际上只是作为入口点,底层实际调用的合约是 TargetFunctions 合约中调用的那些,在我们的例子中是 Counter 合约。

要启动我们的模糊测试器,我们可以在 cd 到仓库根目录后使用 CryticTester 合约中定义的以下命令:

    echidna . --contract CryticTester --config echidna.yaml

这将执行 50,000 次测试,这是 Echidna 的默认 testLimit,每次测试都会尝试不同的目标函数调用组合和不同的输入。

因为我们的测试合约逻辑非常简单,Echidna 能够在几秒钟内找到一个导致 crytic_counter_never_zero 不变量测试返回 false 的调用序列,我们可以在控制台中看到输出的调用序列:

有许多不同的调用序列可以打破不变量,每次运行模糊测试器时可能会生成不同的调用序列,你的可能与图片中显示的不完全匹配。

有了一个打破属性之一的调用序列,我们可以使用 Recon reproducer 工具将调用序列转换为 Foundry 单元测试。将这个单元测试添加到我们的仓库中,然后允许我们使用 Foundry 提供的所有工具进行更好的调试,帮助我们识别问题的根源。

在我们的例子中,我们可以使用单元测试更仔细地查看我们所针对的 Counter 的逻辑,可以看到 _incrementHelper 函数打破了我们在定义的不变量中做出的假设,因为它允许 number 变量被设置为 0。

总结

在本文中,我们看到了如何使用 Recon Builder 工具来搭建我们的不变量测试,这样我们就不必对测试设置做出设计决策。

Builder 允许我们轻松识别仓库中所有合约中的所有公共/外部状态改变函数,并决定我们想要将哪些添加到测试套件中。如果没有这个工具,我们就需要手动浏览我们感兴趣的合约,并决定如何构建我们的测试套件,以便模糊测试器可以访问这些状态改变函数。

接下来,我们看到了如何首先用简单的英语定义系统的不变量,使用我们从注释和文档中收集的关于系统应该如何工作的知识。然后,这被转换成一个易于理解的不变量(使用 Echidna 布尔属性格式),模糊测试器将在每次调用我们的目标函数后检查这个不变量。

如果模糊测试器找到一个导致定义的不变量函数返回 false 的调用序列,它将在终端窗口的日志中输出一个破坏性的调用序列,这可以用来识别破坏不变量的原因。

在系统上定义不变量测试套件的一个巨大好处是,它允许我们持续检查代码库中的任何变化是否符合现有的不变量。这对于缓解措施特别有帮助。

在上面的例子中,你可以尝试对 Counter 合约进行修改,使其真正符合我们为其定义的不变量,然后尝试对其运行测试。你能让所有的测试都通过吗?

非常感谢 @alcueca 为本文提供的编辑帮助和反馈!

我是 AI 翻译官，为大家转译优秀英文文章，如有翻译不通的地方，在这里修改，还请包涵～