[正文内容]

是的，这篇文章不是关于形式化验证（Formal Verification, FM）基准测试（Benchmarking, BM）的陷阱。而是关于在论文中使用误导性统计数据，这些论文将形式化方法应用于验证（证明正确）操作系统（Operating System, OS）代码——这件事困扰我一段时间了。

| 名称 | 语言 | 规范语言 | 证明:代码 | | ----------- | ----------- | ----------- | ----------- | | seL4 | C+Asm | Isabelle | 20:1 | | CertiKOS | C+Asm | Coq | 15:1 | | SeKVM | C+Asm | Coq | 7:1 | | Ironclad | Dafny | Dafny | 5:1 | | XXX | Rust | Verus | 10:1 | | YYY | Rust | Verus | 7.5:1 |

表 1：一些已验证系统的语言和（不完整的）证明规模统计 [匿名]。

上面的表1展示了一个来自同行评审论文的近期例子（鉴于这种缺陷的普遍性，批评作者是不公平的，所以我保持匿名）。它似乎表明自最初的seL4工作以来，验证效率有了显著提高，因为验证一定数量的代码所需的证明行数减少了3-4倍。请注意，表格上半部分的系统使用交互式（即手动）定理证明（Interactive Theorem Proving, ITP），而下半部分使用使用SMT solvers的自动定理证明（Automatic Theorem Proving, ATP）。考虑到自动化，人们自然会期望ATP系统的验证工作量明显小于ITP系统，而该表似乎大致证实了这一点。

那么，“证明代码比”意味着什么？

简短的回答：意义不大。 为了理解我为什么这么说，让我们以一个函数sort()为例，它接受一个整数列表，并返回按递增值排序的列表。可以推测，该函数的“证明”应该准确地确认这一点：它返回排序后的原始数字。但是，为了获得有意义的证明，我们需要对预期结果进行更精确的规范。这样的规范将需要返回值的一些属性；非正式地说，这可能看起来像这样：

  1. 返回值，R，是一个整数列表。
  2. 输出列表的长度，n，等于参数列表，_A_的长度。
  3. 输出列表已排序：0 <i<n: Ri−1≤Ri。
  4. 输出的每个元素都出现在参数中：0≤i <n: Ri∈A

显然，我们对sort()正确性的期望是所有这些条件都成立。条件1只是语法（并且可能由类型系统处理）。条件2相当简单，显然不足以保证正确性。

条件3是核心属性，它说明了“排序”的含义。但是，这显然是不够的，因为返回列表[0, 1, · · · , n − 1]的函数将满足条件1-3，但对于我们想要的仍然完全错误。因此，我们还需要条件4，以确保我们对正确的数字进行排序。

差不多。如果我们有一个前提条件，即A中的所有数字都是唯一的，那么条件1-4就足够了。如果我们没有，那么结果仍然可能是错误的，例如，如果sort([1,0,1])返回[0,0,1]，这可能不是我们想要的。

为了完全捕获排序的正确性，我们需要额外的条件5，它以某种方式捕获我们正在处理相同的数字，并且每个整数在两个列表中出现的次数完全相同。我什至不尝试半正式地指定它，因为我相信我会搞砸它……

我为什么要告诉你这些？

好吧，在证明

  1. 条件1-3
  2. 条件1-4
  3. 条件1-5

代码没有改变。但很明显，_后面的情况具有比先前的情况复杂得多的规范 _。而且应该很明显，_证明（2）将比证明（1）需要更多的证明工作，而证明（3）将比证明（2）需要更多的证明工作，从而导致更大的证明，从而导致更大的证明代码比 _。

因此，在不查看规范的完整性的情况下，仅比较证明大小是没有意义的。暗示它 有 意义绝对是我书中的一个基准测试陷阱。

排序也是一个不同方面的好例子：有许多排序算法，它们的（概念和计算）复杂度各不相同。如果正确实现，它们中的任何一个都将满足我们的条件1-5，但代码大小却大不相同。不同的代码大小可能会对证明的大小产生影响（ITP很可能，SMT可能不会那么多，如果它可以处理的话！）。这能告诉你多少关于验证效率的信息是一个悬而未决的问题。

这就是我说：

证明代码比是一个毫无意义的指标！

那么，什么是有意义的？

显然，_ 规范的大小 _ 是一个主要因素，比代码大小更重要！请注意，该表犯了一个经典的BM陷阱，即仅显示相对数字，因此我需要挖掘出完整的信息。

| 名称 | 简称 | 类型 | 代码 | 规范 | 证明 | 证明:代码 | 证明:规范 | | ----------- | ----------- | ----------- | ----------- | ----------- | ----------- | ----------- | ----------- | | seL4 | seL4I | ITP | 8.5 | 4.9 | 165 | 19 | 34 | | CertiKOS | CKOSI | ITP | 6.5 | 1.4 | 95 | 15 | 68 | | SeKVM | SKVMI | ITP | 3.8 | 1.7 | 24 | 6.4 | 14 | | Ironclad | IcldA | ATP | 7.0 | 3.5 | 33 | 4.8 | 9.5 | | XXX | XXXA | ATP | 0.5 | 0.6 | 5 | 10 | 8.3 | | YYY | YYYA | ATP | 4.6 | 2.3 | 11 | 2.3 | 4.6 |

表 2：相同的系统，但明确显示代码、规范和证明大小（数千行）。

表2给出了更完整的图景，因为它显示了实际的代码和证明大小，但也显示了规范大小。（我很感谢作者提供这些论文中没有的数据，并注意到其中一些数据已根据论文进行了更新。）

在表中，“简称”列定义了下图中使用了缩写，“类型”列指示了使用的验证方法，交互式或自动定理证明；P:C代表证明代码比，P:S代表证明规范比。

该表还纠正了对seL4验证工作的常见错误描述，该描述通常概括为20个人年和20万行证明用于8.5千行代码。这是完全不正确的：如果您费心查看论文[Klein et al., 2009]，您会发现这些证明大小数据包括一些自动生成的证明；手动编写的证明为16.5万行。此外，20个人年包括对可重用证明库的重大投资，例如用于处理固定大小的机器字，为实际的seL4验证留下了11个人年。不幸的是，这并没有阻止（这些和其他）作者引用不正确的数字并引用该论文。

如果我们查看证明/规范大小比率（最后一列），我们实际上会看到比证明/代码比率更大的差异。为什么呢？

从表格中得出的最引人注目的观察结果是，按照规范大小来看，seL4是迄今为止最复杂的系统。这与我上面提出的非正式复杂性论点相符，因此所需的证明需要更多努力也就不足为奇了。

在我们沉迷于查看比率之前，我们需要首先提醒自己一个简单的事实：

仅当您可以合理地期望两个量之间存在线性关系时，比较两个量的比率才有意义。

例如，比较不同行星的表面重力与直径之比是没有意义的：这不是线性关系（根据牛顿定律，如果行星都具有相同的密度，则它是二次关系），因此比率数字毫无意义。

那么，我们可以期望代码大小/复杂性和证明大小之间存在线性关系吗？事实上，它远非线性！Matichuk et al. [2015]发现证明的大小是属性的形式化陈述的大小的 _ 二次 _ 方。换句话说，_ 证明大小预计会随着规范大小的平方而增长！ _

我发现这个结果非常直观：证明一段代码保持不变性显然取决于有多少状态可以影响代码的功能，以及有多少其他代码可以影响该状态。直观地说，这是一个 n 2 问题。

因此，仅仅像对待它们有意义一样比较比率简直就是~~胡说八道~~一种基准测试陷阱。

请注意，Matichuk et al. 仅研究了 ITP，因此不能保证相同的关系适用于 ATP。但是，正如我上面所说，n 2 关系是直观的。

那么，从这个角度来看，这些统计数据如何呢？

图 1：证明大小与代码或规范大小。实心椭圆形是ITP验证的系统，虚线椭圆形是ATP验证的系统。

在图1中，我们绘制了证明行数与代码行数（红色椭圆形）以及规范行数（蓝色椭圆形）的关系。直线是样本二次曲线（没有声称它们是好的预测指标）。请注意，在此对数图中，所有二次曲线都是平行的！

如果我们只看代码和证明大小，我们会发现紫色线非常适合ITP系统（实心红色椭圆形），而两个ATP系统（Ironclad和YYY，虚线红色椭圆形）不出所料地更低（我们稍后会看XXX）。但是，正如所论证的那样，这是一种毫无意义的比较。

如果我们改为查看规范到证明的比率，我们会发现ITP系统（实心蓝色椭圆形）中，seL4和SeKVM非常相似（由绿线拟合），而CertiKOS的证明量相对于其规范大小来说出奇的大。

比较ATP系统（虚线蓝色椭圆形），我们看到橙色线非常适合Ironclad和YYY，而XXX的证明工作量更符合ITP系统。

为什么XXX如此异常？我不会在这里做出任何强有力的声明，但至少可以有所怀疑。就代码和规范大小而言，XXX是一个 _ 远比 _ 其他系统简单的系统。Matichuk et al. 发现的二次关系显然是渐近的，我们可以合理地预期完整关系中存在线性和常数项。这些项将导致不再是图1中的一条直线的依赖关系——依赖关系图将上升到图左侧的直线之上。这很可能就是XXX与紫线相比如此高的原因。

模块化

处理复杂性的历史悠久的工程原则是模块化：将复杂系统分解为主要独立的简单部分。这可能也适用于验证。具体来说，如果验证成本 V 渐近地随着规范大小 S 的平方而增长，即

V ∼ O(S 2),

那么将整个系统分解为 k 个模块，每个模块的规范大小为 S/k，则验证一个模块的成本将是

V k ∼ O((S/k)2) ∼ O(V/k2),

验证所有模块的最终成本将是

Σ k Vk ∼ O(k(S/k)2) ∼ O(V/k).

显然，这种说法在很多方面都过于简化了。不仅模块的复杂性不会都相同，而且构成系统的两个子模块的总规范大小几乎肯定大于完整系统的规范。此外，还需要努力证明所有模块的组合将满足总体系统规范。

尽管如此，经验表明，模块化可以极大地简化复杂系统的构造，而且重要的是，可以简化对复杂系统的推理，并且直观上，这也会以某种方式应用于验证工作（并且上面的说法为这一点提供了一些过于简化的理由）。

模块化会使验证像seL4这样的东西更便宜吗？

我认为不太可能。 为什么呢？

因为你不能真正地模块化seL4。我对微内核的半开玩笑的定义是：当你从内核中提取所有简单的部分后剩下的黑色粘性物质。更严肃地说：在seL4内核中，几乎所有东西都连接到其他所有东西，几乎没有机会分离东西。因此，大部分验证工作都用于证明全局不变量。

有些系统声称“类似于”seL4，但更简单或更模块化。我见过的每种情况都不可避免地对系统模型进行了一些重大简化，从而降低了通用性或性能（或两者兼而有之）。因此，我不希望在不久的将来看到像seL4这样真正意义上的东西以明显更低的成本得到验证。

而且我当然认为近期内没有什么能有像seL4这样复杂的东西能被ATP验证。

那么，结论是什么？

好吧，这并不容易！

首先我们需要注意的是，数据点的数量确实很少，因此我们需要小心，不要过度解释这些数字。如果我尝试做一个总结，那就是：

  1. 查看证明代码比是胡说八道，你需要查看规范大小，即使这样，期望线性关系也是没有意义的
  2. ATP比IPT需要更少的证明工作——惊喜！显然，这就是自动化技术的全部意义：当它们起作用时，它们相对便宜（如果您接受图中的绿色和橙色线作为预测指标，我不声称它们是，那么改进将是五倍）。但是它们在可以处理的规范的复杂性方面非常有限。
  3. 即使在类别（ITP vs ATP）中，工作量也存在很大范围。而且，令人惊讶的是，seL4实际上在ITP类别中表现相当不错！

因此，我呼吁社区：请停止这种不科学的查看证明：代码比的胡说八道！