合约测试 - 如何定义不变性

如何定义不变性

如何实际定义可以拯救你免受漏洞的“不变性”

引言

不变性可以在你的智能合约部署之前发现关键漏洞，避免它们在生产环境中被人利用。在这方面，即使不是一个了解你系统所有潜在攻击向量的安全专家，仍然是可以实现的。

不变性测试是设定后无须干预的。它可以找到代码中难以发现的问题，并为你做繁重的工作。你只需要确保你已经正确地定义了不变性，这样模糊器就能找到漏洞。

在本系列的第一篇文章中，我们介绍了如何在示例代码库中使用Recon构建器搭建不变性测试框架。我们还定义了一个简单的不变性测试，以便反驳我们关于系统行为的主张。

本文将探讨不变性到底是什么。它将概述如何在ERC4626储蓄库上定义不变性。

首先，我们将专注于定义不变性的四种属性类型。然后，我们将查看ERC4626储蓄库的每种类型的示例。

这里是进行不变性测试的魔力开始的地方。我们可以对我们的代码库进行批判性思考，从而为理解代码实际执行的内容打下基础。

不变性究竟是什么？

在本系列的第一篇文章中，我们频繁提到这个术语，并大致定义为“关于系统的陈述应该始终为真”。但这到底意味着什么呢？

这意味着，借助智能合约系统和一些规范，我们可以使用不变性来定义它应该如何行为。我们可以设置界限，规定它应该做什么或不应该做什么。

属性与不变性密切相关，但它们的陈述仅在特定上下文中成立。例如，如果我们有一个ERC20代币：

• 不变性：用户余额的总和绝不应大于总供应量（totalSupply）。

• 属性：用户的余额只能在调用转账（transfer）和铸造（mint）函数后增加。

四种属性类型

由于属性在其定义上不那么限制，我们将讨论如何从属性的角度定义不变性。我们可以将不变性视为始终成立的属性。

在此演示文稿中，Certora列出了编写不变性时我们感兴趣的四种基本属性类型。

这些属性类型是：

• 有效状态（Valid States）

• 状态转换（State Transitions）

• 变量转换（Variable Transitions）

• 高级属性（High-Level Properties）

我们现在将看看定义这些属性类型的内容，并在下一节查看如何为储蓄库定义它们。

有效状态

智能合约是简单的状态机，合约的变量值定义其当前状态。类似地，系统中所有合约的变量值定义系统状态（system state）。

智能合约可能依赖于有效状态来执行其逻辑。我们测试系统，以确保它只停留在这些有效状态中。发现的任何无效状态都是可能导致意外行为的漏洞。

例子

在像Uniswap这样的协议中使用的著名AMM不变性是x*y = k，我们可以将所有不符合这一条件的其他状态定义为无效状态。因此，如果可以通过外部函数调用达到x*y != k的状态，这将暗示系统中存在一个漏洞。

由Uniswap xy=k不变性定义的曲线。来源：https://uniswapv3book.com/milestone_0/constant-function-market-maker.html

状态转换

如果我们已经确定了一组有效状态，如上所述，我们还可以为这些有效状态之间的转换定义正确的行为。除此之外，我们还可以添加额外的前置条件，以便仅在满足前置条件的情况下检查这些状态转换。

例子

在借贷协议中，用户在存入一些抵押品（前置条件）之前，不应该能够借取资金（属性）。

在这种情况下，状态转换是系统应该无法从用户没有借款头寸（borrow position）的状态转换到有借款头寸（borrow position）的状态，除非已满足已存入抵押品的前置条件。

这是借贷协议的一个关键属性。如果破裂，系统可能会破产并无法偿还所有贷方。

变量转换

正如我们已经提到的，系统状态由其变量的值定义。其中一些变量必须以某种方式行为。我们可以通过变量转换的属性概述这些变量的预期行为。

例子

在任何期望收取费用的协议中，收取的总费用应始终增加。我们可以在负责费用核算的变量上定义这样的属性。

这种属性的破裂可能意味着费用未被收取或可能被盗。

高级属性

高级属性描述了更广泛的系统行为。它们通常关联多个有形元素。相比之下，像上述提到的具体属性则为有形系统元素定义了预期行为。

例子

在一个ERC4626储蓄库中，每份股份的价格应仅在存入或提取操作时发生变化。

这个高级属性涵盖了变量转换和状态转换。将其定义为高级属性简化了实现，使得不再需要定义每个贡献其关系的复杂关系。

理解目标

既然我们了解了可以为任何系统定义的不同类型的属性，我们将看看如何在一个实际系统上做到这一点。第一步是了解系统的预期行为。

你作为开发者的知识或者文档将有所帮助。对于外部贡献者来说：READMEs、白皮书和NatSpec应该有助于概述系统应该如何行为。

了解系统应如何工作的并不需要深入到每个函数的实现细节。事实上，过早这样做通常会使你偏离轨道，影响你对不变性的定义。

把这视为不变性测试的黄金法则：你想要定义系统应该如何行为，而不是它实际是如何行为的。

在我们的示例中，我们将使用ERC4626储蓄库，因为它们在许多不同的DeFi项目中普遍实现，并且其属性由于是由标准定义而广泛适用。

定义属性

我们现在将使用上述定义的不同类型来定义属性。

请注意，这不是ERC4626储蓄库属性的完整列表。你将需要更多以确保实现该标准的合约按预期工作。

如果定义自己的属性似乎有些压倒，可以预约与我们的视频通话，我们可以帮助你定义它们。有经验于定义属性可以是测试有意义场景以发现漏洞与实现更复杂单元测试之间的决定性因素。我们将利用我们的经验，确保你的属性一流，配合我们的不变性写作练习！

有效状态

由于我们知道用户必须首先存入/铸币才能获得股份，我们知道：

1. 股份代币（share tokens）的总供应量必须 >= 每个用户账户的股份之和。

如果这个属性不成立，意味着股份没有完全由储蓄库的资产支持。这将导致破产。最后从储蓄库提款的用户将无法按资产获得他们的股份金额。

我们可以为储蓄库定义的另一个有效状态是：

2. 储蓄库中的总资产（totalAssets）必须可根据股份总供应量（totalSupply）进行赎回。

如果这不可能，则意味着会出现会计问题，当用户提款时可能会留下多余的碎款（dust amounts）在储蓄库里。

状态转换

我们知道用户必须存入资产来获得股份。为了确认这一点，我们可以定义一个属性。它表明：

1. 储蓄库的基础资产余额（underlying asset balance）必须随着铸币股份的比例增加。

这确保用户不能铸造的股份超过他们所存入的资产，这也会导致破产。

同样，我们可以声明：

2. 如果用户试图存入超出maxDeposit返回值的金额，则该函数应当回退（revert）。

这可能表明储蓄库的存款功能中使用的数学可能不安全，可能导致用户余额溢出，从而被错误报告。

变量转换

股份核算必须反映可赎回的基础资产。因此：

1. 当赎回股份时，储蓄库的 totalSupply必须按照被销毁股份的比例减少。

如果这个属性不成立，可能会导致股份价格计算错误，使得未被支持的股份导致新存款人的股份价格被抬高。

如果我们的储蓄库实现收取提款费用，我们可以声明：

2. 用于跟踪收取的费用的变量不得少于预期费用金额而增加。

这将意味着应用的费用数学存在不一致，导致协议收取的费用少于预期。

高级属性

对于我们的高级属性，我们将使用在定义中给出的同一属性作为例子。

1. 每份股份的价格在进行存入/提取操作外，不应更改。

如果我们添加一个将基础资产捐献给储蓄库的函数，这个属性将使我们能够通过捐赠少量资产来捕捉著名的股份价格通货膨胀漏洞。

我们还可以普遍声明，如果我们的储蓄库没有应用费用：

2. 存入/铸币和提取/赎回应该是对称的。

换句话说，对于一定存入的金额，如果相同金额被提取，应接收到原始存入的金额。

这种宽泛的规范可以让我们捕捉存入 -> 提取流中可能存在的任何不规则性。这些不规则可能表明在拥有复杂的存入/提取逻辑的储蓄库中存在潜在问题。

一旦我们将我们定义的属性作为代码，不变性工作的运行器将在我们运行工作时自动生成这个报告，这样我们就可以查看哪些属性成立，哪些属性破裂。

结论

上述示例展示了属性可以覆盖的行为范围。在多次定义属性后，你将开始对系统中需要定义哪些属性形成直觉。你对每个类别定义的参考将越来越少。

在本文中，我们探讨了其核心，不变性明确定义了我们的系统应该如何行为，通过明确允许我们测试其应该或不应该做的事情。然后我们看到如何将我们期望行为的定义缩小为：

• 属性 - 在特定条件下成立的陈述

• 不变性 - 在所有可能条件下成立的陈述

然后我们看到如何为ERC4626储蓄库定义这些属性类型。

在本系列的下一篇文章中，我们将看到如何在Solidity中实现一些这些属性，以便我们用模糊器进行评估。

在此期间，你能想到ERC4626规范所需的更多属性吗？你能否使用我们在第一篇文章中涵盖的技术实现这里定义的任何属性？

你是否相信不变性测试的力量，但不想自己做所有事情？与我们联系，我们可以帮助你实现不变性，在你做的每次提交中确保它们始终运行，并在开发pipeline的每一步保障你的代码安全。

致谢

本文中的属性定义取自Certora创建的该演示文稿。虽然他们在进行形式验证评估的背景下明确定义，但属性本质上与用于评估它们的方法无关。

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