CertiKOS:迈向抗黑客操作系统的一步 2017-03-10 09:20:19

$888.88
所属分类 :财政

耶鲁大学的研究人员推出了CertiKOS,这是世界上第一个运行多核处理器并防御网络攻击的操作系统科学家认为这可能会导致新一代可靠安全的系统软件由计算机科学教授钟绍领导在耶鲁大学,研究人员开发了一种操作系统,该系统结合了形式验证,以确保程序能够像设计师所期望的那样精确地执行 - 这是一种可以防止从家用电器和物联网(IoT)设备到自动驾驶汽车的任何攻击的安全措施他们在CertiKOS上发表的论文于11月2日至4日在加利福尼亚州萨凡纳举行的第12届USENIX操作系统设计与实施研讨会上发表

计算机科学家一直认为,计算机操作系统的核心应该是一个小而值得信赖的内核

促进系统软件和硬件之间的通信但操作系统a变得复杂,所需要的只是代码中的一个薄弱环节 - 通过传统测试几乎无法检测到 - 使系统容易受到黑客攻击CertiKOS的一个主要突破是它支持并发,这意味着它可以在多个中央处理器(CPU)内核上同时运行多个线程(小程序编程指令)这使CertiKOS与其他先前验证的系统区别开来,并允许CertiKOS在现代多核机器上运行CertiKOS架构也设计为高度可扩展 - 也就是说,它可以采用新的功能并用于不同的应用程序域并发允许多个程序线程的重叠执行,这使得无法考虑所有情况并通过传统测试消除系统中的所有裂缝长期以来认为,这种系统的复杂性也使得功能相关的形式验证成为可能有问题或过于昂贵的“至少在20世纪中期以来,功能正确的系统软件的构建一直是计算的重大挑战之一,”美国国家科学基金会(NSF)项目主任Anindya Banerjee表示

CertiKOS部分通过其计算机远征计划“CertiKOS表明,通过机器可检查的数学证据构建经过验证的软件,另外提供证据是可行和实用的 - 它在功能上是正确的”在构建CertiKOS系统时,Shao和他的团队结合形式逻辑和新的,分层的演绎验证技术也就是说,它们仔细地解开内核的相互依赖的组件,将代码组织成大量的分层模块,并为每个内核模块的预期行为编写数学规范使用正式的演绎验证证明系统不同来自检查程序可靠性的传统方法,其中代码编写器针对众多场景测试程序“一个程序可以正确编写99% - 这就是为什么今天你没有看到明显的问题 - 但黑客仍然可以潜入一个特定的设置,程序将不会按预期运行,“Shao说”编写软件的人工作的所有好意,但不能考虑所有情况“CertiKOS验证的操作系统内核是一个关键组件国防高级研究机构(DARPA)高保障网络军事系统(HACMS)计划,用于构建可证明没有网络漏洞的网络物理系统“HACMS团队使用CertiKOS提供的虚拟化功能将受信任和不受信任的组件分开,“DARPA项目经理雷·理查兹说:”这是一项重要的能力,使我们能够有效地建立网络弹性系统在世界上网络安全是一个日益受到关注的问题,这种弹性是一个强大的属性,我们希望系统设计人员能够广泛采用这种属性“只有近几年才能实现像CertiKOS这样的系统,因为经过认证的内核的证明对任何人来说都太大了

检查在过去十年中开发了强大的计算机程序,称为证明助手,可以自动生成和检查大型正式证据 “这是惊人的进步,”康奈尔大学软件安全和计算与信息科学系主任Greg Morrisett说道

“十年前,没有人会预测我们可以证明单线程内核的正确性,中国和他的团队真正为我们其他人开辟了一条壮观的道路“美国国家科学基金会DeepSpec财团总监兼普林斯顿大学计算机科学教授安德鲁·阿佩尔称为CertiKOS,这是一个真正的突破,”并指出它可以作为从经过验证和不可靠的组件组合构建高度安全系统的基础“但同样重要的是,CertiKOS中使用的模块化分层验证方法不仅适用于操作系统,还适用于许多其他类型的软件,”Appel论文:CertiKOS:用于构建经认证的并发操作系统内核的可扩展体系结构来源:耶鲁大学William Weir