我第一次认真进行审计时，打开了仓库里最大的合约并开始逐行阅读。两小时后，我头疼欲裂却一无所获。我已经记住了代码的运作方式，却从未问过它应该保证什么。这是本末倒置的，我花了一段时间才改正这个习惯。

现在我不再先读 Solidity。我先读范围说明，在查看任何函数体之前，我就写下哪些条件必须始终成立。漏洞就是对这些条件的违反。如果你不知道这些条件，那就只是在欣赏代码而已。

第一步：在阅读之前写下不变量

不变量是指协议声称无论谁以何种顺序调用什么，它都始终成立的属性。对于一场竞赛，我从资金和控制权入手，因为这正是严重性所在。

两个问题就能覆盖大部分内容：

  • 谁可以在什么条件下转移资金？
  • 关于账目，哪些条件必须始终成立？

对于一个借贷池形状的协议，我初始的不变量列表如下所示，这些是用通俗语言写成的，在我关心任何实现细节之前：

  • 所有用户存款减去所有借款之和，等于池子的可用流动性加上未偿债务。账目必须一致。
  • 用户只能提取自己余额以内的金额，不能多提，也不能提他人的。
  • 一个仓位只有在真正低于健康阈值时才能被清算。
  • 利息单调递增，绝不会倒退到让某人偿还少于其欠款的程度。
  • 只有借款人，或对不健康仓位的清算人，才能减少债务。
  • 除了治理之外，任何人都不可以更改利率参数或预言机。

请注意，这些不变量没有提及任何函数名称。这些就是承诺。现在，我在比赛剩余时间里的工作就可以简单陈述为：找到一个打破其中一条的调用顺序。

第二步：映射外部入口点

资金不会凭空转移。必须有外部调用才能改变状态。因此，我列出每一个可以从外部到达的函数，因为攻击面就是这个集合，仅此而已。

我在仔细阅读任何内容之前，就用 grep 快速完成这项工作：

# every external / public function in scope
grep -rnE "function .*\b(external|public)\b" src/ \
  | grep -v "view\|pure"

Enter fullscreen mode Exit fullscreen mode

我去掉 view 和 pure 函数，因为它们无法改变状态。剩下的是攻击者可以拉动的控制杆列表。对于借贷池，这通常是熟悉的集合：deposit、withdraw、borrow、repay、liquidate，以及任何存在的管理员设置函数。

然后，我为每个函数标注它可能威胁的不变量。deposit 和 withdraw 威胁账目一致性；withdraw 威胁“只能提取自己余额”规则；liquidate 威胁“仅当不健康时”的规则；设置函数威胁“仅治理可操作”规则。现在我有了一个网格：入口点在纵轴，不变量在横轴，交叉的单元格就是我要去寻找漏洞的地方。

第三步：绘制信任边界

大多数真实的发现都存在于协议信任了本不该完全信任的事物的边界处。在阅读逻辑之前，我先标记每一个边界：

  • 预言机。价格来自哪里？是否可以在单笔交易中被操纵（AMM 的现货价格是典型的陷阱）？如果返回陈旧数据、零值或回滚会发生什么？
  • 管理员和角色。特权角色可以做什么？是否有特权路径可以通过代理或委托调用以代码未预期的方式到达？“管理员可以 rug”通常不在范围内，但“非管理员可以达到仅管理员的效果”是 High 级别问题。
  • 跨合约调用。每个外部调用都是控制离开合约并可能返回的地方（重入），或者被调用方可能以敌对方式行为的地方（具有奇怪转账逻辑的恶意代币、带转账费的代币、弹性供应代币）。
  • 代币假设。代码是否假设 18 位小数？是否假设 transfer 返回布尔值？是否假设转账不收取费用？每一个假设都是一个恶意代币可以跨越的边界。

对于借贷池，预言机边界是我首先要查看的地方，因为“操纵价格、用膨胀的抵押品借贷、卷款走人”是很多 High 级别漏洞的典型模式。

第四步：现在阅读代码，寻找违反不变量的情况

直到现在我才打开函数体。而且我不是把它们当作“这个函数是做什么的”来读，而是当作“这个函数触及了哪个不变量，我能在这里打破它吗”来读。

这里有一个简短的工作示例。伪代码，借贷池形状，故意有 bug：

// invariant at risk: a user can only withdraw up to their own balance
function withdraw(uint256 amount) external {
    uint256 shares = amountToShares(amount);
    // BUG: no check that balanceOf[msg.sender] >= shares
    balanceOf[msg.sender] -= shares;   // underflows? or does it?
    totalShares -= shares;
    token.transfer(msg.sender, amount);
}

Enter fullscreen mode Exit fullscreen mode

采用不变量优先的阅读方式，我不会问“这个函数是否转移代币”。我会问“它是否强制执行了你只能提取自己余额的规则”。答案是否定的，减法之前没有边界检查。在旧版 Solidity 中，这会下溢成一个巨大的余额。在 0.8+ 中，它会回滚，所以可能安全……除非 amountToShares 的取整方式让 shares 为零而 amount 不为零，在这种情况下，你提取了代币却没有扣减任何东西。这就是漏洞所在。我会用 Foundry PoC 验证它，因为一个假设只有在测试失败后才成为一个发现。

再看预言机边界：

// invariant at risk: only genuinely unhealthy positions can be liquidated
function liquidate(address user) external {
    uint256 price = ammPair.getSpotPrice();   // single-block manipulable
    uint256 collateralValue = collateral[user] * price;
    require(collateralValue < debt[user], "healthy");
    // seize collateral, repay debt
}

Enter fullscreen mode Exit fullscreen mode

不变量说清算只发生在仓位真正不健康时。但价格来自一个现货 AMM 读取，一个资金充足的攻击者可以使用闪电贷在单笔交易内推高价格。因此，他们可以让一个健康的仓位看起来不健康，然后清算它并获利。这个漏洞不在于算术，而在于信任了一个可操纵的来源。不变量优先的思考方式能发现它，因为我在第三步就已经将预言机标记为一个边界，远早于阅读这个函数。

为什么这个顺序很重要

如果你先读代码，你就会被它的工作方式所锚定，并开始相信它。作者的思维模型会渗入你的思维。你最终检查的是代码是否实现了它表面上意图要做的事，这与审计恰恰相反。审计是检查代码是否可以被强制去做它绝不能做的事。

不变量优先颠倒了这个框架。你先决定协议承诺了什么，与实现无关。然后，每个函数都是一个针对这些承诺的嫌疑人。当我构建 spectr-ai 时，这就是我试图嵌入其推理方式的结构：先陈述属性，然后根据这些属性检查代码，而不是自由联想“漏洞”。

这也更快。在我本周挑选的这场竞赛中，写下不变量列表大约花了 40 分钟，它把一个 2000 行的代码库变成了一个简短的列表：“这里有六件值得打破的事，以及它们最可能打破的三条边界。”那是一张地图。从第一行读到第二千行，只是在游荡。

当你面对一个不熟悉的代码库时，你是先写下哪些条件必须始终成立，还是直接深入代码并在阅读过程中重建规则？