规范并不存在

# 规范并不存在 来源：https://www.galois.com/articles/specifications-dont-exist *本文是《销售形式化方法的有效之道（与失效之途）》*(https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods)*的配套文章。它最初源于我在2024年末所做演讲的一部分* (https://mikedodds.github.io/files/talks/2024-10-09-n-things-I-learned.pdf)*。* 有些事是困难的，而有些事只是昂贵的。 设想一下：外星人要来灭绝人类。人类派出了最优秀的谈判者，而外星人宣布，只有我们发布一个经过**形式化验证的GCC版本** (https://gcc.gnu.org/)，每一行代码都要验证……而且必须在一年内完成，否则他们将发动可怕的袭击。 在经历了一些可以理解的混乱之后，七国集团的首脑们召唤了Xavier Leroy (https://en.wikipedia.org/wiki/Xavier_Leroy)，递给他一张巨额支票，让他着手去做。很快，全球各地的数学仓库里，数学家们日夜不停地证明着Rocq (https://rocq-prover.org/)定理。协调工作挑战巨大，但他们还是完成了！外星人回家了，Xavier获得了菲尔兹奖、EGOT（指在奥斯卡、格莱美、艾美奖和托尼奖都获奖）以及全部五个诺贝尔奖，1而其他人则继续担忧人工智能。 我想表达的要点是，我们基本上知道如何构建一个经过形式化验证的编译器——我们已经做到了 (https://compcert.org/)。同样，经过形式化验证的**密码库** (https://hacl-star.github.io/)、**解析器** (https://project-everest.github.io/everparse/) 和**微内核** (https://sel4.systems/) 也是如此。GCC尚未经过形式化验证的原因在于，这样做会极其昂贵，其收益不足以证明成本的合理性。但是，如果外星人*真的*出现，我敢打赌，我们能以低于《漫威电影宇宙：第三阶段》(https://en.wikipedia.org/wiki/Marvel_Cinematic_Universe%3A_Phase_Three)（22-24亿美元）的代价完成它。 好，换个故事：外星人要来灭绝人类，他们要求一个经过形式化验证的**网页浏览器**。Xavier这次也带来了（他们这次也请了他），他举起手问，呃……他们具体想要什么？比如，从形式化角度定义，网页浏览器到底是什么？这个问题让外星人既困惑又愤怒！我们肯定有Chrome的形式化规范吧，不是我们构建的吗？然后，嗯，人类就这样完了。 问题在于，我们*没有*Chrome的形式化规范，也没有文字处理器的，甚至没有像PDF文档格式这样更简单东西的形式化规范。除了少数领域，**规范并不存在**——我不仅是指目前还没人写出来，而是我们有理由相信*无法写出精确且一致的规范*。如果第二类外星人出现，我们将不得不快速发明大量全新的计算机科学，我不知道即使是漫威宇宙的资金能否完成。 ### 形式化规范应既是形式化的，又是具体的 我们（暂且不考虑外星人）首先为什么需要形式化规范？ 形式化规范以足够精确的方式表述*我们想要什么*，可以作为系统的摘要或说明。我们可以检查规范，而不是去检查系统本身。这通常并不决定系统的每一个细节（它是地图，而非领土）。例如，Rust借用检查器 (https://doc.rust-lang.org/1.8.0/book/references-and-borrowing.html) 保证了一个简单的规范：*“此程序不会产生内存错误。”*如果你给我一个安全的Rust程序，它可能做很多事，但不会做*那种*事。 如果我们想形式化验证任何东西，就需要一个形式化规范。否则，我们在验证什么？实际进行验证可能意味着数学毕业生在仓库里写Rocq定理，也可能意味着运行Rust借用检查器。但没有规范，我们就无从开始。 形式化方法由来已久，人们尝试为很多东西编写过规范。但根据经验法则，最有用的形式化规范通常具有以下特征： - *数学上简洁：*我们可以用相对简单的数学概念集合来编写规范。 - *易于推理：*我们可以利用规范来理解系统，无论是通过人类直觉还是形式化分析。 - *封装性：*系统的“内部”和“外部”之间有清晰的边界，规范描述了在这个边界上发生什么。 - *广泛共识：*系统的设计者和用户都同意它应该符合规范——地图是对领土的良好描述。 - *在变化下稳定：*当系统演进时，规范不会*变化太大*——地图抽象掉了小的差异。 有些系统似乎非常自然地符合这些要求——例如编译器、密码库、解析器和微内核。我们可以说这些系统是*自然可形式化的*。2如果这个列表看起来很熟悉，没错：这些正是形式化验证的成功案例！ 我有一个假设：一旦你有了一个高质量的形式化规范，验证一个系统*并不困难，只是昂贵*。对于形式化验证的爱好者来说，这里还有很多未挖掘的价值。编译器、微内核以及其他组件都是安全关键的部件，但今天我们使用的几乎没有经过形式化验证。打电话给七国集团，是时候了，让我们来验证GCC吧！*（文章结束，合上笔记本电脑）* 等等，不，还有内容。有些人看到CompCert和SeL4后会问：“为什么我们不能形式化验证*我的*系统？”嗯，我认为自然可规范化的系统是一个*非常小且无代表性的细分领域*。在现实世界中，大多数系统非常难以规范化，如果我们想对更多世界进行形式化验证，这是一个大问题。 ### 实际上，存在的规范太多了 我们可能没有形式化规范，但开发者一直在编写*非正式*规范。一个系统可能有多种类型的规范，这些规范承载着重要信息： - *散文文档*——面向内部的设计文档、面向外部的用户手册和指南，以及白皮书、RFC等类似文件。 - *幻灯片*——惊人地普遍，尤其是在美国政府中。 - *系统本身*——尤其是对于遗留系统，系统可能就是“它本身”，任何变更按定义都是违反规范的。 - *用户故事*——对于像网页浏览器这样的用户面向应用，用户故事集可能是真正的顶层规范，但通常很难将它们形式化表达。 - *单元和集成测试*——通常最接近形式化规范，但仅限于单个输入或场景。 - *许多许多其他东西*，包括参考实现、内联注释、团队中默认/实践知识、客户偏好、监管要求、咖啡店餐巾纸上的潦草笔记…… 事实上，有太多*部分的*规范，覆盖不完整，而且彼此不匹配。当我在为Galois的客户规划项目时，经常有这类对话： **我：**“你有[你们庞大系统]的规范吗？” **客户：**“有，这是两页PPT的幻灯片。” *~和/或~* **客户：**“有，这是一份7000页的、半结构化的散文需求文档。” 所有这些都导致了尝试形式化验证相关系统时出现的这种对话： **我：**“我们发现系统执行了[某个操作]，但你们的规范意味着[另一个操作]。” **客户：**“哦，嗯，那没关系。” *~或~* **客户：**“对，我们6个月前改了那个。” 一个人进行过大约4万次这样的对话后，我发现他们考虑转行当马戏团小丑或者直接跳河了。 你也可以尝试和客户坐下来*编写*形式化规范： **我：**“你希望规范允许[某种行为]吗？” **客户：**“呃……我不知道，我没想过那种情况。” **我：**“如果你允许它，你就还得允许[其他某种行为]。这要紧吗？” **客户：**“我也不知道那种情况……这要花多长时间？” 我逐渐认为编写形式化规范*本身就是一项非常困难的任务*。它需要对系统有全局的、自上而下的视角，而设计者和工程师通常没有，或者更准确地说，*不需要*。相比之下，非正式规范可以是模糊的、局部的、灵活的。非正式规范的目的是作为人与人之间的沟通机制，因此它们可以是“虽错但有用”的，并且略去了系统中不感兴趣的方面。这是一个优点，但也导致了难以形式化的系统。 我认为系统通常是自上而下设计*并且*增量式增长的。大多数系统具有某种程度的自上而下的结构，但很少有系统具有数学上一致且覆盖所有行为的规范。其结果是，大多数系统的某些核心功能遵循某种形式规范，但一旦超出这个核心，我们就迅速进入模糊地带，不清楚系统应该做什么，或者设计者是否应该关心。3 ### *Le PDF n’a pas eu lieu*4 让我们深入一个具体的例子：*便携式文档格式，PDF*。在很多方面，这本应是一个容易规范化的案例。毕竟，PDF不是什么深奥的东西——你可以下载一个并在数十亿台设备中的任何一台上打开它。PDF还有一个由PDF协会 (https://pdfa.org/) 开发的**维护良好的标准** (https://www.iso.org/standard/75839.html)、大量的示例以及众多实现，从爱好者项目到安全关键系统都有。 但即便如此，PDF*并未*对实现应做什么达成共识，也没有一个与现有实现行为相匹配的规范，更没有对错误或不安全文档的明确定义。因此，今天似乎不可能为PDF编写一个精确且一致的形式化规范。 在一个大型PDF数据集中，会有一些已知是坏的示例——格式错误，旨在引发某种漏洞；也有一些已知是好的示例，它们严格符合标准。但我们还有大量（事实上是大多数）文档，我们能做的只有耸耸肩。它们可能是好的也可能是坏的，我们只是不知道。 我们称这张图为“厄运土豆”。这看起来是个荒谬的情况，怎么回事？一个原因是PDF阅读器有动机解析尽可能多的文档。如果你收到一个PDF却打不开，你很可能会怪罪PDF阅读器，而不是创建该文档的程序。为了避免这种情况，每个PDF阅读器都会尝试修复非标准文档中的错误，而它们的做法都略有不同。同一个非标准文档可能被不同的PDF阅读器解释为两种不同的方式。 我感觉自己像雅克·德里达在写这段，但结果是*PDF并不存在*，至少不是以可以形式化的离散类别意义存在。相反，存在一个模糊的边界，某个东西可能被视为PDF，也可能不被视为。这本来也没什么不好，但问题是，大量实际PDF都存在于这种临界区域！ 在DARPA SafeDocs项目 (https://www.darpa.mil/research/programs/safe-documents) 中，Galois花费了数年时间致力于PDF的形式化。我们与PDF协会紧密合作，使用我们为此构建的新语言DaeDaLus (https://github.com/GaloisInc/daedalus)。我为我们所做的工作感到自豪，但在项目结束时，我们的形式化PDF规范是不具描述性的（它与真实PDF阅读器不同）、不具规范性的（它并未描述我们认为应该是正确行为的东西），并且如何达成更严谨且被接受的规范尚不明朗。 你可以在这里阅读Galois关于PDF的工作 (https://doi.ieeecomputersociety.org/10.1109/SPW54247.2022.9833889)，也可以在这里了解DaeDaLus，我们构建的用于描述文档格式的语言 (https://dl.acm.org/doi/10.1145/3656410)。 ### *结论：*Do What I Mean [](https://xkcd.com/568/)xkcd 568. (https://xkcd.com/568/) 许可协议：CC BY-NC 2.5 好，再说一个故事：当前时代的形式化验证一直被*证明*的成本所主导。规范则退居其次——我们连具有简单规范的系统都还验证不了，何必担心其他的呢？现在，得益于**现代AI的进步** (https://www.galois.com/articles/o3-frontier-math-and-the-future-of-mathematics)，我们可能很快生活在一个奇异的世界里，那里证明既廉价又丰富。如果那样，我认为我们将迅速验证每个编译器和微内核，然后发现我们卡住了。即使是Claude也无法告诉我们该想要什么。 当今的形式化验证非常有用，但对于大多数系统来说，编写验证所需的*完整*规范非常困难。然而，其他类型的规范很受欢迎：例如，测试用例就是一种有限的、局部的规范。关键在于测试用例立即有用，且不会给开发团队带来过高的成本。我们需要找到具有这些优点的系统规范方法，避免强加一个根本不存在的、完整而一致的规范观。 形式化验证中有个老生常谈：编写规范往往会发现系统中的大部分缺陷。对我来说，这暗示了规范与*编程*之间的类比——两者都是表达我们想要什么的工具。从一个角度看，这是悲观的想法：没有工具能减轻我们澄清想法的负担。但另一方面，这给了我一些希望。编程非常困难，但通过精心设计工具，我们已经让它为数亿人所用。凭借运气和技巧，或许我们也能为规范做到同样的事。 我们才刚刚开始。有很多事情要做。而且我们需要留意那些外星人。 1 不是那个经济学的假奖 2 我不想贬低发明现有规范技术所付出的努力。这些自然可规范化的系统只是*在今天的规范工具下*才如此，这些工具代表了半个世纪的协同工作。 3 啊哈，你说，我们应该坚持让工程师*从*严格的正式规范*开始*构建每个系统。在大多数情况下，我怀疑这能否通过成本效益测试 (https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods)。 4 Avec toutes mes excuses à Jean Baudrillard（向让·鲍德里亚致以全部歉意）