DeFi 中的舍入误差：1 Wei 如何让你损失数百万美元

随着 DeFi 领域变得更加成熟和巩固，一些类型的 bug 变得越来越少见。重入攻击、访问控制绕过和首次存款者攻击等，web3 安全研究人员和开发者都对此有充分的了解。因此，我们看到这种“经典”的攻击向量几乎已经成为过去。但似乎有一类 bug 即使在 2025 年仍然非常普遍——舍入误差。在过去的两年里，舍入误差造成的损失超过了 $1 亿美元。

在本博客中，我们将介绍舍入误差，并展示即使是很小的误差，哪怕只有 1 wei，也可能演变成严重的漏洞。我们将解释为什么这些误差对人类来说很难发现，但通过自动化的形式验证很容易发现。最后，我们将演示如何使用这些技术在活跃的协议中发现 bug。

但是等等！一个 1 wei（例如 1E-18 以太币）的误差怎么会导致严重的 bug？显然，我们不会认为攻击者从协议中获取额外的 wei 是一种重大盗窃。但是，在某些（但不是所有！）情况下，舍入误差可以通过以下几种机制产生巨大的影响：

• 1 wei 被设计成价值很高，因此每个舍入误差都至关重要，例如，当协议意外地向下舍入为零而不是一时。这可能发生在错误地向下舍入代表资金所有权的份额或扭曲多个代币的流动性池的情况下（例如，ZkLend (2025), Abracadabra (2024), Wise Lending (2024), Hundred Finance (2023), Raft (2023))
• 1 wei 使合约的执行发生巨大变化，例如，意外地采用了新的代码分支（例如，KyberSwap (2023)）。
• 1 wei 价值足以反复运行攻击。这主要发生在 gas 成本非常低的区块链中，以使其有利可图（SPL Swap (2022), Yieldly (2022)）

但是，像舍入差异这样小的东西，通常只有 1 wei，怎么会导致数百万的损失？要理解这一点，我们需要深入了解一下，看看为什么这些 bug 不可避免且难以捕获。

因为 EVM 只支持整数，所以每次开发者需要实现一些除法运算（例如，用于比率计算或单位转换）时，他们都必须决定是将结果实数向下、向上还是四舍五入到最接近的整数。每个决定都为舍入误差留下了空间。虽然有一些既定的经验法则（“始终支持协议进行舍入”），但很多时候，人们只是希望舍入问题不会扩大到危急程度。从某种意义上说，舍入误差是不可避免的。

那么，为什么作为一个社区，我们没有像消除其他类型的 bug 那样消除舍入误差呢？

舍入误差对人类来说很难，对计算机来说很容易

我认为，舍入误差很难被协议的程序员和审计协议的安全研究人员发现，因为人类不擅长推理寻找舍入问题所需的逻辑。通常，我们可以很好地掌握给定协议的整个逻辑状态机，并在脑海中尝试找出漏洞：

• 攻击者是否可以重复交易以允许双重支付？
• 协议是否允许所有者窃取资金？
• 协议参数的更改是否会导致不可逆转的拒绝服务？

一旦提出这些问题，人类很容易验证。另一方面，舍入误差需要更多的数学推理（尤其是在整数上！），不幸的是，我们并不擅长。（例如，请参阅我们的博客文章 Solidity 定点库中的问题）

在最简单的情况下，我们会看到这样的情况：

function convertToShares(uint256 assets) public view virtual returns (uint256) {
        uint256 supply = _totalSupply;
        if (supply == 0) {
    return assets
        }
return (assets * supply) / totalAssets();
    }

在这里，我们看到了 ERC-4626 金库中资产和份额之间的转换。显然，由于 solidity 中除法运算符的性质，此函数返回的份额数量会向下舍入。这确实与 ERC-4626 指南 相符，并且可以毫不费力地进行验证。

但是许多舍入场景远没有那么清晰。作为一个更详细的例子，考虑以下 Solidity 函数，该函数实现了交换的价格计算。忽略上下文，你能判断舍入方向是否一致吗？

function estimateIncrementalLiquidity(
  uint256 absDelta,
  uint256 liquidity,
  uint160 currentSqrtP,
  uint256 feeInFeeUnits,
  bool isExactInput,
  bool isToken0
) internal pure returns (uint256 deltaL) {
  if (isExactInput) {
    if (isToken0) {
      deltaL = FullMath.mulDivCeiling(currentSqrtP,absDelta * feeInFeeUnits,TWO_FEE_UNITS);
      uint256 tmp = FullMath.mulDivFloor(absDelta, currentSqrtP, TWO_POW_96);
      FullMath.mulDivCeiling(liquidity + deltaL, currentSqrtP, liquidity + tmp);
    } else {
      deltaL = FullMath.mulDivCeiling(C.TWO_POW_96,absDelta  feeInFeeUnits,TWO_FEE_UNITS  currentSqrtP);
      uint256 tmp = FullMath.mulDivFloor(absDelta, TWO_POW_96, currentSqrtP);
      return FullMath.mulDivFloor(liquidity + tmp, currentSqrtP, liquidity - deltaL);
    }
  }
  else
      {
        uint256 a = feeInFeeUnits;
        uint256 b = (FEE_UNITS - feeInFeeUnits) * liquidity;
        uint256 c = feeInFeeUnits  liquidity  absDelta;
        if (isToken0) {
            b -= FullMath.mulDivFloor(C.FEE_UNITS * absDelta, currentSqrtP, TWO_POW_96);
            c = FullMath.mulDivFloor(c, currentSqrtP, TWO_POW_96);
            deltaL = QuadMath.getSmallerRootOfQuadEqn(a, b, c); //(b - sqrt(b  b - a  c)) / a;
            uint256 tmp = FullMath.mulDivFloor(absDelta, currentSqrtP, TWO_POW_96);
            return FullMath.mulDivFloor(liquidity + deltaL, currentSqrtP, liquidity - tmp);
    } else {
            b -= FullMath.mulDivFloor(C.FEE_UNITS * absDelta, TWO_POW_96, currentSqrtP);
            c = FullMath.mulDivFloor(c, TWO_POW_96, currentSqrtP);
            deltaL = QuadMath.getSmallerRootOfQuadEqn(a, b, c); //(b - sqrt(b  b - a  c)) / a;
            uint256 tmp = FullMath.mulDivFloor(absDelta, TWO_POW_96, currentSqrtP);
            return FullMath.mulDivCeiling(liquidity - tmp, currentSqrtP, liquidity + deltaL);
    }
      }
}

当然，答案是否定的（我不是一个施虐狂！）。在 isExactInput 为 true 且 isToken0 为 false 的情况下，存在不一致——- deltaL 被向上舍入，并且在分数的分母中带有减号（此代码基于 Kyberswap 的代码，涉及上述 事件。）。综合考虑，这意味着分数正在变大，这与分数的向下舍入不一致。这些类型的复杂数学难题通常是找到舍入误差所需的推理。

开发者和审计人员在部署前评估代码的时间有限。但是，攻击者有无限的时间来发现舍入误差 bug。在某些情况下，白帽黑客花了一年多的时间在一个协议上寻找关键的舍入误差。仅靠手动审查无法可靠地防御舍入误差。

与人类不同，计算机擅长处理数字。更具体地说，计算机擅长形式验证（FV）——证明一段代码（在我们的例子中，是一个智能合约或整个协议）的数学属性的能力。为了使用 FV，我们需要向形式证明器指定我们要验证的属性类型。证明器可以给我们一个数学证明，证明该属性适用于协议状态机中的所有可行状态，或者给我们一个反例（例如，协议的具体状态和对其合约之一的具体外部函数调用，违反了该属性）。

虽然从蠕虫的角度来看，舍入问题可能看起来很模糊，但从鸟瞰的角度来看，它们变得清晰——我们可以指定代码的一般属性或不变量，我们知道这些属性或不变量应该始终成立。例如，

• ERC-4626 金库中一个份额的价格永远不应降低。
• 除非提取流动性，否则池的不变量永远不应降低。
• 在用户与协议的每次交互中，第三方用户的资金不会损失，除非他们被清算。

如果我们能够为开头列出的一些协议检查这些类型的声明，那么隐藏在协议业务逻辑深处的舍入误差自然会作为违反属性的反例弹出。

野外的舍入误差 - Juice Finance

Juice Finance（或简称 "Juice"）协议是 Blast 区块链中的一个标准杠杆借贷协议，在撰写本文时，它的 TVL 约为几千万美元。在标准的操作过程中，用户锁定一定数量的抵押代币，然后可以借入另一种代币（最高为锁定抵押品金额的某个倍数），用于投资 Juice 预先定义的一些收益策略。

我们不想深入研究 Juice 协议的结构，但需要对其机制有一些浅显的理解。Juice 由四个部分组成：

1. 借贷池 - 为借入的代币提供清算
2. 账户管理器 - 创建和管理（杠杆）账户
3. 账户 - 由账户管理器为每个用户创建的智能合约。持有借入的代币。
4. 策略 - 一组允许账户使用借入的代币投资于收益策略的合约。

该协议的标准流程如下：用户 A 将一些借入的代币（目前为 USDB 或 WETH）存入借贷池，并获得有息流动性代币。用户 B 要求账户管理器开设一个他将拥有的新账户。他提供抵押品（使用 AccountManager.deposit()），这授予他不可转让的 ERC-4626 抵押份额代币。然后，他可以向其杠杆账户借入一些代币，这些代币使用为该账户铸造的虚构债务代币进行核算。账户管理器确保账户是健康的，这意味着账户所有者锁定的抵押品金额加上账户中当前借入的代币金额，除以账户拥有的债务代币金额，大于某个阈值。从这里开始，允许用户将他借入的代币投资于由协议实施的一组具体的收益策略（使用 accountManager.strategyDeposit()）。稍后，在成功产生收益的情况下，允许用户申领利润（使用 account.claim()）。

清算流程比平时更复杂，因为它由几个单独的清算调用组成，这些调用发送到账户管理器。在这里，我们将仅表示其中一个调用 AccountManager.liquidateCollateral()，该调用从不健康的账户中扣押抵押品，将其出售为借入的代币，并使用这些代币偿还债务。

形式验证和违规

在 Certora，我们有一些“黄金法则”，我们总是尝试为每个贷款协议证明（或反驳），包括：

1. 除了价格变动或利息累积之外，贷款头寸不能进入不健康（可清算）状态（有关更多信息，请参阅我们的博客文章“ 圣杯”）。
2. 对于不健康的头寸，清算必须成功（达到一些明显的要求，例如清算人有足够的资金来进行清算）。

在运行第一个属性时，我们发现了两种用户可以将自己或其他用户推入不健康状态的情况。在第一种情况下，证明器发现 AccountManager.deposit() 错误地舍入了铸造给账户的份额数量，因此份额价格下降而不是增加。反过来，这可能会使第三方用户的账户变得不健康。发生这种情况是因为 ERC4626 previewDeposit() 函数执行了两次向下舍入操作（一次是从资产到份额，一次是从份额到资产），从而有效地向上舍入了铸造的份额数量。

在第二种情况下，用户可以清算自己，因为 AccountManager.repay() 方法向下舍入要销毁的份额数量（这听起来很天真，但实际上是正确的），这可能会将用户的头寸推过清算阈值线。这是可能的，因为与用户借入贷款或提取抵押品的情况不同，当用户偿还贷款时，系统不会检查用户账户的健康状况（因为错误地假设偿还贷款永远不会降低健康状况）。

至于第二个属性，Certora 证明器发现了一种特殊设计的头寸不可清算的情况。这发生在调用 accountManager.liquidateCollateral() 期间，当系统尝试将清算账户的资产转移给两个 parties——清算人（msg.sender）和清算奖金的受益人（liquidationFeeTo），通过随后两次调用 _withdrawAssets()，该函数向上舍入账户要销毁的份额数量。与前一种情况一样，这听起来很合理，因为我们是针对被清算的账户进行舍入的。但是，由于向上舍入发生了两次，因此系统会尝试销毁比账户实际拥有的份额更多的份额（当两个向上舍入的分数加起来大于 1 时，会发生这种情况）。因此，尝试清算此类账户的抵押品会导致交易回滚。

重要的是要注意，在这种情况下，FV 并没有处理合约的漏洞利用，而只是指出了可能被利用的弱点（某些属性不再成立）。

不要让舍入误差溜走

舍入误差可能会在 DeFi 协议中引入严重漏洞，这些漏洞通常由于其数学微妙性而在手动审计期间被忽略。

形式验证提供了一种严格、可靠的方法来检测和预防这些问题。通过显式定义协议的不变量并系统地验证它们，你可以在早期发现关键 bug，并在代码上线之前保护你的代码。

如果你正在构建智能合约并希望在它们投入生产之前消除与舍入相关的漏洞，请与我们联系。我们随时为你提供帮助。

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