■徐令予

5月12日一早醒来，全球人终于明白互联网上不全是音乐和鲜花。一个名为“想哭”的勒索病毒袭击了全球上百个国家和地区使用微软操作系统的电脑，原来网络江湖也是波谲云诡、危机四伏。

怎样打造攻不破、摧不垮、百毒不侵的电脑，怎样才能还太平于网民，科学家们为了网络维稳真是操碎了心。

2015年的夏天，一群黑客企图控制一架名为“小鸟”（LITTLE BIRD H-6U）的军用无人直升机，这是亚利桑那州的波音工厂为美军特种作战任务研制的。当时为黑客做了这样的安排：他们开始操作时已经可以访问无人机电脑系统的一部分，他们只需入侵“小鸟”的机上飞行控制电脑，无人机即归他们所有。

一开始，黑客团队可以像侵入家庭WiFi一样轻松地接管直升机。但是在随后的几个月当中，国防高级研究计划局（DARPA）的工程师们开发并实施了一种新型的安全机制—— 一种百毒不侵的软件系统。“小鸟”的计算机系统的关键部分是现有技术完全无法入侵的。尽管把无人机的计算机网络完全开放，黑客团队也一直无法掌握“小鸟”的控制系统，最终以彻底失败而告终。

压制黑客的技术是一种称为软件编程的形式化方法，形式化软件验证需要程序中每个语句的前后都遵循严格的逻辑关系，整个程序测试的确定性就像数学家证明定理一样。

使用形式逻辑规则来指导程序设计起源于上世纪70年代。艾兹格·迪科斯彻首先提出了创建无错代码的想法。他在1976年完成的《编程规则》这部著作为程序验证打下了基础，他也因此获得了图灵奖。

将正确性证明纳入计算机程序编制一直没有得到广泛应用，计算机科学的发展毕竟不能单纯依靠愿望。长期以来，使用形式逻辑规则来指定程序的功能，有些不切实际，因为形式验证信息的程序长度可能是传统程序的5倍。这种编程的额外负担可以通过专用的编程语言和辅助程序减轻一些，但那些辅助软件工具在上世纪七八十年代并不存在。

即使辅助工具有所改进，推广程序验证的更大障碍是：没有人确定是否有必要。虽然一些专家一再强调编码小错误会导致灾难性的后果，但是吃瓜群众看到的是计算机程序大多数情况下工作正常。

但互联网改变了一切，一台计算机的编码错误可能会被黑客利用，导致成千上万台计算机被非法入侵控制，甚至使网络局部瘫痪。当研究人员开始了解互联网对计算机安全的威胁时，程序验证技术终于有了用武之地。首先，研究人员在基于形式化方法的编程技术上取得了巨大进步：改进了支持形式化方法的Coq和Isabelle等验证辅助程序；开发新的逻辑系统，为计算机对代码的推理提供了全新的框架；并且改进了所谓的“操作语义”——本质上是一种具有确切词汇的语言，可以更明确地表达程序究竟应该做什么。

美国的高保证网络军事系统（HACMS）项目显示了如何通过计算机系统分区隔离以保证总体的安全。该项目的第一个目标是创造一个无法入侵的娱乐级四轴飞行器。运行该飞行器的商品化软件是整体单一化的，这意味着如果攻击者突破一点，他就可以控制整个软件。在接下来的两年中，HACMS团队将四轴飞行器任务控制计算机中的代码分区隔离。

该团队还重新制定了软件架构，使用了被HACMS项目经理凯瑟琳·费舍尔称之为“高保证构建块”的东西，这是一种让程序员证明其代码正确无误的工具。其中一个经过验证的构建块可以保证在某个分区内具有访问权限的操作者无法升级越界进入其他分区。

在四轴飞行器取得经验之后，研究人员在“小鸟”军用无人直升机上安装了这个分区隔离软件。在测试中，他们提供了黑客团队进入无人直升机的某一分区，例如摄相机控制分区，但并不是核心功能分区。在无情的数学公式面前，黑客被死死地卡在一个分区中不得“动弹”。

事实上，计算机系统的分区隔离技术与绝密军工厂的管理方式有着某种程度的雷同。近年来，计算机硬件性能的飞速进步，也为计算机系统的分区隔离技术提供了物质基础，今日强大的中央处理器能力和海量的内存空间完全可以支持系统的分区运行管理。

在“小鸟”无人直升机测试之后的一年，DARPA正努力将HACMS项目的工具和技术应用于其他军事技术领域，如卫星和无人自动驾驶车队。

为了捍卫互联网的安全，形式化方法的研究人员正在推动更加雄心勃勃的计划。DeepSpec合作项目力图将过去十年中已经成功通过形式化验证的许多小型模块进行组合，以构建一个经过完全形式化验证的端点到端点的系统，如Web服务器。

而在微软的研究部门，软件工程师正在进行两项雄心勃勃的形式化验证项目。第一个名为珠穆朗玛峰，这是创建一个经过形式化验证的HTTPS版本，新的协议可以有效地保护被称之为“互联网的阿喀琉斯之踵”的网络浏览器。

第二个是为复杂的网络物理系统（如无人机）制定形式化验证规范，这里的挑战可能更为严峻。无人机飞行涉及到机器学习，以及在连续的环境数据流中进行概率判定，如何对不确定性进行推理并制定形式化规范是极大的挑战。

可喜的是，在过去的十年中，软件工程的形式化方法已经有了长足的进步，从事该项研究的科学家们应对未来持谨慎乐观的态度。

（http：//blog.sciencenet.cn/u/lxu2800）