seL4 嵌入式作業系統

簡介

seL4 是衍生自 L4 的微核心作業系統 ， 而 L4 則衍生自 L3。

L3/L4 都是 Jochen Liedtke 所創建的，因為 Jochen Liedtke 認為微核心作業系統不必然是沒效率的，但是第一代的微核心作業系統 MACH 的效能不太好。

MACH 是美國《卡內基梅隆大學》所開發的微核心作業系統，企圖用微核心技術替代 UNIX 作業系統，但最後沒有成功，不過卻成了《微核心的共同祖先》。

Jochen Liedtke 在 1988 年創建了 L3 ，L3 有一個很高效的行程間通訊 (IPC, Interprocess Communication) 機制，並在 Technischer Überwachungsverein 這個機構使用了好幾年，證明效率和安全性都還不錯。

在 L3 當中，一次系統呼叫的時間比 Unix 所花費的一半還少，但是 MACH 的一次系統呼叫花費時間卻是 UNIX 的五倍。

L4 作業系統家族

即便效率已經很好了，但是 Jochen Liedtke 還是不夠滿意，因為他知道 L3 所承襲的 MACH 機制還有很多無效率之處，為了榨乾每一滴效能，他重新設計出了 L4 作業系統，除了引入更高效的設計之外，整個核心全部使用 x86 組合語言打造。

後來 Jochen Liedtke 到了 Karlsruhe 大學繼續主持 L4 的開發，所以新版本稱為 L4Ka:Pistachio，並且引入了 C++，還讓 L4Ka 可以在 ARM/x86 兩種平台上執行。L4ka 釋出後，原本組合語言版的 L4 就很少再繼續被使用維護了。

Jochen Liedtke 在 2001 年去世了，得年 48，但欣慰的是 L4 已經吸引了其他研究者的投入，德國 TU Dresden 技術大學的 TUD:OS 小組，開發出了 L4/Fiasco 版本，讓整個作業系統幾乎隨時都可以被中斷，並且達到極短的中斷延遲，成為真正的《即時作業系統》 (Real Time Operating System)。

L4/Fiasco 被用在 DROPS (The Dresden Real-Time Operating System Project) 當中，但可惜後來沒有繼續使用《隨時可中斷》的特性，因為這樣的程式很難寫。

L4/Fiasco 後來演化為 L4Ka::Pistachio，並且設計了一組跨平台的 API，

澳洲的新南威爾斯大學 (University of New South Wales,UNSW) 也投入了 L4 的研究與改良，並且發現將驅動程式寫在使用者空間，效能幾乎和寫在核心一樣好。於是他們創造出一個 稱為 Wombat 的作業系統。Wombat 是一個架在 L4 之上的高度可移植作業系統，可以支援 x86, ARM, MIPS 等處理器。後來這組人換工作到了澳洲的 NICTA (National ICT Australia) 研究中心，並且創建出 NICTA::L4-embedded 專案，這個專案後來被用在高通 (Qualcomm) 的 Mobile Station Modem 晶片組上，成為了商業產品的一部分。

領導 NICTA::L4-embedded/ERTOS 專案的 Gernot Heiser 教授，後來創立了 Open Kernel Labs (OK Labs) 這家公司，並且以 OKL4 的品牌進行商業化，並將其用在 Nokia 的 Symbian 與 Google 的 Android 作業系統上，光 2012 年就出貨超過 15 億份。

蘋果 A 系列的處理器，包含了一個稱為 Secure Enclave 的協同處理器，就是跑在這個 L4 系統上的。

seL4

2006 年 NICTA 發展出第三代微核心的 seL4 作業系統，目標是成為安全可靠，經過正規驗證 (formal proof) 的系統。 2009 年 seL4 通過了 formal proof 程序，確認 seL4 核心與規格相符，該驗證規則是用 Haskell 撰寫的一組測試程式。於是 seL4 成為全世界第一個被驗證的通用作業系統。

2014 年 NICTA 將 seL4 核心用 GPLv2 授權開放原始碼，大部分函式庫則是用 BSD 2-clause 授權，2020 年 seL4 在成立了基金會，並且納入了 Linux 基金會下以開放原始碼組織營運。

以下是 seL4 的官網與相關資源，我們的電子書也將從這裡取材，請搭配原始碼一起閱讀。

• seL4 嵌入式作業系統 -- https://sel4.systems/
  • 支援 RISC-V -- https://github.com/seL4/seL4/tree/master/src/arch/riscv
  • Tutorial -- https://docs.sel4.systems/Tutorials/
  • 白皮書 -- https://sel4.systems/About/seL4-whitepaper.pdf
  • https://docs.sel4.systems/projects/sel4test/

seL4 目前支援三個平台，包含 x86/ARM/RISC-V ，而且 RISC-V 版本也已經被驗證通過了 。

結語

除了 seL4 之外，還有其他人也繼續研究並發展 L4 的相關作業系統，以下是幾個範例：

1. Osker, an OS written in Haskell
2. CodeZero is an L4 microkernel for embedded systems with a focus on virtualization and implementation of native OS services. There is a GPL-licensed version, and a version that was relicensed by B Labs Ltd., acquired by Nvidia, as closed source and forked in 2010
3. F9 microkernel, a BSD-licensed L4 implementation, is dedicated to ARM Cortex-M processors for deeply embedded devices with memory protection.
4. The NOVA OS Virtualization Architecture is a research project with focus on constructing a secure and efficient virtualization environment with a small trusted computing base. NOVA consists of a microhypervisor, a user level hypervisor (virtual machine monitor), and an unprivileged componentised multi-server user environment running on it named NUL. NOVA runs on ARMv8-A and x86-based multi-core systems.
5. WrmOS is a real-time operating system based on L4 microkernel. It has own implementations of kernel, standard libraries, and network stack, supporting ARM, SPARC, x86, and x86-64 architectures. There is the paravirtualized Linux kernel (w4linux) working on WrmOS.