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

seL4綜述——可能是一個以權(quán)限控制為基礎(chǔ)的微內(nèi)核

——————————seL4相關(guān)理念——————————

1. 由于seL4官方文檔未區(qū)分Thread和Process，因此下文表述均采用線程

2. 關(guān)于權(quán)限，seL4描述為能力，明確的抽象出3大基本元素：

Read、Write、Grant(權(quán)限授予，即傳遞)。

#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. 顯式的權(quán)限控制

seL4的權(quán)限控制是顯式的，seL4的一切操作

(下文提到的seL4提供的基礎(chǔ)服務(wù))

都要在CSpace存在相關(guān)權(quán)限的情況下才能執(zhí)行

?

4. 權(quán)限：Grant

seL4的權(quán)限以CNode為單位可被復(fù)制、轉(zhuǎn)移。

由于權(quán)限的可復(fù)制即可產(chǎn)生子權(quán)限，因此可以形成權(quán)限樹。

CSpace即據(jù)此組織CNode，形成有向圖。

?

5. 線程的VSpace和CSpace

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

CSpace為Capability Space，

為seL4內(nèi)核的Capability全面控制提供基礎(chǔ)

6. 線程的IPC Buffer

存在于其他線程通訊、與內(nèi)核通訊需要的線程，

在創(chuàng)建時即加入IPC Buffer，為后期IPC的基礎(chǔ)，

為設(shè)置IPC Buffer的線程不能對外通訊。

?

7. 內(nèi)存管理

seL4僅可能分配出power(2,n)且大于16byte的內(nèi)存

?

8. 一般平臺無關(guān)內(nèi)存對象大小

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. 其他平臺相關(guān)對象

TCB對象——一般1KB/512bytes

頁表相關(guān)對象

ASID相關(guān)對象

——————————seL4詞匯解釋——————————

?

1. Capability——權(quán)限的復(fù)合體，內(nèi)容豐富

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

每個線程不光有地址空間(VSpace)，

還有CapabilitySpace。

?

線程想要調(diào)用系統(tǒng)功能，將會通過調(diào)用

能力空間中的能力來實現(xiàn)系統(tǒng)功能

(如IPC會調(diào)用endpoint capability)

?

2. CNode(capability node)

Capability的基礎(chǔ)承載者，

創(chuàng)建時即確定擁有的slot數(shù)量(power of 2)，

slot用于保存Capabilities，

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

也由此，當(dāng)父CNode的Capability被取消時，

其子將會遞歸取消此Capability。

?

3. TCB 一般線程控制塊

?

4. Endpoints

為線程間通訊提供支持(詳述見IPC)

?

5. Notification 一般信號機(jī)制

poll

?

6. Untyped Memory 未類型內(nèi)存

Untyepd內(nèi)存可被Retype成seL4定義的一些內(nèi)存對象。

?

7. CDT樹(capability derivation tree)

——追蹤源capability復(fù)制出的capability。

?

CDT雖是獨立的概念，但在實際實現(xiàn)是CNode對象的一部分

(其實現(xiàn)可能是CNode數(shù)據(jù)結(jié)構(gòu)中)

seL4_Untyped_Retype()//大致是申請內(nèi)存

seL4_CNode_Mint();//復(fù)制CNode(可能包含權(quán)限降低)

seL4_CNode_Copy();//復(fù)制CNode

seL4_CNode_Mutate();//遷移CNode(可能包含權(quán)限降低)

上述函數(shù)均生成子capability，均被CDT追蹤。

8. Slot——一段物理內(nèi)存空間的實體。

?

——————————seL4基礎(chǔ)服務(wù)——————————

1. 線程(Threads)

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

1.1 每一個線程，都會有相應(yīng)的CSpace(Capability Space)

和VSpace(Virtual Space)；

同時，線程還會有IPC buffer,

用于實現(xiàn)線程間通訊(詳述見1.3 IPC)。

1.2 每一個線程都有其歸屬的調(diào)度域

(此處調(diào)度域與linux中存在很大區(qū)別)。

內(nèi)核在完成編譯時就確定了此內(nèi)核中的調(diào)度域的個數(shù)，

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

調(diào)度域內(nèi)可存在多個線程(無上限)，

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

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

?

2. 地址空間(Address space)

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

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

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

以及通過ASID Pool使用ASID。

?

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

seL4線程間通訊通過endpoint(我認(rèn)為應(yīng)該是某種端點的含義)進(jìn)行，

消息內(nèi)容的第一段為tag段，

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

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

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

seL4對IPC通訊的支持并不關(guān)心內(nèi)容，

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

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

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

?

4. Notification

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

?

5. Device primitive

seL4驅(qū)動是作為非特權(quán)程序執(zhí)行在內(nèi)核外，

內(nèi)核通過IPC實現(xiàn)硬件終端的分發(fā)。

?

6. Capability Spaces(CSpace)

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

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

?

seL4以線程為單位擁有CSpace,

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

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

當(dāng)然也就包含所有其子線程的CSpace。

?

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

slot中有(或無)capability；

當(dāng)slot的Capability為另一個CNode，即可形成有向圖；

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

?

另：

線程發(fā)生系統(tǒng)調(diào)用，就會找到線程CSpace中,

關(guān)于這個系統(tǒng)調(diào)用Capability的address，

進(jìn)而讀取到相應(yīng)slot，slot內(nèi)容決定此系統(tǒng)調(diào)用是否執(zhí)行。

?

內(nèi)核通過CNodes對象管理線程的CSpace；

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

根據(jù)父子進(jìn)程，CSpace通過CNode產(chǎn)生逐級依賴)

?

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

?

1. seL4_Untyped_Retype()

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

?

2. seL4_TCB_SetSpace()/seL4_TCB_Configer()

設(shè)置TCB的CSpace、VSpace和EndPoint等

?

3. seL4_TCB_WriteRegisters()

關(guān)于棧指針和指令指針的一些操作

?

4. seL4_TCB_Resume()

激活線程，線程將會加入其父所在CPU調(diào)度

?

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

?

6. seL4_TCB_SetAffinity()

在多核平臺，可設(shè)置此線程的執(zhí)行CPU

?

?

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

?

1.緩存溢出免疫(基于嚴(yán)苛的capability設(shè)計)

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中指針指錯數(shù)據(jù)類型免疫(原理未知)

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.內(nèi)存泄漏免疫(基于嚴(yán)苛的capability設(shè)計)

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.算術(shù)溢出/異常免疫(原理未知)

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總結(jié)————————————

1. seL4內(nèi)核層面的顯式權(quán)限控制可以提供很高的安全保障，如DDOS不再有效。

?

2. seL4提供的內(nèi)存管理類類似于伙伴系統(tǒng)，能夠有效減少內(nèi)存碎片的產(chǎn)生,同樣，不靈活的內(nèi)存管理模式應(yīng)該難以對內(nèi)存充分利用。

?

3. seL4的IPC基于Endpoint，受制于Capability，短消息由于采用CPU寄存器傳遞，效率不會明顯下降，但長消息機(jī)制依賴于IPC Buffer的復(fù)制，效率不高。

?

4. seL4的調(diào)度域根本隔離，帶來的安全保障我并未想到，但調(diào)度域的靜態(tài)設(shè)置應(yīng)該會帶來域內(nèi)線程對用戶響應(yīng)的延遲，造成用戶操作卡頓。

?

因此，基于上述分析，?

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

其顯式的權(quán)限管理也可以帶來安全，

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

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

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

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

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

詳細(xì)分析其可能存在的缺陷、困難再考慮是否應(yīng)用。

?

?

seL4后續(xù)

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

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

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

?

用戶態(tài)用

seL4_IRQHandler_SetNotification()

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

?

中斷到達(dá)，線程處理完后

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

?

seL4_IRQHandler_Clear()接觸這個Notification的注冊

?

seL4沒在主線中支持DMA

但對于x86

seL4支持了IOMMU

?

也是作為一種能力

?

seL4使用musl libc

seL4可能會有文件系統(tǒng)(同濟(jì)裴喜龍)

seL4用的是gcc -O1，

有形式驗證過的編譯器CompCert

?

Norman Feske是搞Genode的，

Genode是微內(nèi)核之上的系統(tǒng)框架，

這個系統(tǒng)框架類似linux的rootfs，

Norman Feske把Genode移植到seL4了。

?

寫于2018.10

總結(jié)

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

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