今日，形式化方法的研究人员的目标也变得更为现实。在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，每日阅读趣味文章。