耶鲁大学的研究人员推出了CertiKOS，它是世界上第一个在多核处理器上运行并能抵御网络攻击的操作系统。科学家认为，这可能会导致新一代可靠，安全的系统软件。耶鲁大学计算机科学教授钟绍带领他们的研究人员开发了一个操作系统。该系统结合了形式验证，以确保程序准确地执行其设计者预期的工作—一种安全保护措施，可以防止从家用电器和物联网(IoT)设备到自动驾驶汽车和数字货币的任何事物受到黑客攻击。他们在CertiKOS上的论文在11月2-4日在佐治亚州萨凡纳举行的第12届USENIX操作系统设计和实现研讨会上发表。
可以相信，计算机操作系统的核心应该是一个小的，可信任的内核，该内核可以促进系统软件和硬件之间的通信。但是操作系统很复杂，它所要做的只是代码中的一个薄弱环节(实际上是通过传统测试无法检测到的)，从而使系统容易受到黑客的攻击。
CertiKOS的主要突破之一是它支持并发，这意味着它可以在多个中央处理单元(CPU)内核上同时运行多个线程(编程指令的小序列)。这使CertiKOS与其他先前已验证的系统脱颖而出，并使CertiKOS可以在现代多核计算机上运行。CertiKOS体系结构还被设计为高度可扩展的-也就是说，它可以具有新的功能并可以用于不同的应用程序域。
并发允许重叠执行多个程序线程，这使得不可能考虑所有情况并通过传统测试消除系统中的所有漏洞。长期以来，许多本领域的人认为，这种系统的复杂性也使得对功能正确性的形式验证成为有问题的或昂贵的。
国家科学基金会(NSF)计划主任Anindya Banerjee说：“至少从20世纪中叶开始，构建功能正确的系统软件一直是计算的一大挑战。”该基金会的部分资金来自CertiKOS的努力计算程序中的远征。“ CertiKOS证明，构建经过验证的软件是可行且实用的，该软件还可以通过机器可检查的数学证明来提供功能正确的证据。”
在构建CertiKOS系统时，Shao和他的团队结合了形式逻辑和新的分层演绎验证技术。也就是说，他们仔细地解开了内核相互依存的组件，将代码组织成大量的分层模块，并为每个内核模块的预期行为编写了数学规范。使用形式演绎验证来验证系统与使用常规方法来检查程序的可靠性不同，在常规方法中，代码编写者会在多种情况下对程序进行测试。
邵说：“一个程序可以正确地编写99%，这就是为什么今天您看不到明显的问题，但是黑客仍然可以潜入某个特定的设置中，该程序将无法正常运行。” “编写该软件的人全心全意地工作，但无法考虑所有情况。”
经过CertiKOS验证的操作系统内核是美国国防部高级研究局(DARPA)的高保障网络军事系统(HACMS)计划的关键组成部分，该计划用于构建可证明没有网络漏洞的网络物理系统。
DARPA计划经理Ray Richards说：“ HACMS团队使用CertiKOS提供的虚拟化功能将受信任的组件与不受信任的组件分开。” “这是一项重要功能，可让我们有效地构建具有网络弹性的系统。在网络安全日益受到关注的世界中，这种弹性是一个强大的属性，我们希望它将被系统设计人员广泛采用。”
直到最近几年，像CertiKOS这样的系统才有可能成为现实，因为认证内核的证据对于任何人来说都太大了。在过去的十年中，已经开发了功能强大的计算机程序，称为证明助手，可以自动生成和检查大型正式证明。
“这是惊人的进步，”康奈尔大学软件安全领域的领先专家，计算和信息科学系主任格雷格·莫里塞特(Greg Morrisett)说。“十年前，没有人能预测到我们可以证明单线程内核的正确性，更不用说多核内核了。钟先生和他的团队为我们其他人开创了辉煌的道路。”
NSF的DeepSpec联盟的负责人，普林斯顿大学的计算机科学教授安德鲁·阿佩尔(Andrew Appel)称CertiKOS是“真正的突破”，并指出它可以作为通过验证和不可信组件的组合构建高度安全系统的基础。
“但同样重要的是，CertiKOS中使用的模块化分层验证方法将不仅适用于操作系统，还适用于许多其他类型的软件，” Appel说。
