ハイパーバイザ

ハイパーバイザとは、1台の物理ハードウェア上に複数の仮想マシン（VM）を作り出し、それぞれで別のOSを互いに分離した状態で同時に実行させる基盤ソフトウェアであり、CPU・メモリなどの計算資源を仮想化してVM間に割り当てる役割を担うものである。

詳細解説

ハイパーバイザは、物理ハードウェアの上に複数の仮想マシン（VM）を作り、CPU時間・メモリ・デバイスへのアクセスを仮想化して各VMに割り当てる。各VMの中では独立したゲストOSが動き、VM同士はハイパーバイザの管理する境界で分離される。実行形態により2つに大別され、**型1（Type 1）**はホストのハードウェア上で直接動作するベアメタル型（例: KVM、Hyper-V、VMware vSphere）、**型2（Type 2）**は既存のホストOS上のソフトウェアとして動作するホスト型である（Red Hat公式ドキュメント）。安全系を汎用ホストOSの上に載せる構造は成立しないため、車載で用いられるのは型1である。

マイクロカーネルとの関係も押さえておきたい。seL4公式のwhitepaperは、seL4がマイクロカーネルであると同時にハイパーバイザでもある、と明記している——seL4 の上にVMを作り、その中でLinuxのような本格的なゲストOSを動かせる。小さく検証可能なカーネルがVM分離の土台を兼ねる、という両概念の収斂が起きている。

SDVにおける位置づけ

SDVのE/Eアーキテクチャ統合では、従来は機能ごとに専用マイコンを割り当てていた構成を、少数の高性能SoCへ集約する流れが進む——seL4 whitepaperも、混合臨界システムの背景として「集約（consolidate）への要求」を挙げる。このとき、安全性の要求水準が異なるソフトウェア——たとえば高い保証が求められるメータークラスタやADAS系と、Android等を動かすIVI（情報系）——が同じチップに同居することになり、ハイパーバイザによるVM分離が混合臨界の代表的な実装になる。情報系の障害や侵害が安全系に波及しないことを、区画の境界で論証できるかが設計の焦点となる。

ただし「ハイパーバイザを使えば分離が保証される」わけではない。分離・リアルタイム性の保証水準は実装と検証のされ方に依存し、形式検証を持つもの（seL4）から商用RTOSベースのものまで幅がある。製品の選定では、何がどの根拠で保証されているか（形式検証の範囲・安全規格の認証状況）を製品単位で確認することが出発点になる。