EC2 の正式検証済み「アイソレーションエンジン」が仮想マシンの分離に数学的保証を提供

本日、Amazon Web Services (AWS) の Elastic Compute Cloud (EC2) にて、最新世代の汎用 CPU である Graviton5 を搭載した初のインスタンスタイプとなる新しい M9g および M9gd インスタンスの一般提供を開始しました。Graviton5 は前世代からコア数を倍増させ、96 から 192 へと増加しています。また、これらは Nitro Hypervisor の構成要素であり、仮想マシン (VM) を互いに隔離する唯一の役割を担う新しい Nitro Isolation Engine（分離エンジン）を採用した初のインスタンスタイプでもあります。本稿では、論理の法則への準拠を機械的に検証する推論ステップを行う Isabelle/HOL（高次論理）証明支援ソフトウェアを用いて、Nitro Isolation Engine が正しく動作し、仮想マシンの間で隔離を強制することをどのように証明したかを説明します。Nitro Isolation Engine は、商用クラウド環境で展開された初の形式検証済みハイパーバイザの重要な構成要素です。私たちの Isabelle/HOL モデルと証明は、機械検証された数学的記述で 330,000 行に及びます。これは、現実的なオペレーティングシステムの検証が実現可能であることを初めて示した画期的プロジェクトである seL4 と規模において匹敵し、私たちの研究のインスピレーション源ともなりました。ただし、seL4 とは異なり、Nitro Isolation Engine は商用クラウド環境向けに設計されており、Graviton5 ユーザーにとって常時オン機能として生産用ハードウェアに搭載されています。Amazon の 2025 年 re:Invent コンファレンスでの講演では、私たちの形式検証手法を紹介しました。本ブログ記事では、形式検証作業の主要な側面とその相互関係について非公式な概要を提供します。 分離カーネルとは何か？ John Rushby は 1981 年に「分離カーネル」という用語を考案し、システムを隔離されたコンパートメントに分割する最小限の OS コンポーネントを記述するために使用しました。その核心となる考え方は、ポリシーとメカニズムを分離することです。分離カーネルは、何を隔離するか、リソースをどのように割り当てるか、どの仮想マシンをスケジューリングするかといった決定を行いません。これらの決定は他で行われます。代わりに、分離カーネルは隔離の強制にのみ焦点を当てており、この明確な目的により、完全な OS カーネルと比較して実装がはるかにシンプルになります。 2017 年の導入以来、Nitro Hypervisor は EC2 における隔離の強制を担当してきましたが、同時にビジネスロジック、デバイスドライバ、AWS 固有の機能も処理していました。この複雑さが正しさの証明を非常に困難にしています。さらに、Nitro Hypervisor は当初から検証のために設計されたものではありませんでした。ハイパーバイザの重要な隔離論理を最小限のコンポーネントである Nitro Isolation Engine に集約することで、検証や監査が可能な規模へと縮小し、顧客に対して隔離がどのように強制されているかについて前例のない可視性を提供しています。また、Nitro Isolation Engine は形式検証に自然に適した Rust 言語で記述されました。 Nitro Hypervisor は依然としてポリシー（仮想マシンの作成、リソース割り当て、移行、スケジューリング）を処理しますが、現在は特権が剥奪されており、ゲストの状態に触れるあらゆる操作を実行するには Nitro Isolation Engine に依頼する必要があります。Nitro Isolation Engine は、アクションを起こす前にすべてのリクエストをチェックします。 仕様と証明 私たちの作業の2つの主要な部分は、仕様（specifications）と証明（proofs）です。形式仕様はシステムの期待される動作を正確に記述し、証明はその実装がこれらの仕様に合致していることを確立します。Nitro Isolation Engine に関する私たちの定理は、4 つ種類の性質に対応しています：機密性と完全性。許可された情報フローのみが発生すること。例えば、ゲストのメモリ割り当ては再利用前に必ずスクラブされます。機能的正しさ。実装が仕様通りに正確に動作すること。ランタイムエラーの不在。Rust における None オプション値のアンラップなど、プログラム実行を停止させるような誤ったコマンド呼び出しなどのランタイムエラーが存在しないこと。メモリスafety（安全性）。バッファオーバーフローや NULL ポインタ参照などの問題が存在しないこと。 実際には、最初の3つの性質は機密性と完全性を別個に扱うため、それぞれ異なる証明技術を使用する関係上、機能検証の結果として集団的に扱います。 機能検証 機能検証における主要な部分は、Rust 言語のコアサブセットの形式化であるμRust（"micro Rust"）、仕様を正確に記述するために分離論理（Separation Logic）を用いた表現力豊かな仕様記述言語、そしてプログラムがその仕様に対して正しいことを証明するためのカスタム証明自動化を備えた検証技術である最弱事前条件計算（weakest-precondition calculus）です。これらすべては、2025 年に AutoCorrode ライブラリとしてオープンソース化した汎用証明インフラストラクチャの一部です。 より詳細には、μRust は Rust プログラミング言語の制限付きサブセットであり、Nitro Isolation Engine を記述するのに十分な表現力を持ちつつ、トレイトや動的ディスパッチなどの高度な Rust 機能を意図的に除外したため形式推論に適しています。μRust の形式意味論は、Isabelle/HOL における浅い埋め込み（shallow embedding）として定義されており、これはμRust の意味が高次論理、すなわち Isabelle/HOL の「ホスト言語」を用いて定義されることを意味します。 μRust プログラムの仕様は、事前条件と事後条件を持つ契約として定義されます。これらはプログラム実行前のシステム状態および実行後のシステム状態に関するアサーションです。私たちの契約は「完全正しさ（total correctness）」を指定しており、これは事前条件を満たすすべての状態において、プログラムが必ず終了し、結果としての状態が事後条件を満たすことを意味します。この完全正しさの条件は、プログラムがメモリスafety であり、ランタイムエラーがないことも保証します。 私たちの仕様は、低レベルなポインタ操作を行うプログラムについて推論するために設計された分離論理（Separation Logic）を用いて記述されています。分離カーネルの比較的小さな規模にもかかわらず、Nitro Isolation Engine の検証においては、形式検証で可能なことの限界に近い領域で動作しており、私たちの仕様と証明は非常に大規模に成長しています。 例えば、以下の仕様は、実行中のゲスト仮想 CPU が自分自身をオンにしようとする（誤ったリクエスト）際に何が起こるかを捉えています： 上記の仕様は複雑ですが、それが直感的に捉えているのは明白です。この状況では、Nitro Isolation Engine は、呼び出し元として動作するには仮想 CPU がすでにオンになっている必要があることを認識し、したがって定義されたエラーコード AlreadyOn を返します。システム状態に関する他のすべての要素は変更されません。 仕様における複雑さは、私たちのモデリングの深さと、Nitro Isolation Engine の実装においてこの段階に到達するまでに他のいくつかのエラーチェックがすでに実行されている必要があるという事実を反映しています。 μRust プログラムがその仕様に対して正しいことを証明するために、標準的な最弱事前条件計算を使用します。最弱事前条件計算は、特定の操作後のプログラム状態が指定された状態範囲から外れないようにする最も制限の少ない制約を体系的に特定する方法です。例えば、「x + y」という式の最弱事前条件とは、x と y の値が加算でオーバーフローしない状態のことです。証明義務（proof obligation）は、契約の事前条件が計算された最弱事前条件を含意することを示すことです。 機密性と完全性 機密性と完全性における最初の主要な部分は、Nitro Isolation Engine の動作を遷移関係として捉える高レベル仕様であり、システムの各「高レベル」ステップ（例えばハイパーコール）は原子遷移となります。この仕様は、機能検証の結果で使用されるより具体的な分離論理の仕様と、別の証明アイデアであるリファインメント（Refinement）を用いて厳密に接続されています。 2 つ目の主要な概念は非干渉性（noninterference）です。非干渉性は、機密性と完全性を数学的に精密にするために使用する不可分性の保存という考え方です。その考え方は、あるステップの前に観測者にとって2つの状態が区別できない場合、その後も区別不能でなければならないということです。 この考え方がなぜ機密性を捉えるのかの直感的な理由は、観測者がそのステップによって何も新しいことを学んでいないからです。不可分性の保存が機密性を保証する理由を理解するのは微妙です。2 つの単純なマシン A と B を考えてみましょう。それぞれに1つの公開レジスタと1つのプライベートレジスタがあります。観測者は、公開レジスタが一致する場合にそれらを区別できないと考えます。つまり、プライベートレジスタは隠されています。 以下の図において、A と B は区別できません： 次に、プライベートレジスタに基づいて分岐し、公開レジスタに 1 を割り当てるプログラムを実行した場合どうなるかを考えてみましょう。結果として生じるマシン A' と B' は異なる公開レジスタを持つようになります—つまり、区別可能になってしまいます！賢明な観測者はこれを利用して元のプライベート値を推論でき、この不可分性の保存の失敗は、観測者への不正な情報フローに対応します。 さらに続く内容 私たちの検証作業の主要な部分に関するこの概要をお楽しみいただけたことを願っています。適合性テストや並行コードについての推論をどのように処理するかなど、共有できる他の多くの側面があります。これらは今後の投稿で詳しく紹介する予定です。

背景や根拠まで確認しますか？

関連記事

調べる

選ぶ

サイト