seL4 开放微内核项目获得了 ACM 软件系统奖，这是计算机系统领域最受尊敬的国际组织计算机协会 (ACM) 颁发的年度奖项。 该奖项授予在数学操作证明领域取得的成就，这表明完全符合以正式语言给出的规范，并认可在关键任务应用程序中使用的准备情况。 seL4 项目表明，不仅可以在工业操作系统级别完全形式化地验证项目的可靠性和安全性，而且可以在不牺牲性能和通用性的情况下实现这一点。
ACM 软件系统奖每年颁发一次，以表彰对行业产生决定性影响、引入新概念或开辟新商业应用的软件系统的开发。 奖励金额为35万美元。 在过去的几年里，ACM 奖项授予了 GCC 和 LLVM 项目，以及它们的创始人 Richard Stallman 和 Chris Latner。 其他获奖的项目和技术还有 UNIX、Java、Apache、Mosaic、WWW、Smalltalk、PostScript、TeX、Tcl/Tk、RPC、Make、DNS、AFS、Eiffel、VMware、Wireshark、Jupyter Notebooks、Berkeley DB 和 eclipse .
seL4 微内核的体系结构以删除在用户空间中管理内核资源的部分以及对此类资源应用与用户资源相同的访问控制方式而著称。 微内核不提供用于管理文件、进程、网络连接等的开箱即用的高级抽象，相反，它仅提供用于控制对物理地址空间、中断和处理器资源的访问的最小机制。 用于与硬件交互的高级抽象和驱动程序以用户级任务的形式在微内核之上单独实现。 这些任务对微内核可用资源的访问是通过规则的定义来组织的。
来源： opennet.ru