保护SushiSwap的Trident：深入探讨DeFi漏洞与形式验证

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

1) 制定系统的必须保持的属性或要求（下面称为“不变量”或“规则”）

2) 使用 Certora 的自动验证工具找到一个违反不变量的具体场景 — 对池变量的特定赋值以及一个破坏该属性的操作

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

Trident 协议的一些背景

该 bug 涉及自动化市场制造商 合约 的恒定产品池 (CPP)。在 CPP 中，流动性提供者 (LPs) 存入两种基础代币（Token0 和 Token1）以换取 LP 代币。他们可以在后续操作中 销毁 LP 代币以重新索回 Token0 和 Token1 的比例金额。

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

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

步骤 1：制定不变量

销毁 LP 代币以换取基础代币的能力暗示了一个重要的不变量：如果有任何 LP 代币（totalSupply 大于 0），则 reserves₀ 和 reserves₁ 都不应该变为零（否则池无法生产基础代币）。更正式地说：

totalSupply = 0 ↔ reserves0 = 0

和

totalSupply = 0 ↔ reserves1 = 0

Certora Prover 允许我们在合约的规范中编写这个不变量：

步骤 2：找出违规

Certora 的 Prover 检查系统的每一种可能的状态和每一种可能的操作，确保这个不变量始终成立。如果有可能违反这个条件，证明者会生成一个具体示例，显示可能出现的问题。从这个反例中，可以找到程序中的缺陷。

令人惊讶的是，该工具显示 burn-single 操作违反了不变量。burn-single 操作结合了销毁和交换：它首先销毁 LP 代币以产生两种基础代币，然后再将一种代币交换为另一种代币（仅产生一种基础代币）。

尽管 swap 和 burn 操作保持了不变量，但组合操作存在一个缺陷，使恶意用户能够排空池子。

理解 burn-single 函数

要理解 burn-single 函数中的 bug，我们需要知道 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 代币供应中的 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 中的价值：

此值被添加到上面的 amount₁（第64行），并将总和转移给 Alice（第71行）。

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

看不见的问题

那么可能出什么问题呢？请记住，储备可能小于余额。Certora Prover 制作了一个场景，展示了如何使用这些内容的不一致：虽然 amount₀ 和 amount₁ 是利用余额计算的，但它们是从储备中减去的（这个问题也被 Cristoph Michel 独立发现，如 Sushi 所告知）。

假设在调用 burnSingle 之前，余额足够高，以至于：

amount0=(liquidity/totalSupply)⋅ balance0=reserve0

（证明者的具体赋值是：balance0=10,000, liquidity=100, totalSupply=1000, reserve0=1000）

Alice 继续 burnSingle 她的 LP。在上面的第 2 步中请求以 {Token1} 兑换此金额时，计算结果为：

getAmountOut(amount0, 0, reserve1 — amount1)

计算出的值将是 reserve1 — amount1。最终，用户将获得储备1 的全部。现在 r eserve1=0 但 totalSupply > 0，违反了不变量。

步骤 3：从破坏的不变量到合约利用

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

假设一个对手，Mallory，拥有一个 CCP 中的一些流动性。首先，她需要达到状态 amount0=(liquidity/totalSupply)⋅ balance0=reserve0。通常，池的余额等于其储备：在每个用户操作后，储备更新为等于余额。如果存在差异，任何用户都可以利用它来获得对她有利的差异。

Mallory 可以通过在 Token0 中进行大量闪电贷来达到该状态，然后将所有资金添加到池的 balance0 中。例如，假设一个池有 1M$ 的 TVL，其中 0.5M$ 是 Token0，剩余的 0.5M$ 是 Token1。如果 Alice 拥有 1% 的所有 TVL，她必须向池中提供额外的 44.5M$ 的 Token0。

Mallory 接着使用 burnSingle 她的 LP，请求以 Token1 收回此金额。Mallory 顺利提取所有 Token1 作为结果。但 Mallory 如何还清在 Token0 中获得的贷款？

通常，程序员可能会依赖系统的基本属性，并在不同地方假设这些属性以进行优化（而不是重复检查它们）。在这里，Swap 函数在检查 仅一个 储备大于 0 时依赖于我们的不变量进行交换：

Trident 假设要么池已初始化，那么两个储备都不为 0，要么池未初始化，那么两个储备都为 0。在 Mallory 的攻击中，仅 reserve1 为 0，但第 194 行的要求是成立的。

因此，为了完成攻击，Mallory 在 zero-reserve1 池中交换单个 Token1。使用上面同样的 getAmountOut 函数，读者可以验证 Mallory 现在获得了池的整个 reserve0。Mallory 然后可以偿还她的贷款。

总结一下，进行攻击的步骤，Mallory 需要：

1. 在 Token0 中进行闪电贷
2. 向 Balance0 添加大量金额
3. 使用 Token1 储备作为输出的 burnSingle
4. 将单个 Token1 交换为 Token0 储备

SushiSwap 的修复

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

结论

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

附录

getAmountOut:

完整的 burnSingle：

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