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

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

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

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

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

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

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

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

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

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