Solidity固定点库中的问题 — Certora漏洞披露

  • Certora
  • 发布于 2023-07-13 12:39
  • 阅读 15

本文探讨了固定点表示法在DeFi应用中的重要性,详细分析了PRBMath库中的一个设计缺陷,该缺陷可能导致严重的安全漏洞,并强调了公共库安全性的重要性。作者建议进行长远解决方案以支持多种舍入模式,并指出了正式规范的重要性。

背景

在计算机科学中,定点表示法是一种通过存储固定数量的小数部分数字(即小数点右侧的数字)来表示实数的方法。很显然,对于任何 DeFi 应用程序,操纵定点数是至关重要的,例如,计算利率、借贷指数、确定AMM价格曲线等。

也许不那么明显的是,即使是微小的舍入或实现错误也会积累和加剧,可能导致套利机会甚至安全漏洞。最近的例子包括:

另请参阅 ERC-4626(代币化保险库)中关于“安全考虑”的部分,其中建议在计算保险库份额时使用不同的相对舍入方向。

关于在 Solidity 中实现高级数学函数的两个优秀资源是 Mikhail Vladimirov 的 Math in Solidity 博客系列,以及 Remco Bloeman 的 网站。后者启发了 Solidity 中最流行、最节省 gas 费用和最复杂的定点库之一——PRBMath 库,由 Paul Razvan Berg 编写。总体而言,这个库写得非常好且受到维护,包括多种功能的单元测试。然而,使用 Equivalence Checker ,我们最近发现了 PRBMath 库中之前未知的设计缺陷,这影响了以下函数:


function mulDivSigned(int256 x, int256 y, int256 denominator) pure
returns (int256 result)
/// @notice 以全精度计算 floor(x*y÷denominator)。

问题很简单,但在 DeFi 上下文中实现时可能导致严重漏洞和资金损失。它出现在每个版本号为 1.1.0 及以上(含 4.0)的 PRBMath 库的实例中。

根据我们的了解,这是自动工具第一次在公共的开源 Solidity 库中发现漏洞。

漏洞描述

粗略而言,PRBMath 用于计算有符号 乘法和除法 的算法可以分为三个步骤 —

1. 提取输入的符号和绝对值:

  • (abs_x,abs_y,abs_d) := (x,y,d) 的绝对值
  • (sign_x,sign_y,sign_d) := (x,y,d) 的符号

// 获取x, y和分母的绝对值。
uint256 xAbs;
uint256 yAbs;
uint256 dAbs;
unchecked {
  xAbs = x < 0 ? uint256(-x) : uint256(x);
  yAbs = y < 0 ? uint256(-y) : uint256(y);
  dAbs = denominator < 0 ? uint256(-denominator) : uint256(denominator);
}
// 获取x, y和分母的符号。
uint256 sx;
uint256 sy;
uint256 sd;
// "sgt"是 "signed greater than" 汇编指令,"sub(0,1)" 是二进制补码中的 -1。
assembly ("memory-safe") {
  sx := sgt(x, sub(0, 1))
  sy := sgt(y, sub(0, 1))
  sd := sgt(denominator, sub(0, 1))
}

2. 通过简化到无符号案例,计算结果的绝对值:


uint256 abs_result = mulDiv(abs_x, abs_y, abs_d);

其中


function mulDiv(uint256 x, uint256 y, uint256 denominator) pure
returns (uint256 result)
/// @notice 计算 floor(x*y÷denominator) 的全精度。

3. 计算整体符号并返回结果:


uint256 overall_sign = sign_x ^ sign_y ^ sign_d;
result = (overall_sign == 0) ? -int256(abs_result) : int256(abs_result);

问题在于步骤2是错误的。实际上我们有:

所以每当结果为负时,我们实际上是向零舍入而不是向负无穷,这导致了一个错位的错误。

影响与适当的披露程序

在进行项目时,审核人员经常根据 严重性 (该漏洞可能造成多大的损害:拒绝服务、资金损失…)和 难度 (恶意行为者将漏洞转化为实际利用的难度有多大)来分类智能合约漏洞。

我们在与一家领先的 DeFi 协议处理尚未发布的 AMM¹ 代码时首次发现了这个漏洞,该协议在计算 交易函数 时使用了 mulDivSigned 。在某些情况下,这个算术错误将使攻击者能够强迫流动性池接受 不利交易²,系统性地抽走 LP-tokens 的价值。

最初,我们将这个漏洞分类为严重程度关键但难度高,并通知了客户,他们在自己的代码中修复了这个问题。然而,当我们注意到这个算术错误发生在多个 PRBMath 库实例中时,我们最初的分类变得复杂,因此可能影响更多系统,包括现有系统。

这带来了一个难题:即使在“经典”计算机安全的世界里,库中的漏洞也 notoriously 危险,很难估计各项目的严重性和难度。这种困难在以太坊中加剧,因为其缺乏对可升级库的本地支持或分发热修复的机制,并且人们(出于 gas 原因)更愿意仅复制 PRBMath 中的特定函数并加以调整,而不是导入整个库。

在咨询了知名安全研究人员 samczsunMudit Gupta 后,我们彻底搜索了公共代码库(包括链外和链上),并私下通知了潜在的易受攻击项目。我们还联系了 PRBMath 的作者 Paul Razvan Berg,他立即与我们通话,并确认了这些发现。

经过调查,我们相信,目前正在使用 PRBMath 的符号算术部分的智能合约非常少。因此,鉴于智能合约的 immutable 特性,公开披露该问题似乎是最好的选择。

缓解措施

为了解决这个问题,Paul 发布了一个临时修复(版本 4.1),将 mulDivSigned 的定义更改为向零舍入:


function mulDiv(uint256 x, uint256 y, uint256 denominator) pure
returns (uint256 result)
/// @notice 以 512 位精度计算 x*y÷denominator。
/// 说明:
/// - 结果向零舍入。

从长远来看,这个问题将作为提供对 PRBMath 多重舍入模式支持的持续计划的一部分而得到长期解决。有关更多信息,请查看此处的讨论。

结论

数学库是 DeFi 生态系统的基本构建块。然而,它们难以做到正确(特别是当人们试图积极优化其 gas 消耗时),并且审核它们可能既乏味又困难。

上述漏洞表明即使在全面的单元测试下,编写系统的正式规范的过程也具有很大的方法论优势(即使只是为了确保没有被忽视或遗漏)。它还作为 CVL 语言可表达性的良好示例——一个基本的 CVL 规范(“等价规范”)

能够检测出数学库的 Solidity 代码中存在的一个为期两年的漏洞,该漏洞涉及大量 Yul 段、众多位操作技巧,甚至还有一点数论——所有这一切 都不需要对实现细节有任何理解

¹ 参见例如调查论文 “SoK: Decentralized Exchanges (DEX) with Automated Market Maker (AMM) Protocols” 以快速回顾 DEX、AMM 以及相关 DeFi 术语。

² 也称为 AMM- 或 CFMM-invariant

  • 原文链接: certora.com/blog/problem...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
Certora
Certora
Securing DeFi through smart contract audits, formal verification, and protocol design reviews.