seL4 微内核获得 2022 ACM 软件系统奖

美国计算机协会 (ACM) 宣布将 2022 年 ACM 软件系统奖项授予 seL4 微内核团队，以表彰他们开发了第一个具有工业强度的高性能操作系统；该系统目前已通过完整的、机械检查的全功能正确性证明。

“2009 年，软件系统获奖者展示了 seL4 微内核，它成为有史以来第一个具有工业强度的通用操作系统，并正式证明了实现的正确性。在随后的几年中，该团队进一步补充证明了 seL4 强制执行完整性和机密性的核心安全属性，将证明扩展到内核的二进制代码，并对一个 protected mode OS 进行了首次健全和完整的最坏情况下的执行时间分析。

seL4 高可靠微内核从根本上改变了研究界对形式化方法所能完成的认识：它表明不仅可以为工业级操作系统完成正确性和安全性的形式化证明，而且可以在不影响性能或通用性的情况下完成。seL4 上持续维护和增长的证明帮助产生了证明工程的新学科 —— 证明过程建模、工作量估算和大规模证明的系统处理的艺术。”

团队成员包括 Gernot Heiser（新南威尔士大学）、Gerwin Klein（Proofcraft）、Harvey Tuch（谷歌）、Kevin Elphinstone（新南威尔士大学）、June Andronick（Proofcraft）、David Cock（苏黎世联邦理工学院）、Philip Derrin (高通)、Dhammika Elkaduwe (佩拉德尼亚大学)、Kai Engelhardt、Toby Murray（墨尔本大学）、Rafal Kolanski（Proofcraft）、Michael Norrish（澳大利亚国立大学）、Thomas Sewell（剑桥大学）和 Simon Winwood（Galois）。

ACM 软件系统奖旨在表彰具有持久影响力的软件系统的开发，这些影响体现在对概念的贡献、商业接受度或两者兼而有之。软件系统奖的奖金为 35,000 美元。软件系统奖的财务支持由 IBM 提供。

seL4 是世界上第一个通过数学方法被证明安全的操作系统内核，并且在安全的基础上还强调高性能，是世界上最快、最先进的 OS 微内核。它对于嵌入式计算系统的安全可信赖方面将会有极大意义，具体来看可能影响到航空电子、自动驾驶汽车、医疗设备、关键基础设施与国防等行业。理论上，seL4 可以用作 Linux 和其它类 Unix 操作系统的底层基础，甚至此前曾被考虑用于 GNU/Linux “真内核” GNU Hurd。