永不停息地改进你的不变性测试

  • Recon
  • 发布于 12小时前
  • 阅读 46

本文讨论了Recon团队如何改善Centrifuge现有的不变性测试套件,主要通过引入最佳实践以简化测试过程并提高代码质量。这些实践包括专门使用断言测试、实现ActorManager、简化无状态测试和采用归纳法简化属性检查,以及设置Fork测试环境,结果揭示了一个之前未知的边界情况。

在我们提出使用新开发的最佳实践改善他们的不变量测试套件后(之前在 第1部分第2部分 讨论过),Centrifuge 团队很快接受了这一提议,期待这将主要帮助他们通过捕捉任何可能偶然引入的错误来编写更清晰的代码。

结果证明,这些新的最佳实践帮助发现了一个尚未被检测的边缘情况。

我们进一步将这些最佳实践浓缩为 create-chimera-app 2,你可以将其作为你模糊测试套件的起点。

在这篇文章中,我们将讨论我们为什么开发这些最佳实践以及如何使用 Centrifuge 作为示例在自己的模糊测试套件中实现它们。

仅使用断言

在 Recon,我们现在只在 Echidna 和 Medusa 中使用断言 测试模式。这个改变使得管理属性变得更加容易,因为我们不再将 布尔属性断言属性 混合。这一改变简化了我们编写属性的方式,同时减少了设计决策并降低了思维负担。

Echidna 还只能同时测试一种模式。因此,如果你还想使用布尔属性,就需要运行多个测试。这就是我们选择仅使用一种属性类型的原因。

在 Centrifuge 代码库中实施这些更改相对简单,我们将布尔属性更改为:

作为布尔属性的 invariant_global_1 属性的先前实现。

改为简单的断言属性:

使用来自 Chimera Assertion 合约的断言实现同一属性的新版本。

这还需要更改 echidna 配置通常用来检测布尔属性的 前缀,该前缀先前设置为“invariant”,现在已恢复为默认的“echidna”。

将这些公共函数与断言结合使用,让模糊测试器可以在任何其他目标函数之后随机调用它们。这使它能够像更高效的布尔属性一样工作,因为在每次调用目标函数后不会进行检查。如果存在一种破坏性的调用序列,我们无需在每次函数调用后检查属性。相反,在正确的破坏性调用序列之后的随机调用仍然会破坏属性并提供一个重现示例。

添加 ActorManager

Actor 允许你以用户的方式决定与你的测试套件交互的地址数量。之前,没有标准化的处理方式,大多数人(包括我们自己)为每个套件实现了不同的解决方案。

我们发现这个问题不断发生,并增加了我们的设置时间。因此,我们创建了一个 ActorManager 合约来跟踪模糊测试设置中的所有 actors。在创建初始测试套件时,认为跟踪多个 actors 所带来的额外开销不值得提供额外的状态空间探索,但现在使用 ActorManager 后,我们可以通过简单的更改来实现这一目标。

ActorManager 的实现,使得更容易地跟踪模糊测试套件中的所有 actors。

通过实现 ActorManager,这个合约继承于 Setup 合约,我们得以在 setup 函数中直接添加多个 actors:

_addActor 函数将新的 actors 添加到 ActorManager 合约的跟踪中。

这还使我们能够确保被测试的属性仅针对我们设置的 actors 进行评估。我们通过在对目标函数处理程序的每次调用中直接使用 actors 来做到这一点,使用 useActor 修饰符来伪装当前 actor。我们现在还会将当前 actor 传递给任何需要传递用户地址的函数参数:

使用 useActor 修饰符让模糊测试器以 _getActor 返回的当前设置的 actor 的身份调用每个目标函数处理程序。

然后,我们可以遍历所有 actors,并检查属性仅对他们成立,因为其他地址不可能以用户的身份与系统进行交互:

仅向我们测试设置中的 actors 铸造的属性示例。

由于有了更多的 actors,模糊测试器能够揭示一个以前未知的边缘情况。下面的奖杯部分对此进行了更多讨论。

由于有了更多的 actors,模糊测试器能够揭示一个以前未知的边缘情况。

简化无状态测试的撤回

之前,我们实现了一个 ERC7540CentrifugeProperties 合约,旨在测试在 ERC7540 奖池 标准实现中的 Centrifuge 特有性质。

因为这些属性检查涉及状态改变操作,所以它们包含对 _doTestAndReturnResult 函数的调用,该函数允许合约中定义的函数作为 无状态测试 通过撤销调用目标函数所做的任何状态更改。

erc7540_9_withdraw 属性执行的提款操作我们不希望在其他调用中保持。

erc7540_9_withdraw_call_target 调用上面定义的属性,并使用 _doTestAndReturnResult 函数撤销状态更改。

通过撤销状态更改,这些函数将不会为 全局属性 的破坏性调用序列作出贡献。这是因为它们所包含的状态更改会使得阅读破坏回调序列变得困难,我们称之为“故事”。这将它们的用途孤立,仅限于作为特定属性更复杂的有状态模糊测试手段。

对于上述测试,这意味着我们可以检查一个 actor 始终能够提取他们的全部余额。但我们不希望这能影响我们的“故事”,因为这意味着我们会将对其他标准目标函数的调用与 erc7540_9_withdraw_call_target 的调用混合在一起,使得理解调用序列中实际发生的事情变得困难。

vault_withdraw 目标简单地执行带有模糊输入的状态更改操作,且其名称描述了其功能,使得理解“故事”中的内容变得更简单。

最近发现任何断言测试可以通过在函数调用结束时简单撤销而更容易地实现无状态,因此 ERC7540CentrifugeProperties 被重构为实现以下修饰符:

statelessTest 修饰符在允许调用的目标函数被加入到基线中以提高覆盖率的同时撤销状态更改。

这使得测试实现更容易阅读和维护:

简化的测试实现。

使用归纳法简化属性

在原始属性实现中,许多使用了用于跟踪系统状态的幻影变量。

原始属性实现,其中 sumOfClaimedRedemptionsmintedByCurrencyPayout 是幻影变量。

然而,我们意识到这类实现往往会通过创建需要始终在其各自处理程序内正确更新的幻影变量增加不必要的复杂性。

这些幻影变量必须在多个处理程序内更新,并跟踪的值实际上是“幻影”,它们并不存在于系统中,而是源自其 期望 状态更新。

现在我们更倾向于首选可以通过归纳法实现的属性,以证明同样的事情,这涉及在给定操作之前和之后直接读取合约的状态。

在通过归纳法证明一个属性时,我们首先需要证明基本情况为真,在我们的案例中,这是在对合约进行任何状态改变操作之前,当模糊测试器可以调用任一全局属性。然后,我们需要证明在归纳步骤中该属性对于任意状态改变操作(调用目标处理程序)也为真。

上述属性的一种实现示例如下:

重构的 invariant_global_2 属性的归纳实现。

在归纳实现中,我们证明对于任何不是调用 claimCancelRedeemRequestpendingRedeemRequest 的减少,escrow 将正确支付通过 actor 赎回的 trancheTokens 数额。

分叉测试设置

分叉测试设置在现有的不变量测试套件中的 setupFork 函数中添加。该函数仅覆盖 setup 函数中部署的合约,使用的是实际部署的值。

用在主网部署的合约和 actor 覆盖最初部署的合约和 actor。

这允许对 Ethereum 主网上的分叉链状态直接测试属性,除了治理模糊测试,允许模拟在 Centrifuge 链上执行的具有侧面效果的行为,然后在它们发生之前在以太坊主网上执行。这样,我们可以更准确地测试 Centrifuge 上是否存在任何逻辑会破坏主网上的假设,因为我们无法在两个链之间进行端到端的属性测试。

奖杯

正如上面提到的,当添加多个 actors 时,模糊测试器发现了一个边缘情况,下面的 Foundry 单元测试展示了这一点:

使用我们的 scraper tool 自动生成的重现器。

这个以前未知的边缘情况表明,请求者可以请求一种被冻结(被阻塞的)接收者的赎回。鉴于被冻结的接收者不得从系统中赎回,这颠覆了预期的功能,因此被 Centrifuge 团队解决。

下一步

为了更有效的分叉测试,下一步将是我们所称的治理模糊测试。这将允许在每次创建有效请求时运行该套件,因为 Centrifuge 使用异步奖池系统,其中请求必须首先在以太坊上创建,然后在 Centrifuge 链上得到批准,然后才能在以太坊上执行。这将允许验证部署合约上的最终履行结果是否导致任何属性破坏。

这是一种有趣的测试可能性,因为我们在初始审查中注意到由于 Centrifuge 链上的错误执行而产生的问题是很有可能的,因为这些行为是完全受信任的。因此,设置这些测试将允许我们系统地验证系统是否可能存在导致这种情况发生的状态。

由于标准的分叉测试设置无法满足我们的模型要求,我们仍然本质上通过请求的金额限制已履行的值,如下所示:

investmentManager_fulfillDepositRequest 函数模拟在 Centrifuge Chain 上执行消息,但依赖于可能会影响模糊测试器的受限值。

因此,仍然存在一个履行执行与我们的建模不符的可能性,从而可能破坏其中一个属性。在这种情况下,最佳的做法是针对从 Centrifuge 链收到的实际履行值进行测试,因为这是在部署系统中执行的内容。

结论

我们已经看到我们如何实施最新的模糊测试最佳实践,以改造 Centrifuge 现有的不变量测试套件,使其更简单、更健壮。

我们所做的更改包括:专门使用断言测试、实现 ActorManager、简化无状态测试、使用归纳法简化属性并创建分叉测试设置。

实施一个 ActorManager 使我们能够发现一个以前未知的边缘情况,证明了即使被测试的基础代码没有变化,不断改善现有测试的好处。

展望未来,Centrifuge 团队还可以实施治理模糊测试,从而给予他们更大的保证,即 Centrifuge 链上没有逻辑会破坏主网以太坊的假设。


如果你读到了这里,你重视你的协议的安全性。

在 Recon,我们提供基于不变量测试的精品审计。通过这一点,你可以同时获得两全其美——由一流研究人员完成的安全审计以及尖端的不变量测试套件。

听起来有趣吗,在这里与我们交谈


  • 原文链接: getrecon.substack.com/p/...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
Recon
Recon
江湖只有他的大名,没有他的介绍。