AWS Nitro Enclavesのセキュリティアーキテクチャ

Confidential Computing Labでは，協力機関との連携のもと，TEEやTPMなどの隔離計算環境のリモートアテステーションを平易かつ厳密に実行するためのオープンソースプロジェクト https://humane-attestation.io/ を推進している．本記事では，ハイパーバイザベースの隔離技術であるAWS Nitro Enclavesを解説し，Humane AttestationプロジェクトにおいてNitro Enclavesのリモートアテステーションのために開発したOSSである Humane-RAFW-NE を紹介する．

本記事で扱うこと

• AWS Nitro EnclavesはAttestation可能な隔離環境だが，ハイパーバイザ・クラウド事業者を信頼した上で，その信頼の強度を最小化するという，TEEとは異なるアプローチを採用している
• ハードウェアオフロードによるソフトウェアTCBの極小化，形式検証によるセキュリティ保証を与えるNitro Systemの設計，Nitro Enclavesが実現する「親VMからの隔離」をTEEと比較して解説する
• Nitro Enclaves向けのRemote Attestationリファレンス実装「Humane-RAFW-NE」を紹介する

はじめに

クラウド上で機密データを扱う際には，計算処理を行うサーバが期待通りのデータ・コードを実行していること（完全性/整合性・Integrity），送信した機密データが第三者（通信経路のみならずクラウドプラットフォーマーのオペレータを含む）から秘匿されていること（機密性・Confidentiality）が，単に事実としてそうであるというだけでなく，検証可能であることが望ましい．

整合性と機密性は独立した項目ではないことに注意する．例えば，攻撃者が当該計算環境内の平文に直接アクセスできないことが保証されていたとしても，当該計算環境内で走るコードがデータ横流し機能を備えていたなら台無しである．よって真に機密性を確保するためには整合性の検証が不可欠である．

Intel TDXやAMD SEV-SNPのようなTrusted Execution Environment（TEE）は上記要求に対する現実解を与える．TEEは，ハードウェアの助けを借りて，計算環境のメモリ領域をアクセス制御・アドレス変換・ページング制御・暗号化など複数の分離手法（Isolation）の組み合わせにより保護された，隔離環境である．ハッシュ木やReverse Map Table（RMP）などによりメモリ整合性保護を提供する場合もある．主要なTEEはRemote Attestation機能を提供する．すなわち，自らの構成情報（プロセッサ情報・SVN・アプリケーション測定値等）のハードウェア署名付きレポート（Attestation Report）を発行する機能を持ち，これを用いてリモートピアに対して自らの整合性及び機密性を証明（Attest）できる．

一方，本記事で解説するAWS Nitro Enclavesは，TEEと同じくAttestableな隔離計算環境であるが，TEEとは異なる脅威モデルに基づいている．TEEはクラウドプラットフォーマー・ハイパーバイザ/ホストOSを信頼しないのに対し，Nitro Enclavesではこれらへの信頼を前提とする．それにもかかわらず，信頼の「強度」を最小化しようと試みている点が，Nitro Enclavesのユニークな特徴である．

本記事では，AWS Nitro Systemのセキュリティアーキテクチャを解説し，Nitro Enclavesがいかなる意味での隔離を実現する技術であるのかを明らかにした上で，Remote Attestationのリファレンス実装であるHumane-RAFW-NEを紹介する．

Overview

先ずは技術的詳細は一切無視して，Nitro Enclavesが何を可能にしてくれるのか，どのような応用がありうるかという話をする．

Nitro Enclavesは，EC2インスタンス（VM）のリソース（vCPU/メモリ）の一部を切り離し，独立したVM（Enclave）を作成する機能である．EnclaveはI/Oが極度に制限されており，親インスタンス上のプロキシを介して外部と疎通する．

Enclaveは親インスタンスから隔離されているだけでなく，冒頭で述べた通り，Enclaveは自らの構成情報をクライアントに証明することができる．よって，クライアントは親インスタンスを信頼することなく，かつ自らの期待する構成情報・動作定義を持つ環境であることを確認した上で，Enclaveを利用することができる．

例えば，VMインスタンス上にコンテナオーケストレーションのプラットフォームを構築し，それを第三者に提供するPaaSモデルを考える．ここでVMとしてNitro Enclavesが有効なEC2インスタンスを，コンテナとしてNitro Enclaveを利用し，SaaSベンダはこのプラットフォーム上でサービスを展開することにする．するとSaaSクライアントはプラットフォームへの信頼なしでサービスを利用できる．

AWS Nitro System

従来の仮想化基盤の問題

従来の仮想化基盤では，ハイパーバイザがI/O仮想化，ネットワーク・ストレージ管理，ハードウェアモニタリング，コントロールプレーンとのやりとりなど多岐にわたる役割を担っていた．これらは全て特権的なソフトウェアとして実装されており，結果としてコードベースが大きくなる．テナントのVMはこの巨大な特権ソフトウェアの上で動作するため，テナントは暗黙的にそのソフトウェア全体を信頼しなければならない．コードベースが大きければAttack Surfaceも大きくなり，脆弱性が混入するリスクも高くなる．

ハードウェアオフロードによるSW layerの極小化

AWS Nitro Systemは，従来ソフトウェアが担ってきた仕事を専用ハードウェア（SoC / ASICs）にオフロードするという根本的に異なるアプローチを採る仮想化基盤である．

Nitro System は以下のHW/SWコンポーネントで構成される：

• Nitro Cards — メインボードとは分離された専用SoC/ASICs．I/O仮想化，ネットワーク処理，ストレージ処理，コントロールプレーンとのやりとりなどを担う
• Nitro Security Chip — メインボードに統合されたセキュリティチップ．ハードウェアの信頼の起点（Root of Trust）として機能する
• Nitro Hypervisor — ソフトウェアとして残る最小限のファームウェアライクなハイパーバイザ（Type 1 Hypervisor）

これにより以下が実現されている：

1. Attack Surfaceの極小化 — 特権ソフトウェアのコードベース，したがってソフトウェアレイヤーのAttack Surfaceが極小化される
2. 信頼すべきSWの極小化 — テナントが暗黙的に信頼しなければならないソフトウェアが大幅に削減される
3. 性能向上 — I/Oパスが専用ASICs上で処理されるため，ホストCPUサイクルを消費しない

形式検証によるセキュリティ保証

特筆すべきは，Nitro System のコアコンポーネントのセキュリティ特性が形式検証（formal verification）により数学的に証明されていることである．具体的には，Isabelle/HOL（高階述語論理ベースの定理証明支援系）による形式的証明（formal proof）や有界モデル検査（bounded model checking）といった手法が用いられている．AWSはこのような形式検証によるセキュリティ保証をProvable security（証明可能なセキュリティ）と呼んで注力している．

形式検証とは，システム及びそのプロパティを形式言語（formal language）によって記述し，それに数学的検証を与える手法である．非網羅的テストが「有限通りの状況に対してバグっていない」ことを示すに留まるのに対し，形式手法は「バグの不存在を数学的に証明する」ものである．つまり，検証対象のプロパティについて，あらゆる入力・状態に対して成立することが数学的に保証される．

しかしながら，形式検証を（暗号通信プロトコルのような抽象レイヤーではなく）具体的なソフトウェアに適用する場合，以下が大きな困難となる．

1. 自然言語で表現された（あるいは言語化すらされていない）要求仕様を，述語論理式やHoareトリプルといった形式仕様記述として表現することの困難
   • 第一に，何が満たされていれば安全と言えるのかといった要求仕様を，数学的に曖昧なく表現可能なレベルまで詰めることが困難である
   • 第二に，要求仕様を実際に形式言語で記述する際にも，（非形式的な要求仕様よりも長大で可読性に欠いた表現をしなければならず）バグが混入しやすく，かつそれに気付き難い
2. システムの記述言語（文法）及び仕様（操作的意味論等）を形式証明系の文法に落とし込むことの困難
3. 実際に定理を形式的証明することの困難
   • 自然言語による証明であれば「A も同様」（ほぼ同一の構造を持った証明を持つことの宣言）とか「同様の操作を繰り返すことで」（数学的帰納法の省略表現）とか言えば済むところ，形式的証明では全てを顕に書かなければならない

一見最も難しそうなのは(3)のようにも見えるが，実際に問題なのはむしろ(1)である．たとえ(3)を完璧にしたところで，当の証明した形式仕様が，本来の期待していたものでなかったなら，全く何の意味もないからである．数学でいえば，有名な未解決問題を証明できたと思ったら，未解決問題の定式化を間違えていて，全く自明な定理を証明していたようなものである．そして，証明の間違いは証明チェッカで確実に検出できるが，形式化の間違いは原理的にチェックできない．

論理学者でありソフトウェア工学者であり史料学者でもあるという異色の経歴を持ち，自らも形式検証の基礎理論の構築に貢献した林晋は，「あるソフトウェア工学者の失敗」と称する自分史において，(1)をValidationの問題，(3)をVerificationの問題として整理した上で，(1)において生じるバグ（形式的仕様のバグ）の困難・深刻さについて語っている．

なぜ(3)がそれほど困難でないのかという点をもう少し掘り下げておく．実は，プログラムの仕様適合性というのは，正しく実装したのであれば，ほぼ自明に近い．プログラムと論理との間には，次のような厳密な対応関係が存在する（Curry–Howard対応）．

これによれば，型 $\tau$ を持つプログラム $P$ を実装するということと，命題 $\phi$ の形式的証明 $\Pi$ を与えるということとは，全く同じことになる．現実のプログラミング言語ではここまで綺麗な対応にはならないとはいえ，プログラムそのものの中には当該プログラムの要求仕様に対する証明の構造が内在している．そして，プログラマが何をしているかといったら，要求仕様（非形式的な命題）が与えられたときに，それを満たすプログラム（証明）を実装しているわけだから，プログラムが出来上がった時点で証明のドラフトが実質的に存在しているのである．必要なのは証明のドラフトを清書することだけである．もちろんこれが膨大かつ退屈な仕事なのであるが，物量で何とかなるとも言える．

AIが賑やかな現代なら「AIに丸投げすればいいのでは？」と思うかもしれない．実際にこれは正しい．形式的証明を書かせる段階では間違いが起きるかもしれないが，出力された証明を証明チェッカで厳密にチェックして，正しい証明を書けるまで書き直させればいい．あるいは人間が主体的に証明を書くにしても，プログラマがコーディングエージェントを使うように，「証明コーディング」エージェントに手伝わせれば良い．

AWSはそのための形式的証明のインフラをAutoCorrodeとして公開している．AutoCorrodeはRustのサブセットで書かれたコードをIsabelle/HOLに埋め込んだり，LLM支援証明をしたりするためのツールなどからなる．これにより非常に重い仕事である形式手法のコストを大幅に削減している．

Rustの採用

Nitro Systemの多くのソフトウェアコンポーネント（Nitro CLI，NSM API Library など）はRustで書かれている．Rustの所有権モデルと強力な型システムは，コンパイル時にメモリ安全性違反を含む広範なバグのクラスを静的に排除する．型検査は軽量な形式検証の一形態と見做すことができ，形式検証の文化がツールチェーンの選択にも反映されている．

注意：信頼モデルについて

Nitro System自体はAttestableではない．つまり，実環境にて稼働しているHypervisorが本当にNitro Hypervisorなのか，ホストマシンにNitro Cards/Nitro Security Chipが本当に搭載されているのか，それらのチップにどのようなファームウェアが走っているのかといった事柄を，外部から暗号学的に検証する手段は提供されていない．（例外的にSEV-SNPが有効な EC2 instanceに関してはCPUのattestationが可能であるが，Nitro EnclavesとSEV-SNPは非両立である．）したがって，ハードウェアへのオフロードによるTCBの最小化にせよ，形式検証の恩恵にせよ，どれもAWSに対する信頼が大前提である．詳細は後述．

Nitro Enclaves

概要

Nitro Enclavesは，親EC2インスタンスから隔離された仮想マシン環境を提供する機能である．Nitro Enclave ImageをDocker fileとして記述し，これをNitro CLIでビルドすることで，Enclave Image File（EIF）を生成する．親EC2インスタンスにおいて，EIFを指定して起動すると，Nitro Hypervisorは，親インスタンスから一定数のvCPUとメモリをホットアンプラグし，このリソースを使って親インスタンスとは独立したVMを作成する．これがNitro Enclaveである．

親インスタンスとEnclaveの間でメモリは共有されないことに注意．Nitro EnclavesはEnclaveを名乗ってはいるものの，SGX EnclaveのようにホストVMの中にあるというよりかは，ホストVMからvCPU及びメモリを切り離して作られる独立したVMに近い．

セキュリティ特性

Nitro Enclavesは標準的なEC2インスタンスがNitro Systemから受けるセキュリティの恩恵を継承した上で，さらに以下の制約によりセキュリティが強化されている：

• 永続ストレージなし — 揮発性メモリのみ
• 外部ネットワークアクセスなし — インターネット接続不可
• 対話的アクセスなし — SSH 等によるログイン不可
• 唯一の通信チャネル — 親インスタンスとの間のローカルvsock接続のみ

これらの制約はEnclaveのAttack Surfaceの最小化に寄与する．

Attestation

Nitro EnclavesはRemote Attestationをサポートする．NSM（Nitro Secure Module）は署名付きの Attestation Document（Attestation Reportに相当）を生成する，Attestation Documentには，EIF測定値（PCR0），カーネル測定値（PCR1），アプリケーション測定値（PCR2），親VMのインスタンスID（PCR4），EIF署名鍵証明書測定値（PCR8），中間CA証明書などが含まれる．Verifierは，AWSのCA証明書を用いてDocumentの署名及び証明書チェーンを検証した後，Documentの内容を期待される値と照合することにより，Nitro Enclaveの整合性と機密性を暗号的に検証できる．

脅威モデル — TEEとの比較

Nitro EnclavesはしばしばTEEと比較されるが，その脅威モデル（threat model）は根本的に異なる．

Intel TDXやAMD SEV-SNPといったTEEでは，プロセッサ（+FW）がTEEの隔離を強制し，ハイパーバイザやクラウドプラットフォーマー自体を信頼境界の外に置く．つまり，TEEのセキュリティモデルでは，ホストマシン管理者がメモリダンプを取得したり，クラウドプラットフォーマーが悪性のハイパーバイザを走らせたりしても，TEE内のデータは保護される（少なくとも設計上はそうなっている）．AttestationもチップベンダがRoot CAとなり，クラウドプラットフォーマーはその信頼チェーンに含まれない．

一方，Nitro Enclavesの隔離はNitro Hypervisorによって強制される．Nitro HypervisorはEnclaveと親VMのメモリ分離を保証し，NSMを介してAttestation Documentを生成するが，これらは全てAWSが開発・運用するソフトウェア/ハードウェアである．AttestationにおけるRoot CAもAWSが担う．さらに，Nitro SystemそのものはAttestationの対象外であるため，Relying Partyは以下を信頼する必要がある：

• Nitro SystemのHW componentsが真正なNitro Hypervisorをロードしていること
• Nitro HypervisorがEnclaveを正しく隔離していること
• NSMが真正なAttestation Documentを生成していること
• AWSがこれらのコンポーネントを悪意を持って改変していないこと

したがって，Nitro Enclavesは親VMからの隔離は実現するが，ハイパーバイザやクラウドプラットフォーマーからの隔離は提供しない．これがTEEとの決定的な違いである．Nitro Hypervisorを信頼すれば，クラウドオペレーターによる侵害が困難になっているということは信じられるが，これはTEEとは違って暗号学的な意味での証明ではない．

以下の図は，各モデルにおける信頼境界（Trust Boundary）の違いを示す．緑の領域が Trust Boundary，すなわち信頼するコンポーネントの範囲である．

Without Confidential Computing

テナントは全てを信頼する．

CC: VM Isolation from HV （SEV-SNP / TDX）

VMの中だけを信頼する．

AWS Nitro Enclaves: VM Isolation from Parent VM

Nitro HypervisorがTCBに含まれる．Nitro HypervisorはType 1 HypervisorなのでHost OSは存在せず，したがってHost OS Adminも存在しない．親VMは信頼境界の外だが，ハイパーバイザは信頼境界の内側にある．ここで，親VMとの関係を完全に無視することにすれば，通常のVMと殆ど同じ図になることに気付くだろう．

Humane-RAFW-NE

概要

Humane-RAFW-NE（Humane Remote Attestation Framework for AWS Nitro Enclaves）は，AWS Nitro Enclaves上で

1. ECDH鍵交換（Elliptic-Curve Diffie–Hellman Key Exchange）
2. Remote Attestation
3. セキュアチャネル経由のAPI呼び出し

というエンドツーエンドのフローを実装したリファレンス実装である．前述の通り，AWS Nitro EnclavesのSWコンポーネントの多くがRustで実装されているため，Humane-RAFW-NEも同様にRustで実装することで，実装の複雑性を削減するとともに，導入を容易にしている．

Humane-RAFWはHumane-RAFW及びHumane-RAFW-MAA（これらはIntel SGXのEPID RA及びDCAP RAのリファレンス実装）に対するNitro Enclaves版として開発したものである．これらの詳細はHumaneシリーズのFounder/開発者である櫻井碧氏による詳細な解説記事を参照されたい：

• 【技術】Intel SGX Attestation詳説 - EPID Remote Attestation編
• 【技術】Intel SGX - MAA版DCAP-RA移行戦闘記

主な差分は，隔離技術（AWS Nitro Enclaves vs. Intel SGX）及び脅威モデル，Client認証（認証用公開鍵の事前登録）の有無，並びに使用言語の違い（Rust vs. C++）である．

アーキテクチャ

Humane-RAFW-NEは以下の3つのコンポーネント（rafwne-client, rafwne-proxy, rafwne-enclave）で構成される：

ここでNitro EnclaveがParent EC2 instanceの中に含まれるように図示されているが，実際のところは親EC2インスタンスから計算リソースをアンプラグして作られる独立なVMである．

Trust Boundary

プロトコルフロー

セッションのライフサイクルは5つのフェーズで構成される：

Phase 1: Session Init

Client が init リクエストを送信すると，EnclaveはNSM API経由でハードウェア乱数生成器（HWRNG）からエントロピーを取得し，セッションIDとエフェメラルECDH P-256鍵ペアを生成して返す．

Phase 2: ECDH Key Exchange

Client側でもエフェメラルP-256鍵ペアを生成し，公開鍵をEnclaveに送信する．双方がECDHで共有秘密を計算し，HMAC-SHA256で以下の3つの対称鍵を導出する：

• SK（Session Key）— Clientがリクエストの暗号化に使用
• MK（MAC Key）— Enclaveがレスポンスの暗号化に使用
• VK（Verification Key）— Attestation Documentにバインド

ここでMAC Keyという名前が付いているのは歴史的事情による．ここでの使い方は単なるResponse Encryption Keyである．

Phase 3: Attestation Verification

EnclaveはNSM API経由でAttestation Documentの生成を要求し，Clientに返す．user_data フィールドには SHA-256(client_pub || enclave_pub || VK) がセットされ，当該ECDHセッションがAttestation Documentに暗号的にバインドされる．

Clientは以下の検証を行う：

1. COSE_Sign1エンベロープのデコード
2. CBOR Attestation Payloadのパース
3. X.509証明書チェーンの検証（AWS Nitro Root CA → 中間CA → リーフ証明書）
4. リーフ証明書の公開鍵によるCOSE署名の検証
5. PCR値の照合（PCR0: Enclaveイメージ，PCR1: カーネル，PCR2: アプリケーションコード）
6. user_data の一致確認

Phase 4: API Call

検証が完了すると，ClientはSKで入力をAES-128-GCM暗号化して送信する．EnclaveはSKで復号し，処理結果をMKで暗号化して返す．ClientはMKで復号する．Proxyは暗号文しか見えないため，データの機密性は保たれる．

Phase 5: Session Close

Clientが close リクエストを送信すると，Enclaveはセッションに関連する全ての鍵を破棄する．

セキュリティ特性

このプロトコルは以下を保証する：

ClientはAttestation Documentの署名をAWS Root CA証明書で検証することにより，Nitro Hypervisorにより発行された真正なAttestation Documentであることを確信できる．つまり

というチェーンを確立できる．

一方，HypervisorからNitro SystemのHardware Root of Trustまでのチェーンについて，Attestationの手段は提供されていない．ただし，ハイパーバイザが真正なAttestation Documentを発行できたということは，AWS Root CAまで辿れる署名鍵（AK Private）を持っているということであるから，それが真正なNitro Hypervisorであることも信頼できる．あとはNitro HypervisorがNitro System以外のハードウェア上にロードされることはないと信じてよいのなら，ハードウェアまで辿れると言えないこともない．ただしこれらは全てAWSへの信頼を前提とする．

まとめ

AWS Nitro Systemは，従来ソフトウェアが担ってきた仮想化の責務を専用ハードウェアにオフロードすることで，信頼すべきソフトウェア層を極小化し，そのコアコンポーネントのセキュリティ特性を形式的手法で数学的に証明するという，独特なアプローチを採る．

Nitro EnclavesはNitro System上に構築された隔離実行環境であり，暗号的なRemote Attestationを通じて，Relying PartyはEnclaveをリモートで検証できる．TEEはハードウェアの助けを借りてハイパーバイザからの隔離を実現したのに対し，Nitro Enclavesはハイパーバイザの助けを借りて親VMからの隔離（及びAttack Surfaceの極小化）を実現する．

これらの違いはNitro Enclavesの有用性を否定するものではない．例えば，親EC2インスタンス上にNitro Enclavesのオーケストレーションのためのプラットフォームを構築し，それを第三者に提供するPaaSモデルを考える．ユーザはPaaSベンダ（親EC2インスタンス管理者）を信頼することなく（AWSへの信頼のみで）サービス利用が可能であり，EnclaveのAttestationも可能である．これは通常のオーケストレーションサービスにはない利点である．用途に応じて適切な隔離技術を選択することが重要である．

参考文献・リンク

• Acompany Co., Ltd. Humane-RAFW-NE (GitHub Repository).
• AWS. Provable security.
• AWS. The Security Design of the AWS Nitro System (PDF).
• AWS. User Guide - AWS Nitro Enclaves (PDF).
• AWS Lab. AutoCorrode (GitHub Repository).
• J.D. Bean, KarimAllah Raslan, and Nathan Chong (2025). Introducing Nitro Isolation Engine: Transparency through Mathematics, AWS re:Invent 2025. Video
• Confidential Computing Consortium. DRAFT Common Terminology for Confidential Computing.
• B. Cook et al. (2018). Model Checking Boot Code from AWS Data Centers. In CAV 2018. DOI: 10.1007/978-3-319-96142-2_28
• D. Mulligan (2026). Nitro Isolation Engine: formally verifying a production hypervisor. Abstract
• Benjamin C. Pierce (2002). Types and Programming Languages, The MIT Press.
  • 翻訳: 住井英二郎 監訳(2013). 型システム入門, オーム社.
• 古森雄一, 小野寛晰 (2010). 現代数理論理学序説, 日本評論社.
• 櫻井碧 (2023). 【技術】Intel SGX Attestation詳説 - EPID Remote Attestation編, プライバシーテック研究所, Acompany Co., Ltd.
• 櫻井碧 (2024). 【技術】Intel SGX - MAA版DCAP-RA移行戦闘記, プライバシーテック研究所, Acompany Co., Ltd.
• 林晋 (2015). あるソフトウェア工学者の失敗―日本のITは何故弱いか (PDF).
• 森真誠, 品川高廣 (2025). 作って理解する仮想化技術─⁠─ハイパーバイザを実装しながら仕組みを学ぶ, 技術評論社.