伟大的安全更新：AI ∧ 形式化方法——RAND的Kathleen Fisher与AWS的Byron Cook
摘要
AI正在降低技能门槛、抬高专家上限，并让网络攻击实现大规模并行化。 Kathleen Fisher的判断是「遗憾的是，以上全部」：从脚本小子到民族国家级对手，所有攻击者都在变强。Byron Cook的补充是，防守方可以把每次事件转化为一个形式化属性，让失败对未来系统改进产生「大得多的爆炸半径」。
形式化方法只能为选定属性提供机器可检验的保证，不能笼统证明系统安全。 实际目标是划定一个运行边界——凭证永不写入日志、所有静态数据均加密，或某类数据永不离开某个区域——而不是穷尽描述每一种行为。假设一层层向下延伸，从操作系统API到处理器模型乃至物理规律，但嘉宾认为，如今的基线太差，单是把门窗关上并锁好，就足以彻底改变风险水平。
HACMS直升机证明，组合式证明可以转化为可信的系统级防护。 一套约10,000行的SEO4内核由约100,000行Isabelle证明支撑，将关键飞行功能与受攻击的摄像头分区隔离；一次搭载2名飞行员的空中红队攻击中，被攻陷的分区反复崩溃、重启，却没有影响飞行。DARPA后来把类似的四轴飞行器防御系统交给DEF CON黑客测试，系统同样未被突破。
AWS已经把形式化推理嵌入商业关键基础设施，而不是把它当成学术式的保证剧场。 IAM Access Analyzer、VPC Reachability Analyzer及相关工具帮助客户分析配置；AWS的策略解释器每秒调用超过10亿次，并已相对于形式化定义的策略语义证明正确。另有工作覆盖密码学、虚拟化、持久性和身份系统，相关证明正逐渐「开始相互接触」。
Automated Reasoning Checks把自然语言策略转化为形式化模型，并用定理证明约束AI输出。 由于最初的翻译本身可能产生幻觉，用户需要检查模型生成的边界案例并持续完善模型；推理时，系统会检查多个翻译是否逻辑等价，因此支持的是「最高99%的验证准确率」，而不是100%。其商业价值在于，为人力资源、分区规划、合规和智能体工作流提供强度异常高的最后一道护栏。
生成式AI可能改写如今不安全代码的叙事：同时生成程序和可独立检查的证明产物。 模型可以搜索归纳不变量、秩函数和并发抽象，这些工作过去需要稀缺的博士级人才；确定性工具则负责验证结果。Fisher预计，只要明确把安全能力纳入奖励目标，GPT-6、Gemini 4、Nova以及开放权重模型都将成为超越人类的安全代码工程师。
一次伟大的软件重写在技术上正变得可行，但决定时间表的可能是激励机制与治理，而非原始能力。 AICC、Google的CodeMender、OpenAI的同类项目以及DARPA的TRACTOR，都指向以更快速度发现、修复和翻译脆弱的遗留代码，包括在适用时通过程序间等价性检查把C迁移到Rust。然而，更安全的系统会诱发更激进的使用——「因为汽车更安全，我们就开得更快」；形式化政策还带来第二重挑战：保留合理例外，同时不把人为偏见重新引入系统。
精读
1. AI让所有攻击者规模化，失败也可能复合成更强的防御
Fisher对威胁的判断是绝对的：「遗憾的是，以上全部。」AI正在协助网络攻击链的每一个环节，提升并行度，让新手、熟练操作者和专家都更有效率。她认识的世界级逆向工程师甚至都「震惊于AI工具有多强」，无论是作为助手还是独立工作。
因此，今天的脆弱软件正同时面对多重威胁：规模化勒索软件和民族国家级攻击、隐蔽入侵、公开攻击，以及失控运行的自主智能体。Cook认为，软件是近期最适合防守的「甜蜜点」，但完整系统还包括同样可能出错的硬件和人。
Cook更乐观的框架是形成反馈回路：防守方可以把每次事件转化为一个属性——不记录凭证、所有静态数据均加密、指定数据永不离开某个区域——再针对后续代码证明这些属性。即使这对当下的安慰有限，每次入侵也可能对未来系统改进产生「大得多的爆炸半径」。
2. 形式化方法从日常类型检查延伸到完整正确性证明
Cook给出的简洁定义是「对证明进行算法式搜索」。证明是「关于某个命题为真的有限论证」，人们由此可以遵循一小组被接受的逻辑规则，在有限时间和有限空间内「推理无限对象」，而规则的每次应用都能由机器检查。
Fisher把形式化方法描述为一整套数学技术谱系：可用性越高，保证的丰富程度通常越低。Java的类型检查器只能证明相对有限的事实——一个整数不会被意外加到函数上——但普通开发者无需理解背后的证明机制，就能获得这层保证。
JavaScript的托管内存提供了另一种基于形式化方法的保证：以整数存储的值不会随后「自行变形」成一个函数。C缺少这种内存安全抽象，除非由其他机制补足，否则会暴露出一个尤其有价值的攻击面。
在困难的一端，CompCert证明C源代码映射到汇编后仍具有相同语义。交互式定理证明可以建立完整的功能正确性，但历史上需要「巨量脑力」；选择哪个属性值得付出这笔成本，本身就是一门艺术，因为谱系上的每个点都可能有用。
3. 有用的安全是建立在明确假设上的有限边界
Cook认为，「100%安全」不是正确的现实目标：一栋完全无法攻破的房子，如果房主丢了钥匙，也会变得无法使用。当前软件更像一栋门窗敞开的房子，因此在试图打造不可攻破的堡垒之前，先把门窗关上并锁好，就已经意义重大。
Fisher更倾向于不完全规定：先定义划定安全运行边界的属性，再让程序员或LLM在多个有效实现中作选择。系统可能需要证明区域数据主权得到保障，却不必证明内存行为的每个细节，尽管在特定场景下，内存安全或其他属性可能不可或缺。
每项保证都建立在假设之上。软件证明可能假定处理器遵循某种指令集行为；证明处理器时，又会依赖更底层的假设，最终一路追溯到物理规律。「假设永远一层层向下延伸」，所以形式化验证提升的是保证程度，而不是提供形而上的确定性。
Fisher故意给出一个荒谬的比较：房间里的空气理论上可能聚集到一个角落，把所有人憋死。理性的信心意味着接受足够稳定的假设；在此基础上，内存安全、解析器生成器和输入校验可以让整类攻击变得足够罕见，使攻击者「去攻击你的邻居，而不是你」。
4. 证明工程从自动TLS检查到定制化虚拟机不尽相同
Cook把形式化方法工具比作「把所有80年代乐队都看一遍，再试着界定什么是流行歌曲」：它们的证明表示、自动化程度和所需专业能力差异巨大。因此，证明长度不存在普适的代码对证明比例。
对于Amazon编写的一套开源TLS实现，Cook称TLS握手的正确性证明完全自动化。基于SAT的推理和归纳不变量发现效果良好，因为密码学循环通常比较简单，也避开了最棘手的递归数据结构。
Amazon的新Isolation Engine虚拟机管理器将进入Graviton 5的AWS技术栈。其Isabelle证明工作涉及复杂属性；按Cook的粗略估计，每名软件工程师大致需要配备1名形式化方法专家，证明脚手架与实现工作量接近一对一。
CompCert的保证同样有边界：早期工作假设航空电子代码是顺序执行的，依赖x86或ARM等ISA模型，并对操作系统或第三方API的行为作出假设；最初的解析器假设后来得到修正。未知的外部行为可以用「恶魔式不确定性」建模，再只在证明需要更强假设的地方逐步细化。
5. HACMS把分区证明带到了空中红队测试
DARPA的HACMS项目于2011-2016年开展，使用SEO4这一经过形式化验证的隔离内核，包含约10,000行C代码和约100,000行Isabelle代码。其核心属性是：一个配置分区中的软件不能干扰另一个分区。
在Boeing的无人Little Bird上，研究人员将摄像头、任务控制和飞行控制功能分离。他们用AADL建模系统架构，从语法生成解析器，并证明系统级属性，例如：任何到达任务控制模块的地面站消息，都必须经过经过认证且加密的通道。
基线测试至关重要。红队仅凭约6周积累的知识，就攻陷了未经修改的军用直升机，令Boeing工程师大吃一惊；随后红队在整个项目中持续跟踪重新设计，因此后续未能攻破新系统，不能归因于不了解新系统。
第二阶段，团队在地面发动攻击；第三阶段则在空中、2名测试飞行员在机的情况下发动攻击。恶意代码可以不断派生进程并令摄像头分区崩溃，但系统只是发现「摄像头分区挂了，那就重启这个分区」。飞行员无法区分这架高保证直升机与普通版本，后来DEF CON黑客也没能攻破相关四轴飞行器。
6. 证明回答的是被提出的问题，而非所有可能重要的问题
Fisher表示，这次飞行主要是向外界展示证据；编写程序的人愿意拿飞行员的生命冒险，项目中的所有人也都基于证明及其周边产物，预期系统不会出问题。硬件或物理手段仍可能发动攻击——仍然可以「向旋翼扔石头」——但在那个场景里，软件攻击的风险可能低于其他手段。
Cook把「如何」与「是什么」分开。即便有一种神奇程序，能够以完美可靠性回答关于任何程序的问题，也会面对无限多种可能的查询：证明了5,000个属性之后，第5,001个问题仍可能暴露出一种此前没人意识到自己不喜欢的行为。
所以「总有更多东西需要证明」。验证可以在假设成立的前提下，确凿建立一个定义清晰的陈述；但它无法保证人类确实选定了所有承重属性、正确建模了环境，也无法保证局部结果已经组合成他们真正关心的系统属性。
7. AWS已把面向客户的分析连接到生产级证明
Cook于2014年加入Amazon时，客户看重灵活的云策略和虚拟网络，却不喜欢无法确认配置是否正确。AWS随后推出IAM Access Analyzer、VPC Reachability Analyzer、S3 Block Public Access，并把形式化推理嵌入Inspector、Config Rules及其他服务。
内部团队则聚焦密码学、虚拟化、存储持久性和身份等高后果领域。他们没有试图一次性证明整个AWS，而是围绕高风险组件建立「关键引理」；随着时间推移，相邻系统的证明开始「相互接触」，逐渐模糊出更大范围的已验证区域。
最强的连接案例是AWS的策略解释器：它每秒被调用超过10亿次，用于判断API操作是否获授权。它相对于最初为客户分析而形式化的策略语言语义，已经被证明是正确的——这直接回答了客户自然会提出的问题：「我怎么知道你确实正确解释了这项策略？」
2022年假期后，高管们迅速把问题焦点从基础设施转向聊天机器人，再转向多智能体的正确性。Cook说，底层数学可以迁移：Family and Medical Leave Act类似于一项S3策略，而证明组合智能体的属性，类似于证明组合微服务为S3提供的是强一致性，而非最终一致性。
8. Automated Reasoning Checks先形式化策略，再约束智能体
该产品有两项工作：形式化描述什么是真的，以及在推理阶段消除由幻觉驱动的错误。生成式模型首先把自然语言资料——例如一份人力资源手册——翻译成适合自动推理的逻辑表示。
这会产生一个表面上的循环论证：用不可靠的模型来构建防范不可靠模型的护栏。AWS的做法是遍历生成的公式，计算具有代表性的边界案例并展示给用户；用户可以用自然语言否定某个答案，触发下一轮翻译和测试。
部署时，系统会对输入生成多个形式化翻译，并询问定理证明器这些翻译是否等价。达成一致只能带来高水平而非绝对的保证——因此是「99%，不是100%」；出现分歧则支持主动追问：如果头等舱旅行和教练陪同出行产生了不同解释，系统可以询问用户究竟指哪一种。
一旦含义得到确定，形式化模型就能证明或证伪合规性。逻辑检查器「完全没有创造性」；它定义了一个由真假答案构成的无限边界，同时允许语言模型在这个边界内自由地创造性组织表达。
9. 规格定义仍比证明或修复代码更难
Cook明确承认，定义预期行为「远远」是最难的部分，尽管后续推理有时也会遇到不可判定或难解问题，包括NP完全问题。他回忆，自己曾在往返楼宇的班车上花费大量时间，只为让团队达成共识，确认他们写下的确实是正确规格。
「所有静态数据均已加密」暴露了问题所在。什么才算加密——从「谷物盒里拿出来的」设备，还是只有获批准的API？什么算静态——特定存储介质中的数据，还是持续在高延迟网络中绕着世界传输的数据？一个看似简单的要求，立即需要多轮细化。
初始实现「不会」满足规格，因此验证会变成反复修复的过程。Nathan观察到，出现疑似漏洞时，1名工程师可能接受其存在，另2名工程师则否认环境条件可能发生；Cook说，穿透这种认知偏差的可靠方法，是构造一个漏洞利用或概念验证。
工具的诊断质量各不相同。有些抽象丢弃了足够多的信息，只能报告不完整的证明；另一些工具则会给出「贯穿全部代码的疯狂路径」以及触发失败的精确输入。具体的反例远比抽象结论更难被工程团队搪塞过去。
10. 持续交付使维护证明成为生产纪律
学术界的形式化方法往往在定理证明后就告结束，但云代码持续变化。生产团队必须把验证整合进CI/CD，伴随实现同步修复证明，并在代码变化与核心论证无关时自动保留已有证明。
底层问题仍然不可判定或难以处理，因此工具有时会「直接去吃午饭」。把变量名从X改成Y，可能改变内部哈希表，使一个此前3秒完成的证明耗时400秒，甚至永远无法返回，尽管程序的相关语义并没有变化。
推理层级从无循环条件分支开始；即使是判断某个分支能否发射火箭，也可能已经是NP完全问题。加入循环或递归后，要证明某个断言永远不会失败，就需要归纳不变量：它在进入循环时成立，在每次迭代中保持成立，并推出被禁止状态不可达。
要证明最终一定终止，还需要秩函数及其支持性不变量；并发场景可能需要依赖—保证条件，对每个线程的环境进行抽象。这些人为创造的产物，正是稀缺专家最关键的地方，因为强大的组合求解器可以在有人提供洞见后完成检查。
11. 生成式AI搜索证明洞见，确定性工具负责裁决
SAT求解器已经把形式化方法从研究型「修道院」带入实用自动化。分布式系统——Cook提到一个名为Malibu的工具——会运行多个求解器、共享学到的引理，并展现出与Transformer模型非常相似的规模定律；这些进步让AWS能够在20秒内可靠推理客户策略和VPC网络。
生成式AI直接攻向剩余的搜索瓶颈：「给我找一个归纳不变量，找一个秩函数，再找一组依赖—保证约束。」每个候选项都可以还原为成熟求解器能够接受或拒绝的组合检查，而云基础设施会并行尝试大量模型与工具组合。
「第37步」的类比还低估了这件事的重要性。一个成功证明通常需要少数人才能找到的洞见，因此Cook说，团队「每一次都濒临第37步奇迹」；模型可以吸收文档、威胁模型、运行计划和旧证明，再搜索新的不变量。
Fisher认为，生成式AI正在「把这件事调到11档」。形式化语言的训练语料稀少，但证明检查器可以认证合成样本，从而生成可信训练数据。她提出的基准测试，将推动模型开发者围绕内存安全、类型安全和输入校验展开竞争，而不只是比拼生成代码的数量。
12. 安全代码模型让伟大重写变得可信，但并非必然发生
Nathan提出的飞轮逻辑成立：模型生成大量证明尝试，检查器保留成功结果，经过认证的证明成为训练数据，而证明成功本身成为代码生成的奖励。对于GPT-6和Gemini 4能否成为超越人类的安全代码工程师，Fisher回答「可以」，并同时点名Nova和开放权重模型。
翻译提供了一条穿越数十年遗留软件的路径。旧程序可以充当新程序的规格，使等价性证明相对更容易处理；Cook提到从Java迁移到Rust，Fisher则指出DARPA的TRACTOR项目正致力于把C翻译成符合惯用写法且内存安全的Rust。
Fisher说，AICC已经展示AI结合网络安全如何「以速度和规模」发现并修复漏洞，Google的CodeMender和OpenAI的类似项目也在做同样的事。技术可能先于社会准备好：网络危害已经上升约20年，而公众一直像「被煮熟的青蛙」一样无动于衷；不过，Y2K证明了协调式修复是可能的。
Cook的提醒是，安全会鼓励冒险：「因为汽车更安全，我们就开得更快。」市场会在安全、性能、功能和可用性之间权衡，例如设备驱动为了让游戏更快而进入内核空间。形式化方法或许能帮助隔离一个高度激进的AI，甚至「隔离超级智能」；但更强的封锁也可能鼓励部署能力更强的系统。
13. 形式化政策可以普及获取，同时让例外显性化
Cook以Portland分区规划为例说明产品机会。如今，计划建造附属住宅单元的人，可能需要找一位在Oregon州Portland执业的建筑师来解读退界要求，包括建筑是否必须距离地界5英尺。会产生幻觉的聊天机器人无法安全替代这个中间人；经过形式化检查的智能体则可能提供准确、低成本、全天候的服务。
政府可以发布政策模型，也可以将其开源、授权，或在不同机构之间组合使用。由于每个答案都能追溯到明确公理，公民可以指出「正是这条公理让规则不公平」，提出修订，并重放此前的对话，查看哪些人的结果会发生变化。
Nathan和Fisher保留了核心反对意见：规则有时需要合理的弹性空间。Cook建议设置不平等的公理类别——有些必须遵守，有些除非必要否则可以规避，最后再设置「Steve怎么说？」这样的升级路径——但Nathan追问，判断究竟应该放在哪里，因为人的裁量既能提供人道的灵活性，也能制造破坏性的偏见。
最后的综合是神经符号AI，正如Cook所说，这是「花生酱和巧克力时刻」。形式化方法提供保证，却僵硬且难以使用；AI灵活、易获取，却不值得信任。两者结合可能产生乘数效应，前提是机构接受Nathan指出的更深层挑战：社会正在「逐渐认识到，弄清真相究竟有多难」。