本記事は 2026 年 8 月 3 日に公開された Clare Liguori、Romain Dura、Al Harris、Richard Threlkeld による “ One agent, every surface: how we built the Kiro agent harness ” を翻訳したものです。 Kiro の開発初期、私たちは開発者の 1 日のなかでエージェント駆動の開発がどのように感じられるべきかを議論し始めました。繰り返し立ち返ったのは、セッションがラップトップとクラウドサンドボックスの間を摩擦なく行き来する姿でした。1 日の終わりにラップトップを閉じても、Kiro セッションはクラウドで動き続けます。コーヒーを取りに行く合間にスマートフォンから状況を確認できます。翌朝、Kiro IDE を開いて中断したところから作業を再開します。 Web 版 Kiro でプロジェクトを開始し、Kiro IDE でコンテキストを追加し、既にテストとイテレーションを進めているターミナルでは Kiro CLI を使い続け、Slack から進捗を確認します。エージェント駆動の開発とは、作業するあらゆるクライアントを横断する 1 つの連続した会話であるべきです。 今年の初め、私たちはエージェントのアーキテクチャがこのビジョンの実現を妨げていることに気づきました。当時、Kiro IDE、CLI、Web の各クライアントは、それぞれ独自のセッションフォーマット、ツールセット、設定モデルを持つ専用のエージェントを実行していました。セッションと環境の間を容易に移動するには、どのクライアントを使っていても、どこで動作していても同じように振る舞う単一のエージェントが必要です。クライアント専用のエージェントアーキテクチャでは、エージェント同士が十分な共通基盤を持っていなかったため、あるクライアントで開始したセッションを別のクライアントに移すことができませんでした。本記事では、3 つのエージェントのコードベースを 1 つの Kiro エージェントハーネスに統合した過程 (もちろん Kiro 自身を使って構築しました) と、私たちのビジョンを実現可能にしたアーキテクチャ上の決定について解説します。 分岐していった 3 つのハーネス Kiro を作り始めた当初、私たちはスピードと実験を優先しました。各クライアントチームが独自のエージェントハーネスを作ることを推奨しました。エージェントハーネスとは、エージェントループ、ツール実行、サブエージェントへの委譲、セッション管理、設定のロード、モデルとの通信を管理するオーケストレーション層のことです。IDE チームは Code OSS の拡張モデルに合わせて TypeScript で、CLI チームはパフォーマンスを重視して Rust で、Web チームは最新のエージェント研究に近い場所に居るために Python で、それぞれ独自に構築しました。 ハーネスを分けたことで各チームは独立して素早くリリースし、イテレーションできましたが、同時にそれぞれのチームが異なる選択をすることも意味しました。セッションストレージはクライアントごとに動作が異なりました。権限システムは独立して設計されており、互換性のない構文を使っていました。CLI は正規表現ベースの allowedCommands / deniedCommands を使い、IDE は trustedCommands にプレフィックスマッチを、denylist にはサブストリングマッチを使っていました。コンパクション戦略も分岐しました。サブエージェントのコンテキスト共有も異なるモデルに従っていました。カスタムエージェントもクライアントごとに動作が違いました。機能セットも分裂しました。仕様駆動開発と powers は IDE のみで動作し、プランモードとコードインテリジェンスは CLI のみで動作していました。 実装コストは時間とともに複利で膨らみました。新しい機能は 3 回作って 3 回保守する必要があり、その結果としてエージェントの挙動がわずかに異なることもありました。バグも 3 回修正する必要がありました。ユーザーはどのクライアントを選ぶかによって不整合を体験することになりました。セッションがクライアントとコンピュートを横断して移動するという私たちのビジョンは、共有のセッションフォーマット、共有のツールセット、共有の設定モデルが存在しないためアーキテクチャ的に不可能でした。各チームの独立性と個別のスピードを維持するために、クライアント間でエージェントの振る舞いに関する契約を合意し、3 つのハーネスそれぞれで実装するという案も検討しました。しかしインターフェースの整合を取ることも、新機能ごとに増えていく調整コストを生みます。新機能ごとに仕様書、3 つの実装、そして同一の振る舞いを継続的に検証する作業が必要になるのです。 転機となったのは、Web 版 Kiro のパブリックローンチの準備を進めていたときでした。Web 版 Kiro を独自のエージェントとともにローンチし、この複利的な実装コストを払い続けるのではなく、各チームが学んだベストな知見を組み合わせた単一のエージェントハーネスを構築することを決めました。単一のハーネスであればチーム間の重複がなくなり、すべての労力を 1 箇所に集中投資できます。 Kiro エージェントハーネスのアーキテクチャ 私たちが早い段階で下した重要なアーキテクチャ判断は、ハーネスを各クライアントにコンパイルして組み込むライブラリではなく、独立したサーバープロセスとして構築することでした。過去の試みから、共有ライブラリでは十分に強い境界を強制できないことがわかっていました。クライアントコードは公開を意図していない内部メソッドを呼び出し始めるか、ライブラリの上に独自のエージェントロジックを重ねてしまいます。そうなれば実装は再び分岐していきます。独立したプロセスであれば、この分離が現実のものになります。ハーネスとクライアントは同じ言語やランタイムを共有する必要がないため、各クライアントは自分のプラットフォームに適したスタックのまま留まれます。 これにより、3 つの密結合したクライアントとエージェントのペアではなく、 ┌────────────┐ ┌────────────────────────────────┐ │ Kiro IDE ├──────│ IDE agent (TypeScript) │ └────────────┘ └────────────────────────────────┘ ┌────────────┐ ┌────────────────────────────────┐ │ Kiro CLI ├──────│ CLI agent (Rust) │ └────────────┘ └────────────────────────────────┘ ┌────────────┐ ┌────────────────────────────────┐ │ Kiro Web ├──────│ Web agent (Python) │ └────────────┘ └────────────────────────────────┘ クライアントと単一のエージェントハーネスとの間にきれいな分離ができました。 ┌─────────────────────────┐ ┌─────────────────────────────────┐ │ Clients │ │ Kiro agent harness │ │ │ │ │ │ UX and presentation │ │ Agent loop │ │ User interaction │───protocol───│ Tools and sub-agents │ │ Platform-native tools │ │ Session state │ │ (optional overrides) │ │ MCP client │ │ │ │ Configuration and steering │ │ │ │ Permissions │ │ │ │ Telemetry │ └─────────────────────────┘ └─────────────────────────────────┘ Kiro エージェントハーネスはコードベースの隣で動作する軽量なプロセスで、高速に起動し、エージェント側のすべてを所有します。クライアントはユーザーがエージェントとどのようにやり取りするか、エージェントの作業をどのように提示するかを所有します。この境界を越える唯一の方法は、定義されたプロトコルインターフェースです。コンパイルされて組み込まれるライブラリではなく独立したプロセスであるため、あらゆるコンピュート上で動作できます。同じハーネスがラップトップ上でも、クラウド上の VM 内でも、クライアントに意識させることなく起動できます。 サーバーとクライアントの間に明確なインターフェースがあるということは、エージェントのコードがクライアントとは独立して進化することを意味します。ハーネスの変更がプロトコルインターフェースに影響を与えない場合 (たとえば新しいツールの追加、プランニングの改善、エージェントループのチューニング)、クライアント側の変更ゼロですぐにすべてのクライアントにリリースできます。たとえば最近、カスタムエージェントのライブリロード機能を追加しました。セッション中に .kiro/agents/ のファイルを編集すると、ハーネスがすぐに検知し、利用可能なコマンドをクライアントに再度通知します。利用可能なコマンドの通知タイプはすでにプロトコルに存在していたため、クライアントの変更は不要でした。どのクライアントも追加の変更なしにこの機能を手に入れられたのです。 サポート対象のクライアントが多様なため、このハーネスは画一的な設計ではありません。クライアントごとに機能が異なり、一部の操作はクライアントネイティブの機能を使ってクライアント層で実装するほうが理にかなっています。クライアントは独自のツールを提供して組み込みツールを抑制でき、自分のフォームファクター (form factor) に合ったものを使えます。たとえば IDE はファイル操作に Code OSS の API を使い、ファイルシステム上で直接動作するハーネスの組み込みツールではなく、独自のファイル読み書きツールを提供しています。エージェントがこれらのクライアント提供ツールのいずれかを実行する必要があるときは、クライアントに通知し、クライアントがツールを実行して結果を返します。 プロトコル: Agent Client Protocol (ACP) クライアントとハーネスの境界を定義するプロトコルとして、 Agent Client Protocol (ACP) を選びました。ACP はエージェントとクライアントの通信を標準化した仕様で、2026 年 6 月に 1.0 に到達しました。このプロトコルは JetBrains の IDE、Xcode、Zed といった IDE や、Obsidian、Emacs、Neovim といったほかのエディターでもサポートされています。私たちは今年の初めに Kiro CLI で ACP を採用した経験 から、これらのアプリケーション内で直接 Kiro とやり取りできるようにしていました。統一されたハーネスにも ACP を採用することにしたのは、サードパーティ製エディター向けだけでなく、Kiro 自身のクライアントと私たち自身のエージェントの間のインターフェースとして使うためです。ACP の 2 つの性質がこれを可能にしました。カスタムメソッドに対する拡張性と、トランスポートの柔軟性です。 ACP は公式にトランスポートとして stdio をサポートしています。これはハーネスがエディターやターミナルの子プロセスとして動作するローカルクライアントで機能します。Web 版 Kiro や iOS アプリのようなリモートクライアントには、別のトランスポートが必要でした。これらのクライアントがクラウドサンドボックスで動作するハーネスに接続できるように、独自の WebSocket ベースのトランスポートを追加しました。クライアントがどのトランスポートを使うかに関わらず、バイナリ、ツール、エージェントの振る舞いは同一です。 ┌─────────────────────────────────────────────────────────────┐ │ Kiro agent harness │ └──────────┬────────────────┬────────────────┬────────────────┘ │ stdio │ stdio │ WebSocket │ │ │ ┌──────┴──────┐ ┌──────┴─────┐ ┌───────┴──────────────┐ │ Kiro CLI │ │ Kiro IDE │ │ Kiro Web · iOS app │ │ (terminal) │ │ (Code OSS) │ │ (browser · mobile) │ └─────────────┘ └────────────┘ └──────────────────────┘ トランスポートを超えて、私たちは ACP のメソッドセットを Kiro-ACP と呼ぶものに拡張しました。標準の ACP は基本的な部分 (セッションのライフサイクル、メッセージのストリーミング、ツール呼び出しのレポート) を扱いますが、Kiro の機能にはそれ以上のものが必要でした。たとえばライブステアリングを追加しました。ユーザーはエージェントの作業中でもメッセージを送信でき、そのメッセージが次の推論ターンで注入されることで、キャンセルや待機なしにエージェントの方向性を調整できます。ACP はメッセージのキューイングをサポートしていないため、ライブステアリングを実現するために新しいメソッドプロパティと通知で ACP を拡張しました。また Kiro の仕様駆動開発ワークフローを専用のメソッド群としてモデル化し、ACP の基本的なツール承認を豊富なマルチスコープの権限システムへと拡張し、コンテキストウィンドウの使用状況とフック実行に関する通知を追加しました。合計で Kiro-ACP はベースプロトコルに加えて 20 を超えるエージェント呼び出し可能なメソッド、15 のクライアント呼び出し可能なメソッド、20 の通知タイプを追加しています。ACP の拡張モデルはこれをきれいに保ちます。仕様どおり、カスタムメソッドはアンダースコアのプレフィックスを使い、Kiro の拡張はすべて _kiro/ 名前空間の下に配置されています。プロトコルをフォークすることなく、Kiro 固有の機能のために拡張できるのです。 結果として、サードパーティのクライアントはファーストパーティのクライアントと同じ方法で接続できます。ACP 互換のクライアントであれば、ツール、サブエージェント、セッション管理、MCP 接続を含む完全なエージェントを利用できます。ファーストパーティのクライアント (IDE、CLI、Web、iOS) は加えて Kiro-ACP の拡張を利用して、ライブステアリング、仕様、リッチな権限 UI、コンテキスト使用量トラッキングといった機能を提供します。 仕様、エージェント、フックがどこでも使える 単一のハーネスがもたらす直接的なメリットは、これまで 1 つのクライアントに閉じ込められていた機能が、同じ設定フォーマットと同じ振る舞いで、どのクライアントでも使えるようになったことです。 仕様駆動開発 は以前は IDE 限定でした。今では CLI ( /spec new で開始できます) と Web 版 Kiro でも動作します。エージェントは仕様ワークフローを駆動する LLM とのやり取りと自動化された推論 (要件の生成、技術設計の作成、作業のタスクへの分解) を扱い、各クライアントは自分のフォームファクターに合った形でそれを提示します。IDE は仕様のアーティファクトを横並びのペインで表示します。CLI はターミナル内でレンダリングします。Web 版 Kiro はブラウザーでインラインレビューとマルチユーザーコラボレーションとともに表示するので、チームが一緒に仕様をイテレーションできます。エージェントは ACP を話し、クライアントは出力をどう提示するかを決めます。 カスタムエージェント は、どのクライアントでも同じ .kiro/agents/ Markdown フォーマットを使います。エージェントには説明、システムプロンプト、タグベースのツール選択 (個別のツール名ではなく read 、 write 、 shell といったシンプルなタグ)、アクセス可能なサブエージェント、インラインの MCP サーバー定義、インラインの権限ルールを定義できます。カスタムエージェントの設定をバージョン管理にコミットすれば、チームメンバー全員がすべてのクライアントで使えるようになります。 --- description: セキュリティ上の問題を確認するコードレビューエージェント tools: [read, shell, "@github"] permissions: rules: - capability: fs_read effect: allow - capability: shell match: ["git diff *", "git log *", "npm audit"] effect: allow mcpServers: github: url: https://api.githubcopilot.com/mcp/ headers: Authorization: Bearer ${GITHUB_TOKEN} --- あなたはセキュリティに重点を置いたコードレビュアーです。現在の差分を レビューし、脆弱性、認証情報の漏洩、安全でないパターンを確認してください。 依存関係のアドバイザリは npm audit で確認してください。 フック は同じ .kiro/hooks/*.json フォーマットを使い、同じトリガー ( SessionStart 、 PreToolUse 、 PostToolUse 、 FileCreate 、 FileSave ) で、すべてのクライアントで同じように動作します。 機能の可用性を超えて、統一されたハーネスは、正しく作るのが難しい領域でも一貫した振る舞いを提供します。コンテキスト管理、コンパクション、要約は、どのクライアントを使ってもすべて同じように動作します。以前はハーネスごとに独自のコンパクション戦略を持っていたため、IDE、CLI、Web クライアントのどれを使っているかによってセッションが長くなるにつれて振る舞いが変わることがありました。今では 1 箇所で実装、テスト、改善される単一の実装があります。統一されたハーネスをクライアント全体に展開して以来、コンテキスト保持を改善するため、ハーネスにより良いコンパクションプロンプトをすでにリリースしています。またハーネスの深い部分でレジリエンスとパフォーマンスの改善もリリースしました。モデル推論リクエストの改善されたリトライロジック、高速な権限評価、より弾力性のある MCP サーバー接続などです。すべてのクライアントがこれらの変更の恩恵を受けます。結果として、どのクライアントを好むかに関わらず、一貫した品質と信頼性が得られます。 単一のポリシー言語 統一ハーネスが登場する前、各クライアントは異なる構文、異なるセマンティクス、異なる設定場所を持つ独自の権限システムを持っていました。CLI は正規表現パターンによる allowedCommands / deniedCommands を使いました。IDE はプレフィックスマッチによる trustedCommands と、サブストリングマッチによる別の commandDenylist を使いました。どちらのクライアントでも権限はツール単位でした。 .env への読み取りを拒否する といった単一の意図は、ファイルを読める各ツール (read、glob、grep、コードインテリジェンス) に対して個別に設定する必要があります。1 つでも見落とすと、エージェントは別のツール経由でそのファイルにアクセスできてしまうのです。ユーザーはツール呼び出しごとに y を押し続けるか、すべてを信頼するかの二択を迫られ、その中間の実用的な選択肢がありませんでした。私たちが求めていたのは、ケイパビリティレベルで意図を表現でき、永続的かつ組み合わせ可能な同意によって承認疲れ (acceptance fatigue) を減らせる権限モデルでした。 今では、形式的に検証されたポリシー言語である Cedar に支えられた、単一のケイパビリティベースの権限モデルがあります。1 つのルールで、すべてのツールにまたがる同種の操作をまとめて対象にできます。 rules: # Block all tools that read files from accessing secrets - capability: fs_read match: [".env", ".env.*", "secrets/**", "**/*.pem"] effect: deny # Allow specific shell commands without prompting - capability: shell match: ["npm test *", "npm run build", "git status"] effect: allow # Allow an MCP server's tools - capability: mcp match: ["github/*"] effect: allow ケイパビリティはツールを機能ごとにグループ化します。 fs_read 、 fs_write 、 shell 、 web_fetch 、 mcp 、 subagent などです。fs_read の deny は、ファイルを読むすべてのツール ( read_file 、 grep_search 、 file_search 、そして今後追加される read 系ツール) を個別に列挙することなくブロックします。 ポリシーは複数のスコープにまたがって合成でき、deny が常に勝つセマンティクスでマージされます。Kiro 自体は変更不可能なセキュリティ不変条件を適用します (たとえば、エージェントは自身の権限ファイルを変更できません)。エンタープライズ管理者は MDM 経由で制限をプッシュできます。ユーザーは自分のルールをユーザーレベルまたはワークスペースレベルで設定します。エージェントプロファイルはその役割に応じた権限を宣言できます。セッションレベルの判断は、作業しながら積み上がっていきます。事前の設定は不要です。ポリシーは同意の判断を下すにつれて自然に育っていき、意味のあるスコープでそれを永続化できます。 ハーネスがビジョンを解き放つ 新しいエージェントハーネスアーキテクチャの成果はすでに現れています。すべてのクライアントが統一ハーネスに移行して以来、クライアント側の変更ゼロで複数の機能をクライアント横断でリリースしてきました。グローバルフックとポリシープリセットもその一例です。 グローバルフック は ~/.kiro/hooks/ でフックを一度定義するだけで、すべてのワークスペースで自動的に発火するため、保存時のリント実行やコミット前のセキュリティチェックといった横断的な振る舞いをプロジェクトごとに複製する必要がなくなります。 ポリシープリセット は edit-workspace や dev-shell のような合成可能な名前付きルールセットで、一般的なワークフローにおけるプロンプト疲れ (prompt fatigue) を減らします。権限にポリシープリセットを追加すると (たとえば policies: [dev-shell, edit-workspace, read-all] )、ハーネスのポリシーエンジンがロード時にそれらを個別のルールに展開します。どちらの機能もハーネスのアップデートだけですべてのクライアントに提供されました。 本記事の冒頭で述べたビジョンには、まだ構築が必要なエージェントの能力 (ケイパビリティ) がいくつかあります。たとえば、環境間でセッションを移動するためのセッションパッケージングや、ローカルとクラウドの両方のセッションをどのクライアントからも制御できる機能などです。統一されたハーネスなら、新しい能力を一度作るだけで済みます。多くの場合、グローバルフックやポリシープリセットのように、クライアント側の変更ゼロですべてのクライアントに配信できます。統一ハーネスがクライアント側の作業を完全になくしたわけではありませんし、そうしたいわけでもありませんでした。ターミナル、デスクトップの IDE、ブラウザー、スマートフォンは異なるインタラクションモデルを持っており、私たちは画一的な体験を提供するのではなく、各クライアントがそのフォームファクターに合った体験に感じられることを望んでいます。新しいエージェントハーネスアーキテクチャなら、エージェントのロジックはクライアント全体で同一で、各クライアントチームはそれとどうやり取りするのがベストかに集中できます。 Kiro のユーザーとして、新しいエージェントハーネスアーキテクチャは、新しい能力がより速く届き、一貫した振る舞いを示し、あなたが好むクライアントに関わらず同じ設定で動作することを意味します。 新しい Kiro エージェントハーネスを試す 新しい Kiro エージェントハーネスは 4 つの Kiro クライアントすべてでライブ稼働しているので、今日から試せます。 Kiro IDE 1.0 は、ケイパビリティベースの権限、タグベースツールとインライン MCP を備えたカスタムエージェント、並列セッションを指揮するためのエージェントフォーカスモード、ドッキング可能なチャットタブ、セッションエクスポートを提供します。 IDE 1.0 のドキュメントと移行方法 を参照してください。 Kiro CLI v3 (アーリーアクセス) は、仕様駆動開発、permissions.yaml、拡張されたフック、新しいエージェント設定フォーマットを備え、ターミナルで同じ統一ハーネスを実行します。 kiro-cli --v3 で試せます。 CLI v3 のドキュメントと移行方法 を参照してください。 Web 版 Kiro (プレビュー) はクラウドサンドボックスでハーネスを実行し、ブラウザーで仕様を使った自律的な開発、マルチリポジトリセッション、GitHub と GitLab の統合を提供します。 サインイン / サインアップ できます。 iOS 版 Kiro (プレビュー) は Web 版 Kiro と同じクラウドセッションにスマートフォンから接続し、ラップトップを開かずに自律的な作業のキックオフ、差分のレビュー、変更の承認を行えます。 アーリーアクセスをリクエスト してください。 翻訳は 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 年 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 は、実行前にすべてのリクエストをチェックします。 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 が自分自身の電源をオンにしようとした場合 (誤ったリクエスト) に何が起こるかを記述したものです。 対象の CPU をオンにするための電源状態関数 PSCI_CPU_ON の仕様。 上記の仕様は複雑ですが、その内容は直感的にはシンプルです。この状況では、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’ は、パブリックレジスタの値が異なるため、 識別可能 になってしまいます。賢い観測者はこれを利用して元のプライベートレジスタの値を導き出せてしまいます。つまり、識別不能性が保存されないということは、観測者への不正な情報フローが生じていることを意味します。 今後の展開 ここまで、検証の取り組みにおける主要な要素の概要をご紹介しました。この取り組みには、適合性テストや、並行コードに関する推論の扱い方など、他にも多くの側面があります。今後の記事でお伝えできることを楽しみにしています。 著者について Dominic Mulligan Dominic Mulligan は、Amazon の Automated Reasoning Group の principal applied scientist です。 Nathan Chong Nathan Chong は、Amazon の Automated Reasoning Group の principal applied scientist です。並行システムコードの正当性、特にハードウェアとソフトウェアの境界領域を専門としています。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。