マイクロカーネル

マイクロカーネルとは、OSのカーネルが担う機能をプロセス間通信・スケジューリング・メモリ管理などの最小限に絞り、デバイスドライバやファイルシステムなどをカーネル外のユーザー空間で動かす設計方式であり、信頼すべきコードの最小化によって障害の隔離と検証可能性を高めるものである。

詳細解説

マイクロカーネルの要点は「カーネル特権で動くコードを最小化する」ことにある。プロセス間通信（IPC）・スケジューリング・メモリ管理といった、ユーザー空間では代替できない最小限の機構だけをカーネルに残し、デバイスドライバ・ファイルシステム・ネットワークスタックなどは独立したユーザープロセスとして動かす。あるドライバの障害がカーネル全体を巻き込まない隔離と、信頼すべきコード（TCB: Trusted Computing Base）が小さいことによる検証可能性が利点であり、seL4 の機能正当性証明はこの設計の到達点にあたる。

SDVにおける位置づけ

安全要求の異なるソフトウェアを同居させるSDVの車載コンピュータでは、「小さく・隔離が強く・検証できる」カーネルが基盤の選択肢として重要になる。マイクロカーネルはその設計類型の代表であり、形式検証と組み合わせることで、混合臨界システムの分離保証を支える。