seL4 核心服務、對象以及基本能力通路和控制

核心服務和對象

微核心提供了一些有限的原始服務，更多複雜的服務要在這些原始服務基礎上像應用程式一樣實作。以此種服務，此系統的功能可以被拓展而不用增加特權模式下的代碼和複雜度，雖然在應用程式域潛在的支援相當廣泛的服務。

seL4 核心基本支援的服務如下：

線程（Threads ）是CPU支援應用程式運作的抽象化。

位址空間（Address spaces）是一塊包含一個應用程式的虛拟記憶體空間，應用程式隻能使用他們自己位址空間下的記憶體。

程序間互動（Inter-process communication{IPC}）允許線程通過終端節點使用消息傳遞進行交流。

原始裝置（device primitive）允許裝置驅動像無特權應用程式一樣實作。此核心輸出硬體裝置終端通過{IPC}《IPC 不知道的查！！！！》消息。

能力空間（capability space）存儲着伴随他們的記錄資訊的核心服務的能力（即。。使用權利）

這一部分給了這些服務的概述，描述了核心對象如何被使用者空間的應用程式所使用，以及描述了新對象如何被建立。

2.1 基本能力通路控制

seL4微核心提供了基本能力通路控制模型，通路控制管理核心的所有服務，為了執行一個操作，一個應用程式必須調用一個他所占有的能力，已經擁有足夠的通路權限去請求服務。用這個，這個系統能夠在隔離軟體元件的條件下初始化，也能夠被授權，通過選擇性的給與特定的通信能力來控制元件間的通信。這使得軟體組建的隔離得到了高度的保證，因為隻有這些操作明确授權被能力占有所承認。

一個能力是一個不能僞造的令牌，參考一個特定的核心對象（如線程控制塊《TCB》），和存儲着控制調用什麼方法的通路權限。從概念上講，一個能力存儲在一個應用程式的能力空間裡。這個空間裡的一個位址指向一個槽（slot）可能也可能不包含一個能力，一個應用程式可能指向一個能力，去請求一個核心服務，比如使用這個槽（slot）的位址去支援能力。這意味着，seL4 微核心能力模型是一個（種族隔離？？？segregated）的執行個體(或者分區)能力模型，能力被内和管理的地方。

能力空間被實作如一個核心管理的能力節點的有向圖。（CNodes），一個能力節點是一個槽的表，一個每個槽都進一步包含能力節點的能力的地方。一個在能力空間的位址然後連接配接能力節點能力形成目标位置的路徑。我們詳細讨論能力節點對象在第三部分。

能力在能力空間中能夠被複制和移動，也能夠被發送通過程序間通信（IPC），這允許帶着特定通路權限的應用程式的建立，給其他應用程式授權，傳遞給一個應用程式權限去新建立（或選擇）核心服務。此外，能力可以鑄造建立派生能力用原始能力的權限的一個子集（從不用更多的權限）。一個新的創造的能力能夠被使用于部分授權。

能力也能夠被撤銷收回權力，撤銷遞歸删除任何能力，已經派生了原始能力.此系統的能力的傳播被一個take-grant（取-予）基本模型所控制。