黑客无法破解的内核

软件蚕食世界，在技术界和科幻小说憧憬的未来，机器将会把人类从大部分的事情中解放出来。不过就像给一个没有司机的世界准备的路线图中描述的担忧一样，软件控制引发的安全风险也会给我们造成极大的威胁。如果软件失去控制或者被恶意控制，那我们可能就会面临世界末日。

一辆无人车被恶意控制的最严重后果也许是恶性交通事故，但有些东西被控制的后果则可能是灾难性的，比如说美国军方正在研制的各种无人武器。如果黑客控制了这些武器，那情况就非常恐怖了。这些武器能不能抵御黑客的破解呢？

DAPRA已经开始了这样的测试。其测试对象是一艘波音小鸟无人武装直升机。黑客得到的条件宽松无比，他们可以任意访问机载计算机，其任务是竭尽所能让直升机失去能力—包括把系统搞崩溃都可以。但无论黑客如何努力，机载计算机的关键系统仍然安然无恙。DARPA希望，作为其高可信网络军事系统（HACMS）的一部分，到2018年能研发成功这种“无法破解”的无人机。这次测试可以算是取得一次阶段性的胜利。

这套系统的内核是seL4，它具备了若干高度安全的特质：比方说只会做设定的事情；没有许可的情况下代码无法变更，也无法访问内存和数据传输。

据开发者Gernot Heiser介绍，seL4实现这些安全特性有两个关键。一是将数据与内核进行隔离的新办法。但更关键的一点是代码可以进行数学上的校验。这一点是这套内核最大的区别：虽然别的内核也具备类似的安全特性，但是seL4的安全性却可以从数学上加以证明自己是无法破解的—即这套系统的完整性和机密性在数学上是可以证明的。

Heiser现在已经加入了新成立的澳大利亚国立研究机构Data61。而seL4的上一版OKL4目前已经部署在数百万智能手机上。Heiser希望，用10年的时间这套系统能部署到任何对安全要求非常高的东西上，比如起搏器、胰岛素泵、电站控制系统、汽车控制系统（克莱斯勒一定很需要这样的东西）等等。

不过，虽然内核不可破解经过了“数学证明”，但是黑客仍有可能通过破坏硬件来攻击目标，比方说欺骗硬件的传感器、阻塞通信或其他信号等，这些仍然会构成会毁灭性影响。未来的安全保障依然任重道远。