红队拿到直升机相机分区的控制权也没能弄坠它，形式化方法到底锁死了什么

2016 年，一架波音无人小鸟直升机载着两名试飞员起飞。DARPA 红队被允许在相机分区里放任何代码，目标不是搞崩一个分区，是让整架直升机掉下来。

试飞员全程没察觉异样。落地后他们才知道自己飞的是被攻击过的版本。真正崩的只有相机分区自己，系统检测到它挂了，重启了事。

这是 DARPA HACMS 项目第三阶段的一幕。项目负责人 Kathleen Fisher 后来当过 DARPA 信息创新办公室总监，现在是 RAND 网络安全计划主任，2026 年 2 月要去英国 ARIA 当 CEO。同台的 Byron Cook 是 Amazon 副总裁兼杰出科学家，2014 年加入后把形式化方法带进了 AWS 的核心基础设施。

这集播客把一门被称作「修道院里的学问」的冷门技术讲成了可执行的工程路线。听完最强烈的感受是：AI 正在同时加速攻击和防守，而形式化方法是少数能把某些漏洞「一次性关死」的手段。

AI 让整条攻击链上所有人都变强了

主持人 Nathan Labenz 问了一个很实际的问题：AI 对网络攻防的真实影响，到底哪些是炒作，哪些是真的。

Kathleen 的回答毫不含糊：全都在发生。AI 在攻击链的每个阶段、每个技能层级上提供帮助。不懂的人变得懂一点，懂一点的人变得更懂，专家变得更高效。攻击者还能以前所未有的规模并行作业。

我那些世界顶级的逆向工程同事，看到 AI 工具帮他们干活的效果时都惊呆了。

从脚本小子到勒索软件团伙到国家级攻击者，AI 让每一层都变强。这是坏消息。

Byron 补了一个乐观版本。过去几十年，软件安全在很大程度上依赖「机制的缺失」：人写代码，写完也不太清楚程序到底在干什么，于是雇几个靠谱的人边写边看。这叫社会技术机制。现在有了 agentic AI 工具，行业开始从社会技术机制转向形式化。每次安全事故发生，团队可以写下「我们永远不要再进入那个状态」，把这条性质写进代码里。每次事故对未来系统的改进半径，比过去大得多。

Kathleen 把这个判断拉回地面：现在的软件满是漏洞，AI 会让这些漏洞更容易被利用。同一套技术也能反过来让软件更少漏洞。软件是硬件、软件、人这三层里最容易快速改善的一层。

已经能看到的具体进展包括 Google 的 CodeMender 项目、OpenAI 的类似工作，以及 AI Cyber Challenge 竞赛展示的结果：AI 加网络安全能以速度和规模发现并修复 bug。

形式化方法：从 Java 类型检查器到 CompCert

Byron 给了一个极简定义：算法化地搜索证明。证明是一个有限的论证，说某件事为真。你可以用有限的时间和空间去推理无限的东西，前提是有一套像国际象棋那样的规则，两千年来社会沉淀下来的少数几条，比如肯定前件式。你严格遵守这些规则做论证，现在可以靠算法去搜索这些论证。生成式 AI 在这件事上表现相当好：帮你找证明，再交给只认这些规则的检查器去验证。

Kathleen 把光谱展开了。形式化方法不是一招鲜，是一整套数学技术，让机器能检查你确实把活干对了。光谱的一端很好用，保证也弱：Java 的类型检查器就是形式化方法。你写 Java、跑编译器，它证明你不会把整数和函数相加，不会把数据当成别的类型乱搞。用过类型系统，就用过形式化方法，只是保证比较薄。

另一端是交互式定理证明器，证明完整功能正确性。CompCert 是经过验证的 C 编译器，证明 C 代码映射到汇编代码后语义完全一致。做这个证明要用到博士级脑力，每一步逻辑都被机器检查。

中间还有大量工具，保证强度和投入精力都在中间地带。用哪一档，是门手艺。

主持人追问 CompCert 还剩哪些假设。Byron 说，大概是对底层硬件的假设。Kathleen 补充：假设 x86 或 ARM 指令集正确，他们对 ISA 有模型但没去证明 ISA 本身。早期版本还有对解析器的假设，后来发现不对，修了。他们假设单线程，因为面向航空电子软件。调用操作系统时，假设操作系统 API 的行为。第三方 API 也一样。好消息是外部世界可以用「恶魔式非确定性」建模：不知道某个调用返回什么，就用一个公式表示「我不知道」。非确定性在形式化工具里是已经付过费的能力，相当好用。

所以结论是：永远有假设，一层套一层。证明微处理器正确，就要假设物理定律成立。你只能不断提高保证，拿不到 100%。

那架直升机：把系统级性质证出来

HACMS 项目的核心故事值得完整讲一遍。

seL4 是一个分离内核，澳大利亚团队证明过它的完整功能正确性。核心性质是：系统可以配置成不同隔间，一个隔间里的代码无法干扰另一个隔间。大约 1 万行 C 代码，配了约 10 万行 Isabelle 证明。投入这么大，是因为它是可以复用的积木。

HACMS 的执行者用 seL4 把直升机上的代码分成分区。相机分区经过分析，判定为对飞行安全不重要，坏人拿走也没关系。任务控制计算机负责和地面站通信。飞行计算机负责让直升机飞起来。

团队用 AADL 架构描述语言给整个系统架构建模。通信协议不用手写，写的是语法，规定消息格式必须长什么样。然后用解析器工具证明性质，用加密工具证明加密性质，用 seL4 拿到隔离性质。他们证明的是系统级属性：从地面站到任务控制计算机的唯一通路必须经过认证和加密。

红队分三个阶段。第一阶段攻未修改的平台，波音工程师很惊讶红队六周知识就能攻进去。第二阶段在地面攻击。第三阶段在飞行中攻击，两名试飞员在机上。

结果前面说过了。相机分区反复崩溃，红队能在自己的分区里放 fork 炸弹，系统检测到就重启那个分区。飞行操作完全不受影响。试飞员分辨不出自己飞的是高保证版本还是普通版本。

还有个后续。DARPA 把同款技术改造的四轴飞行器带回 DEF CON 的航空航天村，几年后让黑客随便试，没人能攻进去。Kathleen 说这证明了这类技术经得起时间。当然还是有假设，大概率能从硬件攻进去，软件这条路被堵得很死。

AWS 十年：每秒被调用十亿次的策略解释器

Byron 2014 年到 Amazon 时，客户喜欢策略语言的灵活性，也喜欢虚拟网络的灵活性，唯独不喜欢「不知道自己写对没有」。

第一批工具是给客户自己用的：IAM Access Analyzer 推理策略，VPC Reachability Analyzer 推理网络可达性，S3 Block Public Access，Inspector，Config 规则。内部则挑了几个必须做对的地方：密码学、虚拟化基础设施、存储持久性、身份基础设施。

最能说明问题的是策略解释器。你调用任何一个 AWS API，系统把主体和资源相关的所有策略收集起来，交给这个解释器，做出允许或拒绝的决定。这段代码每秒被调用超过 10 亿次，现在已被证明正确。

这里「正确」有精确含义：相对于之前那套工具里定义的策略语言语义。这是工具开始互相连接的例子。先定义语义，再给客户工具去形式化推理自己的策略，客户接着问「我怎么知道你的解释器符合这个语义」，那就去证。

s2n 是 Amazon 写的开源 TLS 实现，全公司都在用。证明它的 TLS 握手正确，完全自动，底层用 SAT 求解器加归纳不变式发现。密码学代码的循环通常很简单，不涉及复杂数据结构，简单启发式就够用。

另一个极端是 2025 年发布的 Isolation Engine，一个新的 hypervisor，会进入 AWS 的 Graviton 5 栈，用 Isabelle 定理证明器证了一堆性质。Byron 估的团队比例大约是形式化方法专家和工程师一比一。

把 HR 手册变成可验证的逻辑

这是整集里对 AI 工程师最直接有用的部分。AWS 的 Automated Reasoning Checks 声称能把 AI 幻觉压下去，交付最高 99% 的验证准确率。

流程是这样的。你手里有一份自然语言政策，比如家庭医疗休假法（FMLA）的条文，写的时候压根没考虑过软件实现。现在你想让 AI 来审批休假申请。

第一步，把自然语言翻译成形式逻辑。可以是线性时序逻辑、分支时序逻辑、SMT、Lean。今天你直接让 Claude 干这事也行，产品在底层做的就是这个。

问题来了：用生成式 AI 做形式化，可整件事的目的就是对付生成式 AI 的幻觉。怎么办？

系统会遍历那个公式的结构，计算出所有有代表性的边界情况，带着非专家走一遍「你会得到什么答案」。你不喜欢某个答案，用自然语言说为什么不满意，回到生成式 AI 重新翻译。这其实复刻了形式化方法行业几十年的工作方式：一个形式化专家配一个领域专家，看一堆例子，领域专家说「你搞错了，你没理解这个假设」，改，再来，直到找不出问题。

部署之后，用户的提问被翻译成自然语言，映射回形式模型，证真或证伪。翻译这一步也有讲究：做多次独立翻译，用定理证明器检查几次翻译彼此等价。等价就说明翻译可信度较高，这就是 99% 而非 100% 的来源。不等价就触发一种「主动倾听」：一个翻译说头等舱，另一个说经济舱，回去问用户你指的是哪个，或者查数据库。

Byron 举了个更能说明「规格才是难点」的例子。「所有静态数据都加密」听起来很合理。什么叫加密？从街边买的加密盒子算不算？那不算的话怎么定义？什么叫静态？数据在网络里飞来飞去，靠延迟一直转圈从没落盘，算不算静态？光这一条就要来回细化三四轮。

还有个反复出现的组织难题。你找到一个疑似 bug，叫三个工程师来看，一个说是 bug，两个说不是，环境条件不可能触发。吵不出结果。唯一能服众的办法是写出利用代码，证明它真能发生。有些工具很擅长直接吐出触发路径，有些工具只说「证明没通过」，你自己猜。

产品化的意义在于把这件事的门槛降下来。波特兰的 ADU（后院小房子）审批是个好例子。现在你得请建筑师，最好是熟悉波特兰而不是波特兰缅因州规则的那种。退缩线规则、限高规则、什么时候可以贴着地界建，中介帮你搞定，你不知道他是不是做到最优。如果规则被形式化、开放出来，普通人可以 24 小时随时问，答案可验证，还能反过来讨论某条公理本身是否公平。保存历史对话，改了规则重放一遍，看哪些答案会变。

大模型和形式化方法的化学反应

Byron 给了一个四层阶梯，解释了为什么生成式 AI 在这个领域特别有用。

• 没有循环和递归，只有条件表达式。问「火箭会不会被发射」是 NP 完全问题，等价于命题可满足性。SAT 求解器进步惊人，从单机走向分布式，Mallob 这样的工具把大量求解器铺到网络上共享引理，有类似缩放定律的效果。这是 AWS 能在 20 秒内推理你的策略和 VPC 网络的原因。
• 有循环，但只关心某个断言永不失败。这是不可判定问题，要找到归纳不变式。
• 关心「最终」或终止性。要找到排序函数，还要归纳不变式，还要组合推理。
• 并发。多个线程，要用 rely-guarantee 找环境抽象，一次只证一个线程。

第一层工具已经很强。后三层过去也有技术，但真正靠谱的办法往往是雇一个博士拴在工位上。生成式 AI 改变的是：你可以让它找归纳不变式、找排序函数、找 rely-guarantee 约束，剩下的事情退化成组合推理，而组合推理有很好的工具。再叠上云端并行，把不同工具组合跑在不同机器上，挑最满意的答案。

Kathleen 补了训练数据的角度。形式化语言是稀疏语言，公开训练数据不多。但这个领域能自己生成训练数据并自动验证正确性，把验证通过的结果喂回去，飞轮就转起来了。她特别强调需要高质量基准，让前沿模型公司在「代码安全性」这个维度上竞争，而不只是竞争「能写代码」。

如果未来大量代码由语言模型写，能不能让它们写内存安全的、类型安全的、输入验证过的代码？模型本身不在乎，得靠基准和激励去引导。

主持人问：GPT-6 和 Gemini 4 这一代是不是就该在「一次写对安全代码」上超人水平了？Byron 说会，Nova 和开源权重模型也会，而且已经在发生，前一周刚有开放数学难题被证明。

Kathleen 的补充更关键：光有能力不够，还要激励。要给好代码创造激励，给坏代码创造抑制，再给「用好代码替换关键基础设施里的存量坏代码」创造激励。她提到 DARPA 的 TRACTOR 项目，目标是把 C 自动翻译成地道的 Rust，从非内存安全语言迁移到内存安全语言。迁移过程中最容易证的性质之一，就是新旧两个程序等价，因为这时候你已经有规格了。

一个反直觉的冷水：安全技术会让人开得更快

主持人问了个很自然的问题：如果全社会停下来做一次大重写，多久能做完，能不能做到不再需要 AI 攻击者去到处戳漏洞？

Byron 的回答值得单独拎出来。他说每一项安全技术都只是让我们能更猛地往前推。车更安全了，人就开得更快。他讲了个亲历的例子：有家公司原本把设备驱动放在用户空间，因为某些游戏变慢，就把驱动挪进内核空间，保护没了。视频驱动干脆不检查错误条件，因为常见路径要高性能。商业市场在可用性、功能、性能、安全之间做权衡，不会全力押注安全。

这也解释了为什么纯靠市场推动安全进展缓慢。Kathleen 说网络攻击越来越严重这句话已经成立了二十年，大家像温水里的青蛙，一直没真正动员。2000 年千年虫问题倒是动员了一次，全社会一起改代码，最后没出大事。技术会准备好的，问题是什么时候社会有动力去用。

Byron 自己按安全声誉选电脑和手机，愿意为此付溢价，也建议别人这么做。AWS 最近推的 Kiro IDE 主打规格驱动开发，AgentCore Policy 用 Cedar 语言形式化地圈定 agent 可以做什么不可以做什么。这些都是把「声明式编程」重新推到台前的动作。

明天就能用上的几件事

如果你在给企业做生成式 AI 应用，这套方法有一套最小可行路径。先把业务规则从文档里抠出来，翻译成逻辑约束，让领域专家逐条确认边界情况。多跑几路独立翻译做交叉验证，不一致的地方回去问人。部署时把模型输出映射回逻辑层做证真证伪，别让模型自己给自己打分。

给规则系统留一条「去找 Steve」的逃生通道。波特兰 ADU 的例子说明，有些判断需要人的裁量权。把它显式地写成最后一条公理，比藏在提示词里靠谱。Kathleen 提醒的另一面也成立：人的判断有时带来灵活性，有时带来偏见，哪条规则允许裁量、裁量到什么程度，得逐条讨论。

如果你是模型厂或评测机构，安全基准是稀缺品。代码能力已经有大量 benchmark，代码的安全性和可验证性几乎没有。谁先把这块做起来，谁就能让前沿模型的竞争多一个维度。

如果你只是普通用户，最实在的动作是买东西时看一眼厂商的安全记录，愿意为它多付一点钱。商业市场的反馈回路慢，但确实存在。两位嘉宾在结尾达成的共识是，形式化方法和 AI 像花生酱和巧克力，一个给保证但僵硬，一个灵活但不可信。把两者接起来的地方，才是接下来几年真正值钱的手艺。