[email protected]衷心感謝您的拜讀，希望我的分析對您有所幫助；另外，若您發現本文分析錯誤，或seL4版本更新特性變化，您可以發郵件告訴我，以便我能及時更新。考慮到關於資訊量較多，在閱讀過程中難免出現語義難明的詞彙，對於前文出現的所有非公共詞彙，後文均會明確其含義，請耐心閱讀。

seL4綜述——可能是一個以許可權控制為基礎的微核心

——————————seL4相關理念——————————

1. 由於seL4官方文件未區分Thread和Process，因此下文表述均採用執行緒

2. 關於許可權，seL4描述為能力，明確的抽象出3大基本元素：

Read、Write、Grant(許可權授予，即傳遞)。

#define seL4_ReadWrite seL4_CapRights_new(0, 1, 1)

#define seL4_AllRights seL4_CapRights_new(1, 1, 1)

#define seL4_CanRead   seL4_CapRights_new(0, 1, 0)

#define seL4_CanWrite  seL4_CapRights_new(0, 0, 1)

#define seL4_CanGrant  seL4_CapRights_new(1, 0, 0)

#define seL4_NoWrite   seL4_CapRights_new(1, 1, 0)

#define seL4_NoRead    seL4_CapRights_new(1, 0, 1)

#define seL4_NoRights  seL4_CapRights_new(0, 0, 0)

3. 顯式的許可權控制

seL4的許可權控制是顯式的，seL4的一切操作

(下文提到的seL4提供的基礎服務)

都要在CSpace存在相關許可權的情況下才能執行

4. 許可權：Grant

seL4的許可權以CNode為單位可被複制、轉移。

由於許可權的可複製即可產生子許可權，因此可以形成許可權樹。

CSpace即據此組織CNode，形成有向圖。

5. 執行緒的VSpace和CSpace

執行緒的建立會建立VSpace和CSpace，VSpace即虛擬地址空間；

CSpace為Capability Space，

為seL4核心的Capability全面控制提供基礎

6. 執行緒的IPC Buffer

存在於其他執行緒通訊、與核心通訊需要的執行緒，

在建立時即加入IPC Buffer，為後期IPC的基礎，

為設定IPC Buffer的執行緒不能對外通訊。

7. 記憶體管理

seL4僅可能分配出power(2,n)且大於16byte的記憶體

8. 一般平臺無關記憶體物件大小

n-bit Untyped物件power(2,n) bytes(n>=4)

n-bit CNode物件16*power(2,n) bytes(n>=2)

Endpoint物件16 bytes

Notification物件16 bytes

IRQ Control--

IRQ Handler--

9. 其他平臺相關物件

TCB物件——一般1KB/512bytes

頁表相關物件

ASID相關物件

——————————seL4詞彙解釋——————————

1. Capability——許可權的複合體，內容豐富

(可能是seL4最精華的理念，因為seL4的一切據此展開)。

每個執行緒不光有地址空間(VSpace)，

還有CapabilitySpace。

執行緒想要呼叫系統功能，將會通過呼叫

能力空間中的能力來實現系統功能

(如IPC會呼叫endpoint capability)

2. CNode(capability node)

Capability的基礎承載者，

建立時即確定擁有的slot數量(power of 2)，

slot用於儲存Capabilities，

所儲存的Capability為更深層的CNode時，即形成有向圖。

也由此，當父CNode的Capability被取消時，

其子將會遞迴取消此Capability。

3. TCB 一般執行緒控制塊

4. Endpoints

為執行緒間通訊提供支援(詳述見IPC)

5. Notification 一般訊號機制

poll

6. Untyped Memory 未型別記憶體

Untyepd記憶體可被Retype成seL4定義的一些記憶體物件。

7. CDT樹(capability derivation tree)

——追蹤源capability複製出的capability。

CDT雖是獨立的概念，但在實際實現是CNode物件的一部分

(其實現可能是CNode資料結構中)

seL4_Untyped_Retype()//大致是申請記憶體

seL4_CNode_Mint();//複製CNode(可能包含許可權降低)

seL4_CNode_Copy();//複製CNode

seL4_CNode_Mutate();//遷移CNode(可能包含許可權降低)

上述函式均生成子capability，均被CDT追蹤。

8. Slot——一段實體記憶體空間的實體。

——————————seL4基礎服務——————————

1. 執行緒(Threads)

上下文切換、處理器時間分片的基本單位。

1.1 每一個執行緒，都會有相應的CSpace(Capability Space)

和VSpace(Virtual Space)；

同時，執行緒還會有IPC buffer,

用於實現執行緒間通訊(詳述見1.3 IPC)。

1.2 每一個執行緒都有其歸屬的排程域

(此處排程域與linux中存在很大區別)。

核心在完成編譯時就確定了此核心中的排程域的個數，

核心將會定時、迴圈的排程各域。

排程域內可存在多個執行緒(無上限)，

當且僅當執行緒所在排程域正在排程中時，執行緒才可能被排程執行。

1.3 在排程域內，seL4採用256優先順序的搶佔式迴圈排程器。

2. 地址空間(Address space)

虛擬地址空間，由頁表完成地址翻譯。

由於ASID資源限制，seL4設計了一個ASID Pool,

通過ASID Control能力，執行緒VSpace與ASID Pool連結，

以及通過ASID Pool使用ASID。

3. 執行緒間通訊(IPC Inter-process communication)

seL4執行緒間通訊通過endpoint(我認為應該是某種端點的含義)進行，

訊息內容的第一段為tag段，

含有四部分：標誌，訊息長度，能力個數，開放能力的區域。

seL4在IPC通訊時，會盡可能多的使用CPU暫存器，

很多短內容的訊息會直接通過CPU暫存器完成傳遞。

seL4對IPC通訊的支援並不關心內容，

需要使用者層根據IPC訊息的tag、訊息所傳來的能力等獲得訊息全部。

(感覺類似socket？優化了的socket。)

其他細節還很多，在此僅給以簡述。

4. Notification

非阻塞的訊號機制(與linux類似)，比如對多路複用I/O的支援等。

5. Device primitive

seL4驅動是作為非特權程式執行在核心外，

核心通過IPC實現硬體終端的分發。

6. Capability Spaces(CSpace)

CSpace是一個執行緒下CNode組成的的有向圖的集合；

也就是執行緒所擁有的Capability的集合。

seL4以執行緒為單位擁有CSpace,

核心啟動第一個使用者執行緒時即為之建立CSpace，

此CSpace將包含所有其建立的CNode，

當然也就包含所有其子執行緒的CSpace。

CSpace含有CNodes，CNode中address可以找到slot，

slot中有(或無)capability；

當slot的Capability為另一個CNode，即可形成有向圖；

對每個執行緒，其CSpace都存在root CNode，可連通所有節點，

另：

執行緒發生系統呼叫，就會找到執行緒CSpace中,

關於這個系統呼叫Capability的address，

進而讀取到相應slot，slot內容決定此係統呼叫是否執行。

核心通過CNodes物件管理執行緒的CSpace；

(簡單說就是所有CNode都是連在一起的，有著共同的根，

根據父子程序，CSpace通過CNode產生逐級依賴)

——————————seL4建立執行緒——————————

1. seL4_Untyped_Retype()

Retype物件來建立執行緒的TCB

2. seL4_TCB_SetSpace()/seL4_TCB_Configer()

設定TCB的CSpace、VSpace和EndPoint等

3. seL4_TCB_WriteRegisters()

關於棧指標和指令指標的一些操作

4. seL4_TCB_Resume()

啟用執行緒，執行緒將會加入其父所在CPU排程

5. 至此，執行緒將會被執行

6. seL4_TCB_SetAffinity()

在多核平臺，可設定此執行緒的執行CPU

——————————seL4一些特點——————————

1.快取溢位免疫(基於嚴苛的capability設計)

Buffer overflows are a classic security attack against operating systems, trying to make the software crash or even to inject malicious code into the cycle. We have proved that no such attack can be successful on seL4.

2.訪問空指標免疫(原理未知)

Null pointer dereferences are another common issue in the C programming language. In applications they tend to lead to strange error messages and lost data. In operating systems they will usually crash the whole system. They do not occur in seL4.

3.C中指標指錯資料型別免疫(原理未知)

In C it is possible to accidentally use a pointer to the wrong type of data. This is a common programming error. It does not happen in the seL4 kernel.

4.記憶體洩漏免疫(基於嚴苛的capability設計)

Memory leaks occur when memory is requested, but never given back. The other direction is even worse: memory could be given back, even though it is still in use. Neither of these can happen in seL4.

5.算術溢位/異常免疫(原理未知)

Humans and mathematics usually have a concept of numbers that can be arbitrarily big. Machines do not, they need to fit them into memory, usually into 32 or 64 bits worth of storage. Machines also generate exceptions when you attempt to do things that are undefined like dividing by zero. In the OS, such exceptions would typically crash the machine. This does not occur in seL4.

6.未定義行為免疫(原理未知)

There are many static analysis and verification tools that check for the absence of undefined behaviour in C. Our proof explicitly checks that no such undefined behaviour occurs.

——————————seL4總結————————————

1. seL4核心層面的顯式許可權控制可以提供很高的安全保障，如DDOS不再有效。

2. seL4提供的記憶體管理類類似於夥伴系統，能夠有效減少記憶體碎片的產生,同樣，不靈活的記憶體管理模式應該難以對記憶體充分利用。

3. seL4的IPC基於Endpoint，受制於Capability，短訊息由於採用CPU暫存器傳遞，效率不會明顯下降，但長訊息機制依賴於IPC Buffer的複製，效率不高。

4. seL4的排程域根本隔離，帶來的安全保障我並未想到，但排程域的靜態設定應該會帶來域內執行緒對使用者響應的延遲，造成使用者操作卡頓。

因此，基於上述分析， 

seL4的形式驗證是一大亮點，

其顯式的許可權管理也可以帶來安全，

但seL4還很年輕，社群活躍度不是非常高；

seL4的應用開發框架基於C語言，必須採用介面-實體開發模式，

不支援變長引數函式、函式指標等，因此程式碼移植可能存在難度。

基礎設施建設不完善，基於其設計思想的工業應用很少，

若要真正投入使用，需要詳盡分析其核心細節，

詳細分析其可能存在的缺陷、困難再考慮是否應用。

seL4後續

1.seL4中斷通過Notification分發

中斷觸發後，核心signal特定Notification，

執行緒會seL4_Wait()/seL4_Poll()這個notification

使用者態用

seL4_IRQHandler_SetNotification()

之後執行緒開始seL4_Wait()/seL4_Poll()這個notification

中斷到達，執行緒處理完後

seL4 IRQHandler Ack()提示核心處理完，核心可以發進一步的資料或後續中斷

seL4_IRQHandler_Clear()接觸這個Notification的註冊

seL4沒在主線中支援DMA

但對於x86

seL4支援了IOMMU

也是作為一種能力

seL4使用musl libc

seL4可能會有檔案系統(同濟裴喜龍)

seL4用的是gcc -O1，

有形式驗證過的編譯器CompCert

Norman Feske是搞Genode的，

Genode是微核心之上的系統框架，

這個系統框架類似linux的rootfs，

Norman Feske把Genode移植到seL4了。