Wikipedia

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

L4マイクロカーネルファミリーは第二世代マイクロカーネルのファミリーで、一般的にはUnix系のオペレーティングシステムの実装に使われるが他の様々なシステムにも使われる。前身のL3マイクロカーネルと同じように、ドイツのコンピュータ科学者ヨッヘン・リートケによってそれ以前のマイクロカーネルベースのオペレーティングシステムの性能の低さを解決する答えとしてL4は作られた。リートケは性能を最優先に設計したシステムであれば実用的なマイクロカーネルを作ることができるのではないかと考えた。彼のインテルi386のアセンブリ言語でハードコードした最初の実装はコンピュータ産業界の関心を引いた。これを始めとしてL4はプラットフォーム非依存、セキュリティの改善、分離、堅牢性に向けた開発が行われた。

オリジナルのL4カーネルインターフェース(ABI)やその後継がいくつも再実装されている。L4KA::Pistachio(カールスルーエ工科大学)、 L4/MIPS(ニューサウスウェールズ大学)、 Fasco(ドレスデン工科大)，WrmOS(WrmLab)などがある。このためL4はリートケの最初の実装だけを指すのではなくファミリーの名前になっている。 現在ではオリジナルのL4とその改良版のカーネルインターフェースを持つマイクロカーネルファミリーが該当する。L4は広く開発が行われている。一つのバリエーションであるOKL4はOpen Kernel Labs（英語版）(現 ジェネラル・ダイナミクス・ミッション・システムズ)で開発され数十億台のモバイル機器に使われた[1][2]。

設計理念 編集

リートケによるマイクロカーネルの一般的な設計指針は以下のようなものである

ある概念をマイクロカーネル内で実現することが許されるのは、それをカーネルの外に移した場合、すなわち競合する実装が可能となることでシステム必須の機能が妨げられる場合だけである

この考え方に基づいてL4マイクロカーネルはわずかな基本的機構を提供する

  • アドレス空間（抽象化されたページテーブルとメモリ保護の提供）
  • スレッドとスケジューリング（抽象化された実行と一時的な保護の提供）
  • プロセス間通信（分離された領域間の制御された通信）

歴史 編集

Machのような第一世代マイクロカーネルのパフォーマンスの低さから、1990年代半ばに多くの開発者がマイクロカーネルについての考え方全体の再検討を行った。Machで使われる非同期のカーネル内バッファリングプロセス間通信が低い性能の原因の一つであることが分かった。このためMachベースのオペレーティングシステム開発者はファイルシステムやデバイスドライバのような時間的な制約が大きい要素をカーネルの中に戻した[3]（XNU参照）。これはいくらかのパフォーマンス改善をもたらすが、真のマイクロカーネルの極小原則（とその利点の大部分）に大きく反する。

Machのボトルネックの詳細な分析によれば、ワーキングセットが大きすぎる事を示している。IPCコードはメモリ空間的な局所性が特に低い。それが非常に多くのカーネル内のキャッシュミスの原因になっている。この分析により、効率のよいマイクロカーネルでは性能最優先のコードの大部分は少なくとも（第一レベル）キャッシュに収まるものでなくてはならず、できればキャッシュのわずかな部分を占める程度であるべき、という原則が導かれた。

L3 編集

ヨッヘン・リートケは、パフォーマンスに充分注意を払い、（プラットフォーム非依存性に反する形で）マシン固有の設計を行い、うまく作られた小さなIPCレイヤーを使う設計ならば実際のパフォーマンスが大幅に向上することを証明した。 Machの複雑なIPCシステムの代わりに、彼のL3マイクロカーネルはオーバーヘッドを最小限にして単純なメッセージを渡すだけにした。 必要なセキュリティポリシーの定義と実装は、ユーザー空間のサーバーの任務とみなされた。 カーネルの役割は、ユーザーレベルのサーバーがポリシーを実施するのに必要なメカニズムを提供することだけとされた。 1988年に開発されたL3は、例えばTÜV SÜD（ドイツの検査技術協会）[要出典]などで長く使用され安全で堅牢なオペレーティングシステムであることを示した。

 
L4 family tree

L4 編集

L3を使った経験から、リートケはいくつかの他のMachの発想も間違っていると結論づけた。マイクロカーネルの概念をさらに単純化して、高性能化を主眼に設計した最初のL4カーネルを開発した。少しでも性能を出せるように、カーネル全体をアセンブリ言語で記述した結果、IPCはMachの20倍高速になった[4]。このような劇的な性能の向上は、オペレーティングシステムでは稀なことでリートケの業績は新たなL4の実装のきっかけとなり、ドレスデン工科大学やニューサウスウェールズ大学などの大学やリートケが1996年に働き始めるIBMなどのいくつもの研究施設でのL4ベースのシステムの研究が始められた。リートケはIBMのトーマス・J・ワトソン研究所で同僚と共にL4とマイクロカーネルシステム一般の研究と特にSawmill OS[5]の研究を続けた。

L4Ka::Hazelnut 編集

1999年、リートケはカールスルーエ大学のシステムアーキテクチャグループを引き継ぐ形でマイクロカーネルシステムの研究を続けた。高級言語による高性能マイクロカーネルの構築が可能であることを証明するためにグループはIA-32およびARMベースのマシンで動作するカーネルのC++版であるL4Ka::Hazelnutを開発した。この試みは成功し、性能は依然許容範囲とみなされた。そのためアセンブリ言語だけの版のカーネルは実質的に開発中止になった。

L4/Fiasco 編集

L4Kaの開発と並行して1998年にTUドレスデン（ドレスデン工科大）のオペレーティングシステムグループがL4/Fiascoと呼ばれるL4カーネルインターフェースの独自のC++実装の開発を始めた。L4Ka::Hazelnutはカーネル内では全く並行動作を認めず、その後継のL4Ka::Pistachioでは特定の割り込みポイントでのみ割り込みが許可されるのに対してL4/Fiascoは割り込みのレイテンシを小さくするために（極めて小さいアトミック処理の部分を除いて）完全プリエンプティブであった。これはTUドレスデンで開発されていたハードリアルタイム処理が可能なオペレーティングシステムDROPSの基礎として使うための必要性からであった。しかし、完全プリエンプティブな設計の複雑さのためFiascoの後継版のカーネルでは限られた割込みポイントを除いてカーネル内では割込みを禁止する従来のL4の方針に戻された。

プラットフォームの非依存化 編集

L4Ka::Pistachio 編集

L4Ka::PistachioとFiascoの後期バージョン（1.1以降）がリリースされるまでは全てのL4マイクロカーネルは本質的に根本的なところでCPUアーキテクチャに密接に結びつけられていた。L4開発の次の大きな変革は、高い移植性を得ながら高性能を維持するプラットフォームに依存しないAPIの開発であった。カーネルの基本的な考え方は同じであるが新しいAPIは、マルチプロセッサへのより良い対応、スレッドとアドレス空間の間の制約の緩和、ユーザーレベルスレッドコントロールブロック（UTCB）と仮想レジスタの導入など、それ以前のL4のバージョンからは多数の大きな違いがある。2001年の初めに新しいL4 API（バージョンX.2 、バージョン4と呼ばれることもある）をリリースした後、カールスルーエ大学のシステムアーキテクチャグループは新しいカーネルL4Ka::Pistachioの実装を行った。これは性能と移植性の両方を重視して完全にゼロから書き直された。二条項BSDライセンスでリリースされている。

L4/Fiascoの初期バージョン以降 編集

L4/Fiascoは何年にも渡って大きく改良が続けられた。[6][7]

  • Ver.1.1 x86, ARMのいくつかのアーキテクチャをサポートした
  • Ver.1.2 APIの拡張（1.0はv2とX.0 API）
    • 例外IPC CPU例外をユーザーアプリケーションに送信可能
    • バージョンX.2形式のUTCB
    • ローカルIPC
    • Alienスレッド（英語版） システムコールの細かい制御が可能

またFiascoはLinuxのシステムコールへのインターフェースが用意され、Linuxのユーザランドで動かすことができる（Fiasco-UX）。2018年現在、マイクロカーネルFiasco.OCと基本的なユーザー環境のL4Reとしてx86、x86_64、ARM、MIPSのアーキテクチャをサポートして開発が続けられている。L4Re上ではLinuxカーネルを動かすことができる（L4Linux（英語版））[8]。

ニューサウスウェールズ大学とNICTA 編集

開発はニューサウスウェールズ大学（UNSW）でも続けられいくつかの64ビットプラットフォームでL4実装が行われた。この結果がL4/MIPSとL4/Alphaである。リートケのオリジナルは遡ってL4/x86と呼ばれる。UNSWのカーネル（アセンブリ言語とCで書かれている）はリートケのオリジナル同様ゼロから書き起こされたもので移植性が考慮されていなかった。高い移植性を持つL4Ka::PistachioのリリースによりUNSWのグループは自分たちのカーネルを放棄してL4Ka::Pistachioを高度に最適化する事を選んだ。その成果にはその時点での最高速のメッセージパッシングの報告（Itaniumアーキテクチャで36サイクル）もあった。また、ユーザーレベルデバイスドライバがカーネル内のドライバと同等に動作することを実証した。さらにx86、ARM、MIPSの各プロセッサで動くL4上の移植性の高いLinuxであるWombat（英語版）を開発した。XScaleプロセッサにおいてWombatは本来のLinuxに比較してコンテクストスイッチのコストが1/30となることを実証した。

UNSWグループは後に拠点をNICTA（英語版）（オーストラリアの公的情報通信分野研究機関）に移しL4Ka::Pistachioから分岐した新しいL4、NICTA::L4-embeddedを開発した。これは名前が示すように商用の組み込みシステム向けで、メモリの使用量を少なくすることを優先して実装され、複雑さを抑えることを目指した。プリエンプションポイントなしでも高いリアルタイム応答性を維持するため、ほとんど全てのシステムコールは十分短時間で終了するようにAPIは変更された。

商業的展開 編集

2005年11月、NICTAはクアルコム社の移動局モデムチップセット（Mobile Station Modem：MSM）にNICTA版L4を供給することを発表した。[9]これにより2006年後半以降の携帯電話でL4が使われる事になった。2006年8月、UNSWのジャーノット・ハイザー教授と組み込み用リアルタイムOSリーダーのスピンアウトによりOpen Kernel Labs（英語版）（OK Labs）が設立され、商業目的のL4のサポートを行い、OKL4というブランド名の商業利用向けのL4の開発もNICTAと密接に協力して行った。2008年4月にリリースされたOKL4バージョン2.1は一般利用可能なバージョンのL4でCapability-based securityを特徴に持っていた。2008年10月にリリースされたOKL4 3.0は最後のオープンソース版OKL4である。これ以降のバージョンのOKL4はクローズドソースでネイティブハイパーバイザとして動くように書き換えられOKL4 Microvisorと呼ばれるようになった。OK LabsはまたWombatの後継の準仮想化LinuxをOK:Linuxとして供給し、準仮想化したSymbian OSとAndroidの供給も行った。OK LabはNICTAからseL4の権利も取得した。OKL4の出荷は2012年初めには15億台を超えた[2]。ほとんどはクアルコムのワイヤレスモデムチップである。他のものには車載インフォティメントシステムが含まれる。A7以降のAシリーズやTシリーズ、Mシリーズ、SシリーズといったAppleのSoCに含まれるSecure Enclaveコプロセッサ[10]ではNICTAが2006年に開発したL4-embeddedカーネルベースのL4オペレーティングシステムが動作している。これは現在、全てのiOSデバイスおよびAppleシリコンを搭載したMacやApple WatchでL4が出荷されていることを意味し、2021年の総出荷量はおよそ22億台とされる[11]。

高度な保証：seL4 編集

2006年にNICTAのグループはseL4と呼ばれる第3世代マイクロカーネルの設計を開始した。これはコモンクライテリア（Common Criteria：略称CC ISO/IEC 15408規格）を満たす、あるいはそれ以上のセキュリティ要件を満たすために高い安全性と信頼性が得られるような基本方針で設計された。最初からカーネルの形式的証明を目指して開発を行った。性能と検証の時に相反する要求を満たすために、チームはHaskellで書かれた実行可能な定義からソフトウェアによる処理を行いその結果を用る方法をとった[12]。seL4ではオブジェクトのアクセス権についての形式的推論を可能にするために capability-basedアクセス制御 を用いている。

機能の正しさの形式的証明は2009年に完了した[13]。この証明はカーネルの実装がその定義に対して正しいことを示し、従ってデッドロック、ライブロック（あるプロセスがbusy状態のまま実行権を放さなくなってしまう状態を指す）、バッファオーバーフロー、数値演算の例外、初期化していない変数の使用などの実装バグの無いことを意味する。seL4は汎用のOSカーネルとしては初めて証明されたという主張がなされている。[13]

seL4は、カーネルリソースの管理に新しい方法をとっている[14]。カーネルリソースの管理はユーザーレベルに任され、ユーザーリソースと同じCapability-based securityのアクセス制御を受ける。このモデルはチューリッヒ工科大学による研究OSのBarrelfish（英語版）でも採用されたもので、プロパティ分離についての推論を容易にして、seL4がコアセキュリティプロパティの完全性と秘匿性を強制することを後に証明することを可能にするものとなった[15]。NICTAのチームはCから実行可能な機械語への変換の正確さの確認を行い、seL4のトラステッド・コンピューティング・ベースからコンパイラを取り除いた。これは実行可能なカーネルにおいて高度なセキュリティが証明されているという事である。seL4はまた、ハードリアルタイムシステムに必須な完全性と最悪ケースにおける正確な実行時間の解析を行ったと最初に公表された保護モードのOSカーネルである[15]。

2014年7月29日、NICTA（英語版）とジェネラル・ダイナミクス・ミッション・システムズ（英語版）は隅から隅まで検証されたseL4をオープンソースでリリースした。カーネルコードと検証コードはGPLv2で提供され、ほとんどのライブラリとツールは2条項BSDライセンスで提供されている。研究者のコメントによれば、ソフトウェアの形式的証明のコストはより高い信頼性を提供するにもかかわらず従来の「高度な保証」を有するソフトウェアを設計するコストよりも低いとしている[16]。具体的には、従来の「高度な保証」を有するソフトウェアでは1行あたりのコストは1000米ドルであるのに対し、開発中のseL4の1行あたりのコストは400米ドルと見積もられた[17]。

NICTAはアメリカ国防高等研究計画局(DARPA)の高保証サイバー軍事システム計画（High-Assurance Cyber Military Systems(HACMS)の下でプロジェクトパートナーのロックウェル・コリンズ社、ガロア社、ミネソタ大学、ボーイング社と共同でseL4ベースの高保証ドローンを保証ツールとソフトウェアと共に開発した。これはボーイングで開発中の操縦も可能な自律型無人ヘリコプターボーイング AH-6への技術移転も計画されていた。最終的なHACMS技術のデモンストレーションは2017年4月、バージニア州スターリングで行われた[18]。

DARPAはまたジョン・ランチベリー博士の提唱でseL4に関連した中小企業技術革新研究プログラム(SBIR)による出資を行った。seL4によるSBIRを受けた企業にはDornerWorks、Techshot、Wearable Inc、Real Time Innovations、Critical Technologiesなどがある[19]。

その他の研究開発 編集

OskerはHaskellで書かれたOSで、L4の仕様で作られていた。このプロジェクトはマイクロカーネルの研究ではなく関数型プログラミング言語によるOS開発を目的とした[20]。

CodeZeroは組み込みの仮想化とネイティブOSサービスのためのL4マイクロカーネル。これはGPLライセンス版[21]と開発者によって2010年に分岐したクローズドソース版があった[22]。

F9マイクロカーネルはARM Cortex-M3/M4プロセッサの消費電力、メモリ保護に徹底的に注力したゼロから開発されたBSDライセンスのL4実装。

Fiasco.OCは前身のL4/Fiascoから進化した第3世代マイクロカーネル。Fiasco.OCはcapability basedでマルチコアシステムをサポートし、ハードウェア支援による仮想化に対応する[23]。完全に再設計されたユーザーランド環境はL4 Runtime Environment (L4Re)と呼ばれる。クライアント／サーバ通信フレームワーク、共通サービス機能、仮想ファイルシステム基盤、libstdc++やpthread等の一般的なCライブラリなど、マルチコンポーネントシステムを構築するための環境を提供する。これはマルチアーキテクチャ仮想化LinuxシステムのL4Linux（英語版）も提供する。L4ReとFiasco.OCは以前のシステムのL4EnvとL4/Fiascoを置き換えたものでx86（IA-32とAMD64）、ARM、MIPSで動作する。

NOVA Microhypervisorは小さなtrusted computing baseを持つセキュアで効率の良い仮想化環境を構築するための研究プロジェクト。[24][25] NOVAはマイクロハイパーバイザー、ユーザーレベルの仮想マシンモニタ、NUL(Nova User-Level environment)という非特権でコンポーネント化されたマルチサーバーユーザー環境から構成される。NOVAはx86ベースのマルチコアシステムで動作する。

WrmOSはオープンソースでL4ベースのリアルタイムオペレーティングシステム(RTOS)。カーネルは標準ライブラリとネットワークスタックで実装されている。SPARC、ARM、x86、x86_64のアーキテクチャをサポートする。WrmOSはL4 Kernel Reference Manual Version X.2に基づいている。WrmOS上で準仮想化されたLinuxカーネル（w4linux）が動いている。

脚注 編集

  1. ^ https://gdmissionsystems.com/cyber/products/trusted-computing-cross-domain/microvisor-products/
  2. ^ a b "Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. 19 January 2012. 2012年2月11日時点のオリジナルよりアーカイブ。
  3. ^ Amit., Singh,. Mac OS X internals : a systems approach. ISBN 0-13-442654-1. OCLC 919564441. http://worldcat.org/oclc/919564441 
  4. ^ Liedtke, Jochen (December 1993). "Improving IPC by kernel design". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 175–88.
  5. ^ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars (2000). "The Sawmill multiserver approach". ACM SIGOPS European Workshop. Kolding, Denmark. pp. 109–114.
  6. ^ https://os.inf.tu-dresden.de/fiasco/prev/
  7. ^ https://os.inf.tu-dresden.de/fiasco/prev/download/README
  8. ^ http://l4linux.org/overview.shtml
  9. ^ "NICTA L4 Microkernel to be Utilised in Select QUALCOMM Chipset Solutions" (Press release). NICTA. 24 November 2005. 2006年8月25日時点のオリジナルよりアーカイブ。
  10. ^ “Secure Enclave Processorのセキュリティ認証”. Apple Support. 2022年8月15日閲覧。
  11. ^ “世界のiPhoneユーザー、10億人に到達 (2021年1月31日)”. エキサイトニュース. 2022年8月16日閲覧。 “販売されたiPhoneの合計台数は、2020年のレポートでは、約22億台に達するようです。”
  12. ^ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Cock; David; Chakravarty, Manuel M. T. (September 2006). "Running the manual: an approach to high-assurance microkernel development". ACM SIGPLAN Haskell Workshop. Portland, Oregon. pp. 60–71.
  13. ^ a b Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA. 2011年7月15日時点のオリジナルよりアーカイブ (PDF)。
  14. ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). "Kernel design for isolation and assurance of physical memory". 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK. doi:10.1145/1435458. 2010年4月24日時点のオリジナルよりアーカイブ。
  15. ^ a b Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (February 2014). “Comprehensive Formal Verification of an OS Microkernel”. ACM Transactions on Computer Systems 32 (1): 2:1–2:70. doi:10.1145/2560537. 
  16. ^ Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). “Comprehensive formal verification of an OS microkernel” (PDF). ACM Transactions on Computer Systems 32: 64. doi:10.1145/2560537. オリジナルの2014-08-03時点におけるアーカイブ。. https://web.archive.org/web/20140803122308/http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf. 
  17. ^ seL4 Is Free – What Does This Mean For You? - YouTube
  18. ^ "DARPA selects Rockwell Collins to apply cybersecurity technology to new platforms" (Press release). Rockwell_Collins. 24 April 2017. 2017年5月11日時点のオリジナルよりアーカイブ。
  19. ^ “DARPA Agency Sponsor Dr. John Launchbury”. SBIRSource (2017年). 2017年9月29日時点のオリジナルよりアーカイブ。2017年5月16日閲覧。
  20. ^ Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). “A principled approach to operating system construction in Haskell”. Proceedings of the tenth ACM SIGPLAN international conference on Functional programming 40 (9): 116–128. doi:10.1145/1090189.1086380. ISSN 0362-1340. オリジナルの2010-06-15時点におけるアーカイブ。. https://web.archive.org/web/20100615164444/http://web.cecs.pdx.edu/~apt/icfp05.pdf 2010年6月24日閲覧。 
  21. ^ “jserv/codezero: Codezero Microkernel”. 2015年8月15日時点のオリジナルよりアーカイブ。2016年1月25日閲覧。
  22. ^ “Archived copy”. 2016年1月11日時点のオリジナルよりアーカイブ。2016年1月25日閲覧。
  23. ^ Peter, Michael; Schild, Henning; Lackorzynski, Adam; Warg, Alexander (March 2009). "Virtual Machines Jailed - Virtualization in Systems with Small Trusted Computing Bases". VTDS'09: Workshop on Virtualization Technology for Dependable Systems. Nuremberg, Germany.
  24. ^ Steinberg, Udo; Bernhard, Kauer (April 2010). "NOVA: A Microhypervisor-Based Secure Virtualization Architecture". EuroSys '10: Proceedings of the 5th European Conference on Computer Systems. Paris, France.
  25. ^ Steinberg, Udo; Bernhard, Kauer (April 2010). "Towards a Scalable Multiprocessor User-level Environment". IIDS'10: Workshop on Isolation and Integration for Dependable Systems. Paris, France.

関連項目 編集

 
関連ポータルのリンク

外部リンク 編集

 

この項目は、ソフトウェアに関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています（PJ:コンピュータ/P:コンピュータ）。

「https://ja.wikipedia.org/w/index.php?title=L4マイクロカーネルファミリー&oldid=98807741」から取得