seL4と形式検証されたマイクロカーネル

「正しさを証明したカーネル」とは何を意味するか

普通のソフトウェアはテストで「見つけられたバグが無い」状態を目指します。seL4が異なるのは、実装が仕様どおりに振る舞うことを、テストではなく機械チェック済みの数学的証明として示した点です（2009年、豪NICTA——後のData61）。約1万行のCコードという極小サイズが、この証明を現実的にしました。

証明された中核は 機能正当性（functional correctness） ——C実装の振る舞いが抽象仕様の振る舞いに完全に一致する、という性質です。この一致から帰結として、カーネル内にバッファオーバーフロー・ヌルポインタ参照・整数オーバーフロー・未定義動作・無限ループが存在しないことが言えます。仕様にそんな振る舞いが書かれていないからです。テストが「ある入力で落ちない」を確かめるのに対し、証明は すべての入力・すべての実行経路 を一度に覆います。

この設計が成立する土台は、カーネルを薄く保つマイクロカーネルの思想です。背景は マイクロカーネルとモノリシックカーネルの設計比較 を参照してください。

オブジェクトケーパビリティによるアクセス制御

seL4のアクセス制御は、Linuxとは原理が違います。Linuxケーパビリティ は「このプロセスは CAP_NET_RAW を実効集合に持つか」をチェックする——つまり権限は**プロセスに付随する属性（ambient authority）**です。対象を名指しせず、「権限を持っているか」だけを問います。

seL4は オブジェクトケーパビリティ（object capability） 方式を採ります。ここでのケーパビリティは「特定のカーネルオブジェクトへの、特定の操作を許す、偽造不能な参照」です。スレッド・アドレス空間・IPCエンドポイント・ページフレームといったオブジェクトのそれぞれに対し、(対象オブジェクト, 許可されたアクセス権) の組がケーパビリティとして存在します。

Linuxケーパビリティ:  プロセスが集合 {CAP_NET_RAW, ...} を保持
                       → 「権限を持つか」を判定（対象は暗黙）

seL4ケーパビリティ:    参照 = (対象オブジェクト, アクセス権)
                       → 参照を持つこと自体が、その対象への権限

決定的な違いは、権限の表現がカーネル内のデータ構造（CNode で構成されるケーパビリティ空間）にあり、ユーザー空間は番号（capability slot のインデックス）でしか触れないことです。ポインタのように偽造したり、持っていない権限を「作り出す」ことはできません。新しい権限を得る唯一の方法は、既に持っているケーパビリティを誰かが明示的に渡す（移譲・複製）か、新オブジェクトを生成することです。この性質が 権限の最小化（least privilege）を構造的に強制 します。各スレッドは渡された参照の範囲しか触れず、ambient権限が存在しないため「うっかり全権」が原理的に起きません。

IPCをどう高速化したか

マイクロカーネルの宿命的コストは プロセス間通信（IPC） です。seL4はL4系の最小化思想を継ぎ、典型的なIPCを fast-path という特別経路で処理します。

fast-pathが成立する条件——メッセージが十分短い、受信側が待機中、優先度の関係が単純——を満たすとき、カーネルは長い汎用経路（slow-path）を通らず、レジスタに載ったメッセージのまま受信スレッドへ実行を渡します。本質的には コンテキストスイッチ の一種ですが、保存・復元するコンテキストとチェックを極限まで削ることで、IPC往復を数百サイクル級に抑えます。**「機構だけをカーネルに、ポリシーはユーザー空間に」**という分離が、ここでも薄さと速さの両方に効いています。

証明が保証するもの・しないもの

seL4の証明は機能正当性にとどまりません。後続研究で、抽象仕様の上に成り立つ セキュリティ特性 も証明されました。

一方で、証明には 前提（仮定） があり、そこは保証の外です。代表例は、(1) コンパイラが正しくバイナリへ落とすこと（seL4はバイナリ検証で一部この溝も埋めた）、(2) ハードウェアが仕様どおり動くこと（MMUやキャッシュの想定）、(3) 初期ブートや一部のアセンブリ片、(4) DMA を行う周辺機器がメモリ保護を迂回しないこと。つまり「seL4が正しい」は 明示された前提の下で という条件付きであり、Spectre 系のマイクロアーキテクチャ的な情報漏れのように抽象モデルの外にある問題は別の対策を要します。

まとめ

• seL4は約1万行の極小カーネルで、実装が仕様どおりに動く 機能正当性 を機械チェック付きで証明した初の汎用OSカーネル。薄さが検証可能性を生んだ。
• アクセス制御は オブジェクトケーパビリティ——カーネル内に保持される偽造不能な参照で、ambient権限を排し最小権限を構造的に強制する。
• IPCは fast-path とケーパビリティによる事前権限確定で極小化。証明は完全性・機密性・権限保全にも及ぶが、コンパイラ・ハードウェア等の前提の下で という条件付きである。

設計の系譜は マイクロカーネルとモノリシックカーネルの設計比較、通信機構は プロセス間通信（IPC）、特権境界は カーネルモードとユーザーモード も合わせてどうぞ。