第 11 篇：Cetus——2025 年的溢出仍值两亿美元


时间	2025 年 5 月 22 日
涉案	约 $2.2 亿
结局	大部分资金被 Sui 验证者冻结
类别	C3 数值假设失效
语言	⚠️ Move（不是 Solidity）

一、背景：集中流动性的数学

Cetus 是 Sui 上的集中流动性做市商（CLMM，Uniswap V3 那一类）。它的核心数学是：

给定 一个价格区间 [Pa, Pb] 和 一个流动性数量 L，
   算出用户需要存入多少 token A 和 token B。

⟹ 这些公式涉及平方根价格、大整数移位、定点数运算，
   ⭐ 数值范围跨度极大，必须用 128 位甚至 256 位中间量。

⚠️ 这类数学有一个共同特征：中间量可能远大于任何有业务含义的数值。 所以每一步都需要溢出检查——而 Move 的整数运算在溢出时会 abort，开发者因此常常改用手写的"检查 + 移位"来控制行为。

二、漏洞在哪：一个错误的掩码

问题出在一个手写的"带检查的左移"函数上。它的意图是：

checked_shlw(n)  ——  把 n 左移 64 位，
                     ⭐ 如果会溢出就返回 (0, true) 表示错误

正确的判断应该是：
   n 左移 64 位后是否超过 u256 的范围？
   ⟹ 等价于  n >= 2¹⁹²

但实现里用的掩码写错了，判断条件变成了一个远大于正确阈值的值。结果是：

           ┌──────────────┬─────────────────────┬──────────────┐
           │  n < 2¹⁹²    │  ⚠️ 2¹⁹² ≤ n < 错误阈值 │  n ≥ 错误阈值 │
───────────┼──────────────┼─────────────────────┼──────────────┤
正确行为    │   通过        │        拒绝           │    拒绝       │
实际行为    │   通过        │  ⭐⭐ 通过（然后截断）  │    拒绝       │
           └──────────────┴─────────────────────┴──────────────┘

⭐ 落在中间那个区间的输入，检查说"没问题"，然后左移把高位悄悄丢掉了。

⭐这比"没有检查"更危险。

没有检查时，至少还有语言层面的溢出 abort 兜底。 而一个错误的检查，等于主动告诉运行时"我已经确认过了，放行" —— 它把兜底机制也一起关掉了。

三、攻击复盘

① 攻击者构造一个开仓请求，
   把"流动性数量"设成落在那个错误区间里的巨大值

② 系统计算"需要存入多少代币"
     └─ 调用 checked_shlw
     └─ ⚠️ 检查通过（错误地）
     └─ ⭐ 左移截断 ⟹ 算出来的所需代币量变成【极小】

③ 攻击者存入约【一个单位】的代币
   ⟹ 获得对应于天文数量的流动性头寸

④ 立即移除流动性
   ⟹ 按真实的流动性数量结算
   ⟹ ⭐ 取走池子里几乎全部资产

⑤ 对多个池子重复

净效果：用极小的输入换到了极大的份额。这和第 9 篇的 BEC 是同一个形状——只是那次溢出让"应付金额"变成 0，这次是让它变成一个极小值。

止损

Sui 的验证者协调冻结了攻击者地址上的大部分资金。

⚠️ 和第 10 篇完全一样的两难：止损有效，同时证明了这条链的验证者集合小到可以协调行动。止损能力和审查能力是同一个能力。

四、为什么没被发现

① “我们用的是 Move，它比 Solidity 安全”

⭐ Move 确实提供了一些安全优势：
   · 资源类型 ⟹ 代币不能被凭空复制或丢失
   · 整数运算默认在溢出时 abort
   · 更强的形式化验证工具链

⚠️ 但这些都不覆盖【业务逻辑里的数学是否正确】。

⟹ Move 保证了"这个加法不会静默溢出"，
   ⭐ 它管不了"你自己写的溢出检查用错了常量"。

⭐⭐ 语言的安全特性只能消除【那一类】错误。 而每一次你为了绕开语言的默认行为而手写检查，你就退回到了那一类错误里。

② 手写的检查没有对应的测试

一个 checked_shlw 函数应该有的测试：
   □ 恰好不溢出的最大值 ⟹ 应通过
   □ ⭐ 恰好溢出的最小值 ⟹ 应拒绝    ← 关键的那一个
   □ 远超阈值的值       ⟹ 应拒绝
   □ 0 和 1            ⟹ 应通过

⚠️ 如果只测了第 1、3、4 条，
   错误的阈值【完全不会暴露】——
   因为那三个用例在正确和错误的实现下行为相同。

⭐ 只有第 2 条能区分它们，而它恰好是最容易被漏掉的。

③ 边界检查函数看起来"太简单，不值得审"

⚠️ 一个五行的位运算工具函数，
   在几千行的 CLMM 数学库里毫不起眼。

⭐ 但它是【所有金额计算的守门人】——
   按[第 10 篇](https://blog.ifcalm.org/posts/security/blockchain/10-bnb-bridge-iavl/)"每行代码控制多少资金"的排序，
   它应该排在最前面。

五、防御

① 能不手写就不手写

⭐ 优先级：
   ① 用语言/标准库的默认检查（Move 的溢出 abort、Solidity 0.8）
   ② 用经过广泛使用的数学库
      （Uniswap 的 FullMath / TickMath、OpenZeppelin Math）
   ③ ⚠️ 万不得已才手写，且必须有独立测试与审计

② 手写的边界检查必须"两侧夹逼"测试

⭐ 对任何形如 "if (x > THRESHOLD) reject" 的检查，
   必须测这两个值：

      THRESHOLD       ⟹ 期望的行为
      THRESHOLD + 1   ⟹ 相反的行为

⚠️ 只有这一对能证明阈值本身是对的。
   任何离边界很远的测试用例都无法区分
   "阈值写对了" 和 "阈值差了三个数量级"。

③ 把常量算出来，而不是写出来

// ⚠️ 危险：手写一个魔法数，写错了没人看得出来
const MASK: u256 = 0xffffffff_ffffffff_00000000_00000000_...;

// ✅ 更好：让编译器算，意图直接写在代码里
const MAX_BEFORE_SHIFT: u256 = 1 << 192;   // ⭐ 一眼能看出对不对
if (n >= MAX_BEFORE_SHIFT) { return (0, true) };

⭐ 一个能被人类一眼验证的表达式，胜过一个正确但无法核对的十六进制常量。

④ 不变量测试：金额守恒

⭐ 对任何 AMM，这几条不变量能自动抓住本案：

   ① 增加流动性后，池子里两种代币的余额都必须【增加】
   ② ⭐ 用户获得的份额，必须与他【实际存入】的价值成比例
   ③ 存入再立即取出，用户拿回的不能【多于】存入的
      （手续费只会让他拿回更少）
   ④ Σ 所有头寸的价值 ≤ 池子实际余额

⚠️ 本案违反第 ②③④ 条。 用 fuzz 跑"随便存一个数、立刻取出"，第 ③ 条会立刻报警。

⑤ 形式化验证的正确用法

⭐ Move Prover / Certora 这类工具擅长的正是这种事：
   证明 "对所有输入，checked_shlw 返回 false 当且仅当 n < 2¹⁹²"。

⚠️ 但要注意它的边界（见[第 35 讲](https://blog.ifcalm.org/posts/blockchain/35-contract-vulnerabilities/)）：
   ⭐ 它证明的是"实现符合规约"，
      不是"规约是对的"。

⟹ 如果你写的规约本身就用了那个错误的阈值，
   验证器会愉快地证明"实现完全正确"。

六、⭐ 举一反三

核心命题一：错误的检查比没有检查更危险

⭐⭐ 一个错的检查会同时关掉它下游的所有兜底机制，因为后续代码会"相信"这个检查已经做过了。

同类形态：

   · require(amount <= max) 里的 max 算错
        ⟹ 后面所有基于 amount 的计算都不再校验
   · 一个 isValidSignature 实现有 bug 恒返回 true
        ⟹ 整个权限系统失效，而每一处调用看起来都做了检查
   · 一个 onlyOwner 修饰符里的比较写反
        ⟹ 每个函数都"有权限检查"，但没有一个有效
   · ⭐ 一个 checkHealth() 算错抵押率
        ⟹ 清算与借贷同时失效

检查方法：把所有"守门人"函数（返回 bool 或会 revert 的那些）单独列出来，每一个都当作一个独立模块来测试，而不是只在集成测试里顺带覆盖。

核心命题二：更安全的语言不豁免业务逻辑

⭐ 语言/框架能消除的错误类型是【固定的一小类】：

   Solidity 0.8   ⟹ 消除了算术溢出（但不含类型转换）
   Move           ⟹ 消除了资源复制/丢失、默认溢出 abort
   Rust           ⟹ 消除了内存安全问题
   ⚠️ 三者都不能消除："你的公式推导错了"

⟹ 而随着语言变安全，
   ⭐ 剩下的漏洞【比例上】更集中在业务逻辑里 ——
      这意味着审计的重心必须相应移动。

⚠️ 一个副作用值得警惕：用了"安全的语言"会带来心理上的松懈，而本案恰恰是开发者为了绕开语言的默认行为（溢出 abort）而手写检查时出的问题。

核心命题三：单位与量纲

⭐ 这类数学库最容易错的地方，是【单位不一致】：

   · 价格是 Q64.96 定点数，还是 Q128.128？
   · 流动性 L 的单位是什么？
   · 移位 64 位对应的是"乘 2⁶⁴"还是"精度转换"？

⚠️ 一个移位位数写错，就是 2ⁿ 倍的误差 ——
   而它不会报错，只会算出一个数。

⭐ 实践：把定点数格式写进类型名或变量名
      sqrtPriceX96、liquidityQ64
   让不匹配的运算在阅读时就显得刺眼。

一条可以直接执行的检查

把项目里所有【手写的边界/溢出/范围检查】列出来。
对每一个：

   ⭐ ① 它的阈值是"算出来的"还是"写死的十六进制"？
      ② 有没有针对 阈值 和 阈值±1 的测试？
      ③ 如果它错了，下游还有别的东西能兜住吗？

⚠️ 第 ③ 个问题的答案通常是"没有" ——
   这就是为什么这类函数值得单独审计。

七、本案小结

一个手写的"带检查的左移"用错了位掩码，判断阈值远大于正确值，导致本该拒绝的输入通过检查后被静默截断。
⭐⭐ 错误的检查比没有检查更危险：没有检查时语言的溢出 abort 还能兜底，而一个错的检查等于主动告诉运行时"我确认过了，放行"——把兜底机制一起关掉了。
攻击形状与第 9 篇 BEC 相同：BEC 让"应付金额"变成 0，本案让它变成极小值。攻击者用约一个单位的代币换到天文数量的流动性份额。 -⭐ “我们用的是 Move，比 Solidity 安全"救不了：Move 消除的是资源复制和静默溢出，它管不了你自己写的检查用错了常量。而且本案恰恰是开发者为了绕开语言默认行为而手写检查时出的问题。
只有"阈值 ±1"这一对测试能暴露它：离边界远的用例在正确和错误的实现下行为完全相同——而这一对恰恰是最容易被漏掉的。
把常量算出来，不要写出来：1 << 192 一眼能核对，一串十六进制掩码不能。能被人类一眼验证的表达式，胜过一个无法核对的魔法数。
四条 AMM 不变量能自动抓住本案，尤其"存入再立即取出，拿回的不能多于存入的”——fuzz 一跑就报警。
⚠️ 形式化验证证明的是"实现符合规约"，不是"规约是对的"。如果规约里写的就是那个错误阈值，验证器会愉快地证明实现完全正确。
随着语言变安全，剩下的漏洞在比例上更集中于业务逻辑——审计重心必须相应移动。

思考题

为什么说"错误的检查比没有检查更危险"？请用本案说明它如何关掉了语言层的兜底。
正确的阈值应该是 n >= 2¹⁹²。如果掩码写错导致阈值变成 2²⁴⁰，落在 [2¹⁹², 2²⁴⁰) 的输入会发生什么？
为什么"离边界很远的测试用例"无法区分正确和错误的阈值？请构造一组只测远点的用例，说明它们全部通过。
把 const MASK = 0xffff... 改写成一个"能被一眼验证"的表达式。这个改写降低了哪一类错误的概率？
写出本篇那四条 AMM 不变量的伪代码。哪一条最容易实现？哪一条最能抓住本案？
“形式化验证证明的是实现符合规约，不是规约是对的。“请构造一个例子：规约写错了，而验证器给出了"通过”。
Move、Rust、Solidity 0.8 各自消除了哪一类错误？列出三者都不能消除的三类问题。
定点数格式写错一位会造成多大误差？请以 Q64.96 为例计算。
把你项目里所有"守门人"函数（返回 bool 或会 revert 的）列出来。有几个有针对阈值 ±1 的测试？
本案和第 10 篇都以"验证者协调冻结"收场。请讨论：如果两条链的验证者集合都足够去中心化到无法协调，这两起事故的结局会是什么？这是否意味着去中心化有代价？

一、背景：集中流动性的数学#

二、漏洞在哪：一个错误的掩码#

三、攻击复盘#

止损#

四、为什么没被发现#

① “我们用的是 Move，它比 Solidity 安全”#

② 手写的检查没有对应的测试#

③ 边界检查函数看起来"太简单，不值得审"#

五、防御#

① 能不手写就不手写#

② 手写的边界检查必须"两侧夹逼"测试#

③ 把常量算出来，而不是写出来#

④ 不变量测试：金额守恒#

⑤ 形式化验证的正确用法#

六、⭐ 举一反三#

核心命题一：错误的检查比没有检查更危险#

核心命题二：更安全的语言不豁免业务逻辑#

核心命题三：单位与量纲#

一条可以直接执行的检查#

七、本案小结#

思考题#