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 对此表示乐观，认为形式方法研究人员们会找到解决办法。

　　via quantamagazine