在亚马逊2025年re:Invent大会上，亚马逊云科技（AWS）正式发布了Nitro隔离引擎（NIE）。这一软件模块专门负责向AWS客户分配计算资源，同时保障用户数据安全。AWS还宣布，已借助一款名为Isabelle/HOL的证明辅助工具，对隔离引擎的正确性和安全性进行了形式化验证。作为业界首个经过形式化验证的云端虚拟化管理程序，NIE为云安全领域树立了全新标杆。
什么是证明辅助工具
证明辅助工具是一种能够帮助用户构建形式化证明的自动化工具，可用于验证数学定理、硬件或软件系统的正确性等多种场景。目前有多款证明辅助工具被广泛使用，AWS之所以选择Isabelle/HOL，是因为它在表达能力、自动化程度、证明可读性和可扩展性之间取得了最佳平衡。
数学语言与自动化的权衡
数学本身并无固定语言，但我们可以构建专门用于表达数学推理的形式语言，就像编程语言用于描述计算任务一样。编程语言需要在表达能力和运行性能之间寻求平衡，数学语言同样要在表达能力和自动化难易度之间作出取舍。自动化至关重要，因为构建一个形式化证明既耗时又繁琐，就像在瓶中拼装一艘船。
最基础的数学语言是布尔逻辑，其核心是AND、OR、NOT三种二元运算符。由于这种语言足够简洁，针对它的自动求解工具已相当成熟。2016年，卡内基梅隆大学教授Marijn Heule（现任亚马逊学者）与同事将一道悬而未决的数学难题——布尔毕达哥拉斯三元数问题——编码为布尔逻辑，并借助自动求解器完成了迄今规模最大的证明，总大小达200TB。
更丰富的一阶逻辑允许对某一特定领域（如整数集合）进行描述，并定义该领域上的函数，还可以引入"对所有……"和"存在……"等量词。在这种语言中，我们可以表达诸如"所有大于二的素数都是奇数"这样的命题，也可以证明刘易斯·卡罗尔提出的经典三段论：鸭子不会华尔兹；军官从不拒绝华尔兹；我养的禽类都是鸭子；因此，我养的禽类中没有军官。
然而，大多数人更倾向于使用表达能力更强的高阶逻辑，这类语言支持像编程那样定义类型，甚至支持函数类型（类似Haskell等函数式编程语言中的概念）。高阶逻辑远比一阶逻辑丰富，能够表达诸如"任何包含数字1且对加法封闭的集合都包含全部正整数"这类命题，足以覆盖绝大多数数学内容。
表达能力最强的数学语言——依赖类型理论——甚至允许类型接受任意值作为参数，例如T(i)，其中i为整数。最具代表性的此类语言是Lean和Rocq。
证明辅助工具的核心架构
针对一阶逻辑，目前已有功能强大的自动定理证明器；但对于高阶逻辑及更复杂的系统，完全自动化尚无法实现，这正是表达能力强带来的代价。证明辅助工具允许用户以交互方式构建证明，并辅以局部自动化支持及自定义证明搜索能力。这类工具通常采用核心架构，只允许极小部分代码拥有创建定理的权限，从而严格保证逻辑合规性。
证明辅助工具同样支持大规模形式化规范体系的交互式开发。以NIE的验证为例，其基础涵盖Graviton-5处理器架构规范、超调用Rust代码的功能正确性规范，以及待证明的安全属性，这些内容构成了整个25万行形式化证明的主体部分。
HOL与HOL Light：高阶逻辑的应用实践
高阶逻辑由HOL与HOL Light两款紧密相关的证明辅助工具提供支持，自1990年代起已被用于硬件设计验证、浮点算法验证及纯数学研究。AWS高级首席应用科学家John Harrison开发了HOL Light，并利用它对Graviton2芯片上密码学算法的优化版本进行了形式化验证，使数字签名性能提升了最高达94%。由于代码本身极为精密，穷举测试根本无法覆盖所有情况，在部署如此关键的软件之前，只有完整的功能正确性形式化验证才能令人信服。
Isabelle/HOL的独特优势
Isabelle/HOL与其他HOL系统最显著的区别在于其规范语言和证明语言。大多数证明辅助工具要求用户先陈述待证目标，再通过一系列命令将原始目标分解为若干子目标，形成一种类似"打地鼠"的证明流程。而Isabelle（以及在一定程度上的Lean）允许用户将中间目标显式写出，使证明过程更可控，证明文档也更易读。
Isabelle/HOL还具备以下值得关注的特性：
可配置解析器：支持将Rust语言的重要子集嵌入规范描述，这一特性在NIE验证项目中得到了充分利用；
类型类机制：支持有原则的运算符重载，例如"+"不仅适用于各种数值类型，也适用于机器字及其他合适的上下文；
局部模块系统（Locales）：一种轻量级模块化机制，可在证明内部以多种方式定义和解释规范层次；
强大的内置自动化：通过化简和反向链接证明搜索实现高效自动化；
Sledgehammer工具：一键调用更强大的外部自动化推理引擎；
反例查找工具：用于识别实际上为假的命题；
可执行规范的代码生成：支持从可执行高阶规范生成代码，用于一致性测试。
NIE验证的技术实现
在NIE的验证工作中，团队首先在Isabelle/HOL之上实现了一套专用语言——分离逻辑。分离逻辑专为验证操作共享资源的程序代码而设计。团队自行编写了证明自动化模块，同时充分利用了Isabelle内置的自动化能力，因此既可使用分离逻辑，也可在需要时直接使用高阶逻辑。Isabelle展现出足够的健壮性和高效性，能够处理规模极为庞大的子目标——整个25万行的证明，在一台普通笔记本电脑上只需半小时即可完成运行。
Isabelle的代表性应用案例
在NIE之前，Isabelle最具影响力的应用案例当属对seL4微内核的验证。seL4是一款被广泛使用的微内核，其证明在首次发布时同样约有25万行，尽管如今已远超这一规模。seL4开发团队证明了微内核的C语言实现精化了抽象规范，从而保证了核心操作的完整功能正确性。自验证完成以来，经过验证的代码部分至今未发现任何缺陷，尽管测试仍用于覆盖未验证部分及某些无法形式化的假设。
此外，Isabelle还被应用于以下领域：
形式化WebAssembly语言语义，识别其中的错误，并特别证明了其类型系统的可靠性；
构建Cogent编程语言的验证框架；
证明无冲突复制数据类型（CRDT）算法的正确性，该技术广泛用于分布式协同编辑；
形式化大量纯数学研究成果；
在抽象层面验证密码学协议。
Isabelle是一款免费开源工具，可直接下载使用，支持所有主流操作系统，在内存充足的机器上均可运行。
Q&A
Q1：Nitro隔离引擎（NIE）是什么，它解决了什么问题？
A：Nitro隔离引擎是AWS发布的一个软件模块，专门负责向云端客户分配计算资源，同时保障用户数据安全。它的最大亮点是成为了业界首个经过形式化验证的云端虚拟化管理程序，通过Isabelle/HOL工具对其正确性和安全性进行了严格的数学级验证，为云安全设立了新标准。
Q2：Isabelle/HOL和其他证明辅助工具有什么区别？
A：Isabelle/HOL最大的区别在于其证明语言支持将中间目标显式写出，使证明过程更可控、文档更易读。此外，它还具备可配置解析器、类型类机制、局部模块系统、内置自动化和Sledgehammer外部推理引擎等特性，在表达能力、自动化程度和可扩展性之间取得了很好的平衡，特别适合大规模工程级验证任务。
Q3：形式化验证和普通软件测试有什么本质区别？
A：普通软件测试只能覆盖有限的输入场景，无法穷举所有可能情况。而形式化验证通过数学证明的方式，从逻辑上保证程序在所有可能情况下都满足指定属性，不存在遗漏。以NIE的密码学算法验证为例，代码极为精密，穷举测试根本无法覆盖所有情况，只有形式化验证才能在部署前提供足够的安全保障。
热门跟贴