形式化验证助力发现偿付能力漏洞——Balancer V2漏洞报告

形式化验证有助于发现破产漏洞 — Balancer V2 漏洞报告

这篇博文详细介绍了我们在 2021 年 2 月审查 Balancer V2 系统时发现的一个偿付能力问题。该问题已被修复，并且不存在于任何在线版本中。

许多智能合约系统持有用户的资金。这些系统的一个最重要的要求是保持偿付能力——用户存入资产后应该始终能够提取该资产。资不抵债通常表现为拒绝服务——用户只有在其他用户向系统存入足够的资产后才能提取他们的资产（有点像庞氏骗局）。在严重的情况下，资产损失可能是永久性的。

对于所有智能合约，偿付能力没有一个统一的定义。不同的系统有不同的实体、用户权限和资金分配。如果偿付能力被打破，用户可能会损失部分或全部存入的资产。我们将这种破坏称为破产攻击。

破产攻击是严重的。它们通常很难通过手动审计发现，因为系统有许多，甚至无数种可能的状态。使用自动化工具来证明偿付能力可以为系统提供强大的安全保障，并极大地帮助检测通常被其他技术遗漏的错误。

最近，Certora 的自动化工具帮助我们发现了 Balancer V2 中的一次破产攻击。

Balancer 破坏偿付能力的闪电贷漏洞

Balancer V2 提供了一个高效的系统，用于加入、退出流动性池以及与流动性池进行交易。与池的所有交互都通过单个合约完成：Vault。Vault 在一个名为“内部余额”的结构中内部跟踪用户的余额，这对于降低频繁交易的 gas 成本非常有用。Vault 保留系统中所有用户和所有池的所有资金。

Vault 提供了一种闪电贷机制，允许用户显着提高其杠杆率。闪电贷与传统贷款的不同之处在于，它不需要用户提供任何抵押品。相反，它最多需要支付百分之一的费用。此外，它必须在底层交易结束时全额偿还。

闪电贷功能的简化代码如下所示：

Balancer V2 闪电贷功能 - 简化代码。此代码包含一个破产漏洞。代码中积极防止了其他形式的攻击，例如重入、输入数组长度相等等等。为了便于阅读，这些检查已从本文中删除。

此函数获取合约地址 flashLoanReceiver 和两个数组。第一个数组列出了要借用的所有 token，第二个数组列出了要从相应 token 借用的金额。例如，如果输入为 [WETH, DAI] 和 [200, 200]，则 flashLoanReceiver 将借入 200 DAI 和 200 WETH (1)。如果费用为 1%，则接收者需要提供至少 202 WETH 和 202 DAI，否则贷款将恢复。

此代码启用了一次破产攻击。你能发现它吗？

逃避费用

用户可以通过两次提供相同的 token 并将贷款分成两半来支付更少的税款。例如，假设用户想要借入 200 USDC，并且闪电贷费用百分比为 1%。假设他们提供的 token 数组为 [USDC]，金额为 [200]。用户将不得不偿还 202 USDC。

但是，用户可以改为将 token 输入为 [USDC, USDC]，并将金额输入为 [100, 100]。preLoanBalances 将为 [200, 100]。feeAmounts 将为 [1, 1]。在第 29 行，我们检查 USDC 的余额现在是否至少为 201。这意味着用户只需支付 1 USDC 的费用，即税款的一半。

用户可以将贷款金额分成四份：用户借入 [USDC, USDC, USDC, USDC]，金额为 [50, 50, 50, 50]。这样，他们只需支付 0.5 USDC，即应付税款的 25%。该方案可以推广到将贷款分成 N 等份以支付应付费用的 1/N (2)。

我们可以支付更少的费用。给定总贷款金额 T，划分次数 n 和费用百分比 f，最佳输入数组 (3) amounts 为

其中

是：

我们支付的费用是

我们可以通过划分次数呈指数级降低支付的费用！对于 1% 的最大费用，并且 n=10，我们只需支付约 9*10⁻²¹ 作为费用百分比。

破坏偿付能力

正如我们所看到的，用户可以避免支付闪电贷费用。但是，vault 认为它在每次循环迭代中都收取了新的费用。这导致了 vault 偿付能力的潜在违反。

对于给定的 token，Balancer V2 的偿付能力定义为 (4)：

balanceOf(vault) >= sum_of_all_internal_blances + sum_of_all_pool_balances + collected_fees

考虑一个只有两个用户的系统，Alice 和 Bob。Alice 在 vault 中持有 100 个 USDC token，而 Bob 在 vault 中也持有 100 个 USDC token。vault 的 USDC 总持有量为 200 USDC。闪电贷费用为 1%。Bob 借入 token 为 [USDC, USDC]，金额为 [100, 100] 的闪电贷，仅偿还 201 USDC。vault 的内部记录声称收取了 2 USDC 的税收收入。Bob 取回他的 100 USDC。现在 vault 的所有者提取作为税收收入收取的 2 USDC。vault 当前仅持有 99 USDC，而当 Alice 现在尝试提取她的 100 USDC 时，她的请求将被恢复。

请注意，Bob 不必是恶意才能进行这种破产攻击；Bob 正在遵循经济激励措施来支付更少的费用。

解决方案

Balancer 的团队通过要求 token 地址数组按严格升序排序来解决了该错误。这样可以防止多次提供相同的 token 地址作为输入。

修复后的闪电贷代码，已简化

Certora 形式化验证了该漏洞的解决方案。这是形式化验证规则在我们的规范语言中的样子：

Certora 用于捕获错误的规范，已简化

我们定义了输入可加性属性。假设我们从相同的初始状态查看合约的两个不同运行。第一次运行使用单个 token 和金额执行两次闪电贷。第二次运行执行一次闪电贷，但输入数组 tokens 和 amounts 是先抢跑的串联输入数组。请注意，我们没有约束输入的值。特别是，token_a 和 token_b 可以相同。

我们要求闪电贷要么恢复，要么串联运行不能比单独运行返回更少的费用。

旧代码违反了该规则，但修复后的代码符合该规则，正如预期的那样。

(1) 为了简单起见，在本文档中，我们不列出 token 合约的地址，而是写下 token 的名称。

(2) Gas 成本也随着划分次数线性增加。因此，该攻击存在一个硬性限制，即只要逃避的费用超过额外的 gas 成本，我们就会增加划分次数。

(3) 最优性证明将在未来的博文中出现。

(4) 我们假设 token 是“行为良好的”。编写带有后门的 token 来破坏偿付能力属性是很简单的。我们只关心幼稚的、实际可用的 token，例如 DAI 和 USDC。

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