背景
在计算机科学中，定点表示法是一种通过存储固定数量的小数部分数字（即小数点右侧的数字）来表示实数的方法。很显然，对于任何 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 中的特定函数并加以调整，而不是导入整个库。
在咨询了知名安全研究人员 samczsun 和 Mudit 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。
