微內(nèi)核

越大的系統(tǒng)潛在的bug就越多，所以微內(nèi)核在減少bug方面很有優(yōu)勢(shì)，seL4是世界上最小的內(nèi)核之一。但是seL4的性能可以與當(dāng)今性能最好的微內(nèi)核相比。
作為微內(nèi)核，seL4為應(yīng)用程序提供少量的服務(wù)，如創(chuàng)建和管理虛擬內(nèi)存地址空間的抽象，線程和進(jìn)程間通信IPC。這么少的服務(wù)靠8700行C代碼搞定。seL4是高性能的L4微內(nèi)核家族的新產(chǎn)物，它具有操作系統(tǒng)所必需的服務(wù)，如線程，IPC，虛擬內(nèi)存，中斷等。

形式驗(yàn)證

除了微內(nèi)核，seL4另一大特色是完全的形式驗(yàn)證。

seL4的實(shí)現(xiàn)總是嚴(yán)格滿足上一抽象層內(nèi)核行為的規(guī)約，它在任何情況下都不會(huì)崩潰以及執(zhí)行不安全的操作，甚至可以精確的推斷出seL4 在所有情況下的行為，這是了不起的。
研究發(fā)現(xiàn)常用的攻擊方法對(duì)seL4無(wú)效，如惡意程序經(jīng)常采用的緩存溢出漏洞。
使用面向過(guò)程語(yǔ)言Haskell實(shí)現(xiàn)了一個(gè)內(nèi)核原型，用它來(lái)參與形式驗(yàn)證，最后根據(jù)它，用C語(yǔ)言重新實(shí)現(xiàn)內(nèi)核，作為最終內(nèi)核。 順便提一句，seL4有兩只team，kernel team和verification team，而連接這兩個(gè)team的是 Haskell prototype。

在用C開(kāi)發(fā)內(nèi)核的過(guò)程中，seL4對(duì)使用C進(jìn)行了如下限制：
1. 棧變量不得取引用，必要時(shí)以全局變量代替
2. 禁止函數(shù)指針
3. 不支持union

對(duì)seL4的formal verification（形式驗(yàn)證）分為兩步：abstract specification（抽象規(guī)范）和executable specification（可執(zhí)行規(guī)范）之間，executable specification和implementation（實(shí)現(xiàn)）之間。有兩個(gè)廣泛的方法來(lái)進(jìn)行formal verification： model checking（全自動(dòng)）和交互式數(shù)學(xué)證明（interactive mathematical proof ），后者需要手工操作。seL4驗(yàn)證使用的形式數(shù)學(xué)證明來(lái)自Isabelle/HOL，屬于后者。

具體來(lái)說(shuō)seL4的形式驗(yàn)證步驟：
1. 寫(xiě)出IPC、syscall、調(diào)度等所有微內(nèi)核對(duì)象（kernel object）的abstract specification（in Isabelle）
2. 寫(xiě)出如上對(duì)象的executable specification（in Haskell），并證明其正確實(shí)現(xiàn)了第一步的abstract specification，利用狀態(tài)機(jī)的原理，abstract specification的每一步狀態(tài)轉(zhuǎn)換，executable specification都產(chǎn)生唯一對(duì)應(yīng)的狀態(tài)轉(zhuǎn)換。
3. 寫(xiě)C實(shí)現(xiàn)。通過(guò)一個(gè)SML寫(xiě)的C-Isabelle轉(zhuǎn)換器，和Haskabelle聯(lián)合形式證明C代碼和第二步的Haskell定義語(yǔ)義一致。

seL4的實(shí)現(xiàn)被證明是bug-free（沒(méi)有bug）的，比如不會(huì)出現(xiàn)緩沖區(qū)溢出，空指針異常等。還有一點(diǎn)就是，C代碼要轉(zhuǎn)換成能直接在硬件上運(yùn)行的二進(jìn)制代碼，seL4可以確保這個(gè)轉(zhuǎn)換過(guò)程不出現(xiàn)錯(cuò)誤，可靠。seL4是世界上第一個(gè)（到目前也是唯一一個(gè)）從很強(qiáng)程度上被證明是安全的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的硬實(shí)時(shí)性很強(qiáng)。
實(shí)際上OS的verification（驗(yàn)證）早在40年前就開(kāi)始了，而seL4是振奮人心的，一是它擁有很強(qiáng)的屬性（properties）：功能正確性（functional correctness），完整性（integrity）和機(jī)密性（confidentiality），二是這些屬性已經(jīng)被形式驗(yàn)證到代碼級(jí)別，先是C，現(xiàn)在又到了二進(jìn)制。相比于之前人們對(duì)于OS的驗(yàn)證，seL4做得更徹底，但正是借助前人的工作，seL4才能如此優(yōu)秀。

---

內(nèi)核細(xì)節(jié)

seL4的API調(diào)用分兩步：第一，checking，驗(yàn)證參數(shù)，然后確定是否授權(quán)執(zhí)行這個(gè)調(diào)用; 第二，execute，執(zhí)行調(diào)用，永不失敗。
The combined checking phases of all kernel calls are a substantial fraction of the kernel. 看來(lái)對(duì)內(nèi)核調(diào)用的檢查是很重要的部分。

接下來(lái)來(lái)了解一下kernel objects：

CNodes 用于存放capabilities，給線程權(quán)限去調(diào)用某個(gè)對(duì)象上的方法

Thread Control Blocks 表示線程的執(zhí)行

IPC Endpoints 促進(jìn)線程間的通信

Virtual Address Space Objects 為一個(gè)或多個(gè)線程創(chuàng)建虛擬地址空間

Interrupt Objects 讓?xiě)?yīng)用程序可以接收和確認(rèn)來(lái)自硬件設(shè)備的中斷

Untyped Memory 它是seL4內(nèi)存分配的基石

我們?nèi)チ私庖粋€(gè)OS，它的內(nèi)存管理是必不可少的。內(nèi)存分配模塊可以被單獨(dú)驗(yàn)證。在重新使用一塊內(nèi)存之前，所有對(duì)這個(gè)內(nèi)存的引用必須要無(wú)效。seL4不動(dòng)態(tài)為內(nèi)核對(duì)象分配內(nèi)存，內(nèi)核對(duì)象要由應(yīng)用程序控制的內(nèi)存區(qū)域通過(guò)Untyped Memory來(lái)創(chuàng)建，這樣可以精確控制應(yīng)用程序使用的物理內(nèi)存，而且可以做到程序與程序之間物理內(nèi)存的isolation。
seL4是一個(gè)單內(nèi)核棧的操作系統(tǒng)，在啟動(dòng)時(shí)期，seL4會(huì)預(yù)先為內(nèi)核需要的內(nèi)存如代碼區(qū)，數(shù)據(jù)區(qū)和棧分配內(nèi)存。

seL4實(shí)現(xiàn)了一個(gè)capability-based的訪問(wèn)控制模型。每一個(gè)用戶空間的線程有一個(gè)相關(guān)聯(lián)的capability space (CSpace)，這個(gè)空間包含了這個(gè)線程處理的capabilities，也就是說(shuō)它管理著這個(gè)線程訪問(wèn)的資源。

CNode有一些slot，每個(gè)slot需要16字節(jié)的物理內(nèi)存，它可以恰恰保存一個(gè)capability。同其他對(duì)象一樣，CNode必須要通過(guò)seL4 Untyped Retype()在合適數(shù)量的untyped memory上來(lái)創(chuàng)建。

seL4用TCB（thread control block）描述一個(gè)線程，每一個(gè)TCB對(duì)一個(gè)CSpace和VSpace（它們可與其他線程共享），一個(gè)TCB一般有一個(gè)IPC buffer。

seL4提供了消息傳遞機(jī)制用于線程間的通信。

seL4采用256個(gè)優(yōu)先級(jí)的搶占式輪轉(zhuǎn)調(diào)度機(jī)制，當(dāng)一個(gè)線程創(chuàng)建或修改了另一個(gè)線程，它只能將另一線程的優(yōu)先級(jí)設(shè)為比它低或跟它一樣，線程優(yōu)先級(jí)用函數(shù)seL4 TCB Configure() 和 seL4 TCB SetPriority() 來(lái)設(shè)置。

總結(jié)

以上是生活随笔為你收集整理的开源微内核seL4的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。