在开发过程中保护协议 - 从高级不变式到池排空漏洞

Trident 是 SushiSwap 即将推出的平台，旨在启动和运行流动性池，并管理与用户的互动；预计将处理数十亿资产。本文档描述了在其开发过程中发现的一个池 draining 漏洞，以及 SushiSwap 随后的修复。最重要的是，我们描述了 如何 发现了该漏洞，使用了一种可复现的方法 适用于任何 DeFi 池平台。该方法由三个步骤组成：

1) 制定系统的必须保持性质或要求（下面称为“守恒”或“规则”）

2) 使用 Certora 的自动化验证工具来查找违反守恒的具体场景 — 一组特定的池变量分配和一个违反该性质的操作

3) 利用新发现的场景来攻击系统。

Trident 协议的一些背景

这个漏洞涉及经济产品池（CPP）的自动化市场制造商 合约。在 CPP 中，流动性提供者（LP）存入两种类型的基础代币（Token0 和 Token1），以换取 LP 代币。然后，他们可以 销毁 LP 代币以重新获得与其所持有的 Token0 和 Token1 成比例的数量。

Trident 用户可以通过将某种类型的代币转账到池中并接收另一种代币的特定数量来 交换 一种基础代币为另一种基础代币。为了确定汇率，池返回足够的代币，以确保

(reserves0 ⋅ reserves1)ᵖʳᵉ =(reserves0 ⋅ reserves1)ᵖᵒˢᵗ

第一步：制定守恒

将 LP 代币销毁为基础代币的能力暗示了一个重要的守恒：如果存在任何 LP 代币（totalSupply 大于 0），则 reserves₀ 和 reserves₁ 不能为零（否则池无法生成基础代币）。更正式地说：

totalSupply = 0 ↔ reserves0 = 0

和

totalSupply = 0 ↔ reserves1 = 0

Certora Prover 允许我们在合约的规范中写入这个守恒：

第二步：查找违规

Certora 的 Prover 检查系统的每一个可能状态和每一个可能操作，并检查这个守恒将始终保持。如果有可能违反一个条件，证明者会产生一个具体示例，显示可能出错的地方。从那个反例中，可以找到他们程序的缺陷。

令我们惊讶的是，该工具显示 burn-single 操作违反了守恒。burn-single 操作结合了销毁和交换：它首先销毁 LP 代币以生成两种基础代币，然后将一种代币与另一种代币进行交换（仅产生一种基础代币）。

尽管 `swap` 和 `burn` 操作保持了守恒，但组合的操作存在缺陷，使恶意用户能够抽走池中的资产。

理解 burn-single 函数

要理解 burn-single 函数中的漏洞，我们需要了解 Trident 池的工作方式。Trident CPP 合约将池的储备跟踪为 reserve0 和 reserve1（分别对应 Token0 和 Token1）。如果基础代币在没有 CPP 合约干预的情况下被转移，则池持有的实际余额可能会大于存储的储备变量。Trident 将池的实际基础余额称为 balance0 和 balance1。

假设一个用户（Alice）决定使用 burn-single 销毁她的 LP 代币，请求仅以 Token₁ 作为回报（代码中为 TokenOut=Token₁，第 69 行）。让我们一步一步跟随代码：

1. [ 将 LP 代币转换为 Token0 和 Token1 ] 计算 Alice 应得的 Token0 和 Token₁ 的数量，分别称为 amount₀ 和 amount₁：

用户应得的某种代币的数量为当前池对该代币的余额乘以她在总 LP 代币供应中的份额。请注意，这个精确的计算在通过守恒测试的 burn 函数中出现。

2. [ 将生成的 Token0 转换为 Token1 ] Trident 计算 Alice 应获得的 Token1 数量，以交换 amount0 的 Token0。Token0 到 Token1 的转换由 `_getAmountOut` 函数定义，如下所示。由于步骤（1）从池中移除了 amount₀ 的 Token0 和 amount₁ 的 Token1，当前的储备为 reserve0-amount0 和 reserve1-amount1。Trident 根据新的储备值计算 amount₀ 的 Token0 在 Token1 中的价值：

该值会加入上述已经给予 Alice 的 amount₁（第 64 行），并转移给她（第 71 行）。

3. 要结束操作，更新池的储备：

未查看的问题

那么，可能会发生什么问题？记住储备可能小于余额。Certora Prover 构造了一个场景，显示了这些变量使用的一致性问题：虽然 amount₀ 和 amount₁ 使用余额进行计算，但它们是从储备中减去的（这个问题也由 Cristoph Michel 独立发现，正如 Sushi 向我们所说）。

假设在调用 burnSingle 之前，余额足够高，以至于：amount0=(liquidity/totalSupply)⋅ balance0=reserve0

（Prover 的具体分配为：balance0=10,000，liquidity=100，totalSupply=1000，reserve0=1000）

Alice 继续销毁她的 LP。请求在上述步骤 2 中以 Token₁ 获取该金额时，计算为：

_getAmountOut(amount0, 0, _reserve1 — amount1)

计算出的金额将为 reserve1 — amount1。总之，用户将获得全部的 reserve1。现在 reserve1=0，但 totalSupply > 0，破坏了守恒。

第三步：从破坏的守恒到合约利用

现在我们有了一个产生无效状态的具体操作，可以尝试利用这个违规行为来描述对池的完整攻击。

假设对手 Mallory 在 CCP 中有一些流动性。首先，必须达到状态 amount0=(liquidity/totalSupply)⋅ balance0=reserve0。正常情况下，池的余额等于其储备：每次用户操作后，储备都会更新为等于余额。如果存在差异，任何用户都可以利用差异获利。Mallory 可以通过以 Token0 大额闪电贷的方式达到该状态，然后将所有资金添加到池的 balance0。比如，考虑一个总锁定价值（TVL）为 100 万美元的池，其中 50 万美元在 Token0 中，占 50% 的余额，剩下的 50 万美元在 Token1 中。如果 Alice 拥有总电视的 1%，她必须为池提供额外的 445 万美元 Token0。

Mallory 接着继续销毁她的 LP 代币，请求以 Token1 获取该金额。结果她成功提取了所有 liquidity1。但 Mallory 如何偿还以 Token0 借来的贷款？

一般来说，程序员可能会依赖于系统的基本属性，并在不同的位置假设它们进行优化（而不是反复检查）。在这里，Swap 函数在检查 “仅一个” 储备大于 0 之前，依赖了我们的守恒：

Trident 认为，无论池是已初始化的，并且两者都不为 0，还是未初始化的，然后都为 0。在 Mallory 的攻击中，仅 reserve1 为 0，但第 194 行的要求仍然成立。

因此，为了完成攻击，Mallory 在零 reserve1 的池中交换单一 Token1。使用上述相同的 getAmountOut 函数，读者可以验证 Mallory 现在获取了池中的全部 reserve0。Mallory 可以随后偿还她的贷款。

总结一下，进行攻击时，Mallory 需要：

1. 以 Token0 获取闪电贷
2. 向 Balance0 添加大量资金
3. 使用 Token1 储备作为输出进行 burnSingle
4. 将单一 Token1 交换为 Token0 储备

SushiSwap 的修复

SushiSwap 迅速响应并进行了修复：在 burn-single 函数中使用储备而不是余额计算用户应得的代币数量。

结论

思考系统应满足的一般属性是推理 DeFi 系统正确性的有用方法，而无需推理具体的漏洞。这些属性不是系统特定的，不需要理解实现细节或枚举特定漏洞。形式验证可用于检查整个系统是否满足这些一般属性，并识别可利用的漏洞。

附录

getAmountOut:

完整的 burnSingle:

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