[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了。
寫于2018.10