seL4（受形式化驗證的微核心）
/ ess-ee-ELL-four /
作業系統核心向來惡名昭彰地容易出臭蟲，偏偏它又是其他一切都絕對信任的那一個程式——一個核心臭蟲就能讓整台機器當機或被攻陷。seL4 以現有最強的保證來回應這點：它是第一個具有機器檢驗數學證明的通用作業系統核心，證明其 C 實作符合它的規格，且該規格能執行關鍵的安全性質。它刻意做得很小——幾千行——因為驗證只能擴展到小而經審慎設計的程式碼。
具體而言，seL4 是一個微核心，所以它把幾乎一切都留在核心之外：它提供一個極簡的核心——執行緒、定址空間、行程間通訊，以及以能力為基礎的存取控制——並把驅動程式、檔案系統與各種服務推到普通的使用者行程裡。在那個小核心之上坐著證明。驗證建立了一個精化（refinement）：C 程式碼能表現的每一個行為，都是抽象規格所允許的行為，所以實作不存在規格所禁止的行為。由此，更進一步的證明導出像完整性（核心絕不讓某執行緒修改它沒有能力可及的記憶體）與機密性等性質，甚至證明編譯器產出的二進位檔對應於那份已驗證的 C。seL4 中的權威只透過能力——不可偽造的權證——流動，所以「誰能做什麼」是明確且可證明的，而非環境式的。
它之所以重要，在於它是「一個真實、可用的作業系統核心能被形式化驗證」的存在性證明，並被部署在代價值得之處：航空電子、國防、車用，以及其他安全或保安關鍵的系統。但要記牢那些但書。這些保證只關乎核心本身、在所陳述的假設下——證明假設硬體照建模行事、不涵蓋時序或功耗旁路通道（除非另行處理），且對你在其上建構的使用者層軟體的正確性隻字未提。seL4 給你一個可信賴的地基；它並不使其上的系統變得正確，而「已驗證」是關於特定性質的精確主張，並非對完美的一概承諾。
seL4 核心（已驗證）：執行緒、定址空間、IPC、以能力為基礎的存取控制（約 1 萬行） 證明：C 實作精化規格；規格執行完整性 ＋ 機密性 使用者空間（不在此證明驗證範圍內）：驅動程式、檔案系統、你的應用程式 => 一個可信賴的核心，但其上的軟體仍可能是錯的
seL4 驗證的是一個微小、以能力為基礎的微核心；其上的一切——驅動程式、服務、你的應用程式——都在證明之外，必須另行信任或驗證。
seL4 的保證只涵蓋核心本身、在明確假設下（硬體照建模行事；除非另行證明，否則不對時序／功耗旁路通道作主張）。它不會讓其上的使用者層軟體變得正確。「已驗證」是關於一個小核心特定性質的精確陳述，並非整個系統毫無臭蟲的承諾。