基于代码块的安全

编写这种程序需要同时编写形式规范以及帮助编程软件推导代码所必须的额外注释， 因此其长度达到了传统程序的五倍。

用合适的工具可以在一定程度上减轻这一负担，比如专门的编程语言和辅助证明程序。但这些东西在上世纪70年代时还不存在。同时担任形式验证计算机系统开发团体DeepSpec首席研究员的Andrew Appel表示：“当时的很多技术都不成熟，因此到80年代，很多人就对它失去了兴趣。”

即便工具得到了改进，形式验证计算机程序还有另一个问题要解决：没人确定是否有必要用它。虽然形式方法爱好者们总是在说小的程序错误最后会变成灾难性漏洞，但大家看到的却是计算机程序工作得相当好。

的确，这些计算机程序有时候会崩溃，但和巨细无遗地一条条用形式逻辑系统的语言来编写程序相比，丢失未保存的数据或时不时重启机器貌似也可以接受。有时候，连形式规范最早期的领导者也会怀疑其是否有用。在上世纪 90 年代，霍尔逻辑(Hoare logic，首批推导计算机程序正确性的形式系统之一)的发明者 Hoare就承认，也许形式规范是一个不存在的问题的劳动密集性解决方案。他在1995年写道：

十年前，形式方法的研究者们(我是其中错得最厉害的一个)预测，计算机世界会拥抱并感激形式化带来的每一点协助……结果是，全世界并没有碰到我们一开始打算解决的那种问题。

后来出现了互联网。互联网之于编程错误就像是飞机之于传染病：当所有电脑都连接在一起时，不方便但可以忍受的软件漏洞会导致一系列安全问题。

Andrew Appel说道：“有一点我们当时没有特别明白，那就是互联网上有一些软件面向所有黑客开放，如果这种软件里有一个漏洞，它就会成为安全威胁。”

 

在微软研究院开发形式验证版HTTPS协议的计算机科学家Jeannette Wing

在研究人员们开始明白互联网给计算机安全带来的致命威胁后，程序验证就开始焕发第二春了。研究人员们这一次在加强形式方法的技术上取得了很大进展：改进了支持形式方法的辅助证明程序Coq和Isabelle；开发了新的逻辑系统，为计算机提供推导代码的框架；发展改进了运算语义学(operational semantics)，即可以用正确的词语来表达程序应该做什么事了。

微软研究院企业副总裁Jeannette Wing表示道：“所有自然语言都具有歧义性。而在形式规范中，你会写出基于数学的精确规范，以解释你想要程序做什么。”

另外，形式方法的研究人员们也修改了自己的目标。在上世纪七、八十年代，他们想要打造完整的经过形式验证的计算机系统，从芯片到计算机程序。现在，大多数形式方法研究人员都专注于验证更小但更脆弱或系统关键的组成部分，比如操作系统或加密协议。

Jeannette Wing说道：“我们不再宣称要证明整个系统都正确，每一个比特都百分百可靠，连芯片层面也如此。做出这样的宣言很可笑。对于我们能以及不能做什么，我们现在有了更清楚的认识。”

高可靠性军事网络系统项目证明，通过明确定义计算机系统中的一小部分，就能极大地提高安全性。这个项目的最初目标是打造一架无法被黑的娱乐四旋翼无人机。但无人机运行的软件非常庞大，黑客攻破一部分，就能获得整个系统的控制权。于是在接下来的两年里，高可靠性军事网络系统团队将无人机的任务控制计算机程序代码分成了很多块。

他们还用“高可靠性构建模块”重写了软件架构，这些模块可以让程序员们证明自己代码的可靠性。其中一个经过了形式验证的模块可以确保，即便用户取得了一个代码块的控制权，他也不能提升自己的权限来进入其他代码块。

随后，高可靠性军事网络系统团队将这一区块化的软件安装到了“小鸟”无人军事直升机上。在和红方黑客团队的较量中，他们先让黑客们可以访问某一次要功能如摄像头的代码，但黑客们肯定会被困住，因为这经过了数学证明。Kathleen Fisher 说道：“我们用机器从数学上证明了红方肯定无法突破这一代码块，因此他们无法突破也就很顺理成章了。结果与定理一致，也很好确认。”

在“小鸟”无人军事直升机上测试后，美国国防部高级研究计划局就开始将这些工具和技术应用到其他军事技术上，比如卫星和无人驾驶载重卡车。新的项目和过去十年中形式验证传播的方式保持一致：每一个成功的项目都能加强下一个项目。Kathleen Fisher表示道：“人们再也没有借口说这么做太难了。”

　　验证互联网

安全和可靠性是驱动形式方法的两大目标。每过一天，提高这两大目标的需要就会变得越发明显。在2014年，一个本可以被形式规范捕捉到的小编程错误导致了“心脏失血”漏洞，甚至可能让互联网瘫痪。一年以后，两个白帽子黑客证明了我们对联网汽车的最大恐惧：他们成功地控制了别人的大切诺基。

随着安全风险的日益增加，形式方法研究人员们正推动更具野心的计划。Andrew Appel领导的DeepSpec正试图建立一个经过完全验证的端到端系统(就像网络服务器一样)。如果这一计划成功，就能将过去十年中许多更小规模的验证成果组合到一起，比如经过完全验证的操作系统内核。Andrew Appel说道：“DeepSpec现在专注在做但还没有做到的事情是，如何将这些组件用规范接口连接起来。”

在微软研究院中，软件工程师们已经在进行两个雄心勃勃的形式验证项目。第一个项目名为Everest，旨在打造经过形式验证的HTTPS协议。

第二个项目则是希望能为无人机这样的复杂物联网系统开发出经过验证的规范。这个项目面临的挑战非常大。要知道传统软件按离散、确定的步骤执行，无人机软件会根据连续的环境数据流，运用机器学习来计算概率并进行决策。要把这种不确定性形式规范化会需要很多思考。不过形式方法在过去十年中取得了很多进展，Jeannette Wing对此表示乐观，认为形式方法研究人员们会找到解决办法。

(责任编辑：安博涛)