L4 マイクロカーネル ファミリ

L4 は第 2 世代のマイクロカーネルファミリであり、さまざまな種類のオペレーティング システム(OS) を実装するために使用されますが、主にUnix ライクなPOSIX ( Portable Operating System Interface ) 準拠のタイプを対象としています。

L4は、その前身であるマイクロカーネルL3と同様に、以前のマイクロカーネルベースのOSの低パフォーマンスへの対応として、ドイツのコンピュータ科学 者 Jochen Liedtkeによって作成されました。Liedtkeは、他の目標ではなく最初から高性能を目的として設計されたシステムであれば、実用的なマイクロカーネルを生み出せると感じました。1993年に彼が手作業でコーディングしたIntel i386固有のアセンブリ言語コードによる最初の実装は、 Machよりも20倍高速であったことで注目を集めました。^[1] 2年後のフォローアップの出版物^[2]は非常に影響力があると考えられ、2015 ACM SIGOPS Hall of Fame Awardを受賞しました。発表以来、L4はクロスプラットフォームであること、セキュリティ、分離性、堅牢性を向上させることを目的として開発されてきました。

オリジナルの L4カーネル アプリケーション バイナリ インターフェイス(ABI) とその後継には、L4Ka::Pistachio (カールスルーエ工科大学の Liedtke と彼の学生によって実装)、L4/MIPS (ニューサウスウェールズ大学(UNSW))、Fiasco (ドレスデン工科大学(TU Dresden)) など、さまざまな再実装がありました。このため、L4という名前は一般化され、Liedtke のオリジナルの実装だけを指すものではなくなりました。現在では、L4 カーネルインターフェイスとそのさまざまなバージョン を含むマイクロカーネルファミリ全体に適用されます。

L4は広く導入されています。Open Kernel LabsのOKL4という派生版は、数十億台のモバイルデバイスに搭載されています。^{[3] [4]}

マイクロカーネルの一般的な考え方について、Liedtke 氏は次のように述べています。

概念がマイクロカーネル内で許容されるのは、それをカーネル外に移動した場合、つまり競合する実装を許可した場合に、システムに必要な機能の実装が妨げられる場合のみです。^[2]

この精神に基づき、L4 マイクロカーネルは、アドレス空間(ページ テーブルを抽象化し、メモリ保護を提供する)、スレッドとスケジューリング(実行を抽象化し、一時的な保護を提供する)、およびプロセス間通信(分離境界を越えた制御された通信) といったいくつかの基本的なメカニズムを提供します。

L4 のようなマイクロカーネルに基づくオペレーティング システムは、 Linuxなどのモノリシック カーネルや旧世代のマイクロカーネルが内部的に組み込まれているユーザー空間のサーバーとしてサービスを提供します。たとえば、安全なUnix のようなシステムを実装するには、サーバーはMach がカーネル内に組み込んだ 権限管理を提供する必要があります。

Machなどの第一世代のマイクロカーネルのパフォーマンスが低かったため、1990 年代半ばには多くの開発者がマイクロカーネルの概念全体を再検討するようになりました。Mach で使用されていた非同期のカーネル内バッファリングプロセス通信の概念が、パフォーマンスが低い主な理由の 1 つであることが判明しました。このため、Mach ベースのオペレーティング システムの開発者は、ファイル システムやドライバーなどの時間的に重要なコンポーネントをカーネル内に戻すようになりました。^[要出典]これによりパフォーマンスの問題はいくらか改善されましたが、真のマイクロカーネルの最小性の概念に明らかに違反しています (また、その主な利点を無駄にしています)。

Machボトルネックの詳細な分析により、とりわけワーキングセットが大きすぎることが示されました。IPCコードは空間的局所性が乏しく、その結果キャッシュミスが多すぎ、そのほとんどはカーネル内です。^[2]この分析から、効率的なマイクロカーネルは、パフォーマンスが重要なコードの大部分が（第1レベルの）キャッシュ（できればそのキャッシュのごく一部）に収まるほど小さくなければならないという原則が生まれました。

Jochen Liedtke は、パフォーマンスとマシン固有 (クロスプラットフォーム ソフトウェアとは対照的) の設計に細心の注意を払った、適切に設計された薄いプロセス間通信(IPC) 層が、現実世界での大幅なパフォーマンス向上をもたらすことを証明しようとしました。Mach の複雑な IPC システムの代わりに、彼の L3 マイクロカーネルは、オーバーヘッドを追加することなく、単にメッセージを渡すだけでした。必要なセキュリティ ポリシーの定義と実装は、ユーザー スペースサーバーの役割であると考えられていました。カーネルの役割は、ユーザー レベル サーバーがポリシーを適用できるようにするために必要なメカニズムを提供することだけでした。1988 年に開発された L3 は、安全で堅牢なオペレーティング システムであることが証明され、 Technischer Überwachungsverein (技術検査協会)などで長年にわたって使用されました。^[要出典]

L3 の使用経験を経て、リードケは Mach の他のいくつかの概念も見当違いであるという結論に達した。マイクロカーネルの概念をさらに単純化することで、彼は主に高性能を目的として設計された最初の L4 カーネルを開発した。性能を最大化するために、カーネル全体がアセンブリ言語で記述され、その IPC は Mach の 20 倍高速であった。^[1]このような劇的な性能向上はオペレーティングシステムではまれであり、リードケの研究は、1996年にリードケが働き始めたIBM、ドレスデン工科大学、ニューサウスウェールズ大学など、多くの大学や研究機関で新しい L4 実装や L4 ベースのシステムの研究のきっかけとなった。IBM のトーマス・J・ワトソン研究センターでは、リードケと彼の同僚は L4 およびマイクロカーネルベースのシステム全般、特に Sawmill OS の研究を続けた。^[5]

1999 年、リードケはカールスルーエ大学のシステム アーキテクチャ グループを引き継ぎ、マイクロカーネル システムの研究を続けました。高性能マイクロカーネルは高級言語でも構築できるという概念実証として、グループはL4Ka::Hazelnut を開発しました。これはIA-32およびARMベースのマシンで動作するカーネルのC++バージョンです。この取り組みは成功し、パフォーマンスは依然として許容範囲内であり、そのリリースにより、純粋なアセンブリ言語バージョンのカーネルは事実上廃止されました。

L4Ka::Hazelnutの開発と並行して、1998年にドレスデン工科大学のオペレーティングシステムグループTUD:OSは、L4/Fiascoという名のL4カーネルインターフェースの独自のC++実装の開発を開始しました。カーネル内での並行処理を許可しないL4Ka::Hazelnutや、特定のプリエンプションポイントでのみカーネル内での割り込みを許可するその後継のL4Ka::Pistachioとは対照的に、L4/Fiascoは、低い割り込みレイテンシを実現するために完全にプリエンプティブでした（非常に短いアトミック操作を除く） 。これは、L4/Fiascoが、同じくドレスデン工科大学で開発されたハードリアルタイムコンピューティング対応オペレーティングシステムであるDROPS ^[6]のベースとして使用されているため、必要であると考えられました。しかし、完全にプリエンプティブな設計の複雑さから、Fiascoの後のバージョンでは、限られた数のプリエンプションポイントを除いて割り込みを無効にしてカーネルを実行するという従来のL4アプローチに戻りました。

L4Ka::Pistachio と Fiasco の新しいバージョンがリリースされるまで、すべての L4 マイクロカーネルは本質的に基礎となる CPU アーキテクチャに密接に結びついていました。L4 開発における次の大きな変化は、移植性が高くても高性能な特性を維持したクロスプラットフォーム (プラットフォームに依存しない) アプリケーション プログラミング インターフェイス ( API ) の開発でした。カーネルの基本的な概念は同じでしたが、新しい API は、マルチプロセッサ システムのサポートの向上、スレッドとアドレス空間の結びつきの緩和、ユーザー レベルのスレッド制御ブロック (UTCB) と仮想レジスタの導入など、以前の L4 バージョンに比べて多くの重要な変更を提供しました。2001 年初頭に新しい L4 API (バージョン X.2、別名バージョン 4) をリリースした後、カールスルーエ大学のシステム アーキテクチャ グループは、高性能と移植性の両方に重点を置いた新しいカーネルL4Ka::Pistachio を完全にゼロから実装しました。これは、2 条項 BSD ライセンスの下でリリースされました。^[7]

L4/Fiasco マイクロカーネルも、長年にわたって大幅に改良されてきました。現在では、x86 から AMD64、いくつかの ARM プラットフォームまで、さまざまなハードウェア プラットフォームをサポートしています。特に、Fiasco のバージョン (Fiasco-UX) は、Linux 上でユーザー レベルのアプリケーションとして実行できます。

L4/Fiasco は、L4v2 API にいくつかの拡張機能を実装しています。例外 IPC により、カーネルは CPU 例外をユーザー レベルのハンドラー アプリケーションに送信できます。エイリアン スレッドの助けを借りて、システム コールをきめ細かく制御できます。X.2 スタイルの UTCB が追加されました。また、Fiasco には、通信権とカーネル レベルのリソース使用を制御するメカニズムが含まれています。Fiasco では、基本的なユーザー レベルのサービスのコレクション (L4Env という名前) が開発されており、これらを使用することで、現在の Linux バージョン (2019 年 5 月時点では 4.19 ^{[アップデート]}) ( L ⁴ Linuxという名前) を準仮想化できます。

開発はニューサウスウェールズ大学(UNSW)でも行われ、開発者はいくつかの 64 ビット プラットフォーム上に L4 を実装しました。彼らの作業の結果、L4/MIPSとL4/Alphaが生まれ、Liedtke のオリジナル バージョンは後からL4/x86と名付けられました。Liedtke のオリジナル カーネルと同様に、UNSW カーネル (アセンブリと C の混合で記述) は移植性がなく、それぞれがゼロから実装されました。移植性の高い L4Ka::Pistachio のリリースにより、UNSW グループは独自のカーネルを放棄し、高度に調整された L4Ka::Pistachio の移植版を作成することに決めました。これには、報告された中で最も高速なメッセージ パッシングの実装 ( Itaniumアーキテクチャで 36 サイクル) が含まれます。^[8]グループはまた、デバイス ドライバーがユーザー レベルでカーネル内と同様に優れたパフォーマンスを発揮できることを実証し、^[9] x86、ARM、およびMIPSプロセッサー上で動作する、移植性の高い L4 上のLinuxバージョンであるWombat を開発しました。XScaleプロセッサでは、Wombatのコンテキスト切り替えコストはネイティブLinuxに比べて最大50倍低くなります。^[10]

その後、現在NICTA（旧National ICT Australia, Ltd.）にあるUNSWグループがL4Ka::PistachioをNICTA::L4-embeddedという新しいL4バージョンにフォークしました。これは商用組み込みシステムでの使用を目的としたもので、実装上のトレードオフとしてメモリサイズを小さくし、複雑さを軽減することにしました。APIは、リアルタイム応答性を確保するために、ほとんどすべてのシステムコールをプリエンプションポイントを必要としないほど短くするように変更されました。^[11]

2005年11月、NICTAは、 QualcommがモバイルステーションモデムチップセットにNICTAのL4バージョンを導入していると発表しました^[12]。これにより、 2006年後半から販売される携帯電話端末にL4が採用されました。2006年8月、ERTOSのリーダーでUNSW教授のGernot Heiserは、 NICTAと緊密に協力し、商用L4ユーザーをサポートし、 OKL4というブランド名で商用L4の開発をさらに進めるために、 Open Kernel Labs (OK Labs)という会社を設立しました。2008年4月にリリースされたOKL4 μKernelバージョン2.1は、機能ベースのセキュリティを備えたL4の最初の一般提供バージョンでした。 2008年10月にリリースされたOKL4 μKernel 3.0は、 OKL4 μKernelの最後のオープンソースバージョンでした。OK Labs は、Wombat の後継である OK:Linux という準仮想化 Linux や、SymbianOSおよびAndroidの準仮想化バージョンも配布していました。OK Labs は、NICTA からseL4の権利も取得しました。

OKL4の出荷数は2012年初頭に15億を超え、^[4]主にクアルコムの無線モデムチップに搭載されました。その他の展開としては、自動車インフォテインメントシステムなどがあります。^[13]

A7以降のApple Aシリーズプロセッサには、 2006年にNICTAで開発されたL4組み込みカーネルをベースにしたsepOS（Secure Enclave Processor OS）と呼ばれるL4オペレーティングシステム^[14]を実行するSecure Enclaveコプロセッサが含まれています。 ^[15] その結果、L4はAppleシリコンを搭載したMacを含むすべての最新のAppleデバイスに搭載されています。 2015年だけでも、iPhoneの総出荷台数は3億1000万台と推定されています。^[16]

2006年、NICTAグループは、コモンクライテリアなどのセキュリティ要件を満たすのに適した、高度に安全で信頼性の高いシステムの基盤を提供することを目的として、seL4と呼ばれる第3世代マイクロカーネルのゼロからの設計を開始しました。開発は最初からカーネルの形式検証を目指していました。時には矛盾するパフォーマンスと検証の要件を満たしやすくするために、チームはHaskell言語で書かれた実行可能な仕様から始まるミドルアウトソフトウェアプロセスを使用しました。^[17] seL4は、オブジェクトのアクセシビリティに関する形式的な推論を可能にするために、機能ベースのセキュリティアクセス制御を使用しています。

機能的正しさの正式な証明は2009年に完了しました。^[18] この証明は、カーネルの実装が仕様に対して正しいことを保証し、デッドロック、ライブロック、バッファオーバーフロー、算術例外、初期化されていない変数の使用などの実装バグがないことを意味します。seL4は、検証された最初の汎用オペレーティングシステムカーネルであると主張されています。^[18] seL4の研究は、2019 ACM SIGOPS殿堂賞を受賞しました。

seL4はカーネルリソース管理に新しいアプローチを採用しており、^[19]カーネルリソースの管理をユーザーレベルにエクスポートし、ユーザーリソースと同じ機能ベースのアクセス制御を適用します。 Barrelfishでも採用されたこのモデルは、分離特性に関する推論を簡素化し、seL4が整合性と機密性というコアセキュリティ特性を強制するという後の証明を可能にしました。^{[20] NICTAチームは、プログラミング言語}Cから実行可能なマシンコードへの変換の正しさも証明し、コンパイラをseL4の信頼できるコンピューティングベースから外しました。 ^{[21]これは、高レベルのセキュリティ証明がカーネル実行可能ファイルに対して有効であることを意味します。 seL4は、}ハードリアルタイムコンピューティングで使用するための前提条件である、完全で健全な最悪ケース実行時間（WCET）分析 を備えた最初の公開された保護モードOSカーネルでもあります。^[20]

2014年7月29日、NICTAとGeneral Dynamics C4 Systemsは、エンドツーエンドの証明を備えたseL4がオープンソースライセンスの下でリリースされたことを発表しました。^[22] カーネルのソースコードと証明はGNU General Public Licenseバージョン2 （GPLv2）の下でライセンスされており、ほとんどのライブラリとツールはBSD 2条項の下でライセンスされています。2020年4月、seL4の開発と展開を加速するために、 Linux Foundationの傘下にseL4 Foundationが設立されたことが発表されました。^[23]

研究者らは、正式なソフトウェア検証のコストは、従来の「高保証」ソフトウェアの設計コストよりも低いにもかかわらず、はるかに信頼性の高い結果をもたらすと述べています。^[24]具体的には、 seL4の開発中のコード1行のコストは約400米ドルと推定されましたが、従来の高保証システムでは1,000米ドルでした。 ^[25]

国防高等研究計画局（DARPA）の高保証サイバー軍事システム（HACMS）プログラムの下、NICTAはプロジェクトパートナーのロックウェル・コリンズ、ガロア社、ミネソタ大学、ボーイング社と共同で、seL4を使用した高保証ドローンを他の保証ツールやソフトウェアとともに開発し、ボーイング社が開発中のオプションで操縦可能な自律型ボーイングAH-6無人リトルバードヘリコプターへの技術移転を計画している。HACMS技術の最終デモンストレーションは2017年4月にバージニア州スターリングで行われた。 ^[26] DARPAはまた、ジョン・ローンチベリーが開始したプログラムの下、seL4に関連するいくつかの中小企業革新的研究（SBIR）契約に資金を提供している。seL4関連のSBIRを受給した中小企業には、ドーナーワークス、テックショット、ウェアラブル社、リアルタイムイノベーションズ、クリティカルテクノロジーズなどがある。^[27]

2023年10月、NIO社は、同社のseL4ベースのSkyOSオペレーティングシステムが2024年から量産される電気自動車に搭載されると発表した。^[28]

2023年、seL4はACMソフトウェアシステム賞を受賞しました。

Haskellで書かれたOSであるOskerはL4仕様をターゲットにしていましたが、このプロジェクトはマイクロカーネルの研究ではなく、OS開発のための関数型プログラミング言語の使用に主に焦点を当てていました。^[29]

RedoxOS ^[30]はRustベースのオペレーティングシステムであり、これもseL4に触発されており、マイクロカーネル設計を採用しています。

CodeZero ^{[31] は、}仮想化とネイティブOSサービスの実装に重点を置いた組み込みシステム用のL4マイクロカーネルです。GPLライセンス版 [32] と、Nvidia に買収されたB Labs Ltd. によって再ライセンスされ、クローズドソースとして2010年にフォークされたバージョンがあります。^[ 33 ] [ ^{34 ]}

F9マイクロカーネル^{[35]はBSDライセンスのL4実装であり、メモリ保護を備えた深層組み込みデバイス向けの}ARM Cortex-Mプロセッサ専用です。

NOVA OS仮想化アーキテクチャ^[36] は、小規模で信頼できるコンピューティングベースを備えた安全で効率的な仮想化環境^{[37] [38]}の構築に重点を置いた研究プロジェクトです。NOVAは、マイクロハイパーバイザー、ユーザーレベルハイパーバイザー（仮想マシンモニター）、およびその上で実行されるNULと呼ばれる特権のないコンポーネント化されたマルチサーバーユーザー環境で構成されています。NOVAは、ARMv8-Aおよびx86ベースのマルチコアシステムで動作します。

WrmOS ^{[39]はL4マイクロカーネルに基づく}リアルタイムオペレーティングシステムです。カーネル、標準ライブラリ、ネットワークスタックの独自の実装を持ち、ARM、SPARC、x86、x86-64アーキテクチャをサポートしています。WrmOS上で動作する準仮想化Linuxカーネル（w4linux ^[40]）があります。

HeliosはseL4に触発されたマイクロカーネルです。^[41]これはAresオペレーティングシステムの一部であり、x86-64とaarch64をサポートしており、2023年2月現在も活発に開発されています。^[42]

• パイクOS

• Liedtke, ヨッヘン;バートリング、ウルリッヒ。バイエル、ウーヴェ;ハインリヒス、ディートマール。ルーランド、ルドルフ。ザライ、ジュラ（1991年4月）。 「μ-Kernel ベースの OS での 2 年の経験」。ACM SIGOPS オペレーティング システムのレビュー。25 (2): 51–62。土井: 10.1145/122120.122124。S2CID  17602151。
• Liedtke, ヨッヘン;ヘベレン、アンドレアス。パク、ユンホ。ロイター、ラース。ウーリグ、フォルクマール (2000 年 10 月 22 日) 「スタブコードのパフォーマンスが重要になってきています」。システム ソフトウェアによる産業体験に関する第 1 回ワークショップ (WIESS)、カリフォルニア州サンディエゴ、2000 年 10 月の議事録。2006 年 9 月 5 日のオリジナル(PDF)からアーカイブ。2006 年9 月 5 日に取得。(L4カーネルとコンパイラー)
• Cheng, Guanghui; McGuire, Nicholas. L4/Fiasco/L4Linux Kickstart (PDF) .分散 & 組み込みシステム ラボ(レポート). 蘭州大学. 2012 年 3 月 27 日時点のオリジナル(PDF)からアーカイブ。
• Elphinstone, Kevin; Heiser, Gernot (2013 年 11 月)。「L3 から seL4 へ: L4 マイクロカーネルの 20 年間で何を学んだか?」( PDF)。第 24 回 ACM SIGOPS オペレーティング システム原則シンポジウム。米国ペンシルバニア州ファーミントン。pp. 133–150。CiteSeerX 10.1.1.636.9410。doi :  10.1145 / 2517349.2522720。ISBN 978-1-4503-2388-8。L4 設計と実装アプローチの進化

• L4Hq: L4 本部、L4 プロジェクトのコミュニティ サイト。2019 年 10 月 25 日にWayback Machineにアーカイブされました。
• L4 μ-カーネル ファミリ、L4 実装の概要、ドキュメント、プロジェクト
• 公式TUD:OSウィキ
• L4Ka: 実装 L4Ka::Pistachio および L4Ka::Hazelnut
• 公式サイト、seL4
• UNSW: DEC AlphaおよびMIPS アーキテクチャの実装
• OKL4 2008-08-20 にWayback Machineでアーカイブされました: Open Kernel Labs の商用 L4 バージョン 2009-03-19 にWayback Machineでアーカイブされました
• NICTA L4: 研究概要と出版物アーカイブ] 2014-07-17 at the Wayback Machine
• CSIRO の Data61 の Trustworthy Systems Group: seL4 を開発した旧 NICTA グループの現在の本拠地
• Genode オペレーティングシステムフレームワーク: L4 コミュニティの子孫