seL4マイクロカーネルの紹介 [PDF]

• seL4はOSマイクロカーネルであり、最小限のコードでカーネルモードを実行してハードウェア資源を制御し、セキュリティを強化する
• L4マイクロカーネル系に属し、1990年代半ばから開発されている
• ハイパーバイザーとして動作可能で、LinuxのようなゲストOSの実行をサポートする
• 世界で初めて機能的正確性が証明されたOSカーネルであり、コードレベルでの数学的証明が完了している
• きめ細かなアクセス制御のために**Capability（ケーパビリティ）**ベースのセキュリティモデルを使用

seL4の構造とハイパーバイザー機能

• モノリシックカーネル vs マイクロカーネル
  • モノリシックカーネル（Linuxなど）: カーネルコードが巨大でセキュリティ脆弱性が多い → 約2000万行のコード（20M SLOC）
  • マイクロカーネル（seL4）: 最小限のカーネルコードを使用 → 約1万行のコード（10K SLOC）
  • カーネルサイズの縮小 → セキュリティ強化と攻撃対象領域の削減
• seL4はハイパーバイザーの役割も果たす
  • VM上でLinuxのような完全なゲストOSを実行可能
  • 各VMは独立して実行され、相互に干渉できない → 強力な分離を保証
  • 保護プロシージャコール（PPC）→ VM間のセキュアな通信が可能

seL4の検証とセキュリティモデル

• 機能的正確性の検証
  • seL4はコードレベルで機能が数学的に正しいことを証明済み
  • カーネルのすべての動作が仕様どおりに動くことを保証
• トランスレーションバリデーション（Translation Validation）
  • コンパイラが生成したバイナリコードが元のCコードと正確に一致することを証明
  • 自動化されたツールチェーンを通じて実行
• セキュリティ特性の検証
  • 機密性: 明示的に許可された場合のみデータへアクセス可能
  • 完全性: 明示的に許可された場合のみデータを変更可能
  • 可用性: 明示的に許可された場合のみリソースを利用可能

Capabilityベースのセキュリティモデル

• Capabilityとは?
  • 特定のオブジェクトに対するアクセス権を付与するセキュリティトークン
  • オブジェクト参照とアクセス権を一緒にエンコード
  • 詳細なアクセス制御が可能 → 最小権限の原則（Principle of Least Privilege, POLA）を適用
• Capabilityの利点
  • きめ細かなアクセス制御 → 権限の最小化が可能
  • 権限委譲（Delegation）および権限取り消しが可能
  • 強力なセキュリティモデル → 従来のアクセス制御モデル（ACL）より優れている
• Confused Deputy問題の解決
  • 従来のACLベースのシステムでは、セキュリティ状態が主体のセキュリティIDによって決定される
  • seL4ではCapabilityが直接セキュリティ権限を決定 → 明確な権限制御が可能

リアルタイムシステムと混合重要度システムのサポート

• リアルタイムシステム対応
  • seL4は優先度ベースのスケジューリングをサポート
  • すべてのカーネル処理について最悪実行時間（WCET）の分析が完了 → ハードリアルタイムを保証
• 混合重要度システム（Mixed-Criticality System, MCS）対応
  • スケジューリングコンテキストに基づいてCPU資源を割り当て、分離
  • 高優先度のタスクがCPUを独占しないよう制御
  • クリティカルなタスクと非クリティカルなタスクを同時に実行可能

性能と効率性

• 最高性能のマイクロカーネル
  • 性能が重要な場合でもセキュリティを低下させない
  • システムコールとIPCのコストを最小化 → 競合システム比で5倍以上高速
• 競合システムと比べて優れた性能
  • Fiasco.OC: seL4比で約2倍遅い
  • Zircon: seL4比で約9倍遅い
  • CertiKOS: seL4比で約5倍遅い

実世界での適用とサイバーレトロフィット

• 実際の利用事例

  • BoeingのULB（無人ヘリコプター）での適用に成功
  • セキュリティ強化とシステム安定性の向上を確認

• 既存システムの段階的なセキュリティ強化（Incremental Cyber Retrofit）

  • 既存システムをVM上で動かしながら段階的にモジュール化
  • セキュリティを強化しつつ性能低下を最小化

結論

• seL4は機能的正確性、セキュリティ、性能が実証された、世界で最も安全なマイクロカーネルである
• 検証済みのセキュリティモデルと混合重要度システム対応により、さまざまな分野で実用的に利用可能
• 既存システムのセキュリティ強化と性能向上が可能 → セキュリティと性能のバランスを実現した革新的なマイクロカーネル