Amazon Web Services ブログ
形式的検証済みの Nitro Isolation Engine が Amazon EC2 の仮想マシン分離を数学的に保証
本ブログは 2026 年 6 月 10 日に公開された Amazon Science Blog “EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation” を翻訳したものです。
「分離カーネル (separation kernel)」を Nitro セキュリティシステムの他の部分から切り離し、Rust プログラミング言語のサブセットのみを使用して実装したことで、形式的検証が可能になりました。
本日 (2026 年 6 月 10 日)、AWS は Amazon Elastic Compute Cloud (Amazon EC2) の新しい M9g および M9gd インスタンスの一般提供開始を発表しました。これらは、汎用 CPU の最新世代である Graviton5 を搭載した初のインスタンスタイプです。Graviton5 では、コア数が前世代の 96 から 192 に倍増しています。
また、これらは新しい Nitro Isolation Engine を使用する初のインスタンスタイプでもあります。Nitro Isolation Engine は Nitro Hypervisor のコンポーネントであり、その唯一の役割は仮想マシン (VM) を相互に分離することです。この記事では、推論の各ステップが論理法則に従っているかを機械的にチェックするソフトウェアである Isabelle/HOL (高階論理) 定理証明支援系 (proof assistant) を使って、Nitro Isolation Engine が正しく動作し、VM 間の分離を強制することをどのように証明したかを解説します。Nitro Isolation Engine は、商用クラウド環境にデプロイされた初の形式的検証済みハイパーバイザーの重要なコンポーネントです。
Isabelle/HOL によるモデルと証明は、機械的に検証された 330,000 行の数学的記述から成ります。これは、現実的なオペレーティングシステムの検証が実現可能であることを初めて実証した画期的なプロジェクトであり、私たちの取り組みの着想源ともなった seL4 に匹敵する規模です。ただし seL4 とは異なり、Nitro Isolation Engine は商用クラウド環境向けに設計されており、Graviton5 のユーザーに対して常時有効な機能として本番ハードウェア上で提供されます。
2025 年の Amazon re:Invent カンファレンスで行った講演では、形式的検証の方法論を紹介しています。また、ホワイトペーパーでは、検証の範囲や前提条件など、結果の重要な側面をより詳しく解説しています。このブログ記事では、形式的検証の取り組みにおける主要な要素と、それらがどのように組み合わさっているかの概要を、わかりやすくご紹介します。
分離カーネルとは何か
「分離カーネル」という用語は、John Rushby 氏が 1981 年に生み出しました。これは、システムを分離されたコンパートメントに分割する最小限の OS コンポーネントを指します。重要なアイデアは、ポリシーとメカニズムの分離です。分離カーネルは、何を分離するか、リソースをどう割り当てるか、どの VM をスケジュールするかを決定しません。それらの決定は別の場所で行われます。その代わり、分離の強制だけに専念します。この目的の明確さにより、分離カーネルはフル機能の OS カーネルよりもはるかにシンプルに実装できます。
2017 年の導入以来、Nitro Hypervisor は Amazon EC2 における分離の強制を担ってきましたが、同時にビジネスロジック、デバイスドライバー、AWS 固有の機能も処理しています。この複雑さが、正当性の証明を大幅に難しくしています。さらに、Nitro Hypervisor は当初から検証を想定して設計されたものではありませんでした。
ハイパーバイザーの重要な分離ロジックを Nitro Isolation Engine という最小限のコンポーネントに抽出したことで、検証と監査が可能な小さなサイズになり、分離がどのように強制されているかについて、お客様はかつてないレベルの可視性を得られます。また、Nitro Isolation Engine は、形式的検証との相性がより良い言語である Rust で記述しました。
Nitro Hypervisor は引き続きポリシー (VM の作成、リソース割り当て、移行、スケジューリング) を処理しますが、現在は権限が引き下げられており、ゲストの状態に触れるあらゆる操作を Nitro Isolation Engine に依頼する必要があります。Nitro Isolation Engine は、実行前にすべてのリクエストをチェックします。
仕様と証明
この取り組みの 2 つの重要な要素は、仕様と証明です。形式仕様はシステムに期待される動作を正確に記述し、証明は実装がその仕様を満たしていることを立証します。
Nitro Isolation Engine に関する定理は、次の 4 種類の性質を対象としています。
- 機密性と完全性。許可された情報フローのみが発生します。例えば、ゲストに割り当てられたメモリ領域は、再利用の前に必ずスクラブされます
- 機能的正当性。実装は仕様どおりに正確に動作します
- ランタイムエラーの不在。Rust における None オプション値の unwrap (プログラムの実行を停止させる誤ったコマンド呼び出し) のようなランタイムエラーが存在しません
- メモリ安全性。バッファオーバーフローや NULL ポインタ参照といった問題が存在しません
実際には、後者の 3 つの性質は機能検証の結果としてまとめて扱い、機密性と完全性は別途扱います。これは、それぞれに異なる証明手法を用いるためです。
機能検証
機能検証における重要な要素は次のとおりです。1 つ目は μRust (マイクロ Rust) と呼ばれる Rust 言語のコアサブセットの形式化、2 つ目は仕様を正確に記述するための分離論理 (Separation Logic) を用いた表現力の高い仕様記述言語、3 つ目はプログラムが仕様に対して正しいことを証明するための検証手法である最弱事前条件計算 (weakest-precondition calculus) と独自の証明自動化です。これらはいずれも汎用的な証明インフラストラクチャの一部であり、2025 年に AutoCorrode ライブラリとしてオープンソース化しました。
より詳しく説明すると、μRust は Rust プログラミング言語の制限されたサブセットで、Nitro Isolation Engine を記述するのに十分な表現力を持ちながら、形式的な推論にも適しています。これは、トレイトや動的ディスパッチといった高度な Rust の機能を意図的に除外しているためです。μRust の形式的意味論は、Isabelle/HOL への浅い埋め込み (shallow embedding) として定義されています。つまり、μRust の意味は、Isabelle/HOL の「ホスト言語」である高階論理を使って定義されます。
μRust プログラムの仕様は、事前条件と事後条件を持つ契約として定義されます。これらは、プログラム実行前後のシステム状態に関する表明です。この契約は「全正当性 (total correctness)」を規定しています。つまり、事前条件を満たすすべての状態において、プログラムは必ず終了し、その結果の状態は事後条件を満たします。この全正当性の条件は、プログラムがメモリ安全であり、ランタイムエラーがないことも意味します。仕様は、低レベルのポインタ操作プログラムについて推論するために設計された論理である分離論理を使って記述されています。
分離カーネルは比較的シンプルとはいえ、Nitro Isolation Engine の検証は、形式的検証で可能な範囲の限界に近い取り組みであり、仕様も証明も非常に大規模になります。例えば、以下の仕様は、実行中のゲスト仮想 CPU が自分自身の電源をオンにしようとした場合 (誤ったリクエスト) に何が起こるかを記述したものです。
上記の仕様は複雑ですが、その内容は直感的にはシンプルです。この状況では、Nitro Isolation Engine は、呼び出し元として動作するには当該の仮想 CPU が既にオンになっているはずだと判断し、定義済みのエラーコード AlreadyOn を返します。それ以外のシステム状態はすべて変更されません。仕様の複雑さは、モデリングの深さと、Nitro Isolation Engine の実装においてこの時点に到達するまでに他の複数のエラーチェックが既に実行されているという事実を反映したものです。
μRust プログラムが仕様に対して正しいことを証明するには、標準的な最弱事前条件計算を使用します。最弱事前条件計算とは、特定の操作の後のプログラムの状態が、指定された状態の範囲から外れないことを保証できる、最も制約の少ない条件を体系的に特定する方法です。例えば、式 x + y の最弱事前条件は、x と y の値の加算がオーバーフローしない状態です。そのうえで、契約の事前条件が計算された最弱事前条件を含意することを示すのが証明義務となります。
機密性と完全性
機密性と完全性に関する 1 つ目の重要な要素は、Nitro Isolation Engine の動作を遷移関係として記述する高レベルの仕様です。ここでは、システムの各「高レベル」ステップ (ハイパーコールなど) が 1 つのアトミックな遷移となります。この仕様は、リファインメント (Refinement) と呼ばれる別の証明のアイデアを用いて、機能検証の結果で使用されるより具体的な分離論理の仕様と厳密に結び付けられています。2 つ目の重要な要素は、非干渉性 (noninterference) という考え方です。
非干渉性とは、機密性と完全性を数学的に厳密なものにするために使用する、識別不能性の保存という考え方です。あるステップの前に 2 つの状態が観測者にとって識別不能であれば、ステップの後も識別不能なままでなければならない、というものです。これが機密性を表す直感的な理由は、そのステップによって観測者が新しい情報を何も得ていないためです。
識別不能性の保存がなぜ機密性を保証するのかは、少しわかりにくいところです。パブリックレジスタとプライベートレジスタを 1 つずつ持つ、2 つのシンプルなマシン A と B を考えてみましょう。プライベートレジスタは隠されているため、観測者は、パブリックレジスタが一致していれば 2 つのマシンを識別不能とみなします。以下の図では、A と B は識別不能です。
ここで、プライベートレジスタの値によって分岐し、パブリックレジスタに 1 を代入するプログラムを実行するとどうなるかを考えてみましょう。結果として得られるマシン A’ と B’ は、パブリックレジスタの値が異なるため、識別可能になってしまいます。賢い観測者はこれを利用して元のプライベートレジスタの値を導き出せてしまいます。つまり、識別不能性が保存されないということは、観測者への不正な情報フローが生じていることを意味します。
今後の展開
ここまで、検証の取り組みにおける主要な要素の概要をご紹介しました。この取り組みには、適合性テストや、並行コードに関する推論の扱い方など、他にも多くの側面があります。今後の記事でお伝えできることを楽しみにしています。