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

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

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

因特网的发现最初的用户群并非普通人，而是国家军事机构，而我们用的因特网是后来改变出来的。如果说到因特网的发现者不得不提到美国的一个神奇的机构：美国国防部高级研究打算局（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 说道：

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