seL4

seL4とは、実装が仕様どおりに振る舞うこと（機能正当性）の機械検証された形式的証明を持つオープンソースのOSマイクロカーネルであり、アプリケーション間の強い分離を高い保証で実現する基盤として、車載を含む高信頼システムで用いられるものである。

詳細解説

Klein らは2009年のSOSP（ACM Symposium on Operating Systems Principles）で、seL4マイクロカーネルの機械検証された検証を報告し、「我々の知る限り、完全かつ汎用のOSカーネルとしては初の機能正当性の形式的証明」であると述べた。ここでいう機能正当性とは、カーネルの実装が高水準の抽象仕様に常に従って振る舞うことを意味する。カーネルの責務を最小限に絞るマイクロカーネル設計によって信頼すべきコードの規模を小さく保ったことが、この規模の形式検証を現実的にした。その後の証明は公式に「高水準仕様からバイナリコードまで」拡張され、対象となる性質も機能正当性から情報漏えいの不在（機密性）などのセキュリティ性質に及ぶ。

ただし、証明の効力は前提の上に成り立つ。seL4公式は証明の仮定として、アセンブリコード・ブートコード・マシンインターフェース・ハードウェア・DMAを明示しており、これらの欠陥は証明の保証範囲外である。また公式は検証（verification）と認証（certification）を明確に区別しており、形式検証が与えるのは最高水準の保証根拠であって、ISO 26262（自動車）やDO-178C（航空）のような規格認証そのものではない——認証は規格に対する評価プロセスとして別途必要になる。「数学的に証明済み＝無条件に安全・認証済み」と読み替えるのは誤りである。

ライセンスは、カーネルレベルのコードがGPLv2、ユーザーレベルのコードが2条項BSDで提供され（公式LICENSE.md・SPDXタグ管理）、プロジェクトはseL4 Foundationの下で運営されている。

SDVにおける位置づけ

SDVの中核課題のひとつは混合臨界（mixed criticality）——安全性の要求水準が異なるソフトウェア（走行制御とインフォテインメント等）を同一の計算機資源に同居させること——であり、その成立条件は「区画間の干渉が起きないこと」の保証にある。seL4の形式的に証明された分離は、この保証を経験則やテストではなく数学的根拠で与える点で、車載の高保証基盤として注目される。

量産採用の公開事例として、seL4公式サイトはNIOがseL4ベースのOS「SkyOS-M」を搭載した ONVO L60 を量産していることを掲載している（seL4 Summit 2024でのNIO発表）。一方で、車載業界全体での採用規模や他OEMの量産状況について一次情報で確認できる包括的データは見当たらず、本稿では個別の公開事例の記載に留める。