車載ハイパーバイザとは — Type-1とType-2の違いとVM分離の安全

ハイパーバイザ（一台のコンピュータ上で複数のOSを同時に動かす仮想化ソフト）は、SDV（ソフトウェア・デファインドな車）において「安全度の異なるソフトを単一ハードウェアで安全に同居させる」ための基盤である。最高水準の安全制御と、一般的な車内情報系アプリを同じセントラルコンピュータ上で動かすには、両者の間に強く保証された「壁」が要る。本記事は、ハイパーバイザのType-1とType-2の違い、製品の種類、安全論証との関係を整理する。結論を先に言えば、ハイパーバイザの選定は単なる技術選択ではなく、安全認証戦略の根幹に関わる判断である。

ハイパーバイザとは何か

ハイパーバイザとは、一つのハードウェア上に複数の仮想マシン（VM）を作り、それぞれで独立したOSを動かす仮想化の基盤ソフトである。SDVでは、安全度の異なる機能をVMごとに分離し、相互に干渉させないために使われる。

Type-1とType-2——根本的な設計差

ハイパーバイザは大きく二種類に分かれる。

車載では、安全クリティカルな領域にはType-1が構造的に適合し、開発・シミュレーション環境にはType-2が使いやすい、という使い分けが一般的だ。Type-1はハードウェアのCPU仮想化機能を直接管理するため、最高水準の安全制御と非安全な情報系の間に、ハードウェアレベルの隔離を提供できる。

製品の種類——商用とオープンソース

車載ハイパーバイザは、商用製品とオープンソースの双方が競合する。商用領域では、マイクロカーネル型のリアルタイムOSをベースにした製品が最も広く採用され、最高水準の機能安全認証の実績が豊富だが、ランタイムの使用料が生じる。航空・防衛分野の高安全実績を持つ製品が車載に展開する例もある。SoCベンダーが提供する統合ソフトは、安全用のRTOSとAI推論用のLinuxを分離する構成をとる。

オープンソース領域では、形式検証済みのseL4が、VM間隔離を数学的に保証する点で独自の位置を占める。あるメーカーがseL4ベースで量産実績を構築したことは、商用ハイパーバイザの代替としての実用性を示している。研究・試作段階のオープンソースType-1も現れているが、量産実績はまだ限定的だ（本記事は特定製品の優劣は断定しない）。

5VM構成とASIL分解の関係

SDVでは、機能を安全度ごとにVMへ分ける構成（安全制御・運転支援AI・車内情報系・通信・更新管理など）が、ハイパーバイザによるVM間隔離を前提に設計される。各VMに異なる安全度を割り当てれば、機能安全のASIL分解（高い安全要件を複数の低い要件に分割する手法）を構造的に実現できる。最高水準の安全制御を担うVMを最高水準で設計し、他のVMを低い水準で設計しても、VM間の隔離が保証されればシステム全体として最高水準相当を論証できる。

重要なのは、この論証の「強さ」がハイパーバイザの隔離保証の「強さ」に直接依存する点だ。seL4の形式検証による隔離保証は「数学的証明」であり、テストとコードレビューに基づく商用ハイパーバイザの保証（信頼性は高いが「すべての入力に対する保証」ではない）より格段に強い。これが混在クリティカリティ設計の根拠になる。

性能と安全のトレードオフ

ハイパーバイザの導入は、VM間の切り替え負荷を伴う。VM間のデータ転送（AI推論結果を安全制御へ渡すなど）の遅延設計が、システム全体の最悪実行時間を左右する。自動緊急ブレーキのように応答時間が数十ミリ秒に制約される機能では、VM間通信の遅延配分が設計上の最大の制約になる。seL4の通信遅延は公式ベンチマークで極めて低く報告されており、こうした厳しい応答要件に対しても十分なマージンを持つ。隔離の強さと性能の予測可能性を、要件に照らしてどう両立させるかが設計の勘所になる。

まとめ：ハイパーバイザ選定は安全認証戦略の根幹

ハイパーバイザの選定は、隔離保証の強さ（＝安全論証の強さ）と、性能・成熟度・コストのトレードオフを伴う、安全認証戦略の根幹に関わる判断である。自社で具体化する際の論点は次のあたりだ。

• 安全系の隔離に、形式検証済み基盤と商用RTOSのどちらをどこまで使うか。
• VM構成（安全度別の分割）とASIL分解を、どう設計・論証するか。
• VM間通信の遅延配分を、安全機能の応答要件にどう収めるか。

形式検証済みカーネルはseL4マイクロカーネルとはを、形式検証の考え方は形式検証とはを、機能安全はISO 26262と機能安全・ASILの構造をあわせて参照してほしい。自社のSoC・安全要件に即したハイパーバイザ選定は個別性が高く、具体化の段階では外部の視点を入れると論点整理が速い。