?ab12696@qq.com衷心感謝您的拜讀，希望我的分析對您有所幫助；另外，若您發(fā)現本文分析錯誤，或seL4版本更新特性變化，您可以發(fā)郵件告訴我，以便我能及時更新。考慮到關于信息量較多，在閱讀過程中難免出現語義難明的詞匯，對于前文出現的所有非公共詞匯，后文均會明確其含義，請耐心閱讀。

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

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

1. 由于seL4官方文檔未區(qū)分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存在相關權限的情況下才能執(zhí)行

?

4. 權限：Grant

seL4的權限以CNode為單位可被復制、轉移。

由于權限的可復制即可產生子權限，因此可以形成權限樹。

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

?

5. 線程的VSpace和CSpace

線程的創(chuàng)建會建立VSpace和CSpace，VSpace即虛擬地址空間；

CSpace為Capability Space，

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

6. 線程的IPC Buffer

存在于其他線程通訊、與內核通訊需要的線程，

在創(chuàng)建時即加入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的基礎承載者，

創(chuàng)建時即確定擁有的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中存在很大區(qū)別)。

內核在完成編譯時就確定了此內核中的調度域的個數，

內核將會定時、循環(huán)的調度各域。

調度域內可存在多個線程(無上限)，

當且僅當線程所在調度域正在調度中時，線程才可能被調度執(zhí)行。

1.3 在調度域內，seL4采用256優(yōu)先級的搶占式循環(huán)調度器。

?

2. 地址空間(Address space)

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

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

通過ASID Control能力，線程VSpace與ASID Pool鏈接，

以及通過ASID Pool使用ASID。

?

3. 線程間通訊(IPC Inter-process communication)

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

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

含有四部分：標志，消息長度，能力個數，開放能力的區(qū)域。

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

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

seL4對IPC通訊的支持并不關心內容，

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

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

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

?

4. Notification

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

?

5. Device primitive

seL4驅動是作為非特權程序執(zhí)行在內核外，

內核通過IPC實現硬件終端的分發(fā)。

?

6. Capability Spaces(CSpace)

CSpace是一個線程下CNode組成的的有向圖的集合；

也就是線程所擁有的Capability的集合。

?

seL4以線程為單位擁有CSpace,

內核啟動第一個用戶線程時即為之創(chuàng)建CSpace，

此CSpace將包含所有其創(chuàng)建的CNode，

當然也就包含所有其子線程的CSpace。

?

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

slot中有(或無)capability；

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

對每個線程，其CSpace都存在root CNode，可連通所有節(jié)點，

?

另：

線程發(fā)生系統調用，就會找到線程CSpace中,

關于這個系統調用Capability的address，

進而讀取到相應slot，slot內容決定此系統調用是否執(zhí)行。

?

內核通過CNodes對象管理線程的CSpace；

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

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

?

——————————seL4創(chuàng)建線程——————————

?

1. seL4_Untyped_Retype()

Retype對象來創(chuàng)建線程的TCB

?

2. seL4_TCB_SetSpace()/seL4_TCB_Configer()

設置TCB的CSpace、VSpace和EndPoint等

?

3. seL4_TCB_WriteRegisters()

關于棧指針和指令指針的一些操作

?

4. seL4_TCB_Resume()

激活線程，線程將會加入其父所在CPU調度

?

5. 至此，線程將會被執(zhí)行

?

6. seL4_TCB_SetAffinity()

在多核平臺，可設置此線程的執(zhí)行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的調度域根本隔離，帶來的安全保障我并未想到，但調度域的靜態(tài)設置應該會帶來域內線程對用戶響應的延遲，造成用戶操作卡頓。

?

因此，基于上述分析，?

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

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

但seL4還很年輕，社區(qū)活躍度不是非常高；

seL4的應用開發(fā)框架基于C語言，必須采用接口-實體開發(fā)模式，

不支持變長參數函數、函數指針等，因此代碼移植可能存在難度。

基礎設施建設不完善，基于其設計思想的工業(yè)應用很少，

若要真正投入使用，需要詳盡分析其內核細節(jié)，

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

?

?

seL4后續(xù)

1.seL4中斷通過Notification分發(fā)

中斷觸發(fā)后，內核signal特定Notification，

線程會seL4_Wait()/seL4_Poll()這個notification

?

用戶態(tài)用

seL4_IRQHandler_SetNotification()

之后線程開始seL4_Wait()/seL4_Poll()這個notification

?

中斷到達，線程處理完后

seL4 IRQHandler Ack()提示內核處理完，內核可以發(fā)進一步的數據或后續(xù)中斷

?

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

總結

以上是生活随笔為你收集整理的seL4微内核操作系统初期总结 2018.10的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。