T30 · Audit
审计到底在审什么？
- 练习的能力
- Builder
- 动手
- 为你的协议写出五条不变量，用 Fuzzing 让它们被自动检验。
- AI Lab
- 让 AI 从代码反推不变量，自己判断哪些是真正的安全性质，哪些只是实现细节。
一个现实问题
一个团队准备上线，花了一笔不小的钱买审计。
三周后报告回来：17 个发现，2 个高危、5 个中危、10 个低危和信息级。团队认真修完了全部 17 条，审计方复核通过，报告最后一页写着所有问题已解决。他们把报告 PDF 放上官网，宣布「已通过审计」，上线。
三个月后，协议被搬空。
事后复盘时最刺眼的一点不是损失金额，而是：攻击路径在那份报告里一个字都没提。 不是审计方看漏了某一行代码——攻击根本没有用到任何代码漏洞。攻击者做的事是先在外部市场把一个抵押品的价格推上去，再用它借走远超其真实价值的资产。每一步调用都完全合法。
团队去问审计方，得到的回答也挑不出毛病：那份报告的范围写得清清楚楚，是「合约代码实现的正确性」，不包含「协议在极端市场条件下的经济假设」。范围就写在报告第 2 页，他们当时没细看。
于是问题变成了：那份钱到底买到了什么？ 以及，如果 17 个发现全修了还是会被搬空，审计的价值到底在哪一部分？
思想实验
假设你是投资人，要在两个协议之间选一个投。两边都给你看了审计报告。
A 协议的报告：58 页，列了 23 条发现。分级齐全，每条都有代码位置、复现步骤、修复建议和「已解决」标记。读起来非常专业。
B 协议的报告：19 页，只列了 6 条发现，其中没有高危。但它前面有两样 A 的报告里没有的东西：
第一样，一份威胁模型。它写清楚了：这个协议假设谁可能来攻击（普通用户、大户、能借到无限资金的套利者、持有治理代币的人、依赖的外部协议本身）、这些人各自能做到什么、以及协议明确不防御哪些情况（比如「我们假设价格源在单个区块内不会被操纵超过 5%，如果超过，协议会产生坏账」）。
第二样，一份不变量清单。11 条，每一条都是一句「无论发生什么，这件事必须永远成立」的断言，而且每一条都配了一个可以自动跑的测试。比如「所有用户存款之和，永远不大于合约实际持有的资产」。
现在请你判断：哪一份报告让你更敢投？
大多数人的第一反应是 A——发现更多，看起来查得更细。但请再想一层：
- A 的 23 条发现告诉你的是「这些地方曾经写错过，现在改了」。它描述的是过去。
- B 的威胁模型告诉你的是「这个协议认为什么是危险的，以及它承认自己不防什么」。它描述的是边界。
- B 的 11 条不变量告诉你的是「以后每改一行代码，这 11 件事都会被自动重新验证一遍」。它描述的是未来。
A 的报告在交付那一刻就开始过期——团队上线后改的每一行代码，都不在它的覆盖范围里。B 的那 11 条不变量会跟着代码库一直活下去。
你来决定
你的协议再过两个月上线。安全预算只够再做一件事。你选哪个？
观察结果
四个选项不是四选一，但它们确实在回答不同的问题。把它们按「覆盖哪一段时间」摆开，结构立刻就清楚了：
| 手段 | 覆盖的时间窗 | 能发现什么 | 交付后还会不会失效 |
|---|---|---|---|
| 审计 | 上线前的一个快照 | 人能想到、且在范围内的问题 | 你改的下一行代码就不在覆盖里 |
| 不变量 + Fuzzing | 从现在到永远 | 违反你所声明性质的状态 | 不失效，跟着代码库一起活 |
| 监控 | 上线后每一刻 | 已经发生的异常 | 不失效，但需要有人真的去看 |
| 漏洞赏金 | 上线后持续 | 别人想到而你没想到的 | 取决于赏金和攻击收益的比值 |
于是可以得到这一章最重要的一句话：
审计是一次快照，而你的协议要活很多年。
一份审计报告在交付那一刻价值最高，之后每过一天就衰减一点——因为代码在变、依赖在变、市场条件在变，而报告不会跟着变。
那么审计里真正不衰减的部分是什么？
回头看 B 协议那份 19 页的报告。让它保值的不是那 6 条发现，而是威胁模型和不变量清单：前者定义了「什么算危险」，后者把这个定义变成了会自动运行的代码。它们是审计过程的副产品，却比发现列表活得久得多。
这就是为什么这一章的标题是「审计到底在审什么」，而答案是：
审计真正的产出是威胁模型与不变量，不是一份 PDF。
一份只给你发现列表的审计，你买到的是一次性的 bug 修复。一份帮你建立威胁模型和不变量的审计，你买到的是一套能持续运行的安全能力。价格可能一样。
建立模型
这一章给三样可以直接拿走用的东西：威胁模型的四问、不变量的三类写法、四层工具各自的能力边界。
一、威胁模型：四个必须回答的问题
威胁模型不是一篇散文，是四个问题的答案。写不出来就说明你还不知道自己在防什么。
| 问题 | 要写出什么 | 写不出来意味着 |
|---|---|---|
| 谁会来攻击？ | 列出角色：普通用户、大户、能借到无限资金的套利者、治理代币持有人、你依赖的外部协议、你自己的多签持有人 | 你会漏掉整类攻击者，尤其是最后两类 |
| 他们想拿走什么？ | 用户存款、协议金库、LP 的流动性、治理权、还是仅仅让协议停摆 | 你会只防资金，不防可用性 |
| 他们各自能做到什么？ | 每个角色的能力边界：能调哪些函数、能出多少钱、能不能控制交易顺序、能不能等很多个区块 | 你会低估「能借到无限资金」这一条，详见 T29 |
| 你明确不防什么？ | 把放弃的假设写下来，而不是假装它不存在 | 这是最重要的一问，下面单说 |
第四问是区分专业和业余的地方。
每个协议都有它不防的东西。不防私钥泄露、不防依赖的预言机整体失效、不防超过某个幅度的单区块价格操纵、不防监管冻结底层资产。这些放弃是合理的——防住一切等于什么都做不成。
不合理的是不把它们写下来。没写下来会产生三个后果：团队内部对边界的理解不一致；集成方以为你防了而其实没防；出事时无法判断这是「设计如此」还是「出了漏洞」。
写法很简单，一句话一条：
我们假设：价格源在单个区块内的偏离不超过 X%。
如果超过：协议会产生坏债，由保险基金承担，超出部分由 LP 按比例分摊。
我们不防：整个价格源被长时间操纵的情形。缓解手段是心跳检查与偏离熔断。对照 T29 你会发现：威胁模型的第三问，就是 T29 那张攻击成本表的输入。 你列出的每个角色能力，都要能对应到那张表里「资金」和「时间」两项的取值。
二、不变量：三类写法
不变量是一句「无论发生什么，这件事必须永远成立」的断言。好的不变量有三个特征：用状态表达而不是用流程表达、能用一行代码检查、违反了一定意味着出事。
实践中绝大多数有用的不变量落在三类里。
第一类：会计不变量。 关于钱的守恒关系，最容易写也最值钱。
所有用户余额之和 <= 合约实际持有的资产
总供应量 == 所有持有人余额之和
借出总额 + 池中余额 == 存入总额 + 累计利息
每股价值 单调不减（除非发生了清算或坏账）注意第一条用的是小于等于而不是等号——留出的差额是手续费和舍入残留。取整方向必须永远对协议有利，这条在 T28 讲过，这里把它变成了可自动检验的断言。
第二类：权限不变量。 关于谁能做什么。
只有管理员能改参数
参数永远在声明的区间内
合约暂停时，任何会改变余额的函数都无法成功
没有任何路径能让非清算人把别人的抵押品转走第三类：状态机不变量。 关于状态之间的合法转移。
一个仓位要么健康，要么可被清算，不存在第三种状态
已关闭的仓位不能再被操作
每个订单只能被成交一次
健康度低于阈值的仓位，不可能还能继续借出写不变量时最常见的错误，是把实现细节当成不变量。「内部数组长度等于用户数」不是安全性质，它只是你当前实现的一个事实——换一种实现它就不成立了，但协议一点也不会更危险。区分方法只有一条：
问自己：如果这条被违反了，有人会亏钱或者失去控制权吗？如果不会，它就不是安全不变量。
三、四层工具：各自能发现什么
把工具按「发现能力」和「需要你做多少事」排开，选择就不再靠感觉：
| 层 | 它能发现 | 它发现不了 | 你要付出什么 |
|---|---|---|---|
| 编译器与类型系统 | 语法、类型、明显的未初始化 | 任何逻辑问题 | 几乎为零 |
| 静态分析 | 已知模式：重入结构、未检查返回值、危险的低层调用 | 你这个协议特有的逻辑错误 | 装一个工具，然后花时间筛误报 |
| Fuzzing | 违反你声明的不变量的状态组合 | 你没写出来的性质 | 写不变量，这是全部成本 |
| 形式化验证 | 在给定模型下，某性质必然成立或不成立 | 模型本身写错的地方 | 很高，通常只用在最核心的几个函数 |
四层里，Fuzzing 的性价比最突出，原因是它的成本几乎全在「写不变量」这一步，而这一步的产出物本身就是资产——它同时是文档、是回归测试、是给集成方看的安全声明。
静态分析的正确用法是当成过滤器而不是判决书：它的误报率不低，你的工作是快速筛掉误报，而不是逐条辩论。
形式化验证不要一上来就用。它适合的场景很窄：一个函数很关键、逻辑不长、性质能被精确表达。比如「份额与资产的换算函数在任何输入下都不会让先存款的人吃亏」。
四、发现要分三类，不是分级
审计报告习惯按严重程度分级。但你在处理 AI 或工具给出的一堆发现时，更有用的是另一种分类：
- 真问题
- 误报
- 漏报
- 真问题：确实存在，要修。
- 误报：工具或模型认为有问题，实际没有。要能快速判断，不要花时间辩论。
- 漏报：真实存在但没有被任何人发现。你无法直接统计它，只能通过「威胁模型里有没有一整类攻击者被忽略」来间接推断。
开头那个团队的问题，就是一次教科书式的漏报：17 条全是真问题，误报为零，看起来完美——但整个「能借到无限资金的套利者」这一类攻击者不在范围内。
它叫什么
一份说明「谁可能攻击、想拿走什么、能做到什么、以及你明确不防什么」的文档。
它是审计的输入而不是输出。没有威胁模型的审计，等于让人在不知道你要防谁的情况下检查你的门锁。
一句「无论发生什么，这件事必须永远成立」的断言，用状态表达，可被自动检验。
判断它是不是安全不变量只有一条标准：违反了，有人会亏钱或失去控制权吗。
不运行代码，按已知模式扫描源码或字节码。擅长发现重入结构、未检查的返回值、危险的低层调用这类有固定形状的问题。
用它当过滤器，不要当判决书——误报率不低。
自动生成大量随机输入与调用序列，试图找到违反不变量的状态。
有状态 Fuzzing（连续调用多个函数、保留状态）比无状态的强得多，因为真实漏洞几乎都出在调用序列上，而不是单次调用上。
用数学方法证明某个性质在给定模型下必然成立。
它的结论强度远高于测试，但它只在你写下的模型里成立——模型写错了，证明也是错的。适合范围很窄、逻辑很关键的函数。
上线后持续观察链上状态，在异常出现时通知人。
它的价值不在于阻止攻击，而在于压缩「发生」到「发现」之间的时间。对有暂停开关的协议，这段时间几乎直接等于损失金额。
公开承诺：找到并负责任地披露漏洞，可以获得报酬。
有效的前提是赏金上限与攻击收益可比，以及你有能力快速修复。
动手
用 T22 或 T19 里你自己写过的那个协议。如果都没有，用 T7 的存取款合约也可以。
先写威胁模型的四问。 不要跳过这一步直接写不变量——不变量是从威胁模型里长出来的。
四个问题各写三到五行：谁会来攻击、想拿走什么、各自能做到什么、你明确不防什么。第四问至少写两条。
从三类里各挑一条，凑够五条不变量。 建议配比：两条会计类、两条权限类、一条状态机类。
每条写成一句断言，并在旁边注明「违反了会怎样」。写不出后果的那条，划掉重写——它多半是实现细节。
把五条翻译成断言函数。 每条一个函数，内部只做检查，不改状态。
会计类的那两条要特别注意比较方向：用小于等于还是等于，取决于是否存在手续费和舍入残留。方向写反了，Fuzzing 会立刻炸给你看——这是好事。
接上有状态 Fuzzing。 关键是让它连续调用多个函数并保留状态，而不是每次都从初始状态开始。真实漏洞几乎都藏在调用序列里。
先跑一个短回合，确认它真的在调你的函数（打印一下调用计数），再跑长回合。
故意破坏一条，确认它能被抓到。 这一步不能省。
把某个函数里的取整方向改反，或者把一处权限检查注释掉，重跑 Fuzzing。如果它还是全绿，说明你的不变量没有真正生效——可能是断言写在了不会被调用的地方，也可能是 Fuzzing 根本没碰到那条路径。
改回来之前，把失败时它给出的那条调用序列存下来，那是一个现成的回归测试。
记录三个数字：Fuzzing 跑了多少回合、覆盖了哪些函数、最短的失败序列有几步。
最后一个数字最有信息量：失败序列越短，说明这个漏洞越容易被真实攻击者碰到。
做完这一步，你手上就有了一份能跟着代码库一起活下去的安全资产。它也是毕业项目第五阶段要交的东西。
AI Lab
把你的合约代码交给模型，任务分两步。
第一步，让它反推：
这是我的合约代码。请反推出它隐含的不变量——也就是那些
「无论发生什么都必须成立」的性质。
每条输出四个字段：
- 断言（用状态表达，不要用流程表达）
- 它依赖代码里的哪一处（给出函数名与行号）
- 如果被违反，会发生什么
- 你的判断：这是安全性质，还是仅仅是当前实现的一个事实
不确定的标注「不确定」，不要猜。第二步，让它挑自己的毛病：
现在回到你刚才给出的清单，指出其中哪几条其实是实现细节而不是安全性质，
并说明理由。第二步往往比第一步有价值。 模型在反推时倾向于把「当前代码恰好如此」写成不变量，比如「数组长度等于用户数」「某个映射的键总是非零」。这类断言全部成立，但一条都不保护资金。
你的工作是拿着右边的清单逐条过。过完以后统计一个比例：它给出的条目里，有多少是真正的安全性质。 这个比例值得你记下来——它会告诉你，在这类任务上模型能帮你到哪一步。
最后一条验证项最重要：把它的清单和你自己写的威胁模型对照。如果你的威胁模型里有「能借到无限资金的套利者」，而它给出的不变量里没有任何一条涉及单笔交易内的极端状态，那就是一个漏报。模型看得见代码，看不见你的威胁模型。
AI 说完之后，你必须自己验证
- 每一条被判为「安全不变量」的，你都能说出「违反了谁会亏钱或失去控制权」
- 被判为「实现细节」的，确认换一种实现它就不再成立，且协议并不会更危险
- 它引用的函数名、变量名在你的代码里真实存在，没有编造
- 会计类不变量的比较方向（等于还是小于等于）与手续费、舍入残留的实际情况一致
- 它有没有把「当前代码恰好如此」当成「必须永远如此」——这是最常见的错误
- 对照你自己的威胁模型：有没有一整类攻击者，它给出的不变量完全没有覆盖
真实案例
一个协议完成审计并修复全部发现后上线，随后因价格源被操纵而损失大量资金。攻击没有用到任何代码漏洞——每一步调用都合法。
事后争议集中在一点：审计范围里是否包含经济假设。多数情况下，答案写在报告前几页，而多数团队没有细读。
教训不是「审计没用」，而是：审计的范围就是它的能力边界，而范围是你和审计方一起定的。 你如果没提供威胁模型，范围就默认只剩代码实现。
一个金库类协议的全部单元测试通过，覆盖率很高。接上有状态 Fuzzing 后，很快找到一条七步调用序列，使「每股价值单调不减」这条不变量被违反。
原因是几个函数单独看都没问题，但特定顺序下的舍入累积让先进入的人吃了亏。
这类漏洞单元测试几乎发现不了——因为写单测的人和写代码的人是同一个人，他想不到的顺序，也不会写进测试。
一个团队部署了链上监控，异常发生时告警确实触发了。但告警发进了一个平时噪音很大的频道，凌晨没有人值班。
发现时已经过去几个小时，而协议的暂停开关一直可用。
教训：监控的有效性由「谁在什么时间会看到它」决定，不由「有没有部署」决定。 告警要分级，高危告警必须有明确的值班人和响应时限。
一些协议设置了固定的赏金上限，而协议可被触及的资金远高于这个数。
这等于给发现者出了一道简单的算术题。行业里逐渐转向按「可挽回损失的百分比」设定上限，就是为了让这道题的答案变成举报。
这和 T29 的攻击成本表是同一张表：你在调整的是「举报收益」这一项，让它压过「攻击收益」。
改一个变量
审计的范围会被你主动定义，而不是默认落在「代码实现正确性」上。
审计方会针对你声明的攻击者能力去查，也会对你「明确不防」的那几条提出质疑——那几条质疑往往是整份报告里最值钱的部分，因为它们打的是你的假设，而不是你的代码。
成本几乎为零，只是一份你本来就该写的文档。
从「测试时检查」变成「运行时强制」。违反时交易直接回滚，攻击在链上就被挡住了。
代价是 Gas：每笔交易都要多做一遍全局检查。所以现实做法通常是分层——最关键的一两条会计不变量放进运行时，其余留在 Fuzzing 里。
这里的取舍和 T8 的存储成本是同一个性质的问题：安全性通常要用 Gas 去买。
你的代码一行没改，但你的安全假设可能已经变了——它的接口语义、它的手续费行为、它的重入保护，都可能不一样了。
这正是「审计是一次快照」最直接的体现：报告是针对当时那个依赖版本的。
应对方式是把依赖的关键假设也写成不变量，并在监控里加一条「依赖合约的实现地址发生变化」的告警。
前面所有的工作会被这一件事绕过去。不变量、Fuzzing、审计报告都防不住一个拥有全部权限的账户。
这是威胁模型第一问里最容易被跳过的角色：你自己。 多签、时间锁、权限最小化属于这一层，而且它们通常比再买一次审计便宜得多。
带走的问题
谁承担风险？审计报告通常会写明它不对损失负责。风险始终在协议方和用户身上，审计只是降低了概率。把「已通过审计」当成安全保证，是这个行业里代价最高的误读之一。
为什么需要 Blockchain？因为代码公开、状态公开，任何人都能独立验证你的不变量是否成立。这既是压力也是机会：你的不变量可以做成公开的、任何人都能跑的检查，这比一份 PDF 可信得多。
如果补贴停止还有用户吗？这一问在安全语境下换个说法：如果你的团队解散了，这个协议还安全吗？ 靠人工盯盘维持安全的系统，答案是否定的；靠不变量和权限设计维持安全的系统，答案可能是肯定的。
本章自测
威胁模型与不变量清单。
发现列表描述的是「过去这里写错过」，交付那一刻就开始衰减——你上线后改的每一行代码都不在它的覆盖里。威胁模型定义了边界，不变量会跟着代码库一直自动运行。
问一句：如果它被违反了，有人会亏钱或者失去控制权吗？
「所有用户余额之和不超过合约实际持有的资产」——违反了就有人取不出钱，是安全不变量。 「内部数组长度等于用户数」——违反了可能只是实现变了，协议并不更危险，是实现细节。
因为真实漏洞几乎都藏在调用序列里，而不是单次调用的参数里。
单独看每个函数都正确，特定顺序下却会让舍入累积、让状态进入不该出现的组合。无状态 Fuzzing 每次从初始状态开始，永远碰不到这类问题——写单测的人想不到的顺序，它同样想不到。
因为一个永远不会失败的检查和一个不存在的检查，效果完全一样，但前者会给你虚假的安心。
断言可能写在了不会被调用的位置，Fuzzing 可能根本没碰到那条路径。只有让它真的红一次，你才知道它是活的。
这和 T12 里「先写失败用例」是同一条原则。
没有标准答案。检查三件事：
- 你有没有真的写下来，而不是假装不存在？
- 每一条有没有说清「如果发生了，后果由谁承担」？
- 有没有一条涉及你自己——管理员密钥、多签成员、升级权限？
第三条最容易被跳过，而它是前面所有工作的绕过路径。
一句话带走
审计真正的产出是威胁模型与不变量，不是一份 PDF。