AWS Nitro Isolation Engine: AWS Nitro System におけるハイパーバイザーの形式的検証

本ブログは 2026 年 6 月 11 日に公開された AWS Blog “AWS Nitro Isolation Engine: Formally verifying the hypervisor in the AWS Nitro System” を翻訳したものです。

Ali Saidi は AWS の VP 兼 Distinguished Engineer です

何百万ものお客様が、最も機密性の高いワークロードの保護に AWS Nitro System を利用しており、AWS はお客様のデータを保護するイノベーションにおいて業界をリードしています。お客様のデータの安全性と機密性を守ることは AWS の最優先事項であり、データの分離と保護のための専用ハードウェアとソフトウェアへの投資を継続しています。

2017 年、AWS は Nitro System をリリースしました。これは、ゼロオペレーターアクセス (オペレーターがお客様のデータに一切アクセスできない状態) を前提に設計された、初の主要なクラウドプラットフォームです。Nitro System は、次世代のすべての Amazon EC2 インスタンスの基盤となる専用のハードウェアとソフトウェアであり、仮想化、ストレージ、ネットワーキングの機能を専用ハードウェアと最小限のハイパーバイザーにオフロードします。Nitro System では、最も高い権限を持つ AWS オペレーターであっても、認証と監査が行われる管理用 API を通じてのみシステムとやり取りでき、これらの API からお客様のワークロードにアクセスすることはできません。このアーキテクチャはクラウドセキュリティの業界標準を確立し、NCC Group などの第三者機関が独立した立場でこのアプローチの妥当性を確認してきました。

そして今、AWS はさらに水準を高めます。AWS Nitro System の主な役割の 1 つは、インスタンスを互いに分離し、AWS オペレーターからも分離することです。これは 10 年以上にわたり Nitro System アーキテクチャの基盤となってきました。AWS Nitro Isolation Engine は、AWS re:Invent 2025 で初めて発表され、本日 (2026 年 6 月 11 日) よりすべての Graviton5 ベースのインスタンスで一般提供を開始しました。これは Nitro Hypervisor 内の専用コンポーネントであり、この分離を実施し、それを数学的な厳密さで証明する役割を担います。Nitro Isolation Engine は形式的検証を採用しています。形式的検証とは、ハードウェアやソフトウェアが特定のテストケースだけでなく、あらゆる状況で意図したとおりに動作することを数学的に証明する手法です。この徹底的な検証手法により、Nitro は形式的に検証された初のクラウドハイパーバイザーとなり、数学的に証明されたクラウドセキュリティの新しい標準を確立しました。

AWS Nitro Isolation Engine

Nitro System において、AWS Nitro Hypervisor は、すべての仮想マシンについて、権限のないエンティティがお客様のデータを読み取ったり変更したりできないように設計されています。Nitro Isolation Engine は Nitro Hypervisor の専用コンポーネントであり、これらの仮想マシン間の分離を実施します。仮想マシンのメモリ、CPU レジスタの状態、および I/O デバイスへのすべてのアクセスを、Nitro Hypervisor の他の部分に公開される最小限の API セットを通じて仲介します。Nitro Isolation Engine は、お客様のデータへのアクセスを仲介する唯一のシステムコンポーネントです。Nitro Hypervisor の他のコンポーネントは、この制限されたインターフェイスを通じて動作する必要があり、お客様のワークロードに直接アクセスすることはできません。Nitro Isolation Engine のコードベースは最小限に抑えられているため、人による監査が容易になり、バグが混入し得る範囲が減り、その設計と実装に形式的検証を適用することが現実的になっています。

形式的検証

形式的検証は、数学的証明を用いて、システムの形式的モデルの特性が、あり得るすべてのシステム状態とすべての入力において成立することを示します。これは、あり得る状態と入力のうち (場合によっては大規模な) 一部に対してシステムの動作を確認するテストとは対照的です。形式的検証は、従来のテストよりも正確性についてはるかに強い根拠を提供します。Nitro Isolation Engine の場合、分離特性は、あり得るすべてのシステムの動作にわたって保証されます。テストと検証は相互補完的な関係にあります。検証はテストを補強し、テストはまだ検証されていないシステムの領域をカバーして、システムが意図したとおりに動作しているという経験的な裏付けを与えます。

お客様にとって、分離を実施するコードが形式的に検証されていることは、包括的なテストを超える保証となります。テストは引き続き不可欠であり、AWS はテストにおいても高い基準を維持していますが、テストで確認できるのは特定のシナリオに限られます。形式的検証はこれを補完するものであり、テストでカバーされるシナリオだけでなく、あり得るすべてのシナリオにわたって分離特性が数学的に保証されることを意味します。

形式的に検証された特性

Nitro Isolation Engine の形式的検証により、4 つの主要な特性が確立されます。

1. 機密性と完全性 – Nitro Isolation Engine は、ゲスト仮想マシン (VM) の機密性と完全性を維持します。機密性とは、ゲスト VM のプライベートデータが権限のないエンティティによって読み取られないことを意味し、完全性とは、ゲスト VM のプライベートデータが権限のないエンティティによって変更されないことを意味します。

2. 機能的正確性 – 検証されたすべてのハイパーコールは、仕様で定義された期待される動作と一致します。仕様には各ハイパーコールの事前条件と事後条件が記述されており、証明によって、実装がそれらから決して逸脱しないことが立証されます。

3. ランタイムエラーが発生しないこと – コードがランタイムエラーに遭遇することはなく、実装は仕様どおりに動作します。これらの特性の形式的検証を組み合わせることで、検証の対象となるあらゆる一連のイベントに対して Nitro System が分離を維持することが、数学的に厳密に保証されます。現時点では、この検証は、VM の起動、実行、および終了を担う VM のコアライフサイクルのハイパーコールを対象としています。

4. メモリ安全性 – バッファオーバーフロー、NULL ポインタ逆参照、範囲外アクセスなどのメモリ安全性違反が存在しないことを立証します。すべての検証済みソフトウェアと同様に、Nitro Isolation Engine の証明は、Rust コンパイラやハードウェアの正確性などの前提に基づいています。これらの前提、およびエンジニアリングと検証に対する AWS のアプローチについては、Nitro Isolation Engine のホワイトペーパーで詳しく説明されています。

Rust による実装

Nitro Isolation Engine は Rust で実装されています。Rust は、機密性の高いソフトウェアにおけるセキュリティ脆弱性の根本原因となってきた、よくあるプログラミング上の落とし穴を防ぐように設計されたシステムプログラミング言語です。Nitro Isolation Engine に Rust を採用したことで、複数の種類のバグを設計上まとめて排除しています。Rust が適している理由はその型システムにあります。型システムが厳格な所有権規則を適用するため、形式的検証の一部が容易になり、コンパイル時に第一段階の保証が得られます。

まとめ

Nitro Isolation Engine は、お客様のデータの機密性を守るという AWS の継続的なコミットメントを体現するものです。そして、これはまだ出発点にすぎません。AWS は、セキュリティに影響を与える Nitro Isolation Engine のすべての主要コンポーネントに形式的検証を拡張し、新機能が導入されてもそれらの証明を維持し続けます。さらに、Nitro Isolation Engine のソースコードと形式的証明を第三者に提供し、独立した検査およびレビューを受けられるようにする予定です。このレベルの透明性は、クラウドプロバイダーが開かれた姿勢、コード品質、形式的検証をどのように示せるかについて、新しい標準を確立するものと考えています。

AWS Nitro System とコンフィデンシャルコンピューティングの詳細については、以下のリソースをご覧ください。

• AWS Nitro Isolation Engine Whitepaper
• コンフィデンシャルコンピューティング： AWS の視点 (2021)
• AWS Nitro System のコンフィデンシャルコンピューティングに対する第三者評価の獲得 (2023)
• AWS Nitro Whitepaper
• AWS re:Invent 2025 presentation – Introducing Nitro Isolation Engine: Transparency through Mathematics

著者について