一直以来，我们都理所当然地认为程序就像高墙，无法不透风，自然也无法躲过黑客无孔不入的攻击。而这篇首发于quantamagazine 的文章却要颠覆我们的认知了：采用形式验证(formal verification)编写的软件，代码就像“数学证明一样可靠”。那么，它是如何实现的？又能带给我们怎样的惊喜呢？

2015年夏天，一个黑客团队在美国亚利桑那州尝试控制波音的“小鸟”(Little Bird)无人军事直升机。这队黑客的优势在于：他们一开始就能访问这架无人军事直升机计算机系统的一部分。从这里出发，他们需要做的就是黑进“小鸟”的机载飞行控制计算机，进而控制整架直升机。

在这一项目开始时，作为红方的黑客团队可以像破解家用Wi-Fi网络一样，轻易地控制这架直升机。但在接下来的几个月里，美国国防部高级研究计划局的工程师们部署了一种新的安全机制：一个无法被攻占的软件系统。

“小鸟”无人军事直升机计算机系统的关键部分靠现有技术无法攻破，它的代码就像数学证明一样可靠。即便给予了黑客团队六周时间和更多直升机计算机系统的访问权限，他们还是不能攻破“小鸟”无人军事直升机计算机系统的防御。

高可靠性军事网络系统(HACMS)项目发起人、美国塔夫斯大学计算机科学教授Kathleen Fisher表示：“黑客们无法以任何方式扩大控制并干扰机器运行。这一结果让美国国防部高级研究计划局非常高兴，他们说现在终于能用这一技术来保护核心计算机系统了。”

这一让黑客们束手无策的技术是名为形式验证(formal verification)的软件编程风格。和大多数计算机代码不同，采用形式验证风格编写的软件读起来就像是数学证明：每一个声明在逻辑上都承接上一个声明。一个这样的程序可以像证明数学定理一样，无论如何测试都一定会得到正确的结果。

微软研究院研究形式验证和安全的研究员Bryan Parno表示：“你写下的就是一个描述程序行为的数学公式，再利用一些证明检查器来检查声明的正确性。”

早在计算机科学诞生之初，创造形式验证风格软件的想法就已出现。很长一段时间以来，尝试创造形式验证风格软件的企图都徒劳无功，但在过去十年间，“形式方法”方面的进展让开发形式验证风格软件变得越来越靠谱。如今，学术界、美国军方和微软、亚马逊等科技公司正携手探索形式软件验证技术。

随着越来越多的关键社会职能转移到网上，研究人员们对形式软件验证技术的兴趣也越来越浓厚。在以前，计算机还只是局限于家里和办公室，程序漏洞最多也就是让使用者感到不便。但现在，程序漏洞可能会导致巨大危害，任何具备相关知识的人都能利用同一漏洞自由地进出某个计算机系统。

程序验证领域领导者之一的普林斯顿大学计算机科学教授Andrew Appel表示：“在上世纪，如果程序有漏洞，顶多也就是体验糟糕或者程序崩溃。但进入21世纪，漏洞可能成为黑客控制程序并窃取数据的通道。漏洞也从糟糕但可以忍受变成了致命威胁，这就严重多了。”

　　完美程序的梦想

 

高可靠性军事网络系统(HACMS)项目发起人、美国塔夫斯大学计算机科学教授Kathleen Fisher

1973年10月，Edsger Dijkstra产生了一个编写零错误代码的想法。当时他正在参加一次会议，在下榻的酒店里，Edsger Dijkstra熬到深夜来让编程变得更数学化。他在后来回忆道：“这个想法让我很兴奋，于是我凌晨两点半爬起来，写了一个多小时。”这一材料后来扩充成了《编程的修炼》(A Discipline of Programming)一书，并于1976年出版。这本书加上Tony Hoare的工作，建立了将正确性证明融入计算机程序编写过程中的视角。

计算机科学并没有采用这一视角，因为此后很多年里，要实现这一视角看起来非常不切实际，即用形式逻辑规则来明确程序的功能。

形式规范要定义一个计算机程序要做什么事，而形式验证则用来确定无疑地证明程序代码完美地符合了规范。打个比方，比如你要给无人驾驶汽车编写一个把你送到百货商店的计算机程序，你需要定义让汽车实现这一目的的动作：汽车可以左转或右转、刹车或加速、启动或停车。最终，你的程序就是为了实现这一目的而对基本操作进行的合理组合，要求是把你送到百货商店而不是机场。

检查程序是否工作正常的传统方式是跑测试。程序员们会给程序大量输入(或单元测试)，以确保它符合设计要求。如果你的程序是给无人驾驶汽车规划路径的算法，你也许会用多个不同的位置点来测试它。这一基于测试的方法能得到运行正确的软件，但只是在大多数时候针对大多数应用而言。不过，单元测试并不能确保软件永远运行正确，因为没有办法用所有可能的输入来测试程序。即便程序能通过每一个测试，也不能排除它在一些极端情况下运行不正常，进而形成漏洞。在实际的程序中，这种漏洞也许会简单到只是一个缓冲溢出错误，即程序拷贝多了一丁点数据，并覆盖了某一小块计算机内存。这个看起来无害的错误很难彻底根除，是黑客们攻入计算机系统的捷径。

Bryan Parno说道：“只要程序中有一个缺陷，就能成为安全弱点。很难测试所有可能输入的所有路径。”

实际的形式规范要比自动驾驶去百货商店细致得多。比如编写一个确认收到文件，并按收到时间对文件进行排序的程序，形式规范需要规定计数器永远只能增长(好让后面接收的文件序号总比前面收到的文件高)，以及程序永远也不会泄露给文件签名的密钥。

这么说着容易，真正要用形式语言来编写一个计算机能应用的规范却很难，更何况还是要在整个软件编写过程中都这么做。

Bryan Parno表示：“写出机器能识别的形式规范或目标非常考验智商。站在高处说‘不要泄露密码’很容易，真正要把它用数学定义的形式写出来却需要很多思考。”

再比如，给列表或数字排序的程序，程序员可能会这么给它写形式规范：

　　For every item j in a list, ensure that the element j ≤ j+1

(对于列表中的每一项j，确保j ≤ j+1)

然而这个形式规范却有一个漏洞：这个程序员默认输出会是输入的排序结果，即假设列表为[7, 3, 5]，这个程序应该返回[3, 5, 7]，这样就满足了定义。但列表[1, 2] 也满足定义，因为“这是一个排序好了的列表，只不过可能不是我们希望的那种排序好了的列表。”

换言之，要把你想要让程序做的事，用排除了所有可能不正确解释的形式规范表示出来很难。上面的例子还只是一个简单的排序程序，想象一个更抽象的例子，比如保护密码。Bryan Parno说道：“这在数学上是什么意思？定义它也许要写出保护密码的数学描述。安全的加密算法又是什么意思呢？这也是我们一直在研究中一直在思考并取得进展的问题，但要正确应用必须非常小心。”

(责任编辑：安博涛)