Loading article…
L4は、第2世代のマイクロカーネルのファミリーであり、さまざまな種類のオペレーティングシステム（OS）を実装するために使用されますが、主にUnix系で、POSIX（Portable Operating System Interface）に準拠したタイプのOSに使用されます。
L4 は、前身のマイクロカーネルL3と同様に、ドイツのコンピュータ科学者ヨッヘン・リートケによって、以前のマイクロカーネルベースの OS のパフォーマンスの悪さへの対応として作成されました。リートケは、他の目標ではなく、最初から高性能を目的に設計されたシステムであれば、実用的なマイクロカーネルが作れると考えました。1993年に彼が手作業でコーディングした Intel i386専用のアセンブリ言語コードによる最初の実装は、 Machより 20 倍高速であったため注目を集めました。[ 2 ] 2 年後の続編の発表[ 3 ]は非常に影響力があるとみなされ、2015 年のACM SIGOPS殿堂賞を受賞しました。L4 は、導入以来、クロス プラットフォーム化とセキュリティ、分離、堅牢性の向上を目指して開発されてきました。
オリジナルのL4カーネルアプリケーションバイナリインターフェース（ABI）とその後継となるものには、L4Ka::Pistachio（カールスルーエ工科大学のLiedtke氏とその学生によって実装）、L4/MIPS（ニューサウスウェールズ大学（UNSW））、Fiasco（ドレスデン工科大学（TU Dresden））など、さまざまな再実装版が存在する。そのため、 L4という名称は一般化され、もはやLiedtke氏のオリジナル実装だけを指すものではなくなった。現在では、 L4カーネルインターフェースとそのさまざまなバージョンを含むマイクロカーネルファミリー全体を指すようになっている。
L4は広く普及している。Open Kernel LabsのOKL4という派生版は、数十億台のモバイルデバイスに搭載されている。[ 4 ] [ 5 ]
マイクロカーネルの一般的な概念を説明するにあたり、リートケは次のように述べている。
マイクロカーネル内で概念が許容されるのは、それをカーネルの外に移動させる、つまり競合する実装を許可すると、システムの要求される機能の実装が妨げられる場合に限られる。[ 3 ]
この精神に基づき、L4マイクロカーネルはいくつかの基本的なメカニズムを提供します。アドレス空間（ページテーブルの抽象化とメモリ保護の提供）、スレッドとスケジューリング（実行の抽象化と時間的保護の提供）、およびプロセス間通信（分離境界を越えた制御された通信のため）です。
L4のようなマイクロカーネルをベースとしたオペレーティングシステムは、Linuxのようなモノリシックカーネルや旧世代のマイクロカーネルが内部的に組み込んでいるサービスを、ユーザー空間でサーバーとして提供します。例えば、セキュアなUnixライクなシステムを実装するには、サーバーはMachがカーネル内に組み込んだ権限管理機能を提供する必要があります。
Machなどの第一世代マイクロカーネルの性能の低さから、1990年代半ばには多くの開発者がマイクロカーネルの概念全体を見直すことになった。Machで採用されていた非同期カーネル内バッファリングプロセス間通信の概念が、その性能の低さの主な原因の一つであることが判明した。このため、Machベースのオペレーティングシステムの開発者は、ファイルシステムやドライバといった時間制約の厳しいコンポーネントの一部をカーネル内部に戻すことを余儀なくされた。この変更によって性能の問題は多少改善されたものの、真のマイクロカーネルの最小性という概念に明らかに反しており、その大きな利点を無駄にしている。
Machのボトルネックの詳細な分析から、とりわけワーキングセットが大きすぎることが示されました。IPCコードは空間的局所性が低く、キャッシュミスが多すぎ、そのほとんどはカーネル内です。[ 3 ]この分析から、効率的なマイクロカーネルは、パフォーマンスが重要なコードの大部分が（第1レベルの）キャッシュに収まるほど小さくなければならない（できればキャッシュのごく一部）という原則が生まれました。
ヨッヘン・リートケは、パフォーマンスとマシン固有の設計（クロスプラットフォームソフトウェアとは対照的に）に細心の注意を払った、適切に設計されたより薄いプロセス間通信（IPC ）レイヤーが、実際のパフォーマンスを大幅に向上させることができることを証明しようとしました。Machの複雑なIPCシステムの代わりに、彼のL3マイクロカーネルは、追加のオーバーヘッドなしにメッセージを単純に渡しました。必要なセキュリティポリシーの定義と実装は、ユーザースペースサーバーの責務とみなされました。カーネルの役割は、ユーザーレベルのサーバーがポリシーを適用できるようにするために必要なメカニズムを提供するだけでした。1988年に開発されたL3は、安全で堅牢なオペレーティングシステムであることが証明され、例えば技術検査協会（ Technischer Überwachungsverein ）によって長年使用されました。
L3 の使用経験を経て、Liedtke は Mach の他のいくつかの概念も誤っているという結論に至った。マイクロカーネルの概念をさらに単純化することで、主に高性能を目的とした最初の L4 カーネルを開発した。パフォーマンスを最大化するために、カーネル全体がアセンブリ言語で記述され、その IPC は Mach の 20 倍高速だった。[ 2 ]このような劇的なパフォーマンス向上はオペレーティングシステムではまれな出来事であり、Liedtke の研究は、 IBM (Liedtke が 1996 年に働き始めた会社)、ドレスデン工科大学、ニューサウスウェールズ大学など、多くの大学や研究機関で新しい L4 実装や L4 ベースのシステムに関する研究を促した。IBM のThomas J. Watson Research Centerで、 Liedtke と彼の同僚は、特に Sawmill OS など、L4 およびマイクロカーネルベースのシステム全般に関する研究を続けた。[ 6 ]
1999年、リートケはカールスルーエ大学のシステムアーキテクチャグループを引き継ぎ、マイクロカーネルシステムの研究を継続した。高性能マイクロカーネルを高水準言語でも構築できるという概念実証として、グループはIA-32およびARMベースのマシンで動作するC ++版カーネルであるL4Ka::Hazelnutを開発した。この取り組みは成功し、性能も許容範囲内であったため、そのリリースにより、純粋なアセンブリ言語版カーネルは事実上廃止された。
L4Ka::Hazelnut の開発と並行して、1998 年にドレスデン工科大学のオペレーティングシステムグループ TUD:OS は、L4/Fiasco と呼ばれる独自の C++ による L4 カーネルインターフェースの実装の開発を開始しました。カーネル内での並行処理を一切許可しない L4Ka::Hazelnut や、カーネル内で特定のプリエンプションポイントでのみ割り込みを許可する後継の L4Ka::Pistachio とは対照的に、L4/Fiascoは割り込みレイテンシを低く抑えるために、（極めて短いアトミック操作を除いて）完全にプリエンプティブでした。これは、L4/Fiasco が同じくドレスデン工科大学で開発されたハードリアルタイムコンピューティング対応オペレーティングシステムである DROPS [ 7 ]の基盤として使用されているため、必要であると考えられました。しかし、完全にプリエンプティブな設計の複雑さから、Fiasco の後のバージョンでは、限られた数のプリエンプションポイントを除いて割り込みを無効にしてカーネルを実行するという従来の L4 のアプローチに戻ることになりました。
L4Ka::Pistachio と Fiasco の新しいバージョンがリリースされるまで、すべての L4 マイクロカーネルは、基盤となる CPU アーキテクチャに密接に結びついていました。L4 開発における次の大きな転換点は、移植性が向上したにもかかわらず、高いパフォーマンス特性を維持したクロスプラットフォーム (プラットフォーム非依存) アプリケーション プログラミング インターフェイス ( API ) の開発でした。カーネルの基本的な概念は同じでしたが、新しい API は、マルチ プロセッサ システムのサポートの向上、スレッドとアドレス空間間の結びつきの緩和、ユーザー レベルのスレッド制御ブロック (UTCB) と仮想レジスタの導入など、以前の L4 バージョンと比較して多くの重要な変更をもたらしました。2001 年初頭に新しい L4 API (バージョン X.2、別名バージョン 4) をリリースした後、カールスルーエ大学のシステム アーキテクチャ グループが、パフォーマンスと移植性の両方に重点を置いた新しいカーネルL4Ka::Pistachioをゼロから完全に実装しました。これは、2 条項 BSD ライセンスの下でリリースされました。[ 8 ]
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) を準仮想化するために使用されます。 （L4Linuxと名付けられました）。
ニューサウスウェールズ大学(UNSW)でも開発が行われ、開発者たちは複数の 64 ビット プラットフォームで L4 を実装しました。彼らの作業の結果、L4/MIPSとL4/Alphaが生まれ、Liedtke のオリジナル バージョンは後からL4/x86と名付けられました。Liedtke のオリジナル カーネルと同様に、UNSW のカーネル (アセンブリ言語と C 言語の混在で記述) は移植性がなく、それぞれゼロから実装されました。移植性の高い L4Ka::Pistachio のリリースに伴い、UNSW グループは独自のカーネルを放棄し、L4Ka::Pistachio の高度にチューニングされたポートの作成に注力しました。これには、これまで報告された中で最速のメッセージ パッシングの実装 ( Itaniumアーキテクチャで 36 サイクル) が含まれています。[ 9 ]また、このグループは、デバイス ドライバがカーネル内と同様にユーザー レベルでも十分に機能することを実証し、 [ 10 ] x86、ARM、MIPSプロセッサで動作する L4 上のLinuxの移植性の高いバージョンであるWombat を開発しました。XScaleプロセッサでは、WombatのコンテキストスイッチングコストはネイティブLinuxよりも最大50倍低い。[ 11 ]
その後、現在NICTA（旧National ICT Australia, Ltd.）に所属するUNSWグループは、L4Ka::PistachioをフォークしてNICTA::L4-embeddedという新しいL4バージョンを作成しました。これは商用組み込みシステムで使用するためのもので、そのため実装上のトレードオフではメモリサイズの縮小と複雑さの軽減が優先されました。APIは、リアルタイム応答性を高めるためにプリエンプションポイントを必要としないほどほぼすべてのシステムコールを短くするように変更されました。[ 12 ]
2005 年 11 月、NICTA は[ 13 ] Qualcomm がNICTA の L4 バージョンをモバイル ステーション モデムチップセットに展開していることを発表しました。これにより、2006 年後半から販売される携帯電話端末で L4 が使用されるようになりました。2006 年 8 月、ERTOS のリーダーであり UNSW の教授であるGernot Heiser は、商用 L4 ユーザーをサポートし、NICTA と緊密に協力してOKL4というブランド名で商用利用向けの L4 をさらに開発するために、Open Kernel Labs (OK Labs) という会社をスピンアウトしました。2008 年 4 月にリリースされたOKL4 μKernelバージョン 2.1 は、機能ベースのセキュリティを特徴とする L4 の最初の一般利用可能なバージョンでした。2008 年 10 月にリリースされた OKL4 μKernel 3.0 は、OKL4 μKernel の最後のオープンソース バージョンでした。それ以降のバージョンはクローズド ソースであり、 OKL4 Microvisorと呼ばれるネイティブ ハイパーバイザのバリアントをサポートするために書き直されています。 OK Labsは、Wombatの派生版である準仮想化Linux「OK:Linux」や、SymbianOSおよびAndroidの準仮想化バージョンも配布した。また、OK LabsはNICTAからseL4の権利を取得した。
OKL4の出荷数は2012年初頭に15億個を超え[ 5 ] 、そのほとんどはクアルコムの無線モデムチップに搭載されている。その他の用途としては、車載インフォテインメントシステムなどがある[ 14 ] 。
Apple Aシリーズプロセッサ（ A7以降）には、2006年にNICTAで開発されたL4組み込みカーネル[16]をベースとしたsepOS（Secure Enclave Processor OS）と呼ばれるL4オペレーティングシステム[15]を実行するSecure Enclaveコプロセッサが搭載されています。その結果、 Appleシリコン搭載のMacを 含むすべての最新のAppleデバイスにL4が搭載されています。 2015年だけでも、iPhoneの総出荷台数は3億1000万台と推定されています[ 17 ]。
2006年、NICTAグループは、共通基準などのセキュリティ要件を満たすのに適した、高度に安全で信頼性の高いシステムの基盤を提供することを目的として、seL4という名の第3世代マイクロカーネルのゼロからの設計を開始しました。開発は当初からカーネルの形式検証を目指していました。パフォーマンスと検証という、時に相反する要件を満たしやすくするために、チームはHaskell言語で書かれた実行可能な仕様から始まるミドルアウトソフトウェアプロセスを使用しました。[ 18 ] seL4は、オブジェクトのアクセス可能性に関する形式的推論を可能にするために、能力ベースのセキュリティアクセス制御を使用しています。
機能的正当性の正式な証明は2009 年に完了しました。[ 19 ] この証明は、カーネルの実装が仕様に対して正しいことを保証し、デッドロック、ライブロック、バッファオーバーフロー、算術例外、未初期化変数の使用などの実装上のバグがないことを意味します。seL4 は、検証済みの史上初の汎用オペレーティングシステムカーネルであるとされています。[ 19 ] seL4 に関する作業は、2019 年のACM SIGOPS殿堂賞を受賞しました。
seL4 はカーネル リソース管理に斬新なアプローチを採用しており、[ 20 ]カーネル リソースの管理をユーザー レベルにエクスポートし、ユーザー リソースと同じ機能ベースのアクセス制御を適用しています。このモデルはBarrelfishでも採用されており、分離特性に関する推論を簡素化し、seL4 が完全性と機密性というコア セキュリティ特性を強制するという後の証明を可能にしました。[ 21 ] NICTA チームはまた、プログラミング言語Cから実行可能なマシン コードへの変換の正しさを証明し、コンパイラをseL4 の信頼できるコンピューティング ベースから除外しました。 [ 22 ] これは、高レベルのセキュリティ証明がカーネル実行可能ファイルにも適用されることを意味します。seL4 はまた、完全かつ健全な最悪ケース実行時間(WCET) 分析を備えた、公開された最初の保護モード OS カーネルであり、ハードリアルタイム コンピューティングでの使用の前提条件となっています。[ 21 ]
2014 年 7 月 29 日、NICTAとGeneral Dynamics C4 Systems は、エンドツーエンドの証明付きの seL4 がオープンソース ライセンスの下でリリースされたことを発表しました。[ 23 ] カーネルソース コードと証明はGNU General Public License バージョン 2 (GPLv2)の下でライセンスされており、ほとんどのライブラリとツールはBSD 2 条項の下でライセンスされています。2020 年 4 月には、seL4 の開発と展開を加速するために、 Linux Foundationの傘下に seL4 Foundation が設立されたことが発表されました。[ 24 ]
研究者らは、形式的ソフトウェア検証のコストは、従来の「高信頼性」ソフトウェアを設計するコストよりも低いにもかかわらず、はるかに信頼性の高い結果が得られると述べている。[ 25 ]具体的には、 seL4 の開発中のコード1 行のコストは約400 米ドルと見積もられており、従来の高信頼性システムの1,000 米ドルと比較すると低い。 [ 26 ]
国防高等研究計画局 ( DARPA ) の高信頼性サイバー軍事システム (HACMS) プログラムの下で、NICTA はプロジェクト パートナーのRockwell Collins、Galois Inc、ミネソタ大学、Boeingと共に、seL4 を使用した高信頼性ドローンを他の保証ツールやソフトウェアと共に開発し、Boeing が開発中のオプションで有人操縦可能な自律型Boyengine AH-6無人リトルバード ヘリコプターへの技術移転を計画した。HACMS 技術の最終デモンストレーションは、2017 年 4 月にバージニア州スターリングで行われた。[ 27 ] DARPA はまた、John Launchburyが開始したプログラムの下で seL4 に関連する中小企業革新研究(SBIR) 契約にいくつか資金を提供した。seL4 関連の SBIR を受けた中小企業には、DornerWorks、Techshot、Wearable Inc、Real Time Innovations、Critical Technologies などがある。[ 28 ]
2023年10月、Nio Inc.は、seL4ベースのSkyOSオペレーティングシステムが2024年から量産電気自動車に搭載されると発表した。[ 29 ]
2023年、seL4はACMソフトウェアシステム賞を受賞しました。
Haskellで書かれたOSであるOskerはL4仕様をターゲットとしていましたが、このプロジェクトは主にOS開発のための関数型プログラミング言語の使用に焦点を当てており、マイクロカーネルの研究には焦点を当てていませんでした。[ 30 ]
RedoxOS [ 31 ]は Rust ベースのオペレーティングシステムで、seL4 にも影響を受けており、マイクロカーネル設計を採用しています。
CodeZero [ 32 ]は、仮想化とネイティブ OS サービスの実装に重点を置いた組み込みシステム向けの L4 マイクロカーネルです。GPLライセンス版[ 33 ]と、 Nvidiaに買収された B Labs Ltd. によって再ライセンスされ、クローズド ソースとして 2010 年にフォークされたバージョンがあります。 [ 34 ] [ 35 ]
F9マイクロカーネル[ 36 ]はBSDライセンスのL4実装であり、メモリ保護機能を備えた組み込みデバイス向けのARM Cortex-Mプロセッサ専用です。
NOVA OS仮想化アーキテクチャ[ 37 ]は 、小規模な信頼できるコンピューティングベースを備えた安全で効率的な仮想化環境[ 38 ] [ 39 ]の構築に焦点を当てた研究プロジェクトです。NOVAは、マイクロハイパーバイザ、ユーザーレベルハイパーバイザ（仮想マシンモニタ）、およびその上で動作するNULという名前の非特権コンポーネント化されたマルチサーバーユーザー環境で構成されています。NOVAは、ARMv8-Aおよびx86ベースのマルチコアシステムで動作します。
WrmOS [ 40 ]は、L4 マイクロカーネルをベースとしたリアルタイムオペレーティングシステムです。独自のカーネル、標準ライブラリ、ネットワークスタックの実装を持ち、ARM、SPARC、x86、x86-64 アーキテクチャをサポートしています。WrmOS 上では、準仮想化 Linux カーネル (w4linux [ 41 ] ) が動作します。
HeliosはseL4に触発されたマイクロカーネルです。[ 42 ]これはAresオペレーティングシステムの一部であり、x86-64とaarch64をサポートし、2023年2月現在も活発に開発されています。[ 43 ]
{{cite journal}}: CS1メンテナンス: DOIは2025年7月現在非アクティブです（リンク）