微內核seL4 7.0.0版本發布，提供了另外一種基于CMake的構建系統，支持源碼樹外構建和交互式配置。該版本還支持獨立的ia32構建，并包含aarch64的詳細文檔。
seL4是一個高可靠性開源微內核，提供基于端到端驗證的強隔離保障。實際上，這是說seL4代碼庫是uestions#Does_seL4_have_zero_bugs.3F">無Bug的，當“驗證假設”滿足時，就發生指定的行為。正因如此，它已經被用于將運行在同一個處理器上的受信任組件和不受信任組件隔離。
seL4微內核由NICTA開發和維護，并通過了NICTA（現在是Data61的Trustworthy Systems Group）的正式驗證，目前歸General Dynamics C4 Systems（GDC4S）所有。2014年，“為了幫助每個人構建更可信賴（安全、無風險、可靠）的計算機系統”，NICTA和GDC4S決定開源seL4。
功能正確性初步驗證是在2009年通過L4.verified項目完成的。該項目表明，代碼正確地實現了正式的內核規范。后續對該內核的全面正式驗證證明，該規范既能提供期望的高級安全屬性，如“可用性、權限限制、完整性和保密性”，又能提供那些用于代碼及二進制級別轉譯的屬性。總的結果就是一個通用操作系統內核的首次端到端驗證。值得注意的是，10多年來，該驗證一直隨著內核的發展而變化，成為在這種規模下前所未有的驗證。
按照設計，雖然seL4內核有大量的驗證工作，但它仍然保持著很高的性能，實際上，它已經促進了性能優化的實現。當前，驗證提供的屬性和不變量用于獲悉內核的最壞情況執行時間（WCET），從而改進內核實現，進一步減少WCET。類似地，增加的“快速路徑（fastpath）”在可能的時候會自動提升進程間通信（IPC）速度。后來，該驗證經過了擴展，不管是否使用了快速路徑，都可以驗證內核行為是否符合規范。這項工作的結果就是一個速度、安全性、可靠性可證的內核，其應用領域包括國防、汽車、航空、醫療設備和工業自動化。
美國通過SBIR（小型企業創新研究）項目發放了超過230萬美元獎金，用于資助那些與seL4相關的國防項目。在其中一個這樣的項目中，SMACCM團隊使用seL4構建了具有“非法入侵高度復原性”的無人機（UVV）。該團隊使用seL4將運行非關鍵代碼的虛擬化Linux實例和運行在同一塊“任務板（mission board）”上的關鍵代碼隔離開。在紅隊設法非法入侵時，藍隊仍然能夠有效地操作基于seL4的系統。該系統最初開發時使用了一個普通的四軸飛行器，后來換成了由Boeing開發的“無人小鳥（ULB）”無人直升機。但是，seL4不限于國防承包商。由于支持Raspberry Pi 3，基于seL4開發安全、無風險、可靠的系統也在學生的研究范圍內。
雖然seL4在安全操作系統開發領域最先進，但按照定義，它是最小的，不是一個像Linux這樣的全功能操作系統，并沒有包含所有為了提供使用便利的東西，比如，支持各種設備及簡單的進程間通信。
開發和驗證工作的當前狀態來自經常更新的開發和驗證路線圖。常見問題的答案可以從項目的FAQ頁查看。
查看英文原文：seL4 Bug-Free Microkernel 7.0.0
京公網安備 11010502049343號