本ブログは 2026 年 7 月 30 日に公開された AWS Blog “ Extend Amazon Inspector SBOM Generator with Plugins ” を翻訳したものです。 Amazon Inspector は、 Amazon Web Services (AWS) のワークロードを継続的にスキャンしてソフトウェアの脆弱性を検出する、自動化された脆弱性管理サービスです。Amazon Inspector の脆弱性管理機能は、 Amazon Inspector SBOM Generator (inspector-sbomgen) と呼ばれる資産インベントリエンジンによって支えられています。これはスタンドアロンのコマンドラインツールで、コンテナイメージ、ディレクトリ、アーカイブ、ローカルシステム、コンパイル済みバイナリなどから ソフトウェア部品表 (SBOM) を生成します。過去 2 年間で、AWS は inspector-sbomgen のカバレッジを数十のプログラミング言語エコシステム、オペレーティングシステム、広く導入されているアプリケーションへと拡大してきました。 今回、inspector-sbomgen を利用するビルダー向けの新機能として、独自のカスタムパッケージコレクターを記述できる プラグインシステム を発表します。ソースコードのコンパイルや公式リリースを待つ必要はなく、すぐに使い始めることができます。 inspector-sbomgen の最新バージョンは、 Amazon Inspector ユーザーガイド からダウンロードできます。 この記事では、inspector-sbomgen プラグインシステムでできること、これを構築した理由、そして数分で最初のプラグインを書く方法を紹介します。あわせて、プラグインが生成したパッケージコンポーネントを Amazon Inspector の脆弱性スキャンと統合する方法や、セキュリティが強化された予測可能なプラグイン動作を実現するプラグインの安全性モデルについても解説します。 プラグインシステムを構築した理由 ソフトウェアのエコシステムは動的です。新しい言語パッケージマネージャー、ロックファイル形式、エンドユーザーアプリケーションが絶えずリリースされ、その多くは迅速に採用されます。中にはセキュリティの検証がほとんど行われないまま使われるものもあります。その結果、セキュリティチームには可視性のギャップが残ります。つまり、SBOM ツールがまだ認識できないソフトウェアが本番ワークロードで動いているという状態です。お客様からは、こうしたエコシステムの多くを直接インベントリ化したいという要望をいただいてきました。最近まで、それを実現する唯一の方法は、機能リクエストを出して inspector-sbomgen チームがエコシステムに対応し、新しいリリースをデプロイするのを待つことでした。 inspector-sbomgen プラグインシステムは、この状況を変えます。プラグインを使うと、次のことができます。 inspector-sbomgen が標準では対応していないエコシステムへの対応 – 新しいオープンソースエコシステム、ニッチまたは変化の速いパッケージ形式、組織独自のツールなど、inspector-sbomgen を変更することなくインベントリ化できます エコシステム検出の迅速なプロトタイピング – 開発者にも AI コーディングアシスタントにも扱いやすいプラグインシステムを設計しました。プラグインは Lua で記述され、実行時にロードされるため、Go ツールチェーンもコンパイルも不要です。組み込みのテストハーネスを使ってプラグインを繰り返し改善し、すぐに結果を確認できます 安定した基盤の上での構築 – プラグイン API はアーティファクトの種類による違いを抽象化するため、検出ロジックを一度書くだけで、コンテナイメージ、アーカイブ、ローカルシステムなどでシームレスに動作します。また、プラグインは sbomgen の内部構造から分離されているため、コアツールでリグレッションが発生した場合の影響範囲も小さく抑えられます 実際、私たち自身もこのプラグインシステムを内部で活用し、新しいエコシステムのカバレッジを以前より速く提供できるようになりました。 1.13 リリース では、Apache Tomcat、NGINX、MySQL、Redis、WordPress、OpenSSH ツールチェーンなど、これまで Go で実装されていた 20 以上のエコシステムが、プラグインとして sbomgen バイナリに組み込まれています。同じリリースでは、Apache Cassandra、Apache Struts、Conda、Swift パッケージ、AI エージェントコレクター (Amazon Q Developer、Kiro CLI、Claude Code、GitHub Copilot、Ollama) など、10 を超える新しいエコシステムもプラグインとして追加されました。 inspector-sbomgen プラグインの仕組み sbomgen プラグインは 2 段階のパイプラインで動作します。 検出 (discovery) – アーティファクトのファイルシステムをスキャンし、インストール済みパッケージのメタデータを含むファイルを特定します 収集 (collection) – 検出された各ファイルを開き、ファイルの内容を解析して、結果を SBOM にパブリッシュします 内部では、イベントバスが検出プラグインと収集プラグインをつないでいます。検出プラグインは検出したファイルの一覧をイベントとしてパブリッシュし、1 つ以上の収集プラグインがそのイベントをサブスクライブして、パッケージ収集をトリガーします。開発者にとっては、これは オブザーバーパターン としておなじみの動作でしょう。 この分離により、1 つの検出プラグインが複数のコレクターにデータを供給できます。例えば、あるコレクターはパッケージメタデータを抽出し、別のコレクターはシークレットをスキャンし、さらに別のコレクターはポリシーをチェックする、といった構成が可能です。各収集プラグインは、計算コストの高いアーティファクトファイルシステムの再走査を行うことなく、同じファイルリストを利用できます。 5 分で書ける最初のプラグイン inspector-sbomgen を使えば、プラグイン環境を簡単にセットアップできます。 plugin new コマンドで sbomgen に新しいプラグインワークスペースを作成させ、 --with-example フラグを指定すると、すぐに実行できる検出プラグインと収集プラグインのペアがワークスペースに用意されます。 inspector-sbomgen plugin new --with-example 上記のコマンドを実行すると、プラグイン名と、プラグインワークスペースを格納するディレクトリの入力を求められます。カスタム値を指定することも、デフォルト値をそのまま使うこともできます。 Plugin name (identifies the software ecosystem your plugin will inventory, e.g. debian-dpkg, rhel-rpm, python-pip, cmake) [my-custom-ecosystem]: <enter> Project directory [my-sbomgen-plugins]: <enter> Created plugin "my-custom-ecosystem" in my-sbomgen-plugins/ なお、対応するコマンドラインインターフェイス (CLI) 引数でプラグイン名とディレクトリを指定すれば、対話形式のプロンプトをスキップできます。 inspector-sbomgen plugin new \ --with-example \ --name my-custom-ecosystem \ --path my-sbomgen-plugins プラグインワークスペースを作成すると、inspector-sbomgen は次のステップを案内する画面を表示します。開発者や AI コーディングアシスタントに対して、変更が必要なソースファイルや関連ドキュメントの場所を示してくれます。 Next steps: Get started: 1. Open plugin folder in a code editor (VS Code recommended) 2. Add test files that your plugin will discover and parse (e.g., config files, lockfiles, binaries, etc.): my-sbomgen-plugins/discovery/cross-platform/extra-ecosystems/my-custom-ecosystem/_testdata/ Develop: 3. Edit discovery: my-sbomgen-plugins/discovery/cross-platform/extra-ecosystems/my-custom-ecosystem/init.lua 4. Edit collection: my-sbomgen-plugins/collection/cross-platform/extra-ecosystems/my-custom-ecosystem/init.lua Test: 5. Write unit tests: my-sbomgen-plugins/discovery/cross-platform/extra-ecosystems/my-custom-ecosystem/init_test.lua 6. Run unit tests: inspector-sbomgen plugin test --path my-sbomgen-plugins Deploy: 7. Distribute your plugin directory wherever you run inspector-sbomgen: inspector-sbomgen <arguments> --plugin-dir /path/to/my-sbomgen-plugins Example: inspector-sbomgen container --image alpine:latest -o /tmp/sbom.json --plugin-dir /path/to/my-sbomgen-plugins For code completion, install the VS Code Lua language server extension: https://luals.github.io/#vscode-install For more information: - Plugin guide: my-sbomgen-plugins/docs/sbomgen-plugin-developer-guide.md - Testing guide: my-sbomgen-plugins/docs/sbomgen-plugin-testing-guide.md - API reference: my-sbomgen-plugins/docs/sbomgen-plugin-api-reference.md - Documentation: https://docs.aws.amazon.com/inspector/latest/user/sbom-generator.html プラグインワークスペースができたので、その中身を詳しく見てみましょう。 tree my-sbomgen-plugins ├── AGENTS.md ├── collection │   └── cross-platform │   └── extra-ecosystems │   └── my-custom-ecosystem │   └── init.lua ├── discovery │   └── cross-platform │   └── extra-ecosystems │   └── my-custom-ecosystem │   ├── _testdata │   │   ├── empty │   │   └── example.lock │   ├── init_test.lua │   └── init.lua ├── docs │   ├── sbomgen-plugin-api-reference.md │   ├── sbomgen-plugin-developer-guide.md │   └── sbomgen-plugin-testing-guide.md ├── library │   └── sbomgen.lua └── README.md スキャフォールディングされたプロジェクトには、動作する検出プラグインと収集プラグインのペア、 _testdata/ 配下のテストフィクスチャを使ってパスするユニットテスト、統合開発環境 (IDE) 連携用の .vscode/settings.json 、開発者ドキュメントのローカルコピーが含まれています。 スキャフォールディングは、人間と AI コーディングアシスタントの両方が読みやすいように、意図的に簡潔で完結した内容になっています。各ファイルには、それぞれの関数の役割と、プラグイン作成者が記述すべき箇所を説明する明確なコメントが付いています。 プラグインをテストするには、まずパッケージロックファイルやコンパイル済みバイナリなど、スキャン対象となるものが必要です。サンプルプラグインは、次の内容を持つ架空の example.lock をインベントリ化します。 my-package-alpha==1.0.0 my-package-beta==2.3.1 my-package-gamma==0.9.5 付属の検出プラグインは、アーティファクトのファイルシステム内で example.lock のインスタンスを探す方法を知っています。 -- my-custom-ecosystem discovery plugin -- Discovers example.lock files in the artifact file list. function discover() return sbomgen.find_files_by_name({"example.lock"}) end そして、付属の収集プラグインは、 example.lock の内容を解析し、パッケージ情報を出力 SBOM にパブリッシュする方法を知っています。 -- my-custom-ecosystem collection plugin -- Parses example.lock files and extracts package name and version. function collect(file_path) local content = sbomgen.read_file(file_path) if content == nil then return end for line in content:gmatch("[^\n]+") do local name, ver = line:match("^(.+)==(.+)$") if name and ver then sbomgen.push_package({ name = name, version = ver, purl_type = "generic", namespace = "my-custom-ecosystem", component_type = sbomgen.component_types.APPLICATION, }) end end end テストの実行 プラグインにはテストフレームワークが組み込まれているため、実際のアーティファクトをスキャンする前にロジックを検証できます。テストは Lua で記述し、プラグインと同じ場所の init_test.lua に配置して、 _testdata/ 内のフィクスチャデータを参照します。 function test_discovers_packages() local result = testing.scan_directory("_testdata") testing.assert_equals(3, #result.findings) testing.assert_equals("my-package-alpha", result.findings[1].name) testing.assert_equals("1.0.0", result.findings[1].version) end function test_no_findings_for_empty_directory() local result = testing.scan_directory("_testdata/empty") testing.assert_equals(0, #result.findings) end 次のコマンドでテストを実行します。 inspector-sbomgen plugin test --path my-sbomgen-plugins -v === RUN my-custom-ecosystem/discovery/init_test/test_discovers_packages --- PASS: my-custom-ecosystem/discovery/init_test/test_discovers_packages (0.04s) === RUN my-custom-ecosystem/discovery/init_test/test_no_findings_for_empty_directory --- PASS: my-custom-ecosystem/discovery/init_test/test_no_findings_for_empty_directory (0.04s) ok 2 tests passed これは、私たちが設計し得た最も短い開発ループです。Go ツールチェーンも、再ビルドも、コンテナの起動も不要です。テストを書き、実行し、繰り返し改善するだけです。 実際のアーティファクトのスキャン プラグインが結果を生成するには、プラグインが探すファイルを含むアーティファクトを inspector-sbomgen に与える必要があります。サンプルプラグインの場合、 example.lock ファイルを含む任意のディレクトリが対象になります。先ほど生成したフィクスチャがちょうど良い題材です。 inspector-sbomgen directory \ --plugin-dir ./my-sbomgen-plugins \ --path ./my-sbomgen-plugins/discovery/cross-platform/extra-ecosystems/my-custom-ecosystem/_testdata \ -o sbom.json --plugin-dir フラグは、Lua プラグインの読み込み元を inspector-sbomgen に伝えます。生成される SBOM には、 example.lock 内の 3 つのパッケージそれぞれに対応する CycloneDX コンポーネントが含まれます。例を以下に示します。 { "bom-ref": "comp-2", "type": "application", "name": "my-package-alpha", "version": "1.0.0", "scope": "optional", "purl": "pkg:generic/my-sbomgen-plugin/my-package-alpha@1.0.0", "properties": [ { "name": "amazon:inspector:sbom_generator:source_path", "value": "./my-sbomgen-plugins/example.lock" } ] } プラグインが生成するすべてのコンポーネントには、収集元のファイルを記録する amazon:inspector:sbom_generator:source_path プロパティが付いています。そのため、コンポーネントを生成元のアーティファクトまで常にたどることができます。 Amazon Inspector による脆弱性スキャン プラグインが生成したパッケージ情報は、他のコンポーネントと同等の正式な SBOM コンポーネントとして扱われます。Amazon Inspector を含め、CycloneDX SBOM を読み取るあらゆる下流のツールで利用できます。SBOM を Amazon Inspector に送信して脆弱性分析を行うには、 --scan-sbom フラグを追加します (有効な AWS アカウントが必要です)。 inspector-sbomgen directory \ --path ./my-sbomgen-plugins/discovery/cross-platform/extra-ecosystems/my-custom-ecosystem/_testdata \ --plugin-dir ./my-sbomgen-plugins \ --scan-sbom \ --aws-profile your_profile \ --aws-region your_region \ -o /tmp/sbom.json まったく新しいエコシステムに対応する際の重要な注意点 : プラグイン作成者は任意のエコシステムをインベントリ化できますが、Amazon Inspector が脆弱性を報告できるのは、アドバイザリが存在するコンポーネントに限られます。アドバイザリフィードにまだ含まれていないエコシステムのコンポーネントを Amazon Inspector に渡すと、Amazon Inspector は Component skipped: no supported rules found (コンポーネントはスキップされました: サポートされるルールが見つかりません) というプロパティ付きでコンポーネントを返します。以下に例を示します。 { "bom-ref": "comp-1", "name": "my-package-alpha", "properties": [ { "name": "amazon:inspector:sbom_scanner:path", "value": "my-sbomgen-plugins/discovery/cross-platform/extra-ecosystems/my-custom-ecosystem/_testdata/example.lock" }, { "name": "amazon:inspector:sbom_scanner:info", "value": "Component skipped: no supported rules found." } ], "purl": "pkg:generic/my-custom-ecosystem/my-package-alpha@1.0.0", "type": "application", "version": "1.0.0" } これはエラーではなく、想定どおりの動作です。SBOM は正しく生成され、コンポーネントは引き続き追跡され、 source_path によってどのファイルから生成されたかを正確に把握できます。Amazon Inspector がそのエコシステムのアドバイザリカバレッジを追加すれば、プラグインを一切変更することなく、同じ SBOM から脆弱性の検出結果が生成されるようになります。Amazon Inspector がすでにサポートしているエコシステムについては、プラグインが生成したコンポーネントは組み込みスキャナーが生成したコンポーネントと区別なく扱われます。 ファーストクラスの IDE サポート AWS は、プラグインを書くときの生産性と効率を重視しています。オートコンプリートのようなモダンな便利機能なしで Lua を書くのは快適とは言えません。そのため、 plugin new コマンドでスキャフォールディングされたすべてのプラグインプロジェクトには、 library/sbomgen.lua 定義ファイルと、それを VS Code の Lua Language Server 拡張機能に自動的に接続する .vscode/settings.json が付属します。 コード補完と IDE サポートを利用するには、まず sumneko.lua 拡張機能をインストールし、VS Code でプラグインプロジェクトを開きます。これにより、すべての sbomgen.* 関数で次の機能が使えるようになります。 型情報付きのパラメータヒント ホバー時のドキュメント表示 定数のオートコンプリート ( sbomgen.component_types.* 、 sbomgen.groups.* 、 sbomgen.platform.* ) 関数呼び出しの型チェック push_package() に必須フィールドが欠けている場合のインライン警告 この定義ファイルのおかげで、AI コーディングアシスタントによるプラグイン開発もうまく機能します。型情報とドキュメントがツールで読み取れる形式で埋め込まれているため、アシスタントは、素の Lua で記述する場合に比べてはるかに少ない人手の確認で正しいプラグインコードを生成できます。 安全な基盤 プラグインは inspector-sbomgen と同じプロセス内で実際のコードを実行するため、そのコードが安定し、セキュリティが強化された状態を保てるように実行環境を設計しました。すべての Lua プラグインは隔離されたサンドボックス内で実行されます。各 Lua 仮想マシン (VM) は、安全な操作のみが許可されるように、Lua 標準ライブラリの制限されたサブセットにのみアクセスできます。 ファイルシステムへの直接アクセスの禁止 – Lua の io ライブラリはロードされません。すべてのファイル操作は sbomgen.* 関数を経由して sbomgen の内部処理にルーティングされるため、ディスク上のディレクトリ、コンテナイメージ、圧縮アーカイブ、マウントされたボリュームのいずれをスキャンする場合でも、プラグインは同じように動作します サブプロセスの実行や環境の変更の禁止 – Lua の os ライブラリはブロックされているため、プラグインはプロセスの起動、環境変数の変更、アーティファクト外のファイルへのアクセスができません VM のイントロスペクションの禁止 – Lua の debug ライブラリはブロックされています 無制限なコードロードの禁止 – dofile 、 loadfile 、 loadstring は削除されています。 require() は利用できますが、プラグイン自身のディレクトリツリーに制限されているため、プラグインは自身のヘルパーモジュールを共有できる一方、他のプラグインやシステムパスからコードをロードすることはできません プラグインが未処理の Lua エラーを発生させた場合、inspector-sbomgen は警告をログに記録し、次のファイルまたはプラグインの処理を続行します。1 つの不具合のあるプラグインが他のプラグインの実行を妨げることはありません。また、プラグインが inspector-sbomgen の組み込みパッケージコレクターを上書きすることもありません。すべてのプラグインは一意の名前を宣言する必要があり、カスタムプラグインが公式の組み込みプラグインですでに使われている名前を使用した場合、そのカスタムプラグインは警告付きでスキップされます。組み込みプラグインが常に優先されるため、カスタムプラグインがツール自身の検出動作をひそかに置き換えたり隠したりすることはできません。 次のステップ 今すぐ独自のプラグインの構築を始めるには、次の手順に従ってください。 Amazon Inspector ユーザーガイド から最新の inspector-sbomgen をインストールします inspector-sbomgen plugin new --with-example を実行し、プロンプトに従います inspector-sbomgen plugin test --path ./my-sbomgen-plugins -v を実行し、サンプルテストがパスすることを確認します サンプルのロジックを、独自のエコシステム向けの検出ロジックに置き換えます すべての関数、定数、コマンドについては、以下の完全なリファレンスドキュメントで詳しく説明しています。 Lua プラグイン開発者ガイド : プラグインの概念、ディレクトリ構造、ライフサイクル Lua プラグインテストガイド : テストフレームワークのリファレンスとフィクスチャの規約 Lua プラグイン API リファレンス : sbomgen.* API の完全なカタログ まとめ 組織独自のロックファイル形式への対応の追加、新しいオープンソースエコシステム向け検出のプロトタイピング、あるいは自作スキャナーから組織全体で大規模に運用できる仕組みへの置き換えなど、どのような用途であっても、このプラグインシステムは、アイデアから動作する SBOM までの道のりをできる限り短くするように設計されています。皆さんがこれを使って何を作るのか、とても楽しみにしています。 この記事に関するご質問がある場合は、 AWS サポートにお問い合わせください 。 Michael Long Michael は AWS の Amazon Inspector 担当 Senior Security Researcher です。Amazon Inspector SBOM Generator と Amazon Inspector for GitHub Actions の研究開発を率いています。AWS 入社前は、MITRE ATT&CK チームで principal adversary emulation engineer を務めていました。また、U.S. Army (米国陸軍) で約 10 年間、軍事情報およびサイバー作戦に従事しました。 Charlie Bacon Charlie は AWS の Amazon Inspector 担当 Head of Security Engineering and Research です。Amazon Inspector や他の Amazon Security の脆弱性管理ツールを支える脆弱性スキャンおよびインベントリ収集サービスを担当するチームを率いています。AWS 入社前は、金融業界とセキュリティ業界で 20 年間にわたり、研究と製品開発の両分野で上級職を務めました。 Anthony Verleysen Anthony は Amazon Inspector 担当の Senior Technical Product Management です。Amazon Inspector の前は、AWS Systems Manager の Product Manager として Node Management 機能を担当していました。仕事以外では、テニスとサッカーに熱心に取り組んでいます。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

本ブログは 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 著者について Ali Saidi Ali は Amazon Web Services (AWS) のバイスプレジデント兼 Distinguished Engineer です。ミシガン大学でコンピュータサイエンスおよび工学の博士号を取得しています。2017 年に AWS に入社して以来、AWS Nitro System、AWS Graviton、および幅広い EC2 インスタンスファミリーのポートフォリオの設計と開発に注力しています。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

本ブログは 2026 年 4 月 17 日に公開された Amazon Science Blog “ Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine ” を翻訳したものです。 Isabelle/HOL は、数学的な記述の表現力、自動化、スケーラビリティのバランスによって、世界初の形式的に検証されたクラウドハイパーバイザーを実現しました。 2025 年の Amazon re:Invent カンファレンスにおいて、Amazon Web Services (AWS) は Nitro Isolation Engine (NIE) を発表しました。NIE は、お客様のデータのセキュリティを確保しながら AWS のお客様にリソースを提供する役割を担うソフトウェアモジュールです。あわせて AWS は、 Isabelle/HOL という定理証明支援系 (proof assistant) を使用して、この Isolation Engine の正当性とセキュリティ保証を形式的に検証したことも発表しました。世界初の形式的に検証されたクラウドハイパーバイザーとして、NIE はクラウドセキュリティの新しい標準を打ち立てています。 Isabelle はもともと ケンブリッジ大学 と ミュンヘン工科大学 で開発され、現在は世界中の機関や個人による数多くのコントリビューションを取り込んでいます。 定理証明支援系とは、人間のユーザーが形式的証明を構築するのを支援する自動化ツールです。その対象は、数学の定理からハードウェアやソフトウェアシステムの妥当性まで、あらゆるものに及びます。広く使われている定理証明支援系はいくつかありますが、私たちが Isabelle/HOL を選んだのは、表現力、自動化、証明の読みやすさ、スケーラビリティのバランスが私たちの用途に最も適していたからです。これは具体的にどういうことなのでしょうか? コンピュータによる論理的推論 数学に決まった言語というものはありませんが、プログラミング言語が計算タスクを表現するのと同じように、数学的推論を表現するための言語を作ることができます。そして、プログラミング言語に表現力とパフォーマンスのトレードオフがあるように、数学的言語にも表現力と自動化のしやすさのトレードオフがあります。形式的証明の構築は時間がかかり、極めて根気のいる作業であるため (ボトルの中に船を組み立てる作業に似ています)、自動化は不可欠です。 形式的証明の構築は、ボトルの中に船を組み立てる作業に似ています。厳格な論理的制約の中で、すべての部品を正確に組み立てなければなりません。Isabelle/HOL は、この緻密な作業を可能にするツールを提供します。 最も初歩的な数学的言語はブール論理です。これは、AND、OR、NOT といった論理演算子の世界です。この言語は非常にシンプルであるため、強力な自動ソルバーが存在します。2016 年、カーネギーメロン大学の Marijn Heule 教授 (現在は Amazon Scholar ) とその同僚たちは、未解決の数学的問題であるブール・ピタゴラス数問題をブール論理に符号化し、自動ソルバーを使って、200 テラバイトという 史上最大の証明 を作り上げました。 一階述語論理 と呼ばれるより豊かな数学的言語では、整数などの対象領域について語り、その領域上の関数を定義できます。また、「すべての～について」や「～が存在する」という 量化子 を主張に含めることで、ブール論理を超える表現が可能になります。この種の言語では、「2 より大きいすべての素数は奇数である」といった文を表現できます。また、Lewis Carroll による次の定理を証明することもできます。 ワルツを踊るアヒルはいない。ワルツを断る士官はいない。私の家禽はすべてアヒルである。ゆえに、私の家禽の中に士官はいない。 しかし、ほとんどの人は、プログラミングと同じように型を定義できる、さらに強力な数学的言語を好みます。 高階論理 には、 Haskell などの関数型プログラミング言語に見られるような関数型さえ存在します。高階論理は一階述語論理よりもはるかに豊かで、「 数 1 を含み、加法について閉じているすべての集合は、すべての正の整数を含む 」といった文を表現できます。数学の大部分を表現できるほど豊かであると考えられています。 最も豊かな数学的言語である 依存型理論 では、型が任意の値をパラメータとして取ることさえ可能です。例えば T(i) のように、 i を整数とすることができます。この種の言語で最もよく知られているのは Lean と Rocq です。 一階述語論理には強力な自動定理証明器が存在しますが、高階論理やそれ以上の言語では、完全な自動化は利用できません。これが表現力の代償です。 定理証明支援系 を使えば、ユーザーは部分的な自動化の支援を受けながら対話的に証明を構築でき、独自の証明探索をコーディングすることも可能です。定理証明支援系は、論理法則への厳格な準拠を強制します。これは通常、定理を作成する権限をコードの限られた部分にのみ与えるカーネルアーキテクチャによって実現されます。 定理証明支援系は、非常に大規模になり得る形式的仕様の階層を対話的に開発することもサポートします。例えば、Nitro Isolation Engine (NIE) の検証は、Graviton-5 プロセッサのアーキテクチャの仕様、ハイパーコールの Rust コードとその機能的正当性、そして証明すべきセキュリティ特性の仕様の上に成り立っています。形式的証明を構成する 25 万行の大部分は、これらの仕様が占めています。 高階論理は、密接に関連する 2 つの定理証明支援系である HOL と HOL Light でサポートされており、1990 年代からハードウェア設計、浮動小数点アルゴリズム、純粋数学の検証に使われてきました。AWS のシニアプリンシパルアプライドサイエンティストである John Harrison は HOL Light を開発し、暗号アルゴリズムの最適化バージョンを検証することで、Amazon の Graviton2 チップにおけるデジタル署名の パフォーマンスを最大 94% 向上 させました。このコードは繊細であり、網羅的なテストは 現実的ではありません 。このような重要なソフトウェアをデプロイする前に取り得る手段は、完全な機能的正当性の形式的検証しかありませんでした。しかし、ここで注目したいのは Isabelle/HOL です。 Isabelle/HOL の概要 Isabelle/HOL と他の HOL システム (いずれも高階論理に基づいています) の最も目に見える違いは、その仕様記述言語と証明言語です。ほとんどの定理証明支援系では、ユーザーは証明したいことを記述した後、一種のモグラたたきゲームのように、元のゴールを一連のサブゴールに置き換えるコマンドを次々と続けていきます。Isabelle では (Lean でもある程度は)、証明言語によって望ましい中間ゴールを明示的に書き出すことができるため、証明プロセスをより適切に制御でき、より読みやすい証明ドキュメントが得られます。 オンラインには多くの例 があります。 その他の 注目すべき機能 は以下のとおりです。 Rust 言語のかなりの部分を仕様に埋め込むことを可能にした ユーザー設定可能なパーサー 例えば + に、さまざまな数値型だけでなくマシンワードやその他の適切な文脈でも自然な意味を与える、原則に基づいたオーバーロードのための 型クラス 仕様の階層を定義し、証明の中でさえさまざまな方法で解釈できる軽量なモジュールシステムである ロケール (locales) 単純化と後ろ向き連鎖による証明探索を通じた、強力な 組み込みの自動化 さらに強力な外部の自動化にワンクリックでアクセスできる sledgehammer 実際には偽である主張を特定するための 反例発見ツール 適合性のテストに使用した、実行可能な高階仕様からの コード生成 NIE の検証にあたっては、まず 分離論理 (separation logic) と呼ばれる特化した言語を Isabelle/HOL の上に実装することから始めました。分離論理は、共有リソースを操作するプログラムコードの検証のために設計されたものです。私たちは独自の証明自動化をコーディングし、組み込みの自動化も活用しました。そのため、分離論理を使いつつ、必要に応じて通常の高階論理も使うことができました。Isabelle は、非常に巨大なサブゴールにも対処できるほど堅牢かつ効率的であることがわかりました。市販のラップトップを使って、25 万行の証明を 30 分で実行できたのです。 Isabelle/HOL の応用事例 NIE 以前の Isabelle の応用事例として最も印象的なのは、おそらく広く使われているマイクロカーネルである seL4 の検証 でしょう。この証明も最初に発表された時点では約 25 万行でしたが、現在ではさらに長くなっています。seL4 の開発者たちは、マイクロカーネルの C 実装が抽象的仕様を詳細化したものであることを証明し、コア操作の完全な機能的正当性を実現しました。そして、検証されたコード部分ではバグが一切観測されていません。ただし、未検証の部分や形式化できない一部の前提条件をカバーするために、テストは依然として重要な役割を果たしています。 Isabelle は以下のプロジェクトでも使用されました。 エラーの特定、特にその型システムの 健全性の証明 を目的とした、 WebAssembly 言語のセマンティクスの形式化 Cogent プログラミング言語のための 検証フレームワーク の作成 分散編集に使用される、競合のないレプリケートデータ型 (CRDT) のアルゴリズムの 正当性の証明 純粋数学における 数多くの結果の形式化 抽象レベルでの 暗号プロトコルの検証 Isabelle は無料のオープンソースソフトウェアであり、 ダウンロードして利用 できます。十分なメモリを備えたマシンであれば、主要なオペレーティングシステムすべてで動作します。 著者について Larry Paulson Larry Paulson は、ケンブリッジ大学の計算論理学の名誉教授であり、Amazon Scholar です。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。