你相信存在没有漏洞的代码吗？美国人正在研究

万物互联时代的到来，除了为人们的生活提供了便利也带来了众多安全隐患，越来越多的设备更容易遭受黑客攻击。有没有可能诞生一种无法被入侵的代码？

DARPA（美国国防部高级研究计划局）有个HACMS项目，即“高可信军事网络系统”（High-Assurance Cyber Military Systems) ，开发的主要是“formal verification”技术。而其项目目标就是让黑客难以入侵到诸如无人机、军事指挥控制网络系统中。

互联网鼻祖DARPA（美国国防部高级研究计划局）

如今我们每天都会使用互联网，而你是否考虑过网络是由谁发明的呢？

因特网的发明最初的用户群并非普通人，而是国家军事机构，而我们用的因特网是后来转变出来的。如果说到因特网的发明者不得不提到美国的一个神奇的机构：美国国防部高级研究计划局（DARPA）。DARPA成立于美苏冷战 的Dwight David Eisenhower（艾森豪威尔，34任总统 ）任期内，目的是为美国开发尖端技术。

DARPA隶属于五角大楼，是美国国防部一个非常特殊的部门。半个世纪以来，DARPA都对我们的生活产生了巨大影响。我们现在熟知的因特网、隐身技术、移动GPS等都是来自于DARPA这个部门。

我们都已经知道因特网是DARPA研发出的，而网络黑客也是因这项技术衍生出的。技术和互联网的迅速崛起成为安全漏洞频发的借口，对于高级黑客而言，入侵复杂的系统就如同小孩过家家。脆弱的系统和技能先进的黑客日益威胁着用户的安全。如今，DARPA表示自己正在在“防黑客”电脑系统上做出技术努力，这个项目被称为HACMS（高可信军事网络系统)。

据悉，DARPA邀请了一批“从良”黑客参与测试，HACMS在研发过程中让 这些白帽子黑客肆意入侵系统，他们展示了多种方法，可以轻松破解没有安装HACMS的系统和网络；但是在尝试入侵安装了HACMS的系统时，没有一个人成功。 而这项技术目前已经开始被诸如医疗设备等民用领域付诸实践，并且在Github上公布了源代码 。

尝试攻击“小鸟”无人直升机

去年夏天，亚利桑那州某黑客团队尝试控制波音的“小鸟”（Little Bird）无人军事直升机。该黑客团队一开始就被授权了“小鸟”计算机系统的一部分访问权限。 他们要做的就是入侵“小鸟”的机载飞行控制计算机，进而控制整架直升机——这对他们而言原本就不应该是什么难事。

但是作为HACMS项目的一部分，事情当然不会如此简单。 DARPA的工程师们为“小鸟”开发了一种新的安全机制：一个无法被攻占的软件系统。

DARPA给了该黑客团队6周时间，该团队始终没能攻破“小鸟”无人军事直升机计算机系统的。这其中还需要考虑到，在攻击之前，黑客团队就有一定的访问权限，即便如此也仍旧不行。

高可靠性军事网络系统(HACMS)项目发起人、美国塔夫斯大学计算机科学教授 Kathleen Fisher 表示：

“黑客们无法以任何方式扩大控制并干扰机器运行。这一结果让美国国防部高级研究计划局非常高兴，他们说现在终于能用这一技术来保护核心计算机系统了。”

“小鸟”无人军事直升机计算机部署的新系统使用的技术为形式验证(formal verification) ，它的代码就像数学证明一样可靠。每一个证明在逻辑上都承接上一个证明 。一个这样的程序可以像证明数学定理一样，无论如何测试都一定会得到正确的结果。

微软研究院研究形式验证和安全的研究员 Bryan Parno 表示：

“你写下的数学公式就是用来描述程序行为的，再利用一些证明检查器来检查 证明的正确性。”

整个过程包括，反复检查代码是否遵守预定义形式规范（formal specification），这里的形式规范定义了程序要做什么。

打个比方，比如你要给无人驾驶汽车编写一个把你送到百货商店的计算机程序，你需要定义让汽车实现这一目的的动作：汽车可以左转或右转、刹车或加速、启动或停车。最终，你的程序就是为了实现这一目的而对基本操作进行的合理组合，要求是把你送到百货商店而不是机场。

HACMS团队就是将这一区块化的软件安装到了“小鸟”无人军事直升机上。在和黑客团队的较量中，他们先让黑客们可以访问某一次要功能如摄像头的代码，但黑客们肯定会被困住，因为这经过了数学证明。Kathleen Fisher 说道：

“我们用机器从数学上证明了红方肯定无法突破这一代码块，因此他们无法突破也就很顺理成章了。结果与定理一致，也很好确认。”

在“小鸟”无人军事直升机上测试后，DARPA还开始将formal verification技术应用到其他军事技术上，比如卫星和无人驾驶载重卡车。现在，不仅是国防组织（如 DARPA）一直致力于形式验证技术，就连微软、亚马逊等科技公司也在不断加注投资，进行相关产品的研究。

微软研究院的软件工程师们已经在进行两个雄心勃勃的形式验证项目。第一个项目名为 Everest，旨在打造经过形式验证的 HTTPS 协议。第二个项目则是为拥有复杂物联网系统的无人机开发一个正式的规范。

随着越来越多的关键社会职能转移到网上，研究人员们对形式软件验证技术的兴趣也越来越浓厚。在以前，计算机还只是局限于家里和办公室，程序漏洞最多也就是让使用者感到不便。但现在，程序漏洞可能会导致巨大危害，任何具备相关知识的人都能利用同一漏洞自由地进出某个计算机系统。同时，物联网也在短短几年间实现爆发式增长，智能家居、智慧城市正逐渐渗透入我们的生活，这将势必为黑客入侵提供更多场所。期待此次技术开发能改变目前严峻的网络局势。

*原文链接：securitynewspaper、米雪儿编译