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