证明能承诺什么

人们信任软件，通常是因为它经过了测试。有人想到它可能出错的方式，逐一尝试，看着它应付过去。这个办法很管用，直到遇上谁也没想到的那种情况。

证明从另一头入手。它不去尝试各种情况。它用数学说明，一个命题在所有情况下都成立。

所有情况，而不只是试过的情况

拿一个小小的承诺来说：这段代码绝不会读到缓冲区末尾之外。测试可以给它一千个输入，或者十亿个，然后报告说没有一个让它出错。证明说的是另一类话：不存在会让它出错的输入。不是没找到，而是没有。

代价是严格。证明需要一份对代码应当做什么的精确陈述，也就是它的规约，还需要一个把代码每一行都与规约联系起来的论证。对真实的软件来说，这个论证长得没有人能凭肉眼检查。于是由计算机来检查。

由机器检查

这就是“经机器检查”的意思。证明被完整地写出来，使用一种名为证明助手的程序能够读懂的语言，由这个程序对照逻辑规则检查每一步。它不会在第九百页感到疲倦，也不会轻信任何人的话。

seL4 的证明就是这样检查的，使用名为 Isabelle/HOL 的证明助手。这些证明是公开的，任何人都可以重新运行。

seL4 的证明说了什么

seL4 是每个 NoWayOS 系统运行其上的内核：约 10,000 行代码，也是唯一完全控制设备的代码。关键就在于它的规模。关于一万行代码的论证可以做完。关于数千万行代码的论证，目前还做不到。

seL4 Foundation 分层说明了这些证明：

• 代码所做的就是规约所说的，仅此而已。 由此可以得出一份内核做不到的事情的清单：缓冲区溢出、解引用空指针、内存泄漏、除以零。
• 实际运行的程序与被证明的代码一致。 两者之间隔着编译器，所以另有一项证明检查编译器的输出。
• 内核能够把系统的各个部分隔开。 一个部分不能修改另一个部分的数据，不能读取它，也不能夺走它所需的资源，除非被授予了这样的权利。
• **系统能够以设计时确定的状态启动，**所拥有的授权与其描述中列出的完全一致。

并不是每一层都已针对每种处理器和每种配置完成。这一点很重要，后面还会谈到。

证明视为理所当然的东西

证明的范围与它的命题完全一样宽，并且建立在它的假设之上。seL4 把自己的假设写了下来：硬件的行为与其模型一致；最底层的几百行代码是正确的；内核启动之前运行的代码完成了它的工作。保密性的证明不涵盖时序。

对于规约要求的是否是正确的东西，证明不置一词；对于内核之上的软件，也不置一词。经过证明的内核会忠实地隔离一个带有缺陷的程序。缺陷仍然在那里。它只是够不到别的任何东西。

这不是证明的弱点。这正是它们的价值所在：它们精确地说明自己覆盖什么，于是您也就精确地知道还剩下什么。

NoWayOS 的位置

直截了当地说：NoWayOS 运行在 seL4 之上，但目前没有任何 NoWayOS 镜像处于 seL4 已完成的证明范围之内。NoWayOS 使用 seL4 的混合关键性配置，针对我们所用处理器的证明仍在进行中。而 seL4 的证明从来就不覆盖 NoWayOS 自身的代码。所以我们不说 NoWayOS“经过形式化验证”，以后也不会这样说。

每个镜像都会说明自己的位置。镜像旁边有一个文件，逐项列出其内核的配置，并与 seL4 已证明的配置对照。安全页面展示了一个真实的例子。

我们自己的、更小的证明

NoWayOS 的代码通过另一条途径获得保障：Rust、隔离、评审、测试，以及一种更为朴素的证明。

在系统各部分之间传递的消息，其每一个解码器都有有界证明，由名为 Kani 的模型检查器完成。有界证明覆盖不超过规定大小的每一个输入，在这里是解码器所接受的最长记录。在这个界限之内，它是真正的证明：没有任何输入能让解码器发生 panic、溢出或越界读取。超出界限，它什么也不说，所以我们把界限定为可能出现的最长输入。

然后我们故意把解码器改坏，以确认证明能够察觉。一个不可能失败的证明，并不比一个不可能失败的测试更有用。

它实际的分量

证明不会让任何东西变得“无法被黑客攻破”。它让一个命题在所有情况下为真，而所依据的假设，您都可以读到。了解了命题和假设，您就知道自己手里有什么。

正因如此，NoWayOS 构建在拥有这些证明的内核之上，并且逐个镜像地告诉您，这些证明覆盖到哪里。