CERTIKOS：致黑客抗性操作系统的一步

来自Yale University的研究人员已经揭开了Certikos，这是世界上第一个在多核处理器和盾牌抵抗网络攻击的操作系统。科学家认为这可能导致新一代可靠和安全的系统软件。

研究人员由Zhong Shao领导计算机科学教授，开发了一个操作系统，该操作系统融合了正式验证，以确保计划正如其设计人员所预期的 - 可以防止从家电和互联网上攻击任何东西的保障措施（物联网）设备到自动驾驶汽车和数字货币。他们的关于Certikos的论文在第12届Usenix研讨会上介绍了11月2日至4日在萨凡纳，GA。

计算机科学家长期以来，计算机的操作系统应该在他们的核心处于一个小型，值得信赖的内核，这有助于系统软件和硬件之间的沟通。但操作系统很复杂，所需的只是代码中的一个弱链接 - 几乎无法通过传统测试检测 - 留下一个易受黑客攻击的系统。

Certikos的主要突破之一是它支持并发性，这意味着它可以同时运行多个中央处理单元（CPU）内核上的多个线程（小程序化指令的小序列）。除了以前先前经过验证的系统之外，这将CERTIKOS除外，并允许CERTIKOS在现代多核机器上运行。Certikos架构也被设计为高度可扩展 - 即它可以采用新功能，用于不同的应用领域。

并发允许重叠的多个程序线程执行，这使得不可能考虑所有情况并通过传统测试消除系统中的所有裂缝。该领域的许多人们认为，这种系统的复杂性也使功能正确性正式验证有问题或过于昂贵。

“专业纠正系统软件的建设是自20世纪中期以来计算的计算挑战之一，”国家科学基金会（NSF）的计划总监Anindya Banerjee说，这部分通过其努力计算计划中的探险。“Certikos表明，建立验证的软件是可行和实用的，该软件还提供了证据 - 通过机器可检测的数学证据 - 它在功能上是正确的。”

在构建Certikos系统中，邵和他的团队采用正式逻辑和新的分层演绎验证技术。也就是说，他们仔细地解除了内核的相互依存组件，将代码组织成大量的分层模块，并为每个内核模块的预期行为编写数学规范。使用正式的演绎验证来证明系统与检查程序可靠性的传统方法不同，代码编写器在众多场景中测试程序。

“一个程序可以正确地编写99％ - 这就是今天你没有看到明显的问题 - 但是黑客仍然可以潜入一个特定的设置，在那里计划不会按预期行事，”邵说。“写下软件的人与所有良好的意图一起工作，但不能考虑所有情况。”

Certikos已验证的操作系统内核是国防高级研究机构（DARPA）高保证网络军事系统（HACMS）计划的关键组成部分，用于构建可从网络漏洞的网络物理系统。

“HACMS团队使用CERTIKOS提供的虚拟化能力来与不受信任的组件分开信任，”DARPA计划经理Ray Richards表示。“这是一个重要的能力，使我们能够有效构建网络弹性系统。在网络安全是越来越关注的世界中，这种弹性是一个强大的属性，我们希望得到系统设计师的广泛采用。“

只有近年来，只有CERTIKOS这样的系统就可以了，因为认证内核的证据对于任何人来说都是太大的检查。然而，在过去的10年内，已在过去的10年内发出了强大的计算机程序，可以自动产生和检查大型正式证据。

“这是康奈尔大学的计算和信息科学院长的领先专家Greg Morrisett，”这是惊人的进步。“十年前，没有人能够预测我们可以证明一个单线程内核的正确性，更少是多核之一。钟和他的球队真的在我们其他人中真的陷入了壮观的小道。“

Andrew Appel，NSF的DeepSpec联盟主任和普林斯顿的计算机科学教授称为Certikos“真正的突破”，注意它可以作为构建高度安全系统的基础，从验证和不值得信任的组件的组合中建立高度安全的系统。

“但同样重要的是，Certikos中使用的模块化分层验证方法不仅适用于操作系统，而是对许多其他类型的软件，”Appel表示。

纸：CERTIKOS：用于构建认证的并发OS内核的可扩展架构