攻不破、摧不垮、百毒不侵的电脑是怎样练成的？

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

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

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

一开始，黑客团队可以像侵入家庭Wi-Fi一样轻松地接管直升机，易如囊中探物。但在隨后的几个月中，国防高级研究计划局（DARPA）的工程师们开发并实施了一种新型的安全机制，一种百毒不侵的软件系统。“小鸟”的计算机系统的关键部分是现有技术完全无法入侵的，其代码的正确可靠能像数学一样被证明。尽管把无人机的计算机网络完全开放，黑客团队一直无法掌握“小鸟”的控制系统，他们经过连续六周的攻击而不能越雷池于一步，黑客以彻底失败而告终。

压制黑客的技术是一种称为软件编程的形式化方法[1]。过去对传统计算机代码的评估主要是检查它是否在各种情况下都能正常工作，而形式化软件验证如同数学证明：程序中每个语句的前后都遵循严格的逻辑关系，整个程序测试的确定性就像数学家证明定理一样。

大多数传统计算机的程序是如何工作的呢？设想为无人驾驶车编写一个计算机程序。在操作层面上，可以定义汽车在行程中各种必须的操作行为，它们可以是左转、右转、制动或加速。而程序则是按照适当顺序排列的基本操作的汇编，以确保让车子到达杂货店而不是机场。

长期以来对此类程序的评估和验收的传统方法是进行简单的测试。把各种起始和目标的位置输入程序，检查在程序控制下的无人驾驶车辆是否正确到达预定目标。这种测试方法在大多数情况下可以满足我们的要求。但是这种测试法不能保证软件将百分之百地正常工作，因为各种输入和输出的组合无穷无尽，现实环境中总会有罕见的情况发生，总会有不能预测到的“角落”，从而导致程序出错。

在程序的运行中，这些出错和故障当然要不得，但更大的危害可能引起计算机内存缓冲区溢出，为黑客攻击系统提供了跳板，软件中的任何一个缺陷都可能就是系统安全的漏洞。

再举一个例子，考虑对一串数字排序的程序。程序员对排序程序的定义可能会写成这样：

对于列表中的每个元素j，确保元素j≤j+1

然而，这种定义——确保列表中的每个元素小于或等于其后面的元素——隐含了一个错误：程序员假定输出总是输入的一种置换。也就是说，对于输入列表[9,2,5]，期望程序将输出[2,5,9]以满足排序定义。但是列表[2,5,7]也同样满足定义，它也是一个排序列表，但它不是我们希望得到的排序列表。严格地说，除了排序还必须确保输出与输入的元素集合完全一致，这在以往的程序设计中常常被忽视。

换句话说，将一个程序应该做些什么的想法转化为一个正式的规范，同时又要排除可能产生的各种不正确的解释，这常常是十分困难的。上面的例子只是一个简单的排序程序。现在想象一下比排序更抽象的程序，比如保护密码，这在数学上又是什么意思？ 它可能涉及对密码保护进行数学描述，或者对加密算法的安全性作出定义。

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

七十年代末，我在上海交大三系读硕，我的两位同门师兄的选题就是“程序设计自动化验证”，可见当时中国高校对世界科技动向还是挺敏感的。那个年月硕士生课题不少是“高大上”的，但大多严重脱离实际，对课题项目也缺少长期的规划和投入，我估计也难有实质性的收获。

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

即使辅助工具有所改进，推广程序验证的更大障碍是：没有人确定是否有必要。虽然一些专家一再强调编码小错误会导致灾难性的后果，但是吃瓜群众看到的是计算机程序大多数情况下工作正常。当然，有时候会丢失数据或蓝屏死机，但是天又塌不下来，让文秘重新输入数据或者偶尔重新启动计算机又有什么大不了。

但是互联网改变了一切，如同航空旅行的普及导致传染病的飞速传播，当计算机都互相联接在一起，一台计算机的编码错误可能会被黑客利用，导致成千上万计算机被非法入侵控制，甚至使网络局部瘫痪。至少2017年5月12日全球网民尝到了苦头。

当研究人员开始了解互联网对计算机安全的威胁时，程序验证技术终于有了用武之地。首先，研究人员在基于形式化方法的编程技术上取得了巨大进步：改进了支持形式化方法的Coq和Isabelle等验证辅助程序;开发新的逻辑系统(dependent-type theories)，为计算机对代码的推理提供了全新的框架;并且改进了所谓的“操作语义”——本质上是一种具有确切词汇的语言，可以更明确地表达程序究竟应该做什么。

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

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

在四轴飞行器取得经验之后，研究人员在“小鸟”军用无人直升机上安装了这个分区隔离软件。在测试中，他们提供了黑客团队进入无人直升机的某一分区，例如摄相机控制分区，但并不是核心功能分区。在无情的数学公式面前，黑客被死死地卡住在一个分区中不得乱说乱动。“他们以机器检查的方式证明，黑客不能脱离分区，这毫不奇怪，他们就是不能。”凯瑟琳·费舍尔说：“这与定理是一致的，试验也证明了这一点。”

为了帮助非专业人员了解分区隔离技术的基本原理，让我们回顾一下上世纪中国绝密军工厂的管理，这类军工厂不仅门卫森严，而且内部分成密级不同的独立车间，人员不得互相来往。每个产品又必经多个车间加工生产。一个间谍（黑客）进入工厂并混进某个车间已经非常不易，他下足工夫取得车间主任的信任或许获得某种特权，但他最多只能在一个车间中活动，他对整个产品的认识和控制是十分有限的，因为任何试图跨越车间界限的行为会被严格的限制，而且其真实身份会立刻受到特别调查。计算机系统的分区隔离技术与绝密军工厂的管理方式有着某种程度的类同。

近年来计算机硬件性能的飞速进步也为计算机系统的分区隔离技术提供了物质基础，今日强大的中央处理器能力和海量的内存空间完全可以支持系统的分区运行管理。

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

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

在微软的研究部门，软件工程师正在进行两项雄心勃勃的形式化验证项目。第一个名为珠穆朗玛峰，这是创建一个经过形式化验证的HTTPS版本，新的协议可以有效地保护被称之为“互联网的阿喀琉斯之踵”的网络浏览器。第二个是为复杂的网络物理系统（如无人机）制定形式化验证规范，这里的挑战可能更为严峻。无人机飞行涉及到机器学习，以及在连续的环境数据流中进行概率判定，如何对不确定性进行推理并制定形式化规范是极大的挑战。但在过去的十年中，软件工程的形式化方法已经有了长足的进步，从事该项研究的科学家们对未来持有谨慎乐观的态度。

高保证网络军事系统（HACMS）项目主管 凯瑟琳·费舍尔        

[1]形式化方法(Formal Method)是基于严密的、数学上的形式机制的计算机系统研究方法，该知识体系中有6个主要领域，分别为:
① 基础(Foundations);
② 形式化规格(Formal specification paradigms);
③ 正确性验证及演算(Correctness, verification and calculation);
④ 形式化语义(Formal semantics);
⑤ 可执行规范支持(Support for executable specification);
⑥ 其他(Other Topics)。

本文首发于观察者网 2017年5月22日