1.介紹

SEL4微內(nèi)核是一個(gè)操作系統(tǒng)內(nèi)核，被設(shè)計(jì)成在各種應(yīng)用領(lǐng)域中為系統(tǒng)提供安全、安全和可靠的基礎(chǔ)。
作為一個(gè)微內(nèi)核，它為應(yīng)用程序提供了少量的服務(wù)，例如創(chuàng)建和管理虛擬地址空間，線程的抽象，進(jìn)程間通信的抽象。
內(nèi)核的小尺寸也有助于對(duì)最壞情況下的執(zhí)行時(shí)間進(jìn)行完整而合理的分析。
本手冊(cè)從用戶的角度描述sel4內(nèi)核的API。
本文首先簡要概述了seL4微內(nèi)核設(shè)計(jì)，然后介紹了seL4內(nèi)核向用戶空間公開的高級(jí)API。

2.內(nèi)核服務(wù)和對(duì)象

微核提供了有限數(shù)量的服務(wù)原語，更多的復(fù)雜服務(wù)可以作為這些原語之上的應(yīng)用程序來實(shí)現(xiàn)。
這樣，在特權(quán)模式下，系統(tǒng)的功能可以在不增加代碼和復(fù)雜性的情況下進(jìn)行擴(kuò)展，同時(shí)仍然支持各種應(yīng)用程序域的大量服務(wù)。

sel4提供的基本服務(wù)如下：

1.線程是支持運(yùn)行軟件的CPU執(zhí)行的抽象

2.地址空間是每個(gè)包含應(yīng)用程序的虛擬內(nèi)存空間。應(yīng)用程序僅限于訪問地址空間中的內(nèi)存

3.進(jìn)程間通信是經(jīng)過端點(diǎn)允許線程進(jìn)行數(shù)據(jù)傳輸

4.通知提供了一種類似于二進(jìn)制信號(hào)量的非阻塞信號(hào)機(jī)制

5.設(shè)備原語將設(shè)備驅(qū)動(dòng)程序作為非特權(quán)應(yīng)用程序?qū)崿F(xiàn)。內(nèi)核通過IPC消息導(dǎo)出硬件設(shè)備中斷。

6.功能空間存儲(chǔ)內(nèi)核服務(wù)的功能(即訪問權(quán)限)及其簿記信息。（簿記信息是啥？）

本章概述了這些服務(wù)，描述了用戶空間應(yīng)用程序如何訪問內(nèi)核對(duì)象，以及如何創(chuàng)建新對(duì)象

2.1 基于能力的訪問控制

seL4微內(nèi)核提供了一個(gè)基于功能的訪問控制模型。

訪問控制管理所有內(nèi)核服務(wù)，為了執(zhí)行操作，應(yīng)用程序必須調(diào)用其擁有的對(duì)請(qǐng)求的服務(wù)具有足夠訪問權(quán)限的功能。

這樣，系統(tǒng)就可以被配置為相互隔離軟件組件，并且通過有選擇地授予特定的通信能力，在組件之間啟用授權(quán)的、受控的通信。
這使得軟件組件隔離具有高度的保證，因?yàn)橹挥心切┯赡芰φ加忻鞔_授權(quán)的操作才被允許。

一個(gè)功能是一個(gè)不可偽造的令牌，它引用一個(gè)特定的內(nèi)核對(duì)象（比如線程控制塊），并攜帶控制哪些方法可能被調(diào)用的訪問權(quán)限。

從概念上講，能力存在于應(yīng)用程序的能力空間中；這個(gè)空間中的地址指的是一個(gè)插槽，它可能包含也可能不包含能力。

應(yīng)用程序可以引用一個(gè)內(nèi)核服務(wù)的能力，例如使用擁有該能力的插槽的地址。
這意味著，seL4能力模型是隔離(或分區(qū))能力系統(tǒng)的實(shí)例，其中的能力由內(nèi)核管理。

能力空間被實(shí)現(xiàn)為一個(gè)由內(nèi)核管理的能力節(jié)點(diǎn)(cnode)組成的有向圖。CNode是一個(gè)槽位表，每個(gè)槽位可能包含更多的CNode功能。
能力空間中的能力地址是插槽索引與節(jié)點(diǎn)索引的串聯(lián)，形成到目標(biāo)插槽的路徑（這一點(diǎn)后續(xù)再看）

功能可以在功能空間內(nèi)復(fù)制和移動(dòng)，也可以通過ipc傳送。這個(gè)允許創(chuàng)建具有特定訪問權(quán)限的應(yīng)用程序，將權(quán)限委派給另一個(gè)應(yīng)用程序，并將應(yīng)用程序權(quán)限傳遞給新創(chuàng)建（或選定）的內(nèi)核服務(wù)。此外，還可以使用原始功能的一部分權(quán)限創(chuàng)建派生功能（決不能使用更多權(quán)限）。新創(chuàng)建的功能可用于部分授權(quán)。

還可以撤銷功能從而撤銷權(quán)限，撤銷將遞歸地刪除從被撤銷的原始功能派生出來的任何功能。功能在系統(tǒng)中的傳播由一個(gè)基于許可的模型控制。

2.2 系統(tǒng)調(diào)用

seL4內(nèi)核提供了一個(gè)消息傳遞服務(wù)，用于在線程。這個(gè)機(jī)制還用于與內(nèi)核提供的服務(wù)進(jìn)行通信。有一個(gè)標(biāo)準(zhǔn)的消息格式，每個(gè)消息包含一些數(shù)據(jù)字和一些可能的功能。第四章詳細(xì)描述了這些消息的結(jié)構(gòu)和編碼。

線程通過調(diào)用其功能空間中的功能來發(fā)送消息。當(dāng)以這種方式調(diào)用一個(gè)端點(diǎn)功能時(shí)，消息將通過內(nèi)核傳輸?shù)搅硪粋€(gè)線程。
當(dāng)調(diào)用內(nèi)核對(duì)象的功能時(shí)，消息將被解釋為以特定于內(nèi)核對(duì)象類型的方式進(jìn)行的方法調(diào)用。例如，使用格式正確的消息調(diào)用線程控制塊（TCB）功能將掛起目標(biāo)線程。

邏輯上，內(nèi)核提供三個(gè)系統(tǒng)調(diào)用:發(fā)送、接收和輸出。然而，也有一些基本的Send和Receive調(diào)用的組合和變體，例如Call操作，它由來自同一個(gè)對(duì)象的一個(gè)Send和一個(gè)Receive組成。

除了端點(diǎn)和通知之外，內(nèi)核對(duì)象上的方法都映射到發(fā)送或調(diào)用，這取決于方法是否返回結(jié)果。（端點(diǎn)，通知還有方法是什么？）
Yield系統(tǒng)調(diào)用不與任何內(nèi)核對(duì)象相關(guān)聯(lián)，并且是唯一不調(diào)用功能的操作。

完整的系統(tǒng)調(diào)用：
sel4_send：通過指定的功能和應(yīng)用程序傳遞消息以繼續(xù)。如果調(diào)用的功能是一個(gè)端點(diǎn)，并且沒有接收者準(zhǔn)備好立即接收消息，則發(fā)送線程將阻塞，直到消息可以被傳遞。
sel4_NBSend：在端點(diǎn)上執(zhí)行輪詢發(fā)送。它與sel4send（）類似，只是保證不會(huì)阻塞。如果消息不能立即傳遞，即沒有接收者在目標(biāo)點(diǎn)等待，則消息會(huì)自動(dòng)丟棄。
sel4_recv：由線程用于通過端點(diǎn)或通知接收消息。如果沒有發(fā)件人或通知處于掛起狀態(tài)，則調(diào)用者將阻塞，直到可以傳遞消息或通知為止。此系統(tǒng)調(diào)用僅適用于一個(gè)點(diǎn)或非通知功能，在嘗試使用其他功能類型時(shí)會(huì)引發(fā)錯(cuò)誤。
sel4_Call：該調(diào)用將阻塞發(fā)送方線程，直到其消息被傳遞并收到回復(fù)消息為止，當(dāng)sent消息被傳遞到另一個(gè)線程（通過endpoint）時(shí)，內(nèi)核向傳遞到接收方的消息添加了一個(gè)額外的“reply”功能，使接收方有權(quán)回復(fù)原始發(fā)送方。應(yīng)答能力存放在接收方的TCB中的一個(gè)專用插槽中，是一個(gè)單一的使用權(quán)，這意味著內(nèi)核一旦被調(diào)用就會(huì)使它失效。
sel_Reply：用于應(yīng)答sel_call的，并使用產(chǎn)生于sel_call系統(tǒng)調(diào)用的應(yīng)答功能，并存儲(chǔ)在回復(fù)線程的TCB中。
sel_ReplyRecv：是sel_reply和sel_recv的結(jié)合，它存在的主要原因是：通常情況下，響應(yīng)一個(gè)請(qǐng)求并等待下一個(gè)請(qǐng)求可以在單個(gè)內(nèi)核系統(tǒng)調(diào)用中執(zhí)行，而不是在兩個(gè)內(nèi)核系統(tǒng)調(diào)用中執(zhí)行。從應(yīng)答到接收階段的轉(zhuǎn)換也是原子的。
sel_NBRecv:線程使用它來檢查通知對(duì)象上掛起的信號(hào)或端點(diǎn)上掛起的消息，而不阻塞。此系統(tǒng)調(diào)用僅適用于端點(diǎn)和通知對(duì)象功能.
sel4_Yield:是唯一不需要使用某種功能的系統(tǒng)調(diào)用。它會(huì)喪失調(diào)用線程的時(shí)間片的剩余部分，并導(dǎo)致調(diào)用內(nèi)核的調(diào)度程序。如果沒有其他與調(diào)用者具有相同優(yōu)先級(jí)的可運(yùn)行線程，調(diào)用線程將立即使用新的時(shí)間片調(diào)度。

2.3 內(nèi)核對(duì)象

在本節(jié)中，我們簡要概述了內(nèi)核實(shí)現(xiàn)的對(duì)象類型，這些類型的實(shí)例（也稱為對(duì)象）可以由應(yīng)用程序調(diào)用。這些對(duì)象的接口構(gòu)成了內(nèi)核本身的接口。
內(nèi)核服務(wù)的創(chuàng)建和使用是通過創(chuàng)建，操作和組合這些內(nèi)核對(duì)象來實(shí)現(xiàn)的。

CNodes：存儲(chǔ)功能，允許線程調(diào)用特定對(duì)象上的方法，每個(gè)節(jié)點(diǎn)都有固定數(shù)量的插槽（slot），通常是2的冪，這取決于節(jié)點(diǎn)的創(chuàng)建時(shí)間，插槽可以是空的也可以包含功能。

線程控制塊（TCB）：表示seL4中的一個(gè)運(yùn)行線程，線程是調(diào)度、阻塞、非阻塞等的執(zhí)行單元，具體取決于應(yīng)用程序與其他線程的交互。

Endpoints：促進(jìn)了進(jìn)程之間的消息傳輸，IPC是同步的：試圖在端點(diǎn)上發(fā)送或接收消息的線程會(huì)阻塞，直到消息可以傳遞為止，這意味著只有當(dāng)發(fā)送者和接受者在端點(diǎn)匯合時(shí)，消息傳遞才會(huì)發(fā)生，內(nèi)核可以通過一個(gè)拷貝傳遞消息。
端點(diǎn)的功能可以被限制為只發(fā)送或只接收。此外，端點(diǎn)功能可以擁有授予權(quán)，這允許將功能作為消息的一部分發(fā)送

通知對(duì)象：提供一個(gè)簡單的信號(hào)機(jī)制。一個(gè)通知是一個(gè)字大小的標(biāo)志數(shù)組，每個(gè)標(biāo)志的行為都像一個(gè)二進(jìn)制信號(hào)量。操作在單個(gè)操作中向標(biāo)志的子集發(fā)出信號(hào)，輪詢檢查任何標(biāo)志，并阻塞直到任何標(biāo)志被發(fā)出信號(hào)。通知功能可以是僅限信號(hào)的或僅限等待的。

虛擬地址空間對(duì)象：用于為一個(gè)或多個(gè)線程構(gòu)造虛擬地址空間，這些對(duì)象很大程度上直接對(duì)應(yīng)于硬件對(duì)象，因此依賴于體系結(jié)構(gòu)。內(nèi)核還包括用于跟蹤地址空間狀態(tài)的ASID池和ASID控制對(duì)象。

中斷對(duì)象：中斷對(duì)象給應(yīng)用程序接收和確認(rèn)來自硬件設(shè)備的中斷的能力。最初，IRQControl有一個(gè)功能，它允許創(chuàng)建IRQHandler功能。IRQHandler能力允許管理與特定設(shè)備相關(guān)聯(lián)的特定中斷源。它被委托給一個(gè)設(shè)備驅(qū)動(dòng)程序來訪問中斷源。IRQHandler對(duì)象允許線程等待并確認(rèn)單個(gè)中斷。

非類型化內(nèi)存：無類型內(nèi)存是sel4內(nèi)核中內(nèi)存分配的基礎(chǔ)。非類型化內(nèi)存功能只有一個(gè)方法，允許創(chuàng)建新的內(nèi)核對(duì)象。如果方法成功，調(diào)用線程將獲得對(duì)新創(chuàng)建對(duì)象的功能的訪問權(quán)。此外，非類型化內(nèi)存對(duì)象可以劃分為一組較小的非類型化內(nèi)存對(duì)象，允許委托部分(或全部)系統(tǒng)內(nèi)存。我們?cè)谙旅娴恼鹿?jié)中一般地討論內(nèi)存管理。

2.4 內(nèi)核內(nèi)存分配

sel4微內(nèi)核不為內(nèi)核對(duì)象動(dòng)態(tài)分配內(nèi)存，相反，必須通過非類型化內(nèi)存能力，從應(yīng)用程序控制的內(nèi)存區(qū)域顯式創(chuàng)建對(duì)象。
應(yīng)用程序必須有明確的內(nèi)存權(quán)限（通過非類型化內(nèi)存能力）才能創(chuàng)建新對(duì)象，并且所有對(duì)象一旦創(chuàng)建就會(huì)消耗固定數(shù)量的內(nèi)存。
這些機(jī)制可用于精確控制應(yīng)用程序可用的物理內(nèi)存的具體數(shù)量，包括能夠強(qiáng)制隔離應(yīng)用程序或設(shè)備之間的物理內(nèi)存訪問。
除了由硬件規(guī)定的資源之外，內(nèi)核中沒有任何任意的資源限制，因此可以避免許多由于資源耗盡而導(dǎo)致的拒絕服務(wù)攻擊。

在引導(dǎo)時(shí)，seL4預(yù)先分配內(nèi)核本身所需的內(nèi)存，包括代碼、數(shù)據(jù)和堆棧部分（seL4是一個(gè)單內(nèi)核堆棧操作系統(tǒng)）。然后創(chuàng)建一個(gè)初始用戶線程（具有適當(dāng)?shù)牡刂泛凸δ芸臻g）
然后，內(nèi)核將所有剩余內(nèi)存以非類型化內(nèi)存的功能形式交給初始線程，并將引導(dǎo)初始線程所需的一些額外的內(nèi)核對(duì)象功能交給初始線程。然后可以使用seL4 Untyped Retype()方法將這些非類型化內(nèi)存區(qū)域分割為更小的區(qū)域或其他內(nèi)核對(duì)象;創(chuàng)建的對(duì)象被稱為原始無類型內(nèi)存對(duì)象的子對(duì)象。

使用seL4 Untyped Retype()創(chuàng)建對(duì)象的用戶級(jí)應(yīng)用程序，將接收對(duì)結(jié)果對(duì)象的全部權(quán)限。然后，它可以將其對(duì)該對(duì)象擁有的全部或部分權(quán)限委托給一個(gè)或多個(gè)客戶端。

非類型化內(nèi)存對(duì)象表示兩種不同類型的內(nèi)存：通用內(nèi)存或設(shè)備內(nèi)存
通用內(nèi)存可以非類型化為任何其他對(duì)象類型，并用于內(nèi)核提供的非類型化內(nèi)存上的任何操作。設(shè)備內(nèi)存覆蓋由硬件平臺(tái)決定的為設(shè)備預(yù)留的內(nèi)存區(qū)域，這些對(duì)象的使用受到內(nèi)核的以下方式的限制:

設(shè)備非類型化對(duì)象只能重新鍵入到幀或其他非類型化對(duì)象中；例如，開發(fā)人員不能從設(shè)備內(nèi)存創(chuàng)建端點(diǎn)

從設(shè)備中重新類型化的幀對(duì)象不能設(shè)置為線程IPC緩沖區(qū)，或用于創(chuàng)建ASID池

子無類型對(duì)象的類型屬性（是否表示的是通用或設(shè)備內(nèi)存）繼承父親的無類型對(duì)象，也就是說，未類型化設(shè)備的任何子設(shè)備也將是一個(gè)未類型化設(shè)備。開發(fā)人員不能更改無類型的類型屬性。

2.4.1 重用內(nèi)存

到目前為止所描述的模型對(duì)于應(yīng)用程序分配內(nèi)核對(duì)象、在客戶機(jī)應(yīng)用程序之間分配權(quán)限以及獲得這些對(duì)象提供的各種內(nèi)核服務(wù)是足夠的。對(duì)于一個(gè)簡單的靜態(tài)系統(tǒng)配置來說，這一點(diǎn)就足夠了。

seL4內(nèi)核還允許重用非類型化內(nèi)存區(qū)域。只有當(dāng)內(nèi)存中的對(duì)象沒有懸空引用（即功能）時(shí)，才允許重用內(nèi)存區(qū)域。（懸空引用是啥）
這樣生成的樹結(jié)構(gòu)稱為能力派生樹（CDT）。2例如，當(dāng)用戶通過重新鍵入非類型化內(nèi)存來創(chuàng)建新的內(nèi)核對(duì)象時(shí)，新創(chuàng)建的功能將作為非類型化內(nèi)存功能的子功能插入CDT。

對(duì)于每個(gè)非類型化內(nèi)存區(qū)域，內(nèi)核保留一個(gè)水印，記錄之前分配了多少區(qū)域。每當(dāng)用戶請(qǐng)求內(nèi)核在非類型化內(nèi)存區(qū)域中創(chuàng)建新對(duì)象時(shí)，內(nèi)核將執(zhí)行以下兩種操作之一:
如果區(qū)域中已經(jīng)分配了現(xiàn)有對(duì)象，內(nèi)核將在當(dāng)前水印級(jí)別分配新對(duì)象，并增加水印。如果所有先前在區(qū)域中分配的對(duì)象都已被刪除，內(nèi)核將重置水印并從區(qū)域開始重新分配新對(duì)象。

最后，CNode對(duì)象提供的seL4 CNode Revoke()方法銷毀了從參數(shù)capability派生的所有功能。將最后一個(gè)功能撤消到內(nèi)核對(duì)象會(huì)觸發(fā)對(duì)現(xiàn)在未引用的對(duì)象的銷毀操作。這只是清除它、其他對(duì)象和內(nèi)核之間的任何內(nèi)核依賴關(guān)系。

通過對(duì)非類型化內(nèi)存對(duì)象的原始功能調(diào)用sel4cnoderevoke（），用戶將刪除非類型化內(nèi)存對(duì)象的所有子對(duì)象，即指向非類型化內(nèi)存區(qū)域中對(duì)象的所有功能。因此，在這個(gè)調(diào)用之后，沒有對(duì)非類型化區(qū)域中的任何對(duì)象的有效引用，可以安全地重新鍵入和重用該區(qū)域。

2.4.2 對(duì)象大小總結(jié)

在重新鍵入非類型化內(nèi)存時(shí)，了解對(duì)象需要多少內(nèi)存是很有用的。表2.1、2.2和2.3總結(jié)了物體尺寸。

注意cnode和非類型化對(duì)象有變量大小。當(dāng)將非類型化內(nèi)存重新鍵入cnode或?qū)⒎穷愋突瘜?duì)象分解為更小的非類型化對(duì)象時(shí)，使用seL4 untyped Retype()的size bits參數(shù)來指定結(jié)果對(duì)象的大小。表2.1顯示了size bits參數(shù)(n)與seL4 Untyped Retype()之間的對(duì)應(yīng)關(guān)系，以及每個(gè)可變大小對(duì)象的結(jié)果大小。

對(duì)于所有其他對(duì)象類型，大小是固定的，seL4-Untyped_Retype()的size_bits_參數(shù)被忽略。對(duì)seL4UntypedRetype()的一次調(diào)用可以將單個(gè)無類型對(duì)象重新鍵入為多個(gè)對(duì)象。要?jiǎng)?chuàng)建的對(duì)象數(shù)量由它的num_objects參數(shù)指定。所有創(chuàng)建的對(duì)象必須具有相同的類型，由type參數(shù)指定。對(duì)于可變大小的對(duì)象，每個(gè)對(duì)象也必須具有相同的大小。如果所需內(nèi)存區(qū)域的大小(通過對(duì)象大小乘以num_objects來計(jì)算)大于未類型化對(duì)象剩余的未分配內(nèi)存，則會(huì)產(chǎn)生錯(cuò)誤。

3.功能空間

回想一下第2.1節(jié)，seL4實(shí)現(xiàn)了基于功能的訪問控制模型。每個(gè)用戶空間線程都有一個(gè)關(guān)聯(lián)的功能空間(CSpace)，它包含線程所擁有的功能，從而控制線程可以訪問哪些資源。

回想一下，功能駐留在稱為cnode的內(nèi)核管理對(duì)象中。CNode是一個(gè)槽位表，每個(gè)槽位可能包含一個(gè)功能。這可能包括進(jìn)一步擴(kuò)展cnode的功能，形成一個(gè)有向圖。從概念上講，線程的CSpace是有向圖中從CNode能力(CSpace根)開始就可到達(dá)的部分。

CSpace地址指的是一個(gè)單獨(dú)的插槽(在CSpace中的某些cnode中)，它可能包含也可能不包含功能。線程在它們的cspace中使用存放該功能的槽的地址來引用功能。在CSpace中的一個(gè)地址是CNode能力的索引的連接，形成到目標(biāo)槽的路徑;

功能可以在CSpace中復(fù)制和移動(dòng)，也可以在消息中發(fā)送，此外，新的功能可以從舊的功能中的權(quán)限子集來獲得。seL4維護(hù)了功能派生樹(CDT)，它在其中跟蹤這些復(fù)制的功能與原始功能之間的關(guān)系。revoke方法刪除了從所選功能派生的所有功能(在所有cspace中)。服務(wù)器可以使用這種機(jī)制來恢復(fù)它們提供給客戶端的對(duì)象的唯一權(quán)限，或者非類型化內(nèi)存的管理器可以使用這種機(jī)制來銷毀內(nèi)存中的對(duì)象，以便重新類型化。

seL4要求程序員從用戶空間管理所有內(nèi)核內(nèi)的數(shù)據(jù)結(jié)構(gòu)，包括cspace。這意味著用戶空間程序員負(fù)責(zé)構(gòu)造cspace以及其中的尋址功能。本章首先討論能力和CSpace管理，然后討論如何在CSpace中處理能力，即應(yīng)用程序在調(diào)用方法時(shí)如何引用其CSpace中的單個(gè)能力。

3.1 能力和能力空間的管理

3.1.1 CSpace的創(chuàng)建

CSspace是通過創(chuàng)建和操作CNode對(duì)象而創(chuàng)建的。創(chuàng)建一個(gè)CNode時(shí)，用戶必須指定它將擁有的插槽數(shù)，這決定了它將使用的內(nèi)存量。每個(gè)插槽需要16個(gè)字節(jié)的物理內(nèi)存，并且有恰好容納一種能力的容量。
像任何其他對(duì)象一樣，CNode必須通過在適當(dāng)數(shù)量的非類型化內(nèi)存上調(diào)用seL4UntypedRetype()來創(chuàng)建(參見2.4.2節(jié))。因此，調(diào)用者必須能夠在現(xiàn)有cnode中獲得足夠的非類型化內(nèi)存以及足夠的空閑能力槽，以便seL4UntypedRetype()調(diào)用成功。

3.1.2 CNode方法

功能主要通過調(diào)用CNode方法來管理。
CNode支持以下方法：
sel4_cnode_mint（）：從現(xiàn)有功能在指定的CNode插槽中創(chuàng)建新功能。新創(chuàng)建的功能可能比原功能擁有更少的權(quán)限，并且有一個(gè)不同的保護(hù)。sel4nodemint()也可以從一個(gè)未標(biāo)記的功能創(chuàng)建一個(gè)標(biāo)記的功能。

sel4_cnode_copy()：與sel4_cnode_mint（）類似，但新創(chuàng)建的功能與原來的功能具有相同的標(biāo)記和保護(hù)。

sel4_cnode_move（）：在兩個(gè)指定的功能插槽之間移動(dòng)功能。不能將功能移動(dòng)到當(dāng)前所在的插槽中。

sel4_cnode_mutate():可以類似于sel4_cnode_move（）移動(dòng)功能，也可以類似于sel4_cnode_mint（）減少其權(quán)限，但不保留原始副本。

sel4_cnode_rotate():在三個(gè)指定的能力槽之間移動(dòng)兩個(gè)能力。它實(shí)際上是兩個(gè)seL4CNodeMove()調(diào)用:一個(gè)從指定的第二個(gè)插槽到第一個(gè)插槽，一個(gè)從指定的第三個(gè)插槽到第二個(gè)插槽。第一個(gè)和第三個(gè)指定的槽位可能相同。

sel4_cnode_delete():刪除指定slot的能力。

sel4_cnode_revoke():相當(dāng)于對(duì)指定功能的每個(gè)派生子級(jí)調(diào)用sel4_cnode_delete（）。它對(duì)能力本身沒有影響，除非在第3.2節(jié)中概述的非常特殊的情況下。

sel4_cnode_savecaller():將當(dāng)前線程的內(nèi)核生成的應(yīng)答能力從創(chuàng)建它的特殊TCB插槽移動(dòng)到指定的CSpace插槽。

sel4_cnode_cancelbadgesends():取消任何使用相同標(biāo)記和對(duì)象作為指定功能的未完成發(fā)送。

3.1.3 新重新類型化對(duì)象的功能

當(dāng)使用seL4UntypedRetype()將未類型化內(nèi)存重新類型為對(duì)象時(shí)，新重新類型化對(duì)象的功能將被放置在CNode的連續(xù)槽中，該CNode由根、node_index和node_depth參數(shù)指定。node_offset參數(shù)指定將放置第一個(gè)能力的CNode的索引。num_objects參數(shù)指定要?jiǎng)?chuàng)建的功能(以及對(duì)象)的數(shù)量。所有插槽必須為空，否則將導(dǎo)致錯(cuò)誤。所有產(chǎn)生的功能都將放在同一個(gè)CNode中.

3.1.4 能力權(quán)利

如前所述，某些功能類型具有與之相關(guān)聯(lián)的訪問權(quán)限。目前，訪問權(quán)限與端點(diǎn)(見第4章)、通知(見第5章)和頁面(見第7章)的功能相關(guān)聯(lián)。與功能相關(guān)聯(lián)的訪問權(quán)限決定了可以調(diào)用的方法。seL4支持三種正交訪問權(quán)限，即讀、寫和授予。每個(gè)權(quán)利的含義是相對(duì)于各種對(duì)象類型進(jìn)行解釋的，詳見表3.1。
第一次創(chuàng)建對(duì)象時(shí)，引用它的初始能力攜帶最大訪問權(quán)限集。使用諸如sel4nodemint()和sel4 cnodemutate()之類的方法，可以從這個(gè)原始功能中制造出其他不那么強(qiáng)大的功能。如果在這些調(diào)用中的任何一個(gè)中，為目標(biāo)功能指定了比源功能更大的權(quán)限集，那么目標(biāo)權(quán)限將被靜默地降級(jí)為源權(quán)限。

3.1.5 能力派生樹

正如2.4.1節(jié)中提到的，seL4在一個(gè)能力派生樹中跟蹤能力派生。
各種方法，如seL4CNodeCopy()或sel4 cnode mint()，可以用于創(chuàng)建派生功能。并不是所有的功能都支持派生。通常，只有原始功能支持派生調(diào)用，但也有例外。
總結(jié)各種能力類型的能力派生要成功必須滿足的條件，以及如何在每個(gè)案例中報(bào)告能力派生失敗。未列出的功能類型只能派生一次。

顯示了一個(gè)示例功能派生樹，該樹演示了一個(gè)標(biāo)準(zhǔn)方案，頂層是一個(gè)大型非類型化功能，第二層將此功能拆分為兩個(gè)區(qū)域，由他們自己的非類型化功能覆蓋，這兩層都是第一層的子集，左側(cè)的第三級(jí)是第二級(jí)非類型化功能的副本，復(fù)制時(shí)的非類型能力總是創(chuàng)建子級(jí)，而不是兄弟級(jí)，在這個(gè)場(chǎng)景中，非類型化功能被輸入到兩個(gè)獨(dú)立的對(duì)象中，在級(jí)別4上創(chuàng)建兩個(gè)功能，它們都是各自對(duì)象的原始功能，都是從中創(chuàng)建的非類型化功能的子功能。
普通的原始功能可以有一個(gè)級(jí)別的派生功能。這些派生功能的進(jìn)一步復(fù)制將創(chuàng)建兄弟版本，在這種情況下仍在級(jí)別5上。對(duì)于端點(diǎn)和通知功能，這個(gè)方案有一個(gè)例外——它們通過標(biāo)記支持額外的一層深度。原始端點(diǎn)或通知功能將被取消標(biāo)記。使用mint方法，可以創(chuàng)建具有特定徽章的功能副本(見第4.2.1節(jié)，第5.1節(jié))
同一個(gè)對(duì)象的這個(gè)新的、帶標(biāo)記的功能被視為原始功能(“原始帶標(biāo)記端點(diǎn)功能”)，并像其他功能一樣支持一個(gè)派生的子級(jí)別

3.2 刪除和撤銷

seL4中的功能可以被刪除和撤銷。這兩種方法都主要影響能力，但它們可能對(duì)系統(tǒng)中的對(duì)象產(chǎn)生副作用，因?yàn)閯h除或調(diào)用會(huì)導(dǎo)致對(duì)對(duì)象的最后一種能力的破壞。

如上所述，seL4CNodeDelete（）將從指定的節(jié)點(diǎn)插槽中刪除功能。通常，這就是所有發(fā)生的事情。但是，如果它是某個(gè)對(duì)象的最后一個(gè)類型功能，那么這個(gè)對(duì)象現(xiàn)在將被內(nèi)核銷毀，清除內(nèi)核引用中剩余的所有內(nèi)容，并準(zhǔn)備內(nèi)存以供重用。

如果要銷毀的對(duì)象是一個(gè)能力容器，即TCB或CNode，銷毀過程將在銷毀容器之前刪除容器中保存的每個(gè)能力。如果包含的功能是最后的功能，這可能導(dǎo)致進(jìn)一步對(duì)象的銷毀。

sel_cnode_revoke方法將刪除派生樹中指定功能的所有子功能，但是功能的本身不變，如果任何已撤銷的子功能是對(duì)象的最后一個(gè)功能，則會(huì)觸發(fā)相應(yīng)的銷毀操作。

注意:sel4cnoderrecall()可能在兩種特定情況下只能部分完成。第一個(gè)是包含執(zhí)行撤銷的線程的TCB的最后一個(gè)功能(或TCB本身的最后一個(gè)功能)的CNode由于撤銷而被刪除。在這種情況下，執(zhí)行撤銷的線程在觸發(fā)期間被銷毀，撤銷未完成。

第二種情況是，包含作為吊銷目標(biāo)的功能的存儲(chǔ)作為吊銷的結(jié)果被刪除。在這種情況下，執(zhí)行吊銷的權(quán)限將在操作過程中被刪除，并且操作會(huì)中途停止。這兩種情況都可以而且應(yīng)該通過構(gòu)造在用戶級(jí)別避免。
注意，對(duì)于頁表和頁目錄，sel4cnoderrecall()不會(huì)撤銷映射到地址空間的幀功能。他們只會(huì)在空間中消失。

3.3 CSpace 尋址

在執(zhí)行系統(tǒng)調(diào)用時(shí)，線程通過在其CSpace中提供地址來向內(nèi)核指定要調(diào)用的功能。此地址是指調(diào)用方的CSpace中包含要調(diào)用的功能的特定插槽。
cspace的設(shè)計(jì)允許稀疏性，并且查找功能地址的過程必須是高效的。因此，cspace被實(shí)現(xiàn)為受保護(hù)的頁表。

如前所述，CSpace是CNode對(duì)象的有向圖，每個(gè)CNode是一個(gè)槽位表，其中每個(gè)槽位可以是空的，也可以包含一個(gè)功能，該功能可以引用另一個(gè)CNode。回想一下2.3節(jié)，CNode中的插槽數(shù)必須是2的冪。CNode有一個(gè)基數(shù)，也就是2的冪的大小，也就是說，如果一個(gè)CNode有2k個(gè)槽位，那么它的基數(shù)就是k。內(nèi)核在線程的TCB中存儲(chǔ)每個(gè)線程CSpace的根CNode的能力。從概念上講，CNode功能不僅存儲(chǔ)對(duì)它所引用的CNode的引用，而且還攜帶一個(gè)保護(hù)值，見3.3.1節(jié)。

3.3.1 功能地址查找

與虛擬內(nèi)存地址一樣，功能地址只是一個(gè)整數(shù)。與引用物理內(nèi)存的位置(如虛擬內(nèi)存地址)不同，能力地址引用能力槽。當(dāng)查找用戶空間線程提供的功能地址時(shí)，內(nèi)核首先查詢線程的TCB中的CNode功能，該TCB定義了線程的CSpace的根。
然后，它將CNode的保護(hù)值與能力地址的最有效位進(jìn)行比較。如果這兩個(gè)值不同，則查找失敗。如果保護(hù)位是相同的，要看這個(gè)radix位，它最終可能指向下一個(gè)cnode，這個(gè)cnode包含我們要找的能力。那個(gè)slot可能包含cnode也可能包含其他東西，也可能啥都沒有。
如果s包含一個(gè)CNode能力c，并且能力地址中還有剩余的位(在radix之后)還沒有被轉(zhuǎn)換，那么就會(huì)重復(fù)查找過程，從CNode能力c開始，并使用能力地址的剩余位。否則，查找過程成功終止;此處的能力地址指的是能力槽。

• 頂級(jí)CNode對(duì)象，12位保護(hù)設(shè)置為0x000和256個(gè)插槽
• 具有直接對(duì)象引用的頂級(jí)CNode
• 具有兩個(gè)二級(jí)CNode引用的頂級(jí)CNode
• 具有不同防護(hù)和槽數(shù)的二級(jí)CNodes
• 第二級(jí)CNode，包含對(duì)頂級(jí)CNode的引用
• 第二級(jí)CNode，包含對(duì)另一CNode的引用，其中還有一些位需要翻譯
• 第二級(jí)CNode，其中包含對(duì)另一CNode的引用，其中沒有剩余的位要被翻譯
• 第二級(jí)CNodes中的對(duì)象引用

3.3.2 尋址能力

能力地址存儲(chǔ)在一個(gè)CPointer(縮寫為CPTR)中，它是一個(gè)無符號(hào)整數(shù)變量。根據(jù)上面描述的翻譯算法處理功能。兩種特殊情況涉及到CNode能力本身的尋址和一系列能力槽的尋址。

回想一下，上面描述的轉(zhuǎn)換算法將遍歷CNode功能，但仍有需要轉(zhuǎn)換的地址位。因此，為了為CNode能力尋址，用戶不僅必須提供一個(gè)能力地址，而且必須指定要轉(zhuǎn)換的能力地址的最大位數(shù)，稱為深度限制。

某些方法，如seL4UntypedRetype()，要求用戶提供一系列的功能槽。這是通過提供一個(gè)base capability address(引用范圍中的第一個(gè)槽位)和一個(gè)window size參數(shù)來實(shí)現(xiàn)的，該參數(shù)指定范圍內(nèi)槽位的數(shù)量(在基槽位之后有連續(xù)的地址)。

Cap A：第一個(gè)CNode有一個(gè)設(shè)置為0x0的4位保護(hù)和一個(gè)8位基數(shù)。Cap位于插槽0x60中，因此它可以被格式為0x060xxxxx的任何地址引用（其中xxxxx是任意數(shù)字，因?yàn)榉g過程在翻譯地址的前12位之后終止）。為簡單起見，我們通常采用地址0x06000000

Cap B：同樣，第一個(gè)CNode有一個(gè)4位保護(hù)設(shè)置為0x0，還有一個(gè)8位基數(shù)。第二個(gè)CNode通過L2 CNode cap到達(dá)。它還有一個(gè)4位保護(hù)0x0，Cap B駐留在索引0x60處。因此，Cap B的地址是0x00F06000。此地址的轉(zhuǎn)換在前24位之后終止。

Cap C：這種能力是通過兩個(gè)CNodes來實(shí)現(xiàn)的。第三個(gè)CNode通過L3 CNode Cap到達(dá)，該Cap位于第二個(gè)CNode的索引0x00處。第三個(gè)CNode沒有防護(hù)罩，而Cap C位于索引0x60處。因此，它的地址是0x00f00060。此地址的翻譯將保留0位未翻譯

Cap C-G：通過提供0x00F00060的基址（指包含Cap C的插槽）和5的窗口大小來尋址這個(gè)能力插槽范圍。

L2 CNode Cap：回想一下，要定位CNode功能，用戶不僅必須提供功能地址，還必須指定深度限制，即要轉(zhuǎn)換的最大比特?cái)?shù)。L2 CNode Cap位于firstCNode的偏移量0x0F，該節(jié)點(diǎn)有一個(gè)4位的0x0保護(hù)。因此，它的地址是0x00F00000，深度限制為12位。

L3 CNode Cap：這個(gè)功能位于第二個(gè)CNode的索引0x00，由L2 CNode Cap到達(dá)。第二個(gè)CNode有一個(gè)4位的0x0保護(hù)。因此，該功能的地址為0x00F00000，深度限制為24位。注意L2和L3 CNode Caps的地址是相同的，但是它們的深度限制是不同的。

總之，要引用CSpace中的任何功能（或插槽），用戶必須提供其地址。當(dāng)功能可能是CNode時(shí)，用戶還必須提供深度限制。要指定功能插槽的范圍，用戶需要提供起始地址和窗口大小

3.4 查找失敗描述

當(dāng)功能查找失敗時(shí)，將向調(diào)用線程或線程的IPC緩沖區(qū)中的異常處理程序提供失敗的描述。描述的格式總是相同的，但根據(jù)錯(cuò)誤發(fā)生的方式，IPC緩沖區(qū)中的偏移量可能不同。描述格式如下所示。第一個(gè)單詞表示查找失敗的類型，后面單詞的含義取決于此。

3.4.1 無效的根

CSpace CPTR根目錄（在其中查找功能）無效。例如，該功能不是aCNodecap

3.4.2 缺失能力

調(diào)用所需的功能不存在或沒有足夠的權(quán)限

3.4.3 深度不匹配

在解析一個(gè)功能時(shí)，遍歷一個(gè)CNode，該CNode解析的比特?cái)?shù)超過了CPTR中留給解碼的比特?cái)?shù)，或者遇到了一個(gè)非CNode功能，但仍有剩余的比特需要查找

3.4.4 保護(hù)不匹配

解析功能時(shí)，CNode的保護(hù)大小大于剩余的位數(shù)，或者CNode的保護(hù)與解析的PTR的下一位不匹配

4.IPC

seL4微內(nèi)核為線程間的通信提供了一種消息傳遞IPC機(jī)制。同樣的機(jī)制也用于與內(nèi)核提供的服務(wù)進(jìn)行通信。通過調(diào)用內(nèi)核對(duì)象的功能來發(fā)送消息。發(fā)送到端點(diǎn)的消息被指定給其他線程，而發(fā)送到其他對(duì)象的消息則由內(nèi)核處理。本章描述通用的消息格式、端點(diǎn)，以及如何將它們用于應(yīng)用程序之間的通信。

4.1 消息寄存器

每個(gè)消息都包含一些消息字和可選的一些功能。消息字通過將它們放置在線程的消息寄存器來發(fā)送或接收。消息寄存器被編號(hào)，前幾個(gè)消息寄存器是使用物理CPU寄存器實(shí)現(xiàn)的，而其余的由一個(gè)稱為IPC緩沖區(qū)的固定內(nèi)存區(qū)域支持。

這種設(shè)計(jì)的原因是效率：非常短的消息不需要使用內(nèi)存，物理CPU消息寄存器如下所示


每個(gè)IPC消息也有一個(gè)標(biāo)記(結(jié)構(gòu)為seL4MessageInfo_t)。標(biāo)簽由四個(gè)字段組成:標(biāo)簽、消息長度、功能數(shù)量(extraCaps字段)和capsUnwrapped字段。消息長度和功能的數(shù)量決定了發(fā)送線程希望傳輸?shù)南⒓拇嫫骱凸δ艿臄?shù)量，或者決定了實(shí)際傳輸?shù)南⒓拇嫫骱凸δ艿臄?shù)量。標(biāo)簽不被內(nèi)核解釋，它作為消息的第一個(gè)數(shù)據(jù)有效負(fù)載未經(jīng)修改地傳遞。例如，標(biāo)簽可以用來指定請(qǐng)求的操作。
capsUnwrapped字段僅在接收端使用，用于指示接收功能的方式。第4.2.2節(jié)對(duì)此進(jìn)行了描述。

內(nèi)核假設(shè)IPC緩沖區(qū)包含表4.3中定義的seL4IPCBuffer類型的結(jié)構(gòu)。內(nèi)核使用盡可能多的物理寄存器來傳輸IPC消息。當(dāng)傳輸?shù)膮?shù)多于可用的物理消息寄存器時(shí)，內(nèi)核開始使用IPC緩沖區(qū)的msg字段來傳輸參數(shù)。但是，它在這個(gè)數(shù)組中為物理消息寄存器留下了空間。

例如，如果IPC傳輸或內(nèi)核對(duì)象調(diào)用需要4個(gè)消息寄存器(在這個(gè)體系結(jié)構(gòu)上只有2個(gè)物理消息寄存器可用)，那么參數(shù)1和2將通過消息寄存器傳輸，參數(shù)3和4將在msg[2]和msg[3]中。
如果需要，這允許用戶級(jí)對(duì)象調(diào)用存根將在物理寄存器中傳遞的參數(shù)復(fù)制到msg數(shù)組的剩余空間。tag字段的情況類似。在seL4IPCBuffer結(jié)構(gòu)中有這個(gè)字段的空間，內(nèi)核會(huì)忽略它。用戶級(jí)存根可能希望將消息標(biāo)簽從其cpu寄存器復(fù)制到此字段，盡管內(nèi)核提供的用戶級(jí)存根不這樣做。

4.2 Endpoints

端點(diǎn)允許在兩個(gè)線程之間傳輸少量數(shù)據(jù)和功能(即IPC緩沖區(qū))。使用第2.2節(jié)中描述的seL4系統(tǒng)調(diào)用直接調(diào)用端點(diǎn)對(duì)象。

IPC端點(diǎn)使用集合模型，因此是同步和阻塞的。端點(diǎn)對(duì)象可以對(duì)發(fā)送或接收的線程進(jìn)行排隊(duì)。如果沒有接收方準(zhǔn)備好，執(zhí)行seL4Send()或seL4Call()系統(tǒng)調(diào)用的線程將在隊(duì)列中等待第一個(gè)可用的接收方。同樣，如果沒有準(zhǔn)備好發(fā)送方，執(zhí)行seL4Recv()系統(tǒng)調(diào)用或seL4ReplyRecv()的后半部分的線程將等待第一個(gè)可用的發(fā)送方。

4.2.1 endpoint badges

可以創(chuàng)建端點(diǎn)功能，以創(chuàng)建帶有badge(由mint操作的調(diào)用者選擇數(shù)據(jù)字)的新端點(diǎn)功能。當(dāng)用baged權(quán)能發(fā)送消息到端點(diǎn)時(shí)，badge被轉(zhuǎn)移到接收線程的badge寄存器。

帶有零標(biāo)記的端點(diǎn)功能被稱為unbadge。這樣的功能可以在包含該功能的CNode上使用seL4CNodeMutate()或sel4cnnodemint()調(diào)用進(jìn)行標(biāo)記。帶有徽章的端點(diǎn)功能不能被取消標(biāo)記、重新標(biāo)記或用于創(chuàng)建帶有不同徽章的子功能。

只有低28位的徽章可以使用。內(nèi)核會(huì)無聲地忽略任何高4位的使用

4.2.2 權(quán)能轉(zhuǎn)移

如果發(fā)送線程調(diào)用的端點(diǎn)功能具有授予權(quán)限，則消息可能包含將被傳輸?shù)浇邮辗降墓δ?。嘗試在沒有授權(quán)的情況下使用端點(diǎn)功能發(fā)送功能，將導(dǎo)致原始消息的傳輸，而沒有任何功能的傳輸。

要在消息中發(fā)送的功能在發(fā)送線程的IPC緩沖區(qū)的caps字段中指定。該數(shù)組中的每個(gè)條目都被解釋為發(fā)送線程的能力空間中的CPTR。要發(fā)送的功能數(shù)量在消息標(biāo)簽的extraCaps字段中指定。

接收方指定它愿意接收能力的槽位，IPC緩沖區(qū)中有三個(gè)字段:receiveCNode、receiveIndex和receiveDepth。這些字段分別指定根CNode、能力地址和要解析的位數(shù)，以找到放置能力的槽位。第3.3.2節(jié)描述了能力尋址。

接收端能力與原始能力擁有相同的權(quán)利，除非接收端能力缺乏寫權(quán)限。在這種情況下，通過從接收的功能副本中剝離寫權(quán)限，對(duì)發(fā)送功能的權(quán)限被削弱。

請(qǐng)注意，接收線程可以只指定一個(gè)接收槽，而發(fā)送線程可以在消息中包含多個(gè)功能。包含多個(gè)功能的消息可以由內(nèi)核對(duì)象解釋。在消息中的一些額外功能可以展開的情況下，還可以將它們發(fā)送給接收線程。

如果第n個(gè)能力指的是端點(diǎn)的消息通過消息發(fā)送,能力是打開:它的徽章是放在第n個(gè)位置數(shù)組接收機(jī)的徽章,和內(nèi)核設(shè)置第n個(gè)點(diǎn)(從最低有效計(jì)數(shù))capsUnwrapped消息的字段標(biāo)簽。能力本身沒有被轉(zhuǎn)移，所以接收槽可以被用于另一個(gè)能力。

如果接收方收到一條消息，其標(biāo)簽的extraCaps為2,capsUnwrapped為2，則消息中的第一個(gè)能力被轉(zhuǎn)移到指定的接收槽，第二個(gè)能力被打開，將其徽章放置在徽章中。發(fā)送者的郵件中可能存在無法打開的第三種功能。

總結(jié)

以上是生活随笔為你收集整理的sel4 手册总结之介绍与内核服务和对象的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

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