L4マイクロカーネルファミリー – 日本語百科事典辞書

L4_microkernel_family

L4は、第2世代のマイクロカーネルのファミリーであり、さまざまなタイプのオペレーティングシステム（OS）を実装するために使用されますが、ほとんどの場合、Unixライクなポータブルオペレーティングシステムインターフェイス（POSIX）に準拠したタイプです。
L4マイクロカーネルファミリー
デベロッパー
ヨッヘン・リートケ
で書かれている
アセンブリ言語、次にC、C ++
OSファミリ L4 動作状態
現時点の
ソースモデル
オープンソース、クローズドソース
初回リリース
1993 ; 29年前（1993）
マーケティングターゲット
信頼性の高いコンピューティング
で利用可能プラットフォーム
Intel i386、x86、x86-64、ARM、MIPS、SPARC
カーネルタイプ
マイクロカーネル
ライセンス
ソースコード、証明：GPLv2ライブラリ、ツール： BSD2 -clause 前任者ユーメル
公式ウェブサイト
os .inf .tu-dresden .de / L4
L4は、その前身のマイクロカーネルL3と同様に、ドイツのコンピューター科学者 Jochen Liedtkeによって、以前のマイクロカーネルベースのOSのパフォーマンスの低下への対応として作成されました。Liedtkeは、他の目標ではなく、高性能のために最初から設計されたシステムが、実用的なマイクロカーネルを生み出すことができると感じました。1993年に手作業でコーディングされたInteli386固有のアセンブリ言語コードでの彼の最初の実装は、コンピュータ業界への強い関心を呼び起こしました。 L4は、その導入以来、クロスプラットフォームであり、セキュリティ、分離、および堅牢性を向上させるために開発されました。
L4Ka :: Pistachio（カールスルーエ工科大学）、L4 / MIPS（ニューサウスウェールズ大学（UNSW））、Fiascoなど、元のバイナリL4カーネルアプリケーションバイナリインターフェイス（ABI）とその後継機のさまざまな再実装がありました。（ドレスデン工科大学（TUドレスデン））。このため、L4という名前は一般化されており、Liedtkeの元の実装のみを指すものではなくなりました。これは、L4カーネルインターフェイスとそのさまざまなバージョンを含むマイクロカーネルファミリ全体に適用されるようになりました。
L4は広く展開されています。1つのバリアントであるOpenKernelLabsのOKL4は、数十億のモバイルデバイスで出荷されました。
コンテンツ
1 設計パラダイム
2 歴史
2.1 L3 2.2 L4 2.3 L4Ka::ヘーゼルナッツ 2.4 L4/フィアスコ
3 クロスプラットフォーム
3.1 L4Ka::ピスタチオ 3.2 新しいFiascoバージョン 3.3 ニューサウスウェールズ大学とNICTA
4 商用展開
5 高い保証：seL4
6 その他の研究開発
7 も参照してください
8 参考文献
9 参考文献
10 外部リンク

設計パラダイム
マイクロカーネルの一般的な考え方を指定すると、Liedtkeは次のように述べています。
概念がマイクロカーネル内で許容されるのは、それをカーネルの外に移動する場合、つまり、競合する実装を許可することで、システムに必要な機能の実装が妨げられる場合のみです。
この精神で、L4マイクロカーネルはいくつかの基本的なメカニズムを提供します：アドレス空間（ページテーブルの抽象化とメモリ保護の提供）、スレッドとスケジューリング（実行の抽象化と一時的な保護の提供）、およびプロセス間通信（分離境界を越えた制御された通信）。
L4のようなマイクロカーネルに基づくオペレーティングシステムは、Linuxや旧世代のマイクロカーネルのようなモノリシックカーネルが内部に含むユーザースペースのサーバーとしてサービスを提供します。たとえば、安全なUnixライクなシステムを実装するには、サーバーはMachがカーネル内に組み込んだ権利管理を提供する必要が

歴史
Machなどの第1世代のマイクロカーネルのパフォーマンスが低いため、多くの開発者は1990年代半ばにマイクロカーネルの概念全体を再検討しました。Machで使用されている非同期カーネル内バッファリングプロセス通信の概念は、パフォーマンスが低い主な理由の1つであることが判明しました。これにより、Machベースのオペレーティングシステムの開発者は、ファイルシステムやドライバーなどのタイムクリティカルなコンポーネントをカーネル内に戻すようになりました。これはパフォーマンスの問題をいくらか改善しましたが、真のマイクロカーネルの最小性の概念に明らかに違反しています（そしてそれらの主な利点を浪費しています）。
マッハボトルネックの詳細な分析は、とりわけ、そのワーキングセットが大きすぎることを示しました。IPCコードは不十分な空間的局所性を表現しています。つまり、キャッシュミスが多すぎて、そのほとんどがカーネル内にこの分析により、効率的なマイクロカーネルは、パフォーマンスが重要なコードの大部分が（第1レベルの）キャッシュ（できればキャッシュのごく一部）に収まるように十分に小さくする必要があるという原則が生まれました。

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

L4家系図

L4
L3を使用した経験の後で、Liedtkeは、他のいくつかのMachの概念も見当違いであるという結論に達しました。マイクロカーネルの概念をさらに単純化することにより、彼は主に高性能のために設計された最初のL4カーネルを開発しました。パフォーマンスのすべてのビットを抽出するために、カーネル全体がアセンブリ言語で記述されており、そのIPCはMachのIPCよりも20倍高速でした。このような劇的なパフォーマンスの向上は、オペレーティングシステムではまれなイベントであり、Liedtkeの作業は新しいL4の実装を引き起こし、1996年にLiedtkeが作業を開始したIBMを含む多くの大学や研究機関でL4ベースのシステムに取り組んでいます。ドレスデンとUNSW。IBMのThomasJ.Watson Research Centerで、Liedtkeと彼の同僚は、L4およびマイクロカーネルベースのシステム全般、特にSawmillOSの研究を続けました。

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

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

クロスプラットフォーム
L4Ka::ピスタチオ

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

新しいFiascoバージョン
L4/Fiascoマイクロカーネルも長年にわたって大幅に改善されています。現在、x86からAMD64、そしていくつかのARMプラットフォームに至るまでのいくつかのハードウェアプラットフォームをサポートしています。特に、Fiascoのバージョン（Fiasco-UX）は、Linux上でユーザーレベルのアプリケーションとして実行できます。
L4 / Fiascoは、L4v2APIにいくつかの拡張機能を実装しています。例外IPCを使用すると、カーネルはCPU例外をユーザーレベルのハンドラーアプリケーションに送信できます。エイリアンスレッドの助けを借りて、システムコールをきめ細かく制御することができます。X.2スタイルのUTCBが追加されました。また、Fiascoには、通信権とカーネルレベルのリソース使用を制御するためのメカニズムが含まれています。Fiascoでは、基本的なユーザーレベルのサービスのコレクション（L4Envという名前）が開発されており、現在のLinuxバージョン（2019年5月現在4.19 ）（L 4 Linuxという名前）を準仮想化するために使用されています。

ニューサウスウェールズ大学とNICTA
開発はニューサウスウェールズ大学（UNSW）でも行われ、開発者はいくつかの64ビットプラットフォームにL4を実装しました。彼らの仕事の結果、L4/MIPSとL4/Alphaが生まれ、Liedtkeの元のバージョンは遡及的にL4/x86と名付けられました。Liedtkeの元のカーネルと同様に、UNSWカーネル（アセンブリとCを組み合わせて記述）は移植性がなく、それぞれをゼロから実装しました。移植性の高いL4Ka::Pistachioのリリースに伴い、UNSWグループは独自のカーネルを放棄し、メッセージパッシングの実装がこれまでに報告された中で最速（ Itaniumアーキテクチャで36サイクル）を含む、L4Ka::Pistachioの高度に調整されたポートを作成しました。。このグループは、デバイスドライバーがカーネル内と同等にユーザーレベルで十分に機能することも実証し、 x86、ARM、およびMIPSプロセッサーで実行されるL4上のLinuxの移植性の高いバージョンであるWombatを開発しました。XScaleプロセッサでは、Wombatのコンテキスト切り替えコストはネイティブLinuxの最大50分の1です。
その後、UNSWグループは、NICTA（以前のNational ICT Australia、Ltd .）の新しい家で、L4Ka::PistachioをNICTA:: L4-埋め込みという名前の新しいL4バージョンにフォークしました。名前が示すように、これは商用の組み込みシステムで使用するためのものであり、その結果、実装のトレードオフにより、メモリサイズが小さくなり、複雑さが軽減されました。APIが変更され、ほとんどすべてのシステムコールが十分に短くなり、高いリアルタイム応答性を確保するためにプリエンプションポイントが不要になりました。

商用展開
2005年11月、NICTAは、クアルコムがNICTAのL4バージョンをモバイルステーションモデムチップセットに導入することを発表しました。これにより、2006年後半から販売されている携帯電話の携帯電話でL4が使用されるようになりました。2006年8月、ERTOSのリーダーでUNSWの教授であるGernot Heiserは、 Open Kernel Labs （OK Labs）という会社をスピンアウトし、商用L4ユーザーをサポートしてL4をさらに開発しました。NICTAとの緊密な協力によるOKL4のブランド名での商用利用。2008年4月にリリースされたOKL4バージョン2.1は、機能ベースのセキュリティを備えたL4の最初の一般提供バージョンでした。2008年10月にリリースされたOKL43.0は、OKL4の最後のオープンソースバージョンでした。最近のバージョンはクローズドソースであり、OKL4マイクロバイザーという名前のネイティブハイパーバイザーバリアントをサポートするための書き直しに基づいています。OK Labsは、Wombatの子孫であるOK：Linuxという名前の準仮想化Linuxと、SymbianOSおよびAndroidの準仮想化バージョンも配布しました。OK Labsは、 NICTAからseL4の権利も取得しました。
OKL4の出荷は2012年の初めに15億を超え、主にQualcommワイヤレスモデムチップで行われました。その他の展開には、自動車のインフォテインメントシステムが含まれます。
A7以降のAppleAシリーズプロセッサには、2006年にNICTAで開発されたL4組み込みカーネルに基づくL4オペレーティングシステムを実行するSecure Enclaveコプロセッサが含まれています。これは、L4がすべてのiOSデバイスで出荷されていることを意味します。 2015年の総出荷量は3億1000万と推定されています。

高い保証：seL4
2006年、NICTAグループは、コモンクライテリア以降のセキュリティ要件を満たすのに適した、安全性と信頼性の高いシステムの基盤を提供することを目的として、seL4という名前の第3世代マイクロカーネルのゼロからの設計を開始しました。当初から、開発はカーネルのフォーマル検証を目的としていました。時々矛盾するパフォーマンスと検証の要件を満たすのを容易にするために、チームはHaskellで書かれた実行可能仕様から始まるミドルアウトソフトウェアプロセスを使用しました。 seL4は、機能ベースのセキュリティアクセス制御を使用して、オブジェクトのアクセシビリティに関する正式な推論を可能にします。
機能の正当性の正式な証明は2009年に完了しました。証明は、カーネルの実装がその仕様に対して正しいことを保証し、デッドロック、ライブロック、バッファオーバーフロー、算術例外などの実装バグがないことを意味します。初期化されていない変数の使用。seL4は、検証された初めての汎用オペレーティングシステムカーネルであると主張されています。
seL4は、カーネルリソース管理に新しいアプローチを採用し、カーネルリソースの管理をユーザーレベルにエクスポートし、ユーザーリソースと同じ機能ベースのアクセス制御を適用します。このモデルは、Barrelfishでも採用されており、分離プロパティに関する推論を簡素化し、seL4が整合性と機密性のコアセキュリティプロパティを実施することを後で証明するためのイネーブラーでした。 NICTAチームは、プログラミング言語Cから実行可能マシンコードへの変換が正しいことも証明し、コンパイラをseL4のトラステッドコンピューティングベースから除外しました。これは、カーネル実行可能ファイルに対して高レベルのセキュリティ証明が保持されることを意味します。seL4は、ハードリアルタイムコンピューティングで使用するための前提条件である、完全で健全な最悪実行時間（WCET）分析を備えた最初に公開されたプロテクトモードOSカーネルでも
2014年7月29日、NICTAとGeneral Dynamics C4 Systemsは、エンドツーエンドのプルーフを備えたseL4がオープンソースライセンスでリリースされたことを発表しました。カーネルのソースコードとプルーフはGNUGeneralPublic Licenseバージョン2（GPLv2）の下でライセンスされており、ほとんどのライブラリとツールはBSD2条項の下に2020年4月、seL4の開発と展開を加速するために、LinuxFoundationの傘下でseL4Foundationが設立されたことが発表されました。
研究者は、正式なソフトウェア検証のコストは、はるかに信頼性の高い結果を提供するにもかかわらず、従来の「高保証」ソフトウェアのエンジニアリングのコストよりも低いと述べています。具体的には、seL4の開発中の1行のコードのコストは、従来の高保証システムの1，000米ドルと比較して、約400米ドルと見積もられました。
防衛先端研究プロジェクト庁（DARPA）の高保証サイバー軍事システム（HACMS）プログラムの下で、NICTAはプロジェクトパートナーのロックウェルコリンズ、ガロアインク、ミネソタ大学、ボーイングとともに、seL4を使用した高保証ドローンを開発しました。保証ツールとソフトウェア、ボーイングが開発中のオプションで操縦される自律型ボーイングAH-6無人リトルバードヘリコプターへの計画的な技術移転。HACMSテクノロジーの最終デモンストレーションは、2017年4月にバージニア州スターリングで行われました。 DARPAは、ジョン・ラウンチベリー博士が開始したプログラムの下で、seL4に関連するいくつかの中小企業革新研究（SBIR）契約にも資金を提供しました。seL4関連のSBIRを受け取っている中小企業には、DornerWorks、Techshot、Wearable Inc、Real Time Innovations、CriticalTechnologiesが含まれます。

その他の研究開発
Haskellで書かれたOSであるOskerは、L4仕様を対象としていました。このプロジェクトは主にOS開発のための関数型プログラミング言語の使用に焦点を合わせていましたが、マイクロカーネルの研究には焦点を当てていませんでした。
CodeZero は、ネイティブOSサービスの仮想化と実装に重点を置いた組み込みシステム用のL4マイクロカーネルです。GPLライセンスバージョンと、 Nvidiaによって買収され、2010年にフォークされたBLabsLtd .によって再ライセンスされたバージョンが
F9マイクロカーネル BSDライセンスのL4実装は、メモリ保護を備えた深く組み込まれたデバイス用のARMCortex-Mプロセッサ専用です。
NOVA OS仮想化アーキテクチャは、小規模なトラステッドコンピューティングベースを備えた安全で効率的な仮想化環境の構築に焦点を当てた研究プロジェクトです。NOVAは、マイクロハイパーバイザー、ユーザーレベルのハイパーバイザー（仮想マシンモニター）、およびNULという名前で実行されている非特権のコンポーネント化されたマルチサーバーユーザー環境で構成されます。NOVAは、ARMv8-Aおよびx86ベースのマルチコアシステムで実行されます。
WrmOS は、L4マイクロカーネルに基づくリアルタイムオペレーティングシステムです。カーネル、標準ライブラリ、およびネットワークスタックの独自の実装があり、ARM、SPARC、x86、およびx86-64アーキテクチャをサポートしています。WrmOSで動作する準仮想化Linuxカーネル（w4linux ）が

も参照してください
PikeOS

参考文献
^ 「ハイパーバイザー製品：一般的なダイナミクスミッションシステム」。ジェネラルダイナミクスミッションシステムズ。2017年11月15日にオリジナルからアーカイブされました。
^ 「OpenKernelLabsソフトウェアが15億のモバイルデバイス出荷のマイルストーンを超える」（プレスリリース）。KernelLabsを開きます。2012年1月19日。2012年2月11日のオリジナルからアーカイブ。
^ Liedtke、Jochen（1995年12月）。「µカーネル構築について」。Proceedings 15th ACM Symposium on Operating Systems Principles（SOSP）。pp。237–250。2015年10月25日にオリジナルからアーカイブされました。
^ Liedtke、Jochen（1993年12月）。「カーネル設計によるIPCの改善」。オペレーティングシステムの原則に関する第14回ACMシンポジウム。米国ノースカロライナ州アッシュビル。pp。175–188。
^ Gefflaut、Alain; イエーガー、トレント; パク、ユンホ; リートケ、ヨッヘン; エルフィンストーン、ケビン; Uhlig、Volkmar; Tidswell、Jonathon; デラー、ルーク; Reuther、Lars（2000）。「Sawmillマルチサーバーアプローチ」。ACMSIGOPSヨーロッパワークショップ。コリング、デンマーク。pp。109–114。
^ 「DROPS-概要」。ドレスデン工科大学。2011年8月7日にオリジナルからアーカイブされました。
^ l4ka.org：L4Ka :: Pistachioマイクロカーネル引用：「…サポートされているアーキテクチャの多様性により、L4Ka::Pistachioはさまざまなシステムの理想的な研究開発プラットフォームになっています…」
^ グレイ、チャールズ; チャップマン、マシュー; チャブ、ピーター; Mosberger-Tang、David; ハイザー、ゲルノート。「Itanium：システム実装者の話」。USENIX年次技術会議。米国カリフォルニア州アナハイム。pp。264–278。2007年2月17日にオリジナルからアーカイブされました。
^ レスリー、ベン; チャブ、ピーター; FitzRoy-Dale、ニコラス; ゲッツ、ステファン; グレイ、チャールズ; マクファーソン、ルーク; ポッツ、ダニエル; シェン、ユエティン; エルフィンストーン、ケビン; ハイザー、ゲルノート。「ユーザーレベルのデバイスドライバー：達成されたパフォーマンス」。コンピュータサイエンスとテクノロジーのジャーナル。20（5）：654–664。CiteSeerX10.1.1.59.6766。_ 土井：10.1007/s11390-005-0654-4。S2CID1121537。_

^ van Schaik、Carl; ハイザー、ゲルノート。「ARMおよびセグメント化されたアーキテクチャでの高性能マイクロカーネルと仮想化」。組み込みシステム用マイクロカーネルに関する第1回国際ワークショップ。オーストラリア、シドニー：NICTA。pp。11–21。2015年3月1日にオリジナルからアーカイブされました。
^ Ruocco、Sergio。「汎用L4マイクロカーネルのリアルタイムプログラマーツアー」。組み込みシステムに関するEURASIPジャーナル。2008：1–14。土井：10.1155/2008/234710。S2CID7430332。_
^ 「一部のQUALCOMMチップセットソリューションで利用されるNICTAL4マイクロカーネル」（プレスリリース）。NICTA。2005年11月24日。2006年8月25日のオリジナルからアーカイブ。
^ 「インフォテインメントシステム用にボッシュが選択したOpenKernelLabsの自動車用仮想化」（プレスリリース）。KernelLabsを開きます。2012年3月27日。2012年7月2日のオリジナルからアーカイブ。
^ 「iOSセキュリティ、iOS 12.3」（PDF）。AppleInc.2019年5月。
^ Mandt、Tarjei; ソルニック、マシュー; 王、デビッド（2016年7月31日）。「セキュアエンクレーブプロセッサの謎を解く」（PDF）。BlackHatUSA。ラスベガス、ネバダ、米国。2016年10月21日のオリジナルからアーカイブ（PDF）。
^ Elmer-DeWitt、Philip（2014年10月28日）。「予測：Appleは2015年に3億1000万台のiOSデバイスを出荷する」。フォーチュン。2015年9月27日にオリジナルからアーカイブされました。
^ デリン、フィリップ; エルフィンストーン、ケビン; クライン、ガーウィン; コック、デビッド; Chakravarty、Manuel MT。「マニュアルの実行：高保証マイクロカーネル開発へのアプローチ」。ACMSIGPLANHaskellワークショップ。オレゴン州ポートランド。pp。60–71。
^ Klein、Gerwin; エルフィンストーン、ケビン; ハイザー、ゲルノート; アンドロニック、6月; コック、デビッド; デリン、フィリップ; Elkaduwe、Dhammika; エンゲルハルト、カイ; コランスキー、ラファル; ノリッシュ、マイケル; シューエル、トーマス; Tuch、Harvey; ウィンウッド、サイモン。「seL4：OSカーネルのフォーマル検証」（PDF）。オペレーティングシステムの原則に関する第22回ACMシンポジウム。ビッグスカイ、モンタナ州、米国。2011年7月28日のオリジナルからアーカイブ（PDF）。
^ Elkaduwe、Dhammika; デリン、フィリップ; エルフィンストーン、ケビン。物理メモリの分離と保証のためのカーネル設計。組み込みシステムの分離と統合に関する第1回ワークショップ。グラスゴー、英国。土井：10.1145/1435458 。
^ Klein、Gerwin; アンドロニック、6月; エルフィンストーン、ケビン; マレー、トビー; シューエル、トーマス; コランスキー、ラファル; ハイザー、ゲルノート。「OSマイクロカーネルの包括的フォーマル検証」。コンピュータシステムでのACMトランザクション。32（1）：2：1–2：70。CiteSeerX10.1.1.431.9140。_ 土井：10.1145/2560537。S2CID4474342。_

^ シューエル、トーマス; Myreen、Magnus; クライン、ガーウィン。「検証済みOSカーネルの翻訳検証」。プログラミング言語の設計と実装に関するACMSIGPLAN会議。米国ワシントン州シアトル。土井：10.1145/2491956.2462183。
^ 「NICTAによって開発された安全なオペレーティングシステムはオープンソースになります」（プレスリリース）。NICTA。2014年7月29日。2016年3月15日のオリジナルからアーカイブ。
^ 「セキュリティはLinuxFoundationのサポートを取得します」（プレスリリース）。LinuxFoundation。2020年4月7日。2016年3月15日のオリジナルからアーカイブ。
^ クライン、ガーウィン; アンドロニック、6月; エルフィンストーン、ケビン; マレー、トビー; シューエル、トーマス; コランスキー、ラファル; ハイザー、ゲルノート（2014）。「OSマイクロカーネルの包括的フォーマル検証」（PDF）。コンピュータシステムでのACMトランザクション。32：64。CiteSeerX10.1.1.431.9140。_ 土井：10.1145/2560537。S2CID4474342。_ 2014年8月3日のオリジナルからアーカイブ（PDF）。    ^ ハイザー、ゲルノート（2015年1月16日）。seL4は無料です：これはあなたにとって何を意味しますか？。ニュージーランド、オークランド：Linux.conf.au。
^ 「DARPAはサイバーセキュリティ技術を新しいプラットフォームに適用するためにロックウェルコリンズを選択しました」（プレスリリース）。ロックウェル・コリンズ。2017年4月24日。2017年5月11日のオリジナルからアーカイブ。
^ 「DARPAエージェンシースポンサーのジョン・ラウンチベリー博士」。SBIRSource。2017年。 2017年9月29日のオリジナルからアーカイブ。
^ Hallgren、T .; ジョーンズ、MP; レスリー、R .; トルマック、A。（2005）。「Haskellでのオペレーティングシステム構築への原則的なアプローチ」（PDF）。関数型プログラミングに関する第10回ACMSIGPLAN国際会議の議事録。40（9）：116–128。土井：10.1145/1090189.1086380。ISSN0362-1340。_ 2010年6月15日のオリジナルからアーカイブ（PDF）。 ^ 「発表：Codezeroの紹介」。ドレスデン工科大学。
^ “”jserv / codezero：Codezeroマイクロカーネル”。GitHub。2015年8月15日にオリジナルからアーカイブされました。
^ 「コードゼロ：組み込みハイパーバイザーとOS」。2016年1月11日にオリジナルからアーカイブされました。
^ 「アーカイブされたコピー」。2014年2月2日にオリジナルからアーカイブされました。
^ 「F9マイクロカーネル」。GitHub。
^ 「NOVAマイクロハイパーバイザーのウェブサイト」。
^ スタインバーグ、ウド; カウアー、ベルンハルト。「NOVA：マイクロハイパーバイザーベースの安全な仮想化アーキテクチャ」。EuroSys ’10：コンピュータシステムに関する第5回欧州会議の議事録。パリ、フランス。
^ スタインバーグ、ウド; カウアー、ベルンハルト。「スケーラブルなマルチプロセッサユーザーレベル環境に向けて」。IIDS’10：信頼できるシステムの分離と統合に関するワークショップ。パリ、フランス。
^ 「WrmOS」。
^ 「w4linuxはWrmOSで動作する準仮想化Linuxカーネルです」。

参考文献
リートケ、ヨッヘン; バートリング、ウルリッヒ; Beyer、Uwe; ハインリッヒ、ディートマー; ルーランド、ルドルフ; Szalay、Gyula（1991年4月）。「μカーネルベースのOSでの2年の経験」。ACMSIGOPSオペレーティングシステムレビュー。25（2）：51–62。土井：10.1145/122120.122124。
リートケ、ヨッヘン; ヘーバーレン、アンドレアス; パク、ユンホ; Reuther、Lars; Uhlig、Volkmar（2000年10月22日）。「スタブコードのパフォーマンスが重要になりつつあります」。2000年10月、カリフォルニア州サンディエゴで開催された、システムソフトウェアの産業経験に関する第1回ワークショップ（WIESS）の議事録。2006年9月5日にオリジナル（PDF）からアーカイブされました。（L4カーネルおよびコンパイラー上）
チェン、広慧; マクガイア、ニコラス。L4 / Fiasco / L4Linuxキックスタート（PDF）。分散および組み込みシステムラボ（レポート）。蘭州大学。2012年3月27日にオリジナル（PDF）からアーカイブされました。
エルフィンストーン、ケビン; ハイザー、ゲルノート。「L3からseL4へ：20年間のL4マイクロカーネルで何を学んだか？」（PDF）。オペレーティングシステムの原則に関する第24回ACMSIGOPSシンポジウム。米国ペンシルベニア州ファーミントン。pp。133–150。CiteSeerX10.1.1.636.9410 。_ 土井：10.1145/2517349.2522720。ISBN 978-1-4503-2388-8。L4の設計と実装のアプローチの進化

外部リンク
L4Hq：L4本社、L4プロジェクトのコミュニティサイトWaybackMachineで2019-10-25にアーカイブ
公式サイト、seL4
L4マイクロカーネルファミリー、L4実装の概要、ドキュメント、プロジェクト
公式TUD：OS Wiki
L4Ka：実装L4Ka::PistachioおよびL4Ka::Hazelnut
UNSW：DECAlphaおよびMIPSアーキテクチャの実装
OKL4アーカイブ2008-08-20ウェイバックマシン：OpenKernelLabsの商用L4バージョンアーカイブ2009-03-19ウェイバックマシン
NICTA L4 ：研究の概要とアーカイブされた出版物]ウェイバックマシンでの2014-07-17
CSIROのData61の信頼できるシステムグループ：seL4を開発した元NICTAグループの現在の家
Genodeオペレーティングシステムフレームワーク：L4コミュニティの子孫”