Balancer漏洞解析：哪里出了问题，以及为何v3是安全的

这是 Certora 对该事件的分析，以及详细的时间表。

事件如何发生

Balancer 是一种去中心化交易协议，支持各种流动性池之间的代币交换。每个池由一组特定的代币（例如，WETH、wstETH）和一个由不变量管理的交换曲线（例如，恒定乘积、加权乘积等）定义。每个池都会发行自己的流动性代币，称为 Balancer Pool Token (BPT)，它代表了池资产的比例份额。

Balancer 的一些池包括两个值得注意的机制：可组合性和速率放大。可组合池是包含其自身 BPT 作为可交换资产的池。速率放大通过在计算不变量时将某些包装资产（例如，wstETH -> stETH）转换为其基础等价物来调整代币价值。

当用户发起池中两个代币之间的交换并指定他们希望收到的确切金额 (EXACT_OUT) 时，池会计算必须提供多少其他代币才能维持不变量（不包括费用）：

function _swapGivenOut(
       SwapRequest memory swapRequest,
       uint256[] memory balances,
       uint256 indexIn,
       uint256 indexOut,
       uint256[] memory scalingFactors
   ) internal returns (uint256) {
       _upscaleArray(balances, scalingFactors);
       swapRequest.amount = _upscale(swapRequest.amount, scalingFactors[indexOut]);

       uint256 amountIn = _onSwapGivenOut(swapRequest, balances, indexIn, indexOut);

       // amountIn tokens are entering the Pool, so we round up.
       amountIn = _downscaleUp(amountIn, scalingFactors[indexIn]);

       // Fees are added after scaling happens, to reduce the complexity of the rounding direction analysis.
       return _addSwapFeeAmount(amountIn);
   }

在不变量计算中使用的输出金额 (swapRequest.amount) 的放大过程中出现了一个问题。如下面的代码片段所示，该值向下舍入，

function _upscale(uint256 amount, uint256 scalingFactor) internal pure returns (uint256) {
       // Upscale rounding wouldn't necessarily always go in the same direction: in a swap for example the balance of
       // token in should be rounded up, and that of token out rounded down. This is the only place where we round in
       // the same direction for all amounts, as the impact of this rounding is expected to be minimal (and there's no
       // rounding error unless `_scalingFactor()` is overriden).
       return FixedPoint.mulDown(amount, scalingFactor);
   }

而它应该向上舍入。为什么？正如通用的经验法则所指示的那样，舍入应始终有利于协议而不是用户。向下舍入 swapRequest.amount 会导致所需的支付被略微低估：在不变量计算期间，池“认为”用户提取的金额少于他们实际提取的金额，因此它计算出一个较小的 amountIn。因此，在交换之后，不变量可能低于它应该有的值。在大多数情况下，这种差一的差异可以忽略不计。

但是，当一个池是可组合的，攻击者可以通过交易大量的 BPT 代币来换取实际池的代币，从而人为地降低池的流动性。他们甚至不需要事先拥有 BPT：Balancer 允许一个中间的“赤字”状态，用户暂时欠 Vault BPT。随着流动性被人为地推低，舍入差异被放大并且不再可以忽略，这使得攻击成为可能。

一旦不变量被显著降低，结算 BPT 的赤字变得很便宜，使得这种往返对攻击者来说是有利可图的。

事件时间线

UTC+02 时区，2025 年 11 月 3 日：

09:45 对 Balancer 池的攻击开始。

10:15 Certora 注意到 Balancer 的稳定池正在被攻击，并立即开始调查。

11:00 Certora 通知 Balancer 我们正在彻底调查此事。

12:30 漏洞的根本原因被确定：根不变量计算中的一个舍入问题。此外，Certora 验证了导致该错误的底层问题没有出现在 v3 中（即，舍入是正确的）。

14:15 Balancer 联系了 Certora，Certora 将根本原因通知了他们。我们共同决定 Certora 应调查其他 v2 池类型是否也存在漏洞。

18:00 Certora 与 Balancer 分享了对该漏洞的初步分析。

Balancer v3 安全测试

Balancer 团队与安全合作伙伴密切合作。在他们与 Certora 合作的四年中，他们对严格的安全实践进行了大量投资。Balancer 协议的每个版本都经过了多次审计，并通过形式验证和积极的漏洞赏金计划进行了补充。认识到 v2 的复杂性和风险，Balancer 团队在设计 v3 时明确关注简单性和弹性。

Balancer v3 通过设计解决了 v2 中导致一些复杂性的问题。所有池操作都以 18 位小数精度完成，并且放大/缩小由 vault 处理。可组合池被 ERC4626 缓冲区取代，以简化池中的功能。这种新的设计使池操作不那么复杂，更容易验证。

在我们与 Balancer 的合作中，大量的安全重点放在计算、舍入和精度上。在识别出一些可能发生舍入错误的计算后，为协议中的所有计算添加并强制执行了显式舍入方向。

除了手动审查代码外，Certora 还使用了测试和 Certora Prover 来验证所有计算是否正确完成。当 Prover 达到计算的复杂性阻止端到端安全性的形式证明的情况时，添加了额外的测试以确保协议的安全性。

具体来说，虽然 v3 Vault 对于 Certora Prover 来说在计算上仍然很复杂，但我们展示了一个关于简化的池语义的属性，该属性可以捕获这种性质的错误：

swappingBackAndForth

此规则验证了将一些金额从一个代币交换到另一个代币再交换回来不会导致资金的增加。

虽然此规则并未排除所有漏洞场景，但它为用户提供了额外的保证，即此类漏洞极不可能发生，因为 Prover 即使在简单场景中也会考虑所有可能的值，从而捕获源于最微小的流动性金额或不均匀价值分布的错误。

Certora 在 v3 池和 vault 的初始设计中帮助了 Balancer，确保了针对舍入错误、低流动性交换、首次存款人攻击、闪电贷操纵等问题的适当缓解措施。

Balancer v2 审计分析

2022 年，Certora 使用 Certora Prover 和手动审查对 Balancer v2 的稳定池进行了安全审查，目的是证明池合约的关键经济和安全属性的正确性。这项工作主要集中在确保 BPT 供应的偿付能力、资产和铸造的 BPT 的平价以及以有限的方式限制放大因子的行为。

具体来说，我们证明了：

• 所有用户的 BPT 余额之和始终小于或等于池的 totalSupply。
• 在没有相应增加池的总资产的情况下，不可能铸造新的 BPT 代币。

这些属性确保了不会凭空创建代币，并且用户余额始终反映了池持有的实际基础资产。

不幸的是，虽然经过验证的属性在高层次上保证了偿付能力，但它们不足以检测到导致 Balancer v2 稳定池最近漏洞的舍入错误。经过验证的属性没有约束单个交换或舍入行为之间的关系。因此，由于舍入偏差，诸如代币往返交换之类的迭代操作可以系统地增加价值的情况并未被排除。

事后看来，我们已经确定了两个额外的属性，它们本可以捕获此类错误并防止错过舍入漏洞：

1. 往返交换不变性：“将代币兑换成另一种代币然后再兑换回来不应产生比原始余额更多的价值。”

此属性确保任何交换操作的组合都不会导致净代币数量的增加。违反此属性会暴露出舍入不对称性。

2. BPT 份额价值不变性：“对于任何用户操作，单个 BPT 的份额价值不得降低。”

此不变量保证了每个 BPT 的价值（份额比率）在所有有效操作中保持不变或增加。它可以防止 totalAssets 和 totalSupply 之间微妙的去同步，包括那些源于舍入差异或不精确的池不变量计算的去同步。

主要收获

• 偿付能力证明是不够的。 余额的聚合守恒并不意味着舍入安全。需要局部和组合属性，例如交换可逆性和份额价值单调性，我们在贷款协议、AMM 和池 hooks 上经常证明这些属性。具体来说，我们有许多规则确保舍入始终有利于协议，从而防止由于舍入错误导致的漏洞。值得注意的是，我们对 Kamino Lending、Solana 的 Stake Pool 和 EulerEarn 等进行了此类检查。
• 安全测试必须推理数值精度。 抽象 StableMath 函数简化了证明，但也可能掩盖了小的、复合的舍入差异。
• 往返式测试对于 AMM 验证至关重要。 这些测试捕获了仅在顺序操作后才会出现的细微的、突发的矛盾之处。

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