seL4 微内核获得 2022 ACM 软件系统奖
美国计算机协会 (ACM) 宣布将 2022 年ACM 软件系统奖项授予 seL4 微内核团队,以表彰他们开发了第一个具有工业强度的高性能操作系统;该系统目前已通过完整的、机械检查的全功能正确性证明。 “2009 年,软件系统获奖者展示了 seL4 微内核,它成为有史以来第一个具有工业强度的通用操作系统,并正式证明了实现的正确性。在随后的几年中,该团队进一步补充证明了 seL4 强制执行完整性和机密性的核心安全属性,将证明扩展到内核的二进制代码,并对一个 protected mode OS 进行了首次健全和完整的最坏情况下的执行时间分析。 seL4 高可靠微内核从根本上改变了研究界对形式化方法所能完成的认识:它表明不仅可以为工业级操作系统完成正确性和安全性的形式化证明,而且可以在不影响性能或通用性的情况下完成。seL4 上持续维护和增长的证明帮助产生了证明工程的新学科 —— 证明过程建模、工作量估算和大规模证明的系统处理的艺术。” 团队成员包括 Gernot Heiser(新南威尔士大学)、Gerwin Klein(Proofcraft)、Harvey Tuch(谷歌)、Kevin E...
