规格说明书不存在的真相:为什么形式化验证难以普及

加密市场分析

在软件工程的广袤世界里,有一个看似荒谬却普遍存在的真相:规格说明书并不存在。这并非危言耸听,而是我在十五年职业生涯中反复验证的观察。当我们谈论形式化验证、谈论要让软件系统更加可靠和安全时,我们不得不面对一个根本性的障碍:大多数软件系统根本没有、也无法拥有真正意义上的规格说明书。让我们从一个思想实验开始。想象外星人即将毁灭人类,他们提出的唯一条件是人类必须在一年内发布一个经过形式化验证的GCC编译器,每一个代码行都要有数学证明。人类召集了全球最优秀的数学家和技术专家,日以继夜地证明定理,最终奇迹般地完成了任务。

这个故事告诉我们一个重要的事实:我们已经证明了形式化验证编译器是可行的,CompCert和seL4等项目的成功就是明证。这些系统之所以能够被验证,是因为它们具有某些共同特征:编译器、加密库、解析器和微内核等系统天然适合形式化。形式化规格说明的本质是什么?它是一种足够精确的描述,能够作为系统的总结或解释。我们不需要直接审视系统本身,而是通过审视规格说明来理解系统应当做什么。以Rust的借用检查器为例,它的规格说明简洁明了:这个程序不会产生内存错误。无论一个安全的Rust程序做多少事情,它至少保证不会发生内存安全问题。

这正是形式化规格说明的价值所在:它提供了一种可以被数学验证的承诺。然而,当我们把目光从编译器转向更复杂的系统时,情况变得截然不同。假设外星人要求的不是编译器验证,而是形式化验证一个网页浏览器。问题立刻浮现:网页浏览器到底是什么?它的形式化定义是什么?当我们尝试回答这个问题时,会发现答案远非显而易见。Chrome浏览器的行为涉及HTML解析、CSS渲染、JavaScript执行、DOM操作、网络协议处理、安全沙箱机制等无数复杂交互,每个方面都可能存在数不清的边界情况和特殊行为。我们甚至无法确定究竟应该验证什么。

这正是问题的核心所在。形式化规格说明通常需要满足几个关键特征:数学上的清晰性,我们能够用相对简单的数学概念来描述规格;易于推理,我们能够通过人类直觉或形式分析来理解系统;良好的封装性,存在清晰的系统边界,规格说明描述边界处发生什么;广泛的共识,设计者和用户都认可规格应该匹配系统;以及对变化的稳定性,当系统演进时,规格不会发生根本性改变。那些天然适合形式化的系统,比如编译器、加密库、解析器和微内核,恰好完美符合这些特征。编译器将一种语言的代码转换为另一种语言,边界清晰,语义明确。加密库实现已知的数学算法,输入输出行为易于定义。解析器处理结构化数据,语法规则可以精确描述。

这些系统就像是为形式化方法量身定做的舞台。但现实世界中的大多数系统远没有这么规整。拿起任何一家企业的核心业务系统,查看它的需求文档,你会发现什么?可能是几千页的结构化文档,也可能是几十页的幻灯片,还可能根本没有成文的规格,系统只是按照它一直以来的方式运行。开发团队通过口耳相传来理解系统行为,通过无数个深夜调试来积累隐性知识。这种状况在大型遗留系统中尤为严重,代码库可能已经有二十年的历史,没有人真正知道为什么要这样设计,但它就是这样工作的。当我为客户评估形式化验证项目时,经常听到这样的对话。

客户声称拥有规格说明书,实际上只是两页PowerPoint幻灯片或者七千页混乱的需求文档。当我试图根据这些文档进行形式化验证时,问题接踵而至。我发现系统做了某件事,但规格暗示它应该做另一件事。客户的回应要么是这不重要,要么是我们在六个月前已经改了这件事。这样的对话重复几千次之后,很难不让人考虑转行去马戏团表演。即使我们能够坐下来与客户一起编写形式化规格说明,也会遇到意想不到的困难。

我经常问的一个问题是:规格应该允许这种行为吗?客户的回答往往是:我不知道,我没有考虑过这种情况。然后我会解释如果允许这种行为,还必须允许另一种相关行为。客户继续表示对那种情况也不了解,然后焦虑地问这会花多长时间。这种对话揭示了一个深刻的真相:编写形式化规格说明本身就是一项极其困难的任务。它需要一种自上而下的系统视角,而设计者和工程师通常不具备这种视角,或者说他们根本不需要这种视角。相比之下,非正式规格可以模糊、可以局部、可以灵活。

非正式规格本质上是人与人之间的交流工具,因此可以错误但有用,可以省略不感兴趣的系统细节。这既是它的优势,也是导致系统难以形式化的根本原因。让我们深入分析一个具体的例子:PDF文档格式。在许多方面,PDF应该是最容易形式化的情况之一。毕竟PDF无处不在,你可以在数十亿设备上下载并打开一个PDF文件。PDF有PDF协会维护的良好标准,有大量示例存在,有从业余项目到安全关键系统的无数实现。

但即便如此,PDF仍然没有关于实现应该做什么的共识,没有与现有实现行为相匹配的规格,也没有对什么是错误或不安全文档的清晰定义。结果是,今天几乎不可能为PDF编写精确且一致的形式化规格说明。在一组大型PDF数据集中,我们会遇到已知错误的内容,即以某种方式构造来引发漏洞的格式错误文档,也会遇到已知良好的文档,即严格符合标准的文档。但还有大量文档处于灰色地带,我们只能耸耸肩。它们可能是好的也可能是坏的,我们根本不知道。为什么会这样?一个重要原因是PDF阅读器有强烈的动机尽可能多地解析文档。

如果你收到一个PDF但无法打开,你很可能会责怪阅读器,而不是创建文档的程序。为了避免这种投诉,每个PDF阅读器都试图修复非标准文档中的错误,而且每个阅读器都以略微不同的方式修复。这导致同一个非标准文档可能被不同的阅读器以两种不同的方式解释。这种状况让我想起法国哲学家德里达的理论。PDF实际上并不存在,至少不存在一种可以被形式化的离散类别。取而代之的是一个模糊的边界,某些东西可能被认为是PDF,也可能不被认为是PDF。

这本身并没有那么糟糕,糟糕的是大部分实际存在的PDF恰好处于这种边缘地带。在DARPA SafeDocs项目上,Galois花费数年时间研究PDF形式化。我们与PDF协会密切合作,使用了一种名为DaeDaLus的新语言。我为团队的工作感到自豪,但项目结束时,我们的正式PDF规格是非描述性的,与真实PDF阅读器的行为不同;是非规范性的,不能表征我们认为应该的正确行为;而且我们不清楚如何获得更严格和被广泛接受的规格。这个案例说明了什么?即使在看起来最适合形式化的领域,即使投入了大量资源和专业知识,我们仍然无法获得令人满意的规格说明。那么对于更加模糊和复杂的系统,比如企业资源规划系统、医疗设备软件或者自动驾驶汽车的控制系统,情况会好到哪里去呢?现在让我们展望未来。

形式化验证的当前时代一直被证明成本的巨大所主导。既然我们甚至无法验证具有简单规格的系统,为什么还要担心其他一切呢?得益于现代人工智能的进步,我们可能很快就会生活在一个证明变得廉价且丰富的奇怪世界里。如果这种情况发生,我认为我们将很快验证每一个编译器和微内核,然后发现我们陷入了困境。即使是最先进的语言模型也无法告诉我们真正想要什么。这个预测可能看起来违反直觉。我们一直被告知人工智能将彻底改变软件开发,为什么形式化验证不会随之改进?关键在于证明与规格之间的区别。

有了人工智能的帮助,我们可能更容易找到程序的正确性证明,但证明必须基于某种规格。如果没有规格,你就无法证明任何东西。人工智能可以帮你证明你想要的属性,但无法帮你决定你想要什么属性。这就是规格的不可替代性。今天的形式化验证当然非常有用,但对于大多数系统来说,编写验证所需的完整规格是非常困难的。然而,其他类型的规格很受欢迎。

例如,测试用例是一种受限的、部分规格。它的关键在于测试用例立即有用,而且不会给开发团队带来过度的成本。我们需要找到方法来规格化具有这些优点的系统,同时避免强加一种根本不存在完整且一致的视角。形式化验证领域有一个老生常谈的说法:编写规格往往能发现系统中的大部分错误。对我来说,这暗示了规格与编程之间的类比。两者都是表达我们想要什么的工具。

从某种意义上说,这是一个悲观的观点:没有工具可以消除澄清想法的负担。但这也给了我们一些希望。编程非常困难,但通过精心的工具设计,我们已经让数亿人能够编程。如果运气好、技术好,也许我们能为规格做同样的事情。这并不意味着形式化验证没有未来。恰恰相反,对于那些自然可规格化的系统,形式化验证的价值是无可争议的。

编译器、微内核、加密库和关键安全组件都应该采用形式化验证方法。这些系统值得投资,因为它们的风险足够高,而且规格可以清晰定义。但对于大多数其他系统,我们需要采用不同的策略。模糊测试、属性测试、增量验证和基于契约的编程等技术可能更适合这些情况。它们提供的保证不如形式化验证那么强,但它们在不完美规格的现实世界中是实用的。当我们审视软件行业的现状时,会发现一个悖论。

我们花费数十亿美元开发软件,但软件错误的成本同样天文数字。根据一些研究,软件错误每年给全球经济造成数千亿美元的损失。与此同时,我们拥有形式化验证的技术能力,可以消除某些类别的错误,但我们几乎没有使用它。问题不在于技术,而在于经济学和人性。编写形式化规格太难了。验证现有系统太贵了。

交付压力太大了。结果是,我们继续构建充满错误和漏洞的系统,并祈祷这些错误不会被利用。那么我们应该做什么?作为一个行业,我们需要承认规格说明书不存在这个现实,并据此调整我们的方法。对于关键系统投资形式化验证。对于其他系统,采用务实的方法,尽可能多地验证,但不追求完美。改进规格编写工具,使非专家能够表达他们想要的属性。

开发新的验证技术,能够在规格不完整的情况下发现错误。培养下一代工程师,让他们理解规格的重要性,并具备编写规格的技能。我们才刚刚开始。有很多事情要做。形式化验证的梦想不会消失,但它需要变得更加务实和包容。我们不能等待完美规格的出现,然后才开始验证。

我们必须学会在规格不完美的情况下仍然能够提供有价值的保证。这就是软件工程的现实,也是我们在未来十年需要解决的问题。最后,我想用另一个故事来结束这篇文章。一位经验丰富的形式化验证工程师告诉我,他职业生涯中最重要的发现不是某种新技术或新工具,而是接受这样一个事实:完美的规格是不存在的。他说,一旦你接受这一点,你就不再追求乌托邦,而是开始构建能够在不完美世界中工作的真实工具。这可能是形式化验证能够真正普及的唯一途径:从梦想走向实践,从完美走向足够好,从理论走向现实。

而这,正是软件工程真正进步的标志。 。