- seL4 は、セキュリティと安全性が重要な組み込みおよびサイバー・フィジカルシステムを対象とした OS マイクロカーネルであり、ハードウェア資源を分離・多重化するが、完全な汎用 OS ではない
- カーネルモードのコードを約 10 kSLOC まで削減し、TCB と攻撃面を縮小、ファイルシステム・ネットワーク・ドライバのような OS サービスはユーザーモードへ追い出す
- コードレベルの 形式検証 を備えた世界初の OS カーネルであり、正しく構成されたシステムでは機密性・完全性・可用性といったセキュリティ特性までカーネルが保証する
- capability ベースのアクセス制御、WCET 解析、混合重要度リアルタイムシステム対応、ハイパーバイザー機能を組み合わせ、細粒度の分離とリアルタイム性を両立する
- seL4 API は非常に低レベルなため、複雑なシステムを直接構築するのは難しく、静的アーキテクチャが適する場合は Microkit のようなフレームワークを使うのが現実的
seL4が担う範囲
- seL4 は、オペレーティングシステムの低レベル中核部であるマイクロカーネル
- OS は、プロセッサのより高い特権実行モードである カーネルモード でハードウェアと資源を制御する
- アプリケーションはユーザーモードで実行され、OS が許可した方法でのみハードウェアへアクセスする
- マイクロカーネルは、高い特権で実行されるコードを最小化した OS の中核部
- seL4 は、1990年代半ばまでさかのぼる L4マイクロカーネル系 に属する
- seL4 は seLinux とは無関係
- seL4 は完全な OS ではなく、ハードウェア資源を安全に多重化・分離する低レベルカーネル
- ファイルシステム、ネットワークスタック、デバイスドライバといった一般的な OS サービスはカーネル内に存在しない
- こうしたサービスはユーザーモードプログラムとして提供される必要がある
マイクロカーネル構造と攻撃面の縮小
- Linux のような モノリシックカーネル は、ファイル保存やネットワーキングのような OS サービスをカーネルモードのコードとして提供する
- カーネルモードのコードはシステム資源へ無制限にアクセスできるため、バグが権限昇格や任意コード実行につながると、システム全体が損なわれる可能性がある
- Linux カーネルは約 20 MSLOC 規模で、数万件のバグが存在し得ると推定されている
- seL4 のように適切に設計されたマイクロカーネルは、カーネルモードのコードを約 10 kSLOC の水準まで削減する
- これは Linux カーネルより 3 桁小さい規模
- TCB が縮小することで、攻撃面も同時に縮小する
- OS サービスの大半はカーネルの外へ出され、マイクロカーネルはハードウェア周辺の薄いラッパーのように動作する
- 中核となる提供機能は、プログラム間の 分離 と安全な呼び出し機構
- サービスはカーネル内ではなく、別個のサンドボックスで動作するユーザーモードプログラムになる
- 既知の Linux 侵害事例のうち深刻な事例を分析した研究では、マイクロカーネル設計により 29% を完全に排除し、追加の 55% についても、もはや深刻とは分類されない程度まで緩和できた
PPC、capability、細粒度の権限制御
- seL4 は保護付きプロシージャコール（PPC）機構を提供する
- 歴史的理由から IPC という用語が残っているが、IPC という表現は誤解を招き、好ましくない設計につながる可能性がある
- PPC により、あるプログラムが別のサンドボックス内のプログラムの関数を安全に呼び出せる
- マイクロカーネルは PPC において入力と出力を受け渡しし、インターフェースを強制する
- リモート関数は、公開されたエントリポイントからのみ呼び出せる
- 適切な capability を与えられた、明示的に許可されたクライアントだけが呼び出し可能
- capability は、システム内の特定資源へのアクセスを可能にするアクセストークン
- どのエンティティがどの資源へアクセスできるかを非常に細かく制御する
- 最小権限の原則（POLA）を支援する
- Linux や Windows のような主流システムのアクセス制御方式では、このレベルの最小権限の実現は不可能
- seL4 は capability ベースであり、かつ形式検証された世界唯一の OS で、この組み合わせにより世界で最も安全な OS だと主張できるだけの根拠があると評価されている
形式検証とセキュリティ保証
- seL4 は、実装の正確性に対する 形式的・数学的・機械検証済みの証明 を提供する
- この証明は、カーネルが仕様に関して非常に強い意味で「バグがない」ことを意味する
- seL4 は、コードレベルでこのような証明を持つ世界初の OS カーネル
- 実装の正確性に加えて、seL4 はセキュリティ強制に関する追加の証明も提供する
- 正しく構成された seL4 ベースのシステムでは、カーネルが 機密性、完全性、可用性を保証する
- 検証チェーンは seL4 の中核的な差別化要因
- セキュリティ・安全性が重要なシステムでカーネルが信頼の基盤となるには、実装とセキュリティ特性に関する強い保証が必要
リアルタイム性と混合重要度システム
- seL4 は、最悪実行時間（WCET）について完全かつ健全な解析を受けた OS カーネル
- カーネルが適切に構成されていれば、すべてのカーネル操作には時間的境界がある
- その境界も既知である
- この特性は ハードリアルタイムシステム 構築の前提条件
- 厳しく制限された時間内にイベントへ応答できなければ致命的となるシステムを対象とする
- seL4 は混合重要度リアルタイムシステム（MCS）もサポートする
- 信頼性の低いコードが同一プラットフォーム上で同時実行されても、重要な活動の時間的保証が必要な環境を対象とする
- 従来の MCS OS が用いる厳格で柔軟性に欠ける時間・空間パーティショニングとは異なり、seL4 は資源利用率を維持できる柔軟なモデルを提供する
ハイパーバイザーとして使う seL4
- seL4 はマイクロカーネルであると同時に ハイパーバイザー でもある
- seL4 上で仮想マシンを実行できる
- 仮想マシン内では Linux のような一般的なゲスト OS を動かせる
- ゲストとアプリケーションは、seL4 が強制する通信チャネルに従って相互に通信できる
- Linux VM をシステムサービス提供手段として活用できる
- 例示構成では、別個の VM で動作する複数の Linux インスタンスから、ネットワーキングやストレージのようなサービスを借りてくる
seL4 上でシステムを構築する方法
- seL4 API は、他のマイクロカーネルと比べても非常に低レベル
- ハードウェアを安全に管理するために必要な最小限の抽象化しか提供しない
- seL4 は「オペレーティングシステムのアセンブリ言語」にたとえられる
- 複雑なシステムを seL4 上に直接構築する方法は適切ではない
- より高レベルのフレームワークによって、サービス実装コードへの集中と、ハードウェアの複雑さやシステム統合の自動化が必要
- seL4 には 3 つの主要なオープンソースコンポーネントフレームワークがある
- Microkit: protection domain 中心の少数の抽象化で seL4 API を単純化し、別個にコンパイルされたモジュールとカーネルバイナリを統合して、ブート可能イメージを作成する SDK を提供する
- CAmkES: Microkit の前身であり、静的アーキテクチャシステム向けのコンポーネントフレームワークだが、SDK がないためビルド工程がより不便で、オーバーヘッドも大きい
- Genode: 複数のマイクロカーネルをサポートし、x86 プラットフォーム向けのサービスやドライバが豊富で、静的アーキテクチャを強制しないが、seL4 のセキュリティ・安全性機能をすべて活用できず、保証ストーリーもない
- 静的なシステムアーキテクチャが要件に合う限り、seL4 ベースのシステム構築には Microkit が推奨される
- 静的アーキテクチャとは、モジュール集合と通信構造をシステム構成時点で定義するモデル
- このモデルは、自動車や航空機のような複雑なサイバー・フィジカルシステムを含め、ほとんどの組み込みシステム要件に適していると見なされている
1件のコメント
Hacker Newsの意見
seL4 自体は以前からある話だが、マイクロカーネルを超えて、新たに形式検証済みの層やコンポーネントが追加されたのか気になる。
また「証明」という言葉を見ると、感情的に過負荷になって思考が止まってしまう人もいるように見える。形式検証は、安全なITという果てしない問題を解決する万能薬でも、完全無欠なソフトウェアを作り出す方法でもない。
自分の理解では、特定の条件下で特定の要件を満たすという証明であり、その要件と条件はかなり狭い場合があり、仕様の外にある機能や条件については何も述べない、という意味だと思うのだが、おおむね合っているのか気になる。
実務上、セキュリティ専門家は「形式検証済みソフトウェア」を見たときに何を期待するのかも気になる。seL4が満たす仕様が何なのかが、ここでの核心的な情報ではないかと思う。
https://github.com/seL4/seL4/pull/243
https://github.com/seL4/l4v/pull/453
issueトラッカーにもメモリ関連のバグがいくつかある。
https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
興味深いことに、メモリの「register clobbering」を修正したPRにはbugラベルが付いていないため、「bug」でフィルタしても出てこない。以前は証明のおかげでseL4はこうした問題に免疫があると思っていたが、これを見てからは、証明はコミュニティが信じるようになったほど包括的ではないのだと見るようになった。それでもseL4は依然として非常に印象的なソフトウェアだ。
質問に答えると、seL4が満たす仕様はGitHubで公開されている。
https://github.com/seL4/l4v
混合クリティカリティ・スケジューリングは、CPU時間に対するcapabilityベースのアクセス、スレッド実行上限の制限、高クリティカリティ作業の優先順位とリソースアクセスの保証、呼び出し元が寄付したスケジューリング時間で動く「passive servers」を提供する。
MicrokitはseL4上で実際のシステムをはるかに簡単に作れるようにする検証済みの抽象化層で、Device Driver FrameworkはseL4で高性能I/Oを行うためのデバイスドライバ・テンプレート、制御/データプレーン実装、ドライバ作成およびデバイス仮想化のためのツールだ。
形式検証は、特定の条件下で特定の要件が成立することを保証できる。一般に、そうした要件と条件が狭い場合があるというのはその通りだが、seL4自体にはカーネルに期待できる広い範囲の性質を扱う証明が多くあり、その保証は非常に弱い仮定の下でも成立する。Cコンパイラの正しさも仮定せず、コンパイラ出力を見て、コンパイル済みバイナリが要求されたCの意味論に従って動作することを証明する別のツールがある。
seL4が満たす要件には、seL4カーネルのバイナリコードが抽象仕様に記述された動作を正確に実装し、それ以上のことはしない、というものが含まれる。バッファオーバーフロー、メモリリーク、ポインタエラー、ヌルポインタ参照、Cコードの未定義動作、仕様に列挙された明示的な方法以外によるカーネル終了などがない。
仕様とseL4バイナリは、完全性と機密性というセキュリティ特性も満たす。完全性とは、プロセスが明示的な権限のないデータを変更する手段がまったくないという意味で、機密性とは、権限のないデータをいかなる方法でも読み取れないという意味だ。特定のサイドチャネルを通じて間接的にデータを推論できないことまで示している。セキュリティ以外にも、予想最悪実行時間の保証やスケジューリング特性も満たしている。
現在の作業は、より広い採用を目指すLionsOS寄りだ: https://lionsos.org/
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
リソース、ハードウェアアクセス、capabilityをコンパイル時に追跡するために、型レベルプログラミングを多用している。ランタイムで問題を見つけてデバッグするのがあまりにも最悪なので、基盤カーネルの保証の一部をコンパイラ側へ引き上げようとする試みだ。
ゲストのモノリシックカーネルを載せるマイクロカーネルホストが好きなので、サーバではFreeBSD VMの安全層とバックアップとしてseL4を動かしており、その中でrenderfarm、BEAMクラスタ、Jenkins用のjailを使っている。
残念なのは、DragonflyBSDのスレッディングとプロセス内部カーネル、つまりハイブリッドカーネル設計のためのARMポートがないことだ。夢は128コアのAmpere AltraでOpenMoonRayをもっと効率よく動かすことだ。
もはやマイクロカーネル賛否論争そのものに大きな意味はなくなりつつあるように思う。権限のあるサービスへ高速・効率的・安全にアクセスする唯一の方法はハードウェアによる緩和策であり、ソフトウェアにできることには限界がある。
80286と80386の違いに似ている。後者は前者にはなかった、本当のマルチタスク向けハードウェア支援を追加した。その後も、ハイパーバイザーを可能にしたようなハードウェアレベルの保護メカニズムは増え続けている。
特にAppleはSoCに、カーネル、ドライバー、コンポーネントをチップレベルで保護し、実行中のスレッドやポインター使用時に権限を強制する機能を数多く入れている。https://support.apple.com/guide/security/operating-system-in...
だからといってOSが破られないという意味ではないが、権限をソフトウェアだけで管理する戦略よりははるかに効果的だ。こうした機能や類似のものを活用すれば、カーネル構造はもはやそれほど重要ではないように見えるのだが、自分が間違っているのか気になる。
より組み合わせ可能なマイクロ／ハイブリッドシステムからも学べることは多い。たとえばPlan 9は、単一プロトコルである9Pでシステム内のすべてのオブジェクトをユーザー空間に提供する優れたハイブリッドシステムだ。IPやTLSのように、システムコールのオーバーヘッドを避けるため一部はカーネル内にあるので、ハイブリッドである。
もう一つ興味深い設計は、カーネル内部のドライバーが、おおむねハードウェアロジックに対する9Pインターフェースとして機能するだけの最小形になっている点だ。こうすると、ポインターやレコードのような機械上のオブジェクトを探索可能なファイルに変換し、そのファイルを標準的なUnix権限で保護し、ネットワーク越しにコンポーネントを複数のマシンへ容易に分散できる。その結果、ドライバーロジックを安全にユーザー空間プログラムへ押し出せる。
9Pはネットワークやアーキテクチャに対して透過的なので、Arm、x86、mipsなど複数のマシンでそのまま協調作業できる。Plan 9からLinux/UnixやWindowsに戻ると悲しく、もどかしい。柔軟性はほとんど火成岩レベルで、同じこと、つまりファイル／オブジェクト提供をする多数のプロトコルによって、機能が互換性なく継ぎ足されている。
実用的な工学の観点では、モノリシックカーネルのほうが速く、簡単で、リソースも多かったし、セキュリティはCで可能な範囲、つまりベストエフォートと大量のバグだった。その混乱を緩和するために多くのハードウェアが導入された。しかしSeL4なら、プロセス間隔離とルートレベルのエクスプロイトが存在しないことについて非常に高い信頼度があるため、理論上はセキュリティ補助プロセッサが不要かもしれない。だからハードウェア／ソフトウェア共同設計は重要だ。
ただしSeL4チームも、ハードウェアのサイドチャネルを除去するために多くの工学リソースを費やさなければならなかった。現実世界は物理シミュレーションの都合を気にしてくれないので、ハードウェアにも欠陥がある。
ここでのマイクロカーネルの利点は、形式検証で扱えるほど小さいことだ。証明そのものはカーネルサイズの10倍ある。SeL4のコンテキストスイッチはLinuxより一桁倍速いので、性能への影響は無視できる程度のはずだ。しかし魔法のように数百万行規模のモノリシックカーネルを検証できるなら、コンテキストスイッチをしないほうが依然として速い。実際、SeL4チームはスケジューラをユーザー空間へ移そうとしたが、性能コストが大きすぎたためカーネル内に残し、証明の負担に加えた。
むしろハードウェアの主な役割は効率を高めることだ。たとえば最近のマイクロカーネルはすでにMMUのようなハードウェアをうまく活用しているので、かなり堅牢だ。そのうえで、マイクロカーネルの小さな信頼できるコンピューティング基盤がカーネルに信頼性を与え、カーネルとハードウェアが一緒に強固な土台を作る。
結局は、ハードウェアでどこまで「ズル」を許すかという問題だが、全般的にはマイクロカーネルのほうが保護機能をうまく活用する。あるいはエクソカーネルを見てもよい。
https://genode.org/index
seL4サポートのあるオペレーティングシステムだ。
地域の OWASP チャプターで SeL4 の発表をしたことがある。資料を見つけられるかは分からない。
このプロジェクトは本当によくできたものだが、特に汎用コンピューティングでは Linux の代替と見るのはためらわれる。とはいえ、マイクロカーネルが汎用用途全般で悪いという意味ではない。RedoxOS は最近ある程度進展しているように見え、Rust で書かれたマイクロカーネルを使っている。
それでも Redox が成功するなら、それだけでも良い前進だ。seL4 ではこうした性質がさらに極端になる。技術的な長所は優れているが、これまでもそうだったし、今後もおそらく「次の主流」になるための何かを備えることはなさそうだ。政治的な考慮を除けば、マイクロカーネルは成功するだろうし、そうあるべきだと思う。
seL4 が実際に役に立つには、その上に必要なものが多い。幸い、その部分でもオープンソースの取り組みが多く進んでおり、数年前よりずっと良い位置にいる。
静的なシナリオには LionsOS[0] があり、すでにかなり使える。
動的なシナリオには Provably Secure, General-Purpose Operating System[1] があるが、まだ初期段階だ。
どちらも seL4 のウェブサイトからリンクされている Trustworthy Systems の Projects ページ[2]で見つけられる。
[0] https://trustworthy.systems/projects/LionsOS/
[1] https://trustworthy.systems/projects/smos/
[2] https://trustworthy.systems/projects/
このカーネル上で動く OS も、セキュリティ保証が成り立つには 形式検証されている必要があるのか気になる。
もちろんカーネルだけではあまり役に立たないので、カーネル上で実行されるドライバ、ファイルシステムサーバ、その他サービスの設計は依然として重要だ。
Linux を含むほとんどの他のシステムは根本的なレベルで欠陥を抱えているが、seL4 は実際に 安全で信頼できるシステムを作れるようにしてくれる、という点も重要だ。
そのため、高セキュリティのプロセスの横で Linux カーネルを動かしつつ、許可された IPC を除けば互いに分離されているという保証を持てる。
ただし限界はある。DMA は無効にする必要があり、ドライバも形式検証されたものだけを使う必要がある。
seL4 の マルチコアカーネルはまだ検証されていない点も重要だ。
Drew DeVault の Helios Microkernelも見る価値がある。SeL4 ベースだという。
https://ares-os.org/docs/helios/
カールスルーエ大学では L4 が人気だった。詳しく調べたことはないが、実用的に役立つものを作るというより、理論的なアイデアを試すことに主な関心があるプロジェクトのように見えた。
それは20年前の話で、私の見る限り今も大きくは変わっていない。ざっと検索してみると、その上に OS を作ろうとする試みはあるようだが、実際の利用というより概念実証に近く見える。
「OKL4 の出荷数は2012年初めに15億個を超え、その大半は Qualcomm の無線モデムチップだった。ほかの配備先には自動車のインフォテインメントシステムが含まれる」
「A7 以降の Apple A シリーズプロセッサには、L4 オペレーティングシステムを実行する Secure Enclave コプロセッサが搭載されており、この OS は2006年に NICTA で開発された L4-embedded カーネルをベースにした sepOS である。その結果、L4 は Apple silicon を搭載した Mac を含む、現代のすべての Apple デバイスに載っている」
Bellosa の同窓である Rittinghaus は、HN でも何度か紹介された Unikraft[0] に関わっており、ユニカーネル技術を使っている。
[0] https://unikraft.org/
「Secure Enclave Processor は、Apple がカスタマイズした L4 マイクロカーネルのバージョンを実行する」
https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
私の見るところ、L4Re カーネルも Elektrobit Safe Linux の一部だ。
卒業論文では Pistachio ベースの OS を作った。カールスルーエで学んでいたら、おそらく OS 研究に進んでいただろうと、いつも思っていた。
私にもオペレーティングシステム設計のアイデアがあり、検討していた capability は seL4 と同じような介在と委譲の機能を使っていた。そこに書かれていること以外にも利点がある。例えば、音声にフィルタを適用したり、ネットワーク透過性を実現するためにプロキシ capability を使ったりできる。
リアルタイム機能は任意実装として許容できると思っていた。私のアイデアは単一の実装というより、仕様に近いものだった。
もう一つ欲しかった機能は、すべてのプログラムが入出力を除けば 決定論的に動作することだ。入出力なしでは日付・時刻やプログラム実行時間を知ることはできず、プロセッサ機能も確認できない。ハードウェアがサポートしていない機能を使った場合、オペレーティングシステムがエミュレートすることはできる。
これを実装するために、ハードウェア支援とソフトウェア支援を組み合わせて使うつもりだった。文書にはハードウェア実装の capability に対する攻撃メモがあるが、参照文書を持っていないため、その攻撃が私の考えていた方式にも当てはまるかどうかは分からない。
セキュリティの観点では、Linux カーネルの KVM と同じような失敗を見せているように思える。ハイパーバイザが ring 0 にあると、ある VM から別の VM やホスト自体へ脱出する危険がある。
その危険をどう緩和しているのか気になる。
VMM は VM 自体より多くの capability を持たないため、学術的な意味を除けば VM 脱出には価値がない。
元の PDF の8〜10ページを見ればよい。