微內核
越大的系統潛在的bug就越多，所以微內核在減少bug方面很有優勢，seL4是世界上最小的內核之一。但是seL4的性能可以與當今性能最好的微內核相比。
作為微內核，seL4為應用程序提供少量的服務，如創建和管理虛擬內存地址空間的抽象，線程和進程間通信IPC。這麼少的服務靠8700行C代碼搞定。seL4是高性能的L4微內核家族的新產物，它具有操作系統所必需的服務，如線程，IPC，虛擬內存，中斷等。
形式驗證
除了微內核，seL4另一大特色是完全的形式驗證。
seL4的實現總是嚴格滿足上一抽象層內核行為的規約，它在任何情況下都不會崩潰以及執行不安全的操作，甚至可以精確的推斷出seL4 在所有情況下的行為，這是了不起的。
研究發現常用的攻擊方法對seL4無效，如惡意程序經常采用的緩存溢出漏洞。
使用面向過程語言Haskell實現了一個內核原型，用它來參與形式驗證，最後根據它，用C語言重新實現內核，作為最終內核。 順便提一句，seL4有兩只team，kernel team和verification team，而連接這兩個team的是 Haskell prototype。
在用C開發內核的過程中，seL4對使用C進行了如下限制：
1. 棧變量不得取引用，必要時以全局變量代替
2. 禁止函數指針
3. 不支持union
對seL4的formal verification（形式驗證）分為兩步：abstract specification（抽象規范）和executable specification（可執行規范）之間，executable specification和implementation（實現）之間。有兩個廣泛的方法來進行formal verification： model checking（全自動）和交互式數學證明（interactive mathematical proof ），後者需要手工操作。seL4驗證使用的形式數學證明來自Isabelle/HOL，屬於後者。
具體來說seL4的形式驗證步驟：
1. 寫出IPC、syscall、調度等所有微內核對象（kernel object）的abstract specification（in Isabelle）
2. 寫出如上對象的executable specification（in Haskell），並證明其正確實現了第一步的abstract specification，利用狀態機的原理，abstract specification的每一步狀態轉換，executable specification都產生唯一對應的狀態轉換。
3. 寫C實現。通過一個SML寫的C-Isabelle轉換器，和Haskabelle聯合形式證明C代碼和第二步的Haskell定義語義一致。
seL4的實現被證明是bug-free（沒有bug）的，比如不會出現緩沖區溢出，空指針異常等。還有一點就是，C代碼要轉換成能直接在硬件上運行的二進制代碼，seL4可以確保這個轉換過程不出現錯誤，可靠。seL4是世界上第一個（到目前也是唯一一個）從很強程度上被證明是安全的OS。
seL4 is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees. 從這段英文可以看出，seL4的硬實時性很強。
實際上OS的verification（驗證）早在40年前就開始了，而seL4是振奮人心的，一是它擁有很強的屬性（properties）：功能正確性（functional correctness），完整性（integrity）和機密性（confidentiality），二是這些屬性已經被形式驗證到代碼級別，先是C，現在又到了二進制。相比於之前人們對於OS的驗證，seL4做得更徹底，但正是借助前人的工作，seL4才能如此優秀。
--------------------------------------------------------------------------------
內核細節
seL4的API調用分兩步：第一，checking，驗證參數，然後確定是否授權執行這個調用; 第二，execute，執行調用，永不失敗。
The combined checking phases of all kernel calls are a substantial fraction of the kernel. 看來對內核調用的檢查是很重要的部分。
接下來來了解一下kernel objects：
CNodes 用於存放capabilities，給線程權限去調用某個對象上的方法
Thread Control Blocks 表示線程的執行
IPC Endpoints 促進線程間的通信
Virtual Address Space Objects 為一個或多個線程創建虛擬地址空間
Interrupt Objects 讓應用程序可以接收和確認來自硬件設備的中斷
Untyped Memory 它是seL4內存分配的基石
我們去了解一個OS，它的內存管理是必不可少的。內存分配模塊可以被單獨驗證。在重新使用一塊內存之前，所有對這個內存的引用必須要無效。seL4不動態為內核對象分配內存，內核對象要由應用程序控制的內存區域通過Untyped Memory來創建，這樣可以精確控制應用程序使用的物理內存，而且可以做到程序與程序之間物理內存的isolation。
seL4是一個單內核棧的操作系統，在啟動時期，seL4會預先為內核需要的內存如代碼區，數據區和棧分配內存。
seL4實現了一個capability-based的訪問控制模型。每一個用戶空間的線程有一個相關聯的capability space (CSpace)，這個空間包含了這個線程處理的capabilities，也就是說它管理著這個線程訪問的資源。
CNode有一些slot，每個slot需要16字節的物理內存，它可以恰恰保存一個capability。同其他對象一樣，CNode必須要通過seL4 Untyped Retype()在合適數量的untyped memory上來創建。
seL4用TCB（thread control block）描述一個線程，每一個TCB對一個CSpace和VSpace（它們可與其他線程共享），一個TCB一般有一個IPC buffer。
seL4提供了消息傳遞機制用於線程間的通信。
seL4采用256個優先級的搶占式輪轉調度機制，當一個線程創建或修改了另一個線程，它只能將另一線程的優先級設為比它低或跟它一樣，線程優先級用函數seL4 TCB Configure() 和 seL4 TCB SetPriority() 來設置。
