sel4白皮书翻译 | sel4 whitepaper | sel4简介
首發地址：http://trialley.top/pages/53ac44/
CSDN地址：https://blog.csdn.net/lgfx21/article/details/117606097
翻譯與轉發許可：
作者：Gernot Heiser gernot@sel4.systems
翻譯：TriAlley lg139@139.com
翻譯版本：1.2 2020-06-10
原文：https://sel4.systems/About/seL4-whitepaper.pdf
譯者學識淺薄，文中許多專有名詞和英語文化表達尚未明晰，均用括號標注英文原文。如果您有翻譯建議，歡迎評論或郵件告知于我，不勝感激。
vuepress的markdown不支持引文，文中[^1]樣式的字段表示在文末有相應參考文獻
譯注
翻譯中出現了許多容易混淆的名詞，且某些詞組僅在本文檔中初出現過，國內外都找不到其他出處。由于譯者并不是專業翻譯，也不是微內核從業者，因此對這些名詞只能盡量進行進行合理的意譯，不周之處還請批評指正。
摘要
本白皮書對 seL4 進行了介紹。我們將解釋 seL4 是什么 (以及不是什么)，并探討它的特性。我們將解釋是什么使 seL4 有資格成為安全關鍵系統、通用嵌入式嵌入式和信息物理系統(Cyber-Physical System)所選擇的操作系統內核。我們將解釋 seL4 的安全故事(assurance story)、它的防盜和穩定(security and safety)相關特性以及它的基準性能。我們還討論了典型的使用案例和已有系統的漸進式改造案例。
1 seL4 概述
seL4是微內核。
操作系統 (OS) 是一種控制計算機系統資源并提供安全性的底層系統軟件。與用戶態程序不同， OS 可以使用 CPU 的特權模式（kernel mode），這意味著 OS 可以直接訪問硬件。而用戶態程序只能使用用戶模式（user mode），僅可以訪問 OS 允許它訪問的的硬件。
操作系統微內核是操作系統的最小化內核，它將高權限代碼的數量降到最少。seL4 是 L4 微內核家族 的成員，這個家族可追溯到 90 年代中期. (seL4 和 seLinux沒有任何關系)
seL4 是虛擬機管理器
seL4 支持運行客戶操作系統 (如 Linux)。seL4 的交流通道(communication channels)使客戶機和它的應用程序可以彼此通信，本地程序也一樣（as well as with native applications. ）。
在第二章中了解更多關于 seL4 微內核的信息及其作為虛擬機管理器的使用方法。在第七章中了解真實世界的部署場景和現有系統改造方法。
seL4 的正確性驗證
seL4提供了一個正式的、數學的、機器檢查的形式化驗證，這意味著就其規范而言，內核很大程度上上是“沒有bug的”。事實上， seL4 是世界上第一個經過形式化驗證系統1。
seL4 是安全的
除了實現上的正確性之外，seL4還進一步提供了安全性驗證2。在一個正確配置的sel4系統中，內核保證了機密性、完整性和可用性等經典的安全屬性。關于這些證明的更多內容在第三章。
seL4通過能力進行安全高效的訪問控制
能力是訪問令牌，它可以對哪個實體可以訪問系統中的特定資源進行非常細粒度的控制。他們根據最低特權原則(也稱為最低權威原則，POLA)設計，提供強大的防盜能力。這是高安全系統的核心設計原則，在主流系統(如Linux或Windows)中是不可能實現訪問控制的。
seL4 可作為穩定性硬實時操作系統
seL4是世界上唯一一個對最壞情況執行時間(WCET)進行了完整和合理分析的內核(至少在開放文獻中)34。這意味著，如果正確配置了內核，所有的內核操作在固定時間內完成，這是構建硬實時系統的先決條件。在硬實時系統中，如果不能在嚴格限定的時間內對事件作出反應，后果將是災難性的。
seL4是最先進的混合關鍵系統
它為混合關鍵實時系統(MCS)提供了強大的支持。在這些系統中，關鍵活動與在同一平臺上執行的不可信代碼共存，要確保關鍵活動的時效性。一些成熟的MCS操作系統使用嚴格分區的時間和空間資源管理，seL4則通過更靈活的資源管理提高了利用率5。更多關于seL4的實時性和MCS特性見第5章。
seL4是最快的微內核
一般來說，速度和安全二者不可兼得，seL4的獨特之處在于它全都要。seL4支持廣泛的現實世界用例。無論安全性多重要重要，卓越的性能都是必需的。關于seL4性能的更多信息見第6章。
seL4 發音 “s-e-l-four”
sell four這個發音棄用了，現在直接讀字母即可。
2 沒有IPC的虛擬機管理器不是好的微內核
宏內核VS微內核
主流操作系統(如Linux)和微內核(如seL4)之間的區別見圖2.1。
[外鏈圖片轉存失敗,源站可能有防盜鏈機制,建議將圖片保存下來直接上傳(img-kdtIorGn-1635304626728)(https://i.loli.net/2021/05/21/lLrjHg8qmOPIaGX.png)]
左邊是Linux的架構圖。黃色的部分是操作系統內核，它為應用程序提供文件存儲和網絡等服務。所有實現這些服務的代碼都在CPU的特權模式下執行，也稱為內核模式或管理模式，即對系統中所有資源的無限制訪問和控制的執行模式。相反，應用程序以非特權或用戶模式運行，對硬件的訪問受到限制，受限的資源必須通過操作系統訪問。操作系統內部結構為許多層，其中每一層提供由下面的層實現的抽象(The OS is internally structured in a number of layers, where each layer provides abstractions implemented by layers below. 看不懂這句話)。
特權模式代碼的問題在于它很危險：如果這里出了什么問題，就沒什么阻止破壞的辦法了。特別是如果特權模式代碼有一個漏洞，攻擊者可以利用該漏洞以特權模式運行非法代碼(稱為特權升級或任意代碼執行攻擊)，那么攻擊者可以對系統為所欲為。這些缺陷是主流系統中都有的。
當然，軟件錯誤是現實存在的，操作系統也不例外。Linux內核由2000萬行源代碼組成(20 MSLOC)；可以估計它包含成千上萬的bug 6。這顯然是一個巨大的攻擊面！Linux有一個很大的可信計算基礎(TCB)，這個技術是整個系統的子集，整個系統的安全運行依賴于TCB。
微內核設計背后的理念是大幅縮小TCB，從而減少攻擊面。如圖2.1右側所示，僅有很小一部分處于特權模式。seL4有一萬行源代碼(10 kSLOC)，比Linux內核小了三個數量級，攻擊面也相應地縮小了(可能更小，因為bug的密度可能隨代碼大小線性增長)。
很明顯，不可能在如此小的代碼庫中提供與Linux相同的功能。事實上，微內核幾乎不提供任何服務：它只是對硬件的一個薄薄的包裝，僅僅足夠安全地復用硬件資源。微內核主要提供的是隔離，即一個程序可以在不受其他程序干擾的情況下執行的沙箱。同時它提供了一種受保護的過程調用機制(出于歷史原因，稱為IPC)。這允許程序安全地調用另一個程序中的函數。微內核在程序之間傳輸函數的輸入輸出并控制接口使用權：函數只能在一個導出的入口點被調用，并且只能被授權的客戶端調用(第4章)。
關于seL4 IPC怎么用，建議閱讀博客
https://microkerneldude.wordpress.com/2019/03/07/how-to-and-how-not-to-use-sel4-ipc/
微內核系統使用IPC來提供宏內核在內核態中實現的服務。在微內核世界中，這些服務只是程序，與應用程序沒有區別，它們運行在自己的沙箱中，并為應用程序調用提供IPC接口。應用的故障將局限在沙箱內，系統的其余組件則不受影響(譯注：指其余組件的安全性不受影響，但其余組件都無法繼續使用故障組件提供的服務了)。這與宏內核形成了鮮明的對比，在宏內核系統中，內核故障將導致整個系統不可用。
譯注：我覺得作者主要想說微內核可以將不可挽回的故障限制在某用戶進程，內核和其他進程不受影響；而宏內核的內核一旦故障，運行其上的所有軟件就都不可用了。
這種影響可以被量化：我們最近的研究表明，在Linux中所出現的嚴重問題，29%將被微內核設計完全消除，另外55%將被大大減輕，不再被列為關鍵問題7。
seL4是微內核，不是OS
seL4是一個微內核，設計的目的是確保通用性同時最小化TCB。它是L4微內核家族的成員，可以追溯到90年代中期；圖2.2顯示了seL4的起源。它是由我們在UNSW/NICTA的團隊開發的，最近一段時間被稱為可信系統(TS)。當時，我們在開發高性能微內核方面有15年的經驗，并有實際部署的跟蹤記錄：我們的OKL4微內核搭載在數十億高通蜂窩調制解調器芯片上，我們的L4 -嵌入式內核從10年代中期就在所有iOS設備的安全協處理器(secure enclave)上運行。
[外鏈圖片轉存失敗,源站可能有防盜鏈機制,建議將圖片保存下來直接上傳(img-iHl7gqHC-1635304626731)(https://i.loli.net/2021/05/21/JDdEmiT4YNtQush.png)]
作為一個微內核，seL4不包含任何常見的操作系統服務；這些服務是由運行在用戶模式下的程序提供的。這是微內核設計缺陷之一：正常運行總需要很多組件。可以從開源操作系統(如FreeBSD或Linux)移植，也可以從頭開始編寫。但無論如何，編寫組件是一項重要的工作。
為了擴大規模組件規模，我們需要社區的幫助，而seL4 Foundation是使社區能夠為基于seL4的系統合作、開發或移植此類服務的關鍵機制。其中最重要的是設備驅動程序、網絡協議棧和文件系統。我們有相當數量的此類組件，但還需要更多。
的組件開發來說，組件框架很重要，它允許開發人員專注于實現服務本身，不必關注seL4的某些細節。seL4目前有兩個主要的開源組件框架:CAmkES和Genode。
CAmkES是一個針對嵌入式和信息物理系統的框架，這些系統通常是靜態架構，這意味著它們由一組定義好的組件組成，一旦系統完全啟動，這些組件就不會改變。
Genode在很多方面都是一個更強大、更通用的框架，它支持多個微內核，并且已經提供了大量的服務和設備驅動程序，特別是針對x86平臺。它比CAmkES更方便，而且肯定是快速建立復雜系統的方法。然而Genode也有缺點：
seL4是虛擬機管理器
seL4是一個微內核，但它也是一個管理程序:可以在seL4上運行虛擬機，如Linux。
[外鏈圖片轉存失敗,源站可能有防盜鏈機制,建議將圖片保存下來直接上傳(img-RguoLFRr-1635304626733)(https://i.loli.net/2021/05/22/IuRgJkjhWfeXvVt.png)]
這提供了另一種提供系統服務的方法，即讓Linux VM提供系統服務。這樣的設置如圖2.3所示，其中顯示了一些服務如何從多個Linux實例中借用，這些實例作為客戶機運行。
在本例中，我們提供兩種系統服務：網絡和存儲。
網絡是由直接運行在seL4上的本機協議棧提供的，lwIP或PicoTCP是常用的棧。我們沒有移植網絡驅動程序，而是借用Linux的一個驅動程序，這個精簡的Linux客戶機只有一個網卡驅動程序。協議棧通過sel4提供的通道與Linux通信，應用程序同樣通過與協議棧通信獲得網絡服務。注意，在圖中顯示的設置中，應用程序沒有到網卡驅動虛擬機的通道，因此不能直接與它通信：這是通過基于seL4能力而實現的(見第4章)
存儲服務與此類似；文件系統是Linux虛擬機提供的，而存儲驅動程序則是本地的。同樣，組件之間的通信也是受通道限制的，應用程序不能直接與存儲驅動程序通信，兩個Linux虛擬機不能相互通信。
當用作虛擬機管理器時，seL4以特權模式運行(Arm上的EL2, x86上的Root Ring-0, RISC-V上的HS)，這是比客戶機更高的特權級別。seL4只在特權模式執行作為虛擬機管理器所進行的少量工作工作，其余的工作都留給用戶模式。
具體來說，這意味著seL4負責“世界切換”，當虛擬機的執行時間到期時，或者由于某些其他原因必須切出時，seL將進行狀態切換操作。它還捕獲虛擬化異常(Intel虛擬化架構中術語是VM exits )，并將它們轉發給一個用戶級處理程序，稱為虛擬機監視器(VMM)。然后，VMM負責執行模擬操作。
每個VM都一個VMM，VMM與客戶操作系統以及其他VM相互隔離，如圖2.4所示。這意味著VMM不能打破隔離，因此并不比客戶操作系統本身更可信。特別是，這意味著不需要驗證VMM，因為只要不驗證來賓操作系統(通常是Linux)，就不會增加真正的安全性。
譯注：
由該小節可見，在seL4中，VM包含GuestOS與GuestApps，VMM可與VM交流但不能與GuestOS交流。
那么問題來了，VM在seL4中是一個實體還是一個由GuestOS和GuestApps組成的虛擬概念？
另外，VMM和Hypervisor要怎么在中文里進行區分？
seL4不是seLinux
許多人會搞混 seL4 和 seLinux (或許他們以為 seL4 是第 4 代 seLinux；譯注：也可能因為 seL(inux) 縮寫，就像 K8S). 事實上除了都開源， seL4 跟 seLinux 沒有任何關系。他們在代碼或概念上沒有任何交集。 seLinux 不是微內核，它是 Linux 內置的安全框架。雖然比標準 Linux 更安全，但 seLinux 和標準 Linux 面對相同的問題：巨大 TCB 和相當大的攻擊面。換句話說，seLinux 是一個根本不安全的操作系統的組件，因此仍然是根
本不安全的。相比之下， seL4 提供了武裝到牙齒的隔離。
簡而言之， seLinux 并不適合安全要求嚴格的情景，而 seL4 就是為這些用途而設計的。
3 驗證過程(Verification Story)
2009年，seL4成為世界上第一個在源代碼級別上經過機器證明功能正確性(machine-checked functional
correctness proof)的操作系統內核。當時由20萬行證明腳本，是有史以來最大的(我們認為它是第二大)。以前人們以為不會有功能正確(functionally correct)的OS內核，我們證明它是存在的。
從那時起，我們將驗證的范圍進行了擴展，圖3.1顯示了證明鏈，下面將對此進行解釋。重要的是，我們在內核不斷發展的過程中一直保持這個驗證措施：只有在不破壞證明的情況下，才允許提交到主線內核源代碼，否則我們就更新證明代碼(otherwise the poofs are updated as well)。這種證明工程是一種新事物。我們的seL4證明構成了迄今為止最大的還在維護的證明集(proof base)。到目前為止，證明腳本已經超過了100萬行，其中大部分是手工編寫然后用機器檢查的(manually written and then machine checked)。
正確性和安全性
功能正確(Functional correctness)
seL4驗證的核心是功能正確性證明，要確保C代碼沒有缺陷。更準確地說，內核的功能有一個正式的規范，用一種稱為高階邏輯(high-order logic, HOL)的數學語言表示。這由圖中寫著“abstract model”的方框表示。C實現是抽象模型的具體化，這意味著C代碼的可能行為是抽象模型允許的行為的子集。
C語言不是形式化語言；為了允許在定理證明器中對C程序進行推理(我們使用Isabelle/HOL)，必須將其轉換為數學邏輯(HOL)。這是由一個用Isabelle編寫的C解析器完成的。解析器定義了C程序的語義，并根據這個語義形成HOL。這種形式化是數學(抽象)模型的改進(It is this formalisation which we prove to be a refinement of the mathematical (abstract) model)。
請注意，C語言沒有正式的數學語義，而且C語言的某些部分是出了名的微妙，并沒有定義得很好。我們通過將C的限制在該語言的一個定義良好的子集內來解決這個問題，對于這個子集我們有一個明確的語義。然而，這并不能保證我們為該子集假定的語義與編譯器相同。下面將詳細介紹。
我們想讓內核的行為與規范一致，不允許出現于規范不同的行為。這就避免了通常用來攻擊操作系統的操作，如棧溢出、空指針引用、代碼注入或控制流劫持等。
編譯驗證（Translation validation）
一個沒有bug的C內核是很棒的，但是我們仍然受制于C編譯器。這些編譯器(我們使用GCC)本身就是有bug的大型程序。我們那完美的代碼很有可能被編譯成有bug的二進制文件。
編譯器出bug還是小事，就怕編譯器使壞，包含一個木馬程序，在編譯操作系統時構建后門。木馬也可以入侵用來編譯編譯器的編譯器，這樣我們想自己編譯編譯器也沒法避免木馬。Ken Thompson在他的圖靈獎演講中解釋了這一攻擊8。
為了防止有缺陷的或惡意的編譯器，我們另外驗證由編譯器和鏈接器生成的可執行二進制文件。具體來說，我們證明了二進制代碼是C代碼的正確翻譯，因此二進制代碼也符合抽象規范。
譯注：
這部分過于學術化，基礎知識見SAT與SMT。
這張圖的意思大概是把C代碼和編譯后的二進制都轉化為數學描述，看這兩種數學描述功能是否相同。
與C代碼的驗證不同，這個證明腳本不是手寫的，而是通過一個自動工具鏈完成的。它由幾個階段組成，如圖3.2所示。在定理證明器中，處理器指令集(ISA)的形式化模型形式化了二進制；我們使用了RISC-V ISA的L3形式化和廣泛測試的L3 Arm ISA形式化9。
然后，一個用HOL4定理證明程序編寫的反匯編程序將這種低級表示轉換為控制流的圖語言表示。這個變換被證明是正確的。
通過Isabelle/HOL定理證明器中可證明正確的變換，將形式化的C程序轉換為相同的圖形語言。然后我們得到了同一個程序的不同表示，我們需要表明它們是等價的。這有點棘手，因為編譯器對代碼進行了優化。We apply a number of such transformations through rewrite rules on the graph-language representation of the C program (still in the theorem prover, and thus provably correct).
最后，我們得到了兩個非常相似但不相同的程序，我們需要證明它們有相同的語義。從理論上講，這相當于停機問題 (halting problem)，因此是無法解決的。在實踐中，編譯器所做的事情是確定的，這使問題易于處理。我們通過將程序分成小塊扔給多個SMT解決程序來解決這個問題。如果其中一個可以證明所有對應的部分具有相同的語義，那么我們就知道這兩個程序是等價的。
還需要注意的是，被證明符合形式化規范的C代碼和二進制文件都具有相同的Isabelle/HOL形式。這意味著我們對C語義的假設脫離了證明所做的假設(This means that our assumptions on C semantics drop out of the assumptions made by the proofs.)。總之，這些證明不僅表明編譯器沒有引入bug，還證明其C子集的語義和我們定義的語義相同。
安全屬性
圖3.1還顯示了抽象規范和高級安全屬性(機密性、完整性和可用性)(這些通常被稱為CIA屬性)之間的證明。抽象規范實際上對安全很有用：在一個正確配置的系統中，內核將強制執行這些屬性。
譯：關于安全驗證的補充說明，實在不會翻譯了。
These proofs presently do not capture properties associated with time. Our confidentiality proofs rule out covert storage channels but presently not covert timing channels, which are used by such attacks as Spectre. Preventing timing channels is something we are working on [Heiser et al., 2019]. Similarly, the integrity and availability proofs presently do not cover timeliness, but our new MCS model [Lyons et al., 2018] is designed to cover those aspects (see Section 5.2).
證明假設
所有關于正確性的推理都基于假設，無論是正式的推理(如seL4)，還是非正式的推理(當有人思考為什么他們的程序可能是正確的)。每個程序都在某個上下文中執行，它的正確行為不可避免地依賴于對這個上下文中的一些假設。
機器檢查形式推理的優點之一是，它迫使人們明確地做出這些假設。不可能做出未聲明的假設，如果證據依賴于沒有明確聲明的假設，那么它們就不會成功。從這個意義上說，形式推理可以防止忘記假設，或者不清楚假設；這本身就是核查的一大好處。
對seL4的驗證有三個假設：
**硬件按預期運行。**這應該是顯而易見的。內核受底層硬件的支配，如果硬件有bug(或者更糟，有木馬)，那么無論您運行的是經過驗證的seL4還是任何未經驗證的操作系統，都將失敗。硬件驗證超出了seL4的范圍(以及TS的能力);其他人有研究這個的。
**規范是正確的。**這是一個困難的問題，因為沒人知道現在的規范是否完美。當然，有總比沒有強。
可以通過證明有關規范的屬性來降低這種風險，正如我們在安全性證明中所做的那樣，安全性證明表明seL4能夠強制執行某些安全性屬性。這就把問題轉移到了這些屬性的說明上。它們比內核規范簡單得多，減少了誤解的風險。
但數學和物理之間總是存在著鴻溝，任何推理都無法完全消除這一點。形式推理的好處是，你確切地知道差距是什么
**定理證明器是正確的。**這聽起來像是一個嚴重的問題，因為定理證明本身就是一個龐大而復雜的程序。然而，在現實中，這是三個假設中最不值得關注的。因為Isabelle/HOL定理證明器有一個小核心(10 kSLOC)，用來檢查所有與邏輯公理相悖的證明。這個核心已經從廣泛的形式推理領域中檢查了許多大大小小的證明，所以它包含正確性關鍵錯誤的可能性是非常小的。
譯注：我覺得這種套娃證明無窮盡的思想就是古歐洲哲學的精髓了；與我國天人合一的哲學明顯不同。
證明進度
seL4已經或正在被多個架構驗證：Arm、x86和RISC-V。他們的驗證進度各不相同，有的正在研究，有的就是缺錢搞。詳情請參考seL4項目狀態頁面。
CAmkES組件框架
CAmkES is a component framework that allows you to reason about a system architecturally, i.e. as a collection of sandboxed components with defined communication channels. Figure 3.3 shows the main abstractions.
不會翻譯
組件用方框表示。它們表示由seL4封裝的程序、代碼和數據。
[外鏈圖片轉存失敗,源站可能有防盜鏈機制,建議將圖片保存下來直接上傳(img-pseUjkf0-1635304626737)(https://i.loli.net/2021/05/21/T9RBGFlIVgOqvD7.png)]
接口定義了如何調用一個組件，或者如何調用其他組件。接口要么被導入(調用另一個組件的接口)，要么被導出(能夠被另一個導入的組件的接口調用)，共享內存接口除外，它是對稱的。
連接器將同類型的輸入輸出接口連接起來。CAmkES中的連接器總是一對一的。但是通過添加將單輸入復制成多輸出的組件實現廣播或多播功能。
CAmkES系統是用一種正式的體系結構描述語言(CAmkES ADL)指定的，它包含對組件、它們的接口和連接它們的連接器的精確描述。CAmkES對系統設計者的承諾是，ADL中指定的(如圖3.3所示)就是可能產生的交互。特別地，它承諾除了圖中所示的交互之外，沒有其他交互的可能。
當然，這個承諾依賴于seL4，ADL表示必須映射到低級seL4對象和對它們的訪問權限。這就是CAmkES機制所實現的，如圖3.4所示。
在圖的頂部展示了ADL中所描述的結構。這是一個相當簡單的系統，由4個本機組件和一個包含兩個驅動的虛擬機組件。Linux虛擬機只能通過crypto組件連接到其他組件，這就保證了虛擬機只能訪問加密的鏈接，不會泄露數據。
即使是這個簡單的系統也會映射成百上千各seL4對象，CAmkES為我們降低了開發復雜度。
對于sel4級的描述，我們有另一種正式的語言，稱為CapDL(能力分配語言)。系統設計者永遠不需要處理CapDL，它是一個純粹的內部表示。CAmkES框架包含一個編譯器，它自動將CAmkES ADL轉換為CapDL，由左向下的方框箭頭表示。圖左側的框給出了CapDL中描述的seL4對象的簡化表示。
CapDL規范是系統中訪問權限的精確表示，也是seL4強制執行的。這意味著一旦系統進入CapDL規范描述的狀態，它就保證按照CAmkES ADL規范描述的行為，因此體系結構級別的描述足以進一步推理安全屬性(therefore the architecture-level description is sufficient for further reasoning about security properties. )。
因此，我們需要確保系統啟動到CapDL規范所描述的狀態。我們通過第二個箭頭實現了這一點：我們從CapDL生成啟動代碼，一旦seL4自身啟動，就控制并生成規范引用的所有seL4對象，包括描述活動組件的對象，在初始化代碼執行的最后，可以證明系統處于CapDL規范所描述的狀態，因此也處于ADL規范所表示的狀態。
第三個箭頭表示從ADL規范生成的組件之間的膠水代碼。通過連接器發送數據需要調用seL4系統調用，這些系統調用的細節被CAmkES隱藏。膠水代碼使用了這些系統調用。例如，RPC連接器將一個遠程過程調用封裝成了普通函數調用。
在撰寫本文時，關于CAmkES和CapDL的證明還沒有完成，但離完成很近了。
還請注意，所提到的驗證工作都沒有處理定時通道造成的的信息泄漏。這是一個尚未解決的重大問題，但我們就快搞定了。
4 能力
我們在第一章中遇到了一些功能，注意到它們是訪問令牌。現在我們將更詳細地研究這個概念。
什么是能力
如圖4.1所示，一個能力是一個對象引用；它類似于指針(能力的實現通常稱為胖指針)。能力是不可變的指針，指向內核中對應權限類型的對象。
除了指針之外，能力還對訪問權限進行編碼。在基于功能的系統(如seL4)中，調用功能是對系統對象執行操作的唯一方法。
例如，一個操作可能是調用組件中的函數。嵌在該功能中的對象引用指向該對象的接口，并表達調用該函數的權利。(The capability may or may not at the same time convey the right to pass another capability along as a function argument (delegating to the component the right to use the object referenced by the capability argument) )
這是CAmkES抽象級別的高級描述。事實上，在CAmkES里，能力本身被封裝了。
在底層，連接器由端點對象表示，客戶端組件需要具有調用權限的能力。
正是這種細粒度的、面向對象的特性使得能力成為面向安全系統的訪問控制機制。最小化每個組件的能力，這是最低特權原則所要求的。
請注意，能力的這個概念與Linux所稱的能力強大得多，后者實際上是具有系統調用粒度的訪問控制列表(acl)。與所有ACL模式一樣，Linux功能也存在令人困惑的問題，這是許多安全漏洞的根源，下一節將對此進行解釋。seL4的能力沒有這個問題。
seL4能力也不容易受到該引文10中描述的攻擊；這種攻擊適用于直接在硬件中實現的功能，而seL4的能力由內核實現。
有10種類型的seL4對象，它們都由能力引用：
**端點Endpoints **用于執行受保護的函數調用
**應答對象Reply Objects **表示來自受保護過程調用的返回路徑
**地址空間Address Spaces **提供了沙箱(硬件頁表的封裝)
**節點Cnodes **存儲表示組件訪問權限的能力
**線程控制塊Thread Control Blocks **表示線程
**調度上下文Scheduling Contexts **表示在處理器上使用一個時間片的權利
**通知Notifications **是同步對象(類似于信號量)
**幀Frames **表示可以映射到地址空間的物理內存
**中斷對象Interrupt objects **提供對中斷處理的訪問
空類型Untypes未使用的(自由的)物理內存，可以轉換為任何其他類型
為什么要使用能力
細粒度訪問控制
能力提供細粒度的訪問控制，符合最小權限安全原則(也稱為最小權限原則POLA)。這與訪問控制列表(acl)這種更傳統的訪問控制模型形成了對比，后者在主流系統(如Linux或Windows)中使用，但也在商業系統(如INTEGRITY或PikeOS)中使用。
要理解其區別，首先看訪問控制在Linux中是如何工作的：文件(文件訪問權限控制具有代表性)具有一組訪問模式位。其中一組位決定了它的所有者可以對文件執行什么操作，另一組位代表了用戶組中每個成員允許的操作，最后的一組位是授予其他人的默認權限。這是一個面向用戶的方案，以用戶身份區分權限。用戶對權限設置相同的文件享有相同權限。
這是一種非常粗粒度的訪問控制形式。一個典型的場景是，用戶希望用一個不受信任的程序(比如從互聯網上下載)處理一個特定的文件，但希望阻止該程序訪問該用戶的其他文件。在Linux中沒有優雅的方法來做到這一點，人們想出了一些笨重的解決方案，比如chroot，容器等。
有了能力，這個問題很容易解決，因為能力提供了面向對象的訪問控制形式。具體來說，當且僅當請求操作的程序擁有對應能力時，內核才會允許操作繼續進行。在限制場景中，不受信任的應用程序只能訪問被賦予權限的文件。因此Alice調用程序，將一個能力交給程序允許讀取的一個文件，再加上一個能力讓他可以把輸出內容寫到另一個文件里，這個程序不能訪問任何其他事物——這就是最小權限。
中介與授權Interposition and delegation
能力還有很多特性。一個是中介訪問的能力，這是不透明對象引用的結果。如果Alice被賦予了一個對象的能力，她不知道這個對象到底是什么，她所能做的就是調用對象上的方法。
例如，系統設計者可能假裝給Alice的能力指向一個文件，而實際上它指向一個通往安全監視器的通道，安全監視器持有實際能力。監視器可以檢查Alice請求的操作，如果合法Alice執行文件操作，不合法則忽略請求。監視器有效地虛擬化了文件。
中介不僅僅可以用來做安全檢查；該方法可用于包過濾、信息流跟蹤等。調試器可以透明地插入和虛擬化對象調用。它甚至可以懶加載一個對象：Alice調用該對象時，對象才會被創建。
能力的另一個優點是，它們支持安全有效的權限授權。如果Alice想讓Bob訪問她的一個對象，她可以為該對象創建(在seL4中叫mint)一個新能力，并將其交給Bob。然后Bob就可以使用該能力來操作對象，而不需要還給Alice。(相反，如果Alice想要保持對這個過程的控制，它可以使用上一段講的中介技術。)
新能力的權利可能會減少；Alice可以只給Bob只讀權限。Alice可以在任何時候撤銷Bob的訪問權，方法是摧毀她交給Bob的派生能力。
授權功能很強大并且在ACL系統中無法輕松且安全地完成。一個典型使用授權的例子是設置自主管理資源的子系統。當系統啟動時，初始進程擁有對系統中所有資源的權限(除了內核本身使用的少量且固定的資源)。然后，這個初始資源管理器可以通過創建新的進程(子資源管理器)，并賦予他們互不相交的權限，來分割出不同子系統。
然后子系統可以自主地(不參考原始管理器)控制它們的資源子集，同時不相互干擾。只有當他們想要改變原始資源分配時才需要訪問初始管理器。
周圍權限和困惑的副手
acl有一個無法解決的問題，通常稱為混淆代理。讓我們來看一個C編譯器。它接受一個C源文件并產生一個輸出文件，文件名作為參數傳遞。要運行編譯器，用戶Alice必須對編譯器具有執行權限，如圖4.2所示。
假設編譯器還在系統級日志文件中創建了一個用于審計目的的條目。日志文件對普通用戶是不可訪問的，因此編譯器必須以提升的權限執行，以便寫入日志文件(傳統上通過將其設置為setuid程序來完成)。
如果Alice是惡意的，她可以欺騙編譯器去做它不應該做的事情。例如，Alice可以在調用編譯器時指定密碼文件作為輸出文件。除非編譯器非常小心地編寫以避免任何潛在的濫用，否則它將只打開輸出文件(密碼文件)，并使用已編譯的目標代碼覆蓋它。Alice編寫一個程序，使新生成的密碼文件賦予她不應該擁有的特權，這并不需要很多技巧。
這里的基本問題是，當編譯器打開它的輸出文件進行寫入時，操作系統通過查看編譯器的用戶ID來確定訪問的有效性，以確定它是否有訪問該對象的權限。由編譯器決定操作是否有效，使編譯器成為系統TCB的一部分，這意味著必須完全信任它，以便在所有情況下做正確的事情。
ACL系統可以采用一些防御措施來減輕特定的問題,例如,確保密碼文件和日志文件在不同安全域(這不會阻止愛麗絲痛擊日志文件)。這就導致了通常的攻擊和防御的軍備競賽。
這種混淆是由環境權限(ambient authority)引起的：操作的有效性由代理(編譯器)的安全狀態決定，在本例中代理是代表Alice。為了適當的安全性，訪問必須由Alice的安全狀態決定。這意味著命名(對文件的引用)和權限(對文件執行操作的權利)必須耦合在一起，這一原則稱為沒有權限就不指定。如果是這種情況，那么編譯器將使用指定的權限(來自Alice)調用指定的對象(輸出文件)，這樣Alice就不會再混淆代理了。
這正是能力系統所做的。在這樣的系統中，Alice需要擁有三種能力：執行編譯器的能力、讀輸入文件的能力和寫輸出文件的寫能力。她使用執行能力調用編譯器，并將另外兩個能力作為參數傳遞。然后，當編譯器打開輸出文件時，它使用Alice提供的能力進行操作。編譯器使用一個獨立的能力來打開日志文件，使日志和編譯輸出分開。特別是，Alice不可能欺騙編譯器寫入一個她自己無法訪問的文件。
解決“困惑的副手問題”是能力的殺手級應用，因為這個問題無法用acl解決。因此，下次有人試圖向你出售一個安全的操作系統時，不僅要問他們是否有操作系統的正確性證明，還要問它是否使用了基于能力的訪問控制。如果這兩個問題的答案都是否定的，那么你就得到了假貨(原文snake oil 蛇油指假的萬金油)。
5 支持硬實時系統
seL4被設計為一個保護模式的實時操作系統。這意味著，與經典的RTOSes不同，seL4結合了實時能力和內存保護，以確保安全性，并部分支持混合關鍵系統。
一般實時支持
seL4有一個簡單的、基于優先級的調度策略，易于理解和分析，這是硬實時系統的核心需求。內核將自己永遠不會調整優先級，因此用戶是控制者。
另一個需求是有限中斷延遲。與L4微內核家族的大多數成員一樣，seL4在內核模式下執行時禁用中斷。這個設計決策極大地簡化了內核的設計和實現，因為內核(在一個單核處理器上)不需要并發控制。否則，seL4的正式驗證是不可行的，但該設計也使優異的平均情況性能成為可能。
人們普遍認為，為了保持較低的中斷延遲，實時操作系統必須是可搶占的(除了短的臨界部分)。雖然對于在簡單微控制器上運行的傳統非保護模式RTOSes是正確的，但在保護模式系統上并不對，如seL4。因為當運行在一個啟用了內存保護的強大微處理器上時，進入內核、切換上下文和退出內核的時間非常長，不比seL4系統調用少多少。就中斷延遲而言，可搶占設計幾乎沒有什么好處，但復雜性方面的成本將非常高，使得可搶占設計不合理。
只要所有系統調用都很短就行。在seL4中系統調用都很短，但也有例外。特別是撤銷一個能力可能是一個耗時的操作。seL4處理這種情況的方法是將這些操作拆分為短的子操作，使他可以被中斷，被打斷的操作可以在中斷完成后接著執行。
這種方法被稱為增量一致性。每個子操作將內核從一個一致狀態轉換為另一個一致狀態。該操作的結構是這樣的：在中止之后，可以重新啟動該操作，而無需重復中止之前成功的子操作。內核在每個子操作之后檢查掛起的中斷。如果有，它將中止當前操作，此時中斷將強制重新進入內核，由內核處理中斷。當完成時，原始系統調用將重新啟動，然后從它被中止的地方繼續執行，以確保進展。
我們對seL4進行了完整而合理的最壞情況執行時間(WCET)分析，這是唯一有記錄的保護模式OS的最壞情況執行時間分析1112。這意味著我們已經得到了所有系統調用延遲的可證明的硬上界，以及最壞情況下的中斷延遲。
這種WCET分析是支持硬實時系統的先決條件，也是使seL4在競爭中脫穎而出的特性。雖然已經對不受保護的RTOSes進行了完整和可靠的WCET分析，但保護模式系統的行業標準方法是將內核置于高負載下，測量延遲，采用觀察到的最壞的延遲，并添加一個安全系數。不能保證這種方法得到的界是安全的，而且它不適合安全關鍵系統(safety-critical systems)。
我們為Arm v6處理器做了seL4的WCET分析。由于Arm不再提供指令的最壞情況延遲所需的信息，而英特爾也從未為其架構提供這些信息，該系統從此陷入停頓。然而，隨著開源RISC-V處理器的出現，我們將能夠重新進行這一分析。
5.2 混合關鍵系統
什么是混合關鍵系統
關鍵是一個來自安全領域的術語，與組件故障的嚴重程度有關。例如，航空電子標準對故障進行了分類，從對車輛安全沒有影響到災難性故障(造成人員傷亡)。組件越關鍵，所需的保證就越廣泛(也越昂貴)，因此有強烈的動機保持低關鍵(there is a strong incentive for keeping criticalities low. )。
混合關鍵系統(MCS)由不同關鍵的組分(相互作用)組成。它的核心安全要求是一個組件的故障不能影響到任何更關鍵的組件，從而確保關鍵組件獨立于不那么關鍵的組件
傳統上，關鍵系統的每個功能都使用專用的微控制器，即電氣隔離。隨著功能的增長，這種方法導致處理器(及其封裝和布線)的激增，從而導致空間、重量和功率(SWaP)問題，而這正是MCS的目標。
這類似于在同一個系統中同時擁有受信任和不受信任組件的組件，在這兩種情況下，操作系統的核心需求都是強隔離。安全領域的挑戰在于，安全性不僅依賴于功能正確性，還依賴于及時性：關鍵組件通常有實時需求，這意味著它們必須在截止時間前對事件做出響應。
傳統MCS
傳統的MCS操作系統完全隔離部件的時間和空間，一種稱為嚴格時間和空間劃分(TSP)的方法，以ARINC 653航空電子標準ARINC13為例。這意味著每個組件被靜態地分配一個固定的內存區域，并且分區根據預先確定的調度順序和固定的時間片執行。
TSP方法保證隔離，但有嚴重的缺點。最明顯的一個是資源利用不足。每個實時組件必須能夠在它的時間片內完成它的工作，所以時間片必須至少是組件的最壞情況執行時間。組件的WCET可以比通常的執行時間大幾個數量級，因為它必須考慮到異常情況。
此外，確定WCET的安全邊界通常是棘手的。對于關鍵組件，必須非常保守地說服持懷疑態度的認證機構，這通常會導致估值較大。這意味著處理器通常沒有得到充分利用。但是，由于嚴格的分區，空閑時間不能被其他組件使用，因此利用率不佳是一個固有的問題。基本上，通過保留間隙實現強隔離，TSP資源使用率較差。
TSP的另一個大缺點是中斷延遲本身就很高。以圖5.1為例，它可能表示一個(高度簡化的)自動駕駛汽車。關鍵部件是一個控制回路，它每5毫秒執行一次，處理傳感器數據并向執行器發送命令。它的WCET，也就是時間片，是3毫秒。車輛還與一個地面站通信，它可以更新路徑點。因為系統以5毫秒的時間運行，這是可以處理網絡中斷的延遲時間，極大地限制了網絡吞吐量和對外部事件的響應能力。
seL4的MCS
MCS的核心挑戰是操作系統必須提供強大的資源隔離，但是TSP過于簡單(因此不靈活)。就空間資源而言，seL4已經有了一個靈活、強大且可證明安全的模型：對象能力(見第4章)。接下來討論時間資源：對處理器的訪問也由能力控制。
用于處理器時間的seL4能力稱為調度上下文能力。組件只有在擁有這樣的能力時才能獲得處理器時間，并且它可以使用的處理器時間量被編碼在該能力中。這類似于空間對象的訪問權限的工作方式。
在傳統的seL4中(就像在它之前的大多數L4內核中一樣)，線程有兩個主要的調度參數：優先級和時間片，它們決定對處理器的訪問。
優先級決定了線程何時可以執行，如果沒有更高優先級的可運行線程，它可以運行。時間片決定內核在搶占線程之前允許線程運行多長時間(除非它在被一個更高優先級的線程成為可運行線程之前被搶占)。當時間片耗盡時，調度器將再次選擇優先級最高的可運行線程(可能是剛剛被搶占的線程)，并在優先級級別中使用循環策略。
seL4的MCS版本將時間片替換為調度上下文對象的能力，該對象執行類似的功能，但以更精確的方式執行隔離：調度上下文包含兩個主要屬性。(1)時間預算，類似于舊的時間片，并限制線程可以執行的時間。(2)一個時間段，它決定了預算可以被使用的頻率：無論優先級如何，在該時間段內他都會被分到自己時間預算那么長的處理器時間。
調度上下文支持推理一個線程可以消耗多少時間，還有多少時間剩余。可用于防止高優先級線程獨占處理器。
應用于上面的例子，這意味著我們可以給(不太關鍵的)設備驅動程序一個比(關鍵的)控制組件更高的優先級。這允許驅動程序搶占控制，提高響應速度。但是時間預算將阻止驅動程序過度使用CPU。例如，我們給控制器一個3ms的預算(它的WCET)和一個5ms的周期(對應于它運行的頻率)。我們給高優先級驅動3μs預算，周期為10μs，這意味著它在任何情況下都不能消耗超過總處理器時間的30%，但可以足夠頻繁地執行以確保良好的響應性。重要的是，我們可以保證控制器(它需要的可用處理器時間不超過60%)有足夠的時間滿足截止時間。
通過不考慮驅動程序的行為而保證關鍵截止日期，將控制與不受信任的驅動程序隔離。特別是，驅動不需要被認證為安全關鍵。
seL4的時間能力模型解決了MCS的許多其他挑戰，超出了本白皮書的范圍，有興趣的讀者可閱讀這篇文章14。可以說，在所有關鍵操作系統中，seL4提供了最先進和最靈活的MCS支持。
6 安全性能全都要
性能一直是L4家族的標志，seL4也不例外。我們構建seL4是為了實際應用，我們的目標是相對于我們之前擁有的最快的內核而言，IPC性能損失不超過10%。結果是，seL4最終比這些內核還快。
它的性能勝過任何其他微內核。這是一種很難證明的說法，因為競爭對手通常會將他們的性能數據保密(出于非常好的理由!)
然而，我們會利用一切機會，公開宣布這一業績。如果有人不同意，他們需要出示證據。我們還通過一些非正式渠道了解到，其他系統的IPC性能往往比seL4慢2倍到慢得多，通常大約是seL4的10倍。
有幾個獨立的性能對比驗證了我們的優越性。
這篇文章15比較三個開源系統的性能，seL4, Fiasco.OC和Zircon 。它發現seL4 IPC成本比內核進入、地址空間切換和內核退出的硬件限制大約高出10% 20%。Fiasco.OC比seL4慢2倍以上(接近硬件極限的3倍)，Zircon的速度幾乎是seL4的9倍。
這篇文章16比較了CertiKOS和seL4的性能，在CertiKOS中實現雙向IPC花了3820個運行周期，而在seL4中花了1830個周期。然而，事實證明，sel4bench (seL4基準測試套件)在處理x86上的計時器時存在一個bug，導致了夸大的延遲。正確的seL4性能值大約是720個循環，比CertiKOS快5倍以上。另外CertiKOS提供特性非常有限，也沒有基于能力的安全性。
7 實際生產和漸進式改造
一般情況
當計劃使用seL4的安全特性時，第一步應該是確定需要保護的關鍵資產。目標是將可信計算基礎TCB最小化，并使其盡可能模塊化，使每個模塊都成為受sel4保護的CAmkES組件。
另一個重要的準備工作是檢查平臺上seL4的可用性和驗證狀態。顯然，seL4的賣點就是經過形式化驗證。然而，即使在未驗證的平臺上，它也比其他操作系統更安全。但是要牢記，沒有驗證就沒有完全的安全保證。如果您使用的內核沒有為您的平臺進行驗證，或者您魔改了內核，那出了事您一定不要怪我們。
您還需要評估seL4的基礎軟件生態是否滿足您的目的。如果不是，那么這就是社區可以幫助你的地方。有一些公司專門為seL4提供支持。此外，如果您自己開發了任何通常組件，您應該認真考慮在適當的開源許可下與社區共享它們。助人者人恒助之。
改造現有系統
在現實世界中，大多數seL4的部署都不會在本地(native)運行所有內容，有可能以虛擬機的方式運行在seL4上。通常，有一些重要的遺留組件移植起來會很昂貴，因為它們可能依賴目前seL4不支持服務。此外，通常情況下，本地運行這些遺留堆棧不會帶來什么安全性或安全性收益。
使用seL4的虛擬化能力通常是一種實用的方法，第2.3節給出了一些示例。
[外鏈圖片轉存失敗,源站可能有防盜鏈機制,建議將圖片保存下來直接上傳(img-Ob6NrEdy-1635304626741)(https://i.loli.net/2021/05/22/WdCq1MHYB9xwf5Q.png)]
典型的方法是我們所謂的“漸進式改造”，這是當時DARPA項目主任約翰·朗奇伯里創造的術語。如圖7.1所示，通常首先將整個現有軟件堆棧放入在seL4上運行的虛擬機中。顯然，這個步驟在安全性和安全性方面沒有任何價值，它只增加了非常小的開銷。它的重要意義在于，它提供了模塊化的開端。
一個很好的例子是我們的HACMS項目合作伙伴對波音ULB自動直升機進行的網絡改造。最初的系統運行在Linux上，在第一步中，團隊將seL4放在了下面。
下一步出現了兩個組件:特別不受信任的攝像頭軟件被轉移到同樣運行Linux的另一個虛擬機，兩個Linux虛擬機通過CAmkES通道通信。同時，網絡堆棧從VM中取出并轉換為原生CAmkES組件，也與主VM通信。
最后一步是將所有其他關鍵模塊以及(不可信的)GPS軟件放入單獨的CAmkES組件中，移除原來的主VM。最后的系統由許多運行sel4本機代碼的CAmkES組件和一個只運行Linux和攝像軟件的單個VM組成。
結果是，雖然最初的系統很容易被DARPA雇傭的專業滲透測試人員侵入，但最終狀態是高度彈性的。攻擊者可以破壞Linux系統并對其為所欲為，但無法突破并破壞系統的其他部分。這個團隊有足夠的信心證明是在飛行中攻擊。(The team was confident enough to demonstrate an attack in-flight)
總結
seL4是世界上第一個經過形式化驗證的OS內核。
雖然到目前為止有其他經過驗證的內核，seL4仍然是最先進的。它有最全面的驗證過程17。它也是唯一的基于能力的OS驗證，它有最先進的實時性支持。我們的持續研究使得seL4在安全導向內核中始終處于領先水平。例如，我們對通過定時通道泄露信息的系統性和原則性預防18。
除了這種技術上的領先地位，seL4在實際應用方面仍然遠遠領先于其他人：我們從一開始就為現實應用設計seL4，而幾乎所有其他經過驗證的內核都是學術玩具，離現實應用還很遠。事實上，我們只知道另一個(最近)驗證過的系統實際上是可部署的(盡管在更有限的場景中)。
seL4在生產中的應用得益與兩大目標：性能上不妥協(第6章)以及旨在支持最廣泛應用場景的安全策略，后者通過基于能力的訪問控制實現(第4章)。
seL4參與實際生產的10年經驗，顯然幫助我們完善和改進了系統，但我很自豪地說，輕微的、增量的改變就足夠了。唯一的例外是MCS支持(第5.2節)，這需要對模型及其實現進行相當重大的改變，但時間的特權管理是我們在最初設計時已經計劃去做的事情。19。
希望這份白皮書能讓您對seL4有一個大體的認識，讓您知道可以用它做什么，重要的是，讓您知道為什么想要使用它。我希望這將幫助您成為seL4社區的活躍成員，包括加入和參與seL4基金會。
我希望這份文件能夠不斷發展，我也很期待得到反饋。但最重要的是，我很想聽聽您部署seL4的經驗。
致謝
我非常感謝我收到的關于本白皮書早期版本的反饋，這有助于改進它。TS的以下成員對草稿進行了評論：Curtis Millar, Gerwin Klein, Ihor Kuz, June Andronick, Liz Willer, Luke Mondy, Michael Norrish和Zoltan Kocsis。
此外，我還收到了來自社區成員Ben Leslie和Davor Ocelic的評論。
Kim Pastor 在創立基金會品牌方面做了很好的工作。
參考文獻
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, et al. seL4: Formal verification of an OS kernel. In ACM Symposium on Operating Systems Principles, pages 207–220, Big Sky, MT, US, October 2009. URL https://ts.data61.csiro.au/publications/nicta_full_text/1852.pdf ??
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):2:1–2:70, February 2014. URL https://ts.data61.csiro.au/publications/nicta_full_text/7371.pdf. ??
Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury, and Gernot Heiser. Timing analysis of a protected operating system kernel. In IEEE Real-Time Systems Symposium, pages 339–348, Vienna, Austria, November 2011. IEEE Computer Society. URL https://ts.data61.csiro.au/publications/nicta_full_text/4863.pdf. ??
Thomas Sewell, Felix Kam, and Gernot Heiser. High-assurance timing analysis for a high-assurance real-time OS. Real-Time Systems, 53:812–853, September 2017. URL https://ts.data61.csiro.au/publications/csiro_full_text//Sewell_KH_17.pdf. ??
Anna Lyons, Kent McLeod, Hesham Almatary, and Gernot Heiser. Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time. In EuroSys Conference, Porto, Portugal, April 2018. ACM. URL https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf. ??
Simon Biggs, Damon Lee, and Gernot Heiser. The jury is in: Monolithic OS design is flawed. In Asia-Pacific Workshop on Systems (APSys), Korea, August 2018. ACM SIGOPS. URL https://ts.data61.csiro.au/publications/csiro_full_text//Biggs_LH_18.pdf. ??
Simon Biggs, Damon Lee, and Gernot Heiser. The jury is in: Monolithic OS design is flawed. In Asia-Pacific Workshop on Systems (APSys), Korea, August 2018. ACM SIGOPS. URL https://ts.data61.csiro.au/publications/csiro_full_text//Biggs_LH_18.pdf. ??
Ken Thompson. Reflections on trusting trust: Turing award lecture. Communications of the ACM, 27(8):761–763, August 1984. ??
Anthony Fox and Magnus Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Proceedings of the 1st International Conference on Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 243–258, Edinburgh, UK, July 2010. Springer. ??
William Earl Boebert. On the inability of an unmodified capability machine to enforce the–property. In 7th DoD/NBS Computer Security Conference, pages 291–293, September 1984. ??
Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury, and Gernot Heiser. Timing analysis of a protected operating system kernel. In IEEE Real-Time Systems Symposium, pages 339–348, Vienna, Austria, November 2011. IEEE Computer Society. URL https://ts.data61.csiro.au/publications/nicta_full_text/4863.pdf. ??
Thomas Sewell, Felix Kam, and Gernot Heiser. Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis. In IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April 2016. URL https://ts.data61.csiro.au/publications/nicta_full_text/9118.pdf. ??
ARINC. Avionics Application Software Standard Interface. ARINC, November 2012. ARINC Standard 653. ??
Anna Lyons, Kent McLeod, Hesham Almatary, and Gernot Heiser. Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time. In EuroSys Conference, Porto, Portugal, April 2018. ACM. URL https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf. ??
Zeyu Mi, Dingji Li, Zihan Yang, Xinran Wang, and Haibo Chen. SkyBridge: Fast and secure inter-process communication for microkernels. In EuroSys Conference, March 2019 ??
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj?berg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In USENIX Symposium on Operating Systems Design and Implementation, pages 653–669, Savannah, GA, US, November 2016. USENIX Association. ??
Gernot Heiser. 10 years seL4: Still the best, still getting better, August 2019. URL https://microkerneldude.wordpress.com/2019/08/06/10-years-sel4-still-the-best-still-getting-better/. Blog post. ??
Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. Time protection: the missing OS abstraction. In EuroSys Conference, Dresden, Germany, March 2019. ACM. URL https://ts.data61.csiro.au/publications/csiro_full_text//Ge_YCH_19.pdf ??
Gernot Heiser and Kevin Elphinstone. L4 microkernels: The lessons from 20 years of research and deployment. ACM Transactions on Computer Systems, 34(1):1:1–1:29, April 2016. URL https://ts.data61.csiro.au/publications/nicta_full_text/8988.pdf ??
總結
以上是生活随笔為你收集整理的sel4白皮书翻译 | sel4 whitepaper | sel4简介的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： python读取xls文件_用pytho
- 下一篇： Python中7种随机函数总结