徐令予：攻不破、摧不垮、毒不侵的电脑怎样炼成？
【文/ 观察者网专栏作者 徐令予】
5月12日早上醒来，全球人终于明白互联网上不全是音乐和鲜花。一个名为“想哭”的勒索病毒袭击了全球上百个国家和地区使用微软操作系统的电脑，原来网上的江湖波谲云诡、危机四伏。
怎样打造攻不破、摧不垮、毒不侵的电脑，怎样才能还太平与网民，科学家们为了网络维稳真是操碎了心。
据《量子杂志》报道，2015年的夏天，一群黑客企图控制一架名为“小鸟”（LITTLE BIRD H-6U）的军用无人直升机，那是在亚利桑那州的波音工厂为美军特种作战任务研制的装备。当时黑客作了这样的安排：他们开始操作时已经可以访问无人机电脑系统的一部分。从那里开始，他们只需入侵“小鸟”的机上飞行控制电脑，无人机就是他们的了。
LITTLE BIRD H-6U 军用无人直升机
当项目开始时，黑客团队可以像侵入家庭Wi-Fi一样轻松地接管直升机，易如囊中探物。但在随后的几个月中，美国国防高级研究计划局（DARPA）的工程师们开发并实施了一种新型的安全机制，一种百毒不侵的软件系统。“小鸟”的计算机系统的关键部分是现有技术完全无法入侵的，其代码的正确可靠能像数学一样被证明。尽管把无人机的计算机网络完全开放，黑客团队一直无法掌握“小鸟”的控制系统，他们经过连续六周的攻击而不能越雷池于一步，黑客以彻底失败而告终。
“黑客无法以任何方式突破系统和破坏正常的飞行。”塔夫茨大学计算机科学教授和高保证网络军事系统（HACMS）项目的主管凯瑟琳·费舍尔指出，“这个结果使所有的DARPA人员信服，我们实际上可以在我们关心的系统中使用这种技术。”
压制黑客的技术是一种称为软件编程的形式化方法[1]。过去对传统计算机代码的评估主要是检查它是否在各种情况下都能正常工作，而形式化软件验证如同数学证明：程序中每个语句的前后都遵循严格的逻辑关系，整个程序测试的确定性就像数学家证明定理一样。
大多数传统计算机的程序是如何工作的呢？设想为无人驾驶车编写一个计算机程序。在操作层面上，你可以定义汽车在行程中各种必须的操作行为，它们可以是左转、右转、制动或加速。而程序则是按照适当顺序排列的基本操作的汇编，以确保让你到达杂货店而不是机场。
长期以来，对此类程序的评估和验收的传统方法是进行简单的测试。把各种起始点和目标的位置输入程序，检查在程序控制下的无人驾驶车辆是否正确到达预定目标。这种测试方法在大多数情况下可以满足我们的要求。但是这种测试法不能保证软件将百分之百地正常工作，因为各种输入和输出的组合无穷无尽，现实环境中总会有罕见的情况发生，总会有不能预测到的“角落”，从而导致程序出错。
在程序的运行中，这些出错和故障当然要不得，但更大的危害是可能引起计算机内存缓冲区溢出，为黑客攻击系统提供了跳板，软件中的任何一个缺陷都可能就是系统安全的漏洞。
再举一个例子，考虑对一串数字排序的程序。程序员对排序程序的定义可能会写成这样：
对于列表中的每个元素j，确保元素j≤j+1
然而，这种定义——确保列表中的每个元素小于或等于其后面的元素——隐含了一个错误：程序员假定输出总是输入的一种置换。也就是说，对于输入列表[7,3,5]，她期望程序将输出[3,5,7]以满足排序定义。然而，列表[2,5,7]也同样满足定义，它是一个排序列表，但它不是我们希望的排序列表。严格地说，除了排序还必须确保输出与输入的元素集合完全一致，这在以往的程序设计中常常被忽视。
换句话说，将一个程序应该做些什么的想法转化为一个正式的规范，同时又要排除对此可能产生的各种不正确的解释，这常常是十分困难的。上面的例子只是一个简单的排序程序。现在想象一下比排序更抽象的程序，比如保护密码，这在数学上又是什么意思？ 它可能涉及为保护密码进行数学描述，或者对加密算法的安全性作出定义。这些问题提岀并不太难，但找到正确简单的方案却十分不易。
使用形式逻辑规则来指导程序设计起源于上世纪七十年代。1973年10月，艾兹格·迪科斯彻(Edsger Dijkstra)提出了创建无错代码的想法。在会议期间他住在酒店，半夜三更产生了让编程更加数学化的灵感。他在后来回忆道：“我的大脑在燃烧，凌晨2:30离开了我的床，伏案书写了一个多小时。”这些材料成为了他于1976年完成的“编程规则”这部著作的基础，他因此获得了图灵奖——计算机科学的最高荣誉。
但是将正确性证明纳入计算机程序编制一直没有得到广泛的应用，计算机科学的发展毕竟不能单纯依靠愿望。主要是因为长年以来，使用形式逻辑规则来指定程序的功能，即便并非不可能，似乎也是不实际的。包含形式验证信息的程序可能是相同的传统程序的五倍长度。这种编程的额外负担可以通过专用的编程语言和辅助程序减轻一些，但那些旨在帮助软件工程师的工具在上世纪七八十年代并不存在。
即使辅助工具有所改进，推广程序验证的更大障碍是：没有人确定是否有必要。虽然一些专家一再强调编码小错误会导致灾难性的后果，但是吃瓜群众看到的是计算机程序大多数情况下工作正常。当然，有时候会丢失数据或蓝屏死机，但是天又塌不下来，让文秘重新输入数据或者偶尔重新启动计算机又有什么大不了。
到了20世纪90年代，程序验证的鼻祖也开始怀疑它的用处了。图灵奖得主Tony Hoare——“霍尔逻辑”的创始人——也承认软件编程的形式化方法可能既劳民伤财又无的放矢。他在1995年写道：十年前，形式化方法的研究人员（而我是其中最为错误的一位）预测，软件业界将会怀着感激之情拥抱形式化方法带来的成果，而事实证明：我们企图要解决的问题实质上对世界并没有产生多大的影响。
但是互联网改变了一切，如同航空旅行的普及导致传染病的飞速传播，当计算机都互相联接在一起，一台计算机的编码错误可能会被黑客利用，导致成千上万计算机被非法入侵控制，甚至使网络局部瘫痪。至少2017年5月12日全世界尝到了苦头。
当研究人员开始了解互联网对计算机安全的威胁时，程序验证技术终于有了用武之地。首先，研究人员在基于形式化方法的编程技术上取得了巨大进步：改进了支持形式化方法的Coq和Isabelle等验证辅助程序；开发新的逻辑系统，为计算机对代码的推理提供了全新的框架；并且改进了所谓的“操作语义”——本质上是一种具有确切词汇用以表达程序究竟应该做什么的语言。
今日，形式化方法的研究人员的目标也变得更为现实。在20世纪70年代和80年代初期，这些研究人员试图创建可以验证的计算机系统，一个从硬件电路到软件程序的完整系统。如今大多数研究人员侧重于验证系统中较小但特别脆弱或关键的部分，如操作系统和加密协议。
“我们并不声称我们将证明整个系统是正确的，每一点都百分之百的可靠，从上至下直到电子电路的水平。”微软研究院的计算机科学家Jeannette Wing指出：“这些做法是荒谬的。我们更清楚我们能做什么，不能做什么。”
HACMS项目显示了如何通过计算机系统分区隔离以达到总体的安全保证。该项目的第一个目标是创造一个无法入侵的娱乐级四轴飞行器。运行该飞行器的商业软件是一个整体，这意味着如果攻击者突破一点，他就可以控制整个软件。在接下来的两年中，HACMS团队将四轴飞行器的任务控制计算机中的代码分区隔离。
该团队还重新制定了软件架构，使用了被HACMS项目经理凯瑟琳·费舍尔称之为“高保证构建块”的技术，这是一种让程序员证明其代码正确无误的工具。其中一个经过验证的构建块可以保证在某个分区内具有访问权限的操作者无法升级越界进入其他分区。
高保证网络军事系统（HACMS）项目主管 凯瑟琳·费舍尔
在四轴飞行器取得经验之后，HACMS程序员在“小鸟”军用无人直升机上安装了这个分区隔离软件。在测试中，他们提供了黑客团队进入无人直升机的某一分区，例如摄相机控制分区，但并不是核心功能分区。在无情的数学公式面前，黑客被死死地卡住在一个分区中无法乱说乱动。“他们以机器检查的方式证明，黑客不能脱离分区，这毫不奇怪，他们就是不能。”凯瑟琳·费舍尔说：“这与定理是一致的，试验也证明了这一点。”
为了帮助非专业人员了解分区隔离技术的基本原理，让我们回顾一下上世纪中国绝密军工厂的管理，这类军工厂不仅门卫森严，而且内部分成密级不同的独立车间，人员不得互相来往。每个产品又必经多个车间加工生产。一个间谍（黑客）进入工厂并混进某个车间已经非常不易，他下足工夫取得车间主任的信任或许能获得某种特权，但他最多只能在一个车间中活动，他对整个产品的认识和控制是十分有限的，因为任何试图跨越车间界限的行为会被严格的限制，而且其真实身份会立刻受到特别调查。计算机系统的分区隔离技术与绝密军工厂的管理方式有着某种程度的类同。
近年来，计算机硬件性能的飞速进步也为计算机系统的分区隔离技术提供了物质基础，今日强大的中央处理器能力和海量的内存空间完全可以支持系统的分区运行管理。
在“小鸟”无人直升机测试之后的一年，DARPA正努力将HACMS项目的工具和技术应用于其他军事技术领域，如卫星和无人自动驾驶车队。
为了捍卫互联网的安全，形式化方法的研究人员正在推动更加雄心勃勃的计划。DeepSpec合作项目力图将过去十年中已经成功通过形式化验证的许多小型模块进行组合，以构建一个经过完全形式化验证的端到端系统，如Web服务器。
在微软的研究部门，软件工程师正在进行两项雄心勃勃的形式化验证项目。第一个名为珠穆朗玛峰，这是创建一个经过形式化验证的HTTPS版本，新的协议可以有效地保护被称之为“互联网的阿喀琉斯之踵”的网络浏览器。第二个是为复杂的网络物理系统（如无人机）制定形式化验证规范，这里的挑战可能更为严峻。无人机飞行涉及到机器学习，以及在连续的环境数据流中进行概率决定，如何对不确定性进行推理并制定形式化规范是极大的挑战。但在过去的十年中，软件工程的形式化方法已经有了长足的进步，从事该项研究的科学家们对未来持有谨慎乐观的态度。
[1]形式化方法(Formal Method)是基于严密的、数学上的形式机制的计算机系统研究方法，该知识体系中有6个主要领域，分别为:
① 基础(Foundations);
② 形式化规格(Formal specification paradigms);
③ 正确性验证及演算(Correctness, verification and calculation);
④ 形式化语义(Formal semantics);
⑤ 可执行规范支持(Support for executable specification);
⑥ 其他(Other Topics)。
本文系观察者网独家稿件，文章内容纯属作者个人观点，不代表平台观点，未经授权，不得转载，否则将追究法律责任。关注观察者网微信guanchacn，每日阅读趣味文章。