本ブログは 2026 年 5 月 19 日に公開された AWS Blog、” CIRT insights: How to help prevent unauthorized account removals from AWS Organizations ” を翻訳したものです。 AWS Customer Incident Response Team (CIRT) は、お客様がアクティブなセキュリティインシデントから復旧するためのご支援を行っています。この活動の中で、特定の お客様の構成や設計 を悪用する、新しいまたは流行している攻撃手口を発見することがしばしばあります。 これらの手口を理解することは、アーキテクチャ上の意思決定への反映、対応計画の改善、そして実際にこのような状況が発生した場合の検出に役立ちます。 本投稿では、攻撃者がお客様アカウントの制御を奪取した後に取る新しいアプローチを取り上げます。具体的には、お客様の AWS Organizations 実装から該当アカウントを離脱させ、その構造が提供するポリシーや保護を回避する手口です。 本記事で説明する手口は、AWS サービスの脆弱性を利用するものではありません。代わりに、特定の構成や設計によって生じた予期しない機会を悪用し、AWS アカウント内のリソースを不正に使用するものです。 何が起きているのか このアプローチは、攻撃者が organizations:LeaveOrganization 権限の付与を持つクレデンシャルを使用するところから始まります。この権限は LeaveOrganization API コール へのアクセスを提供し、メンバーアカウントから呼び出されると、そのアカウントを Organization から離脱させようとします。 重要な点として、このアプローチでは侵害されたルートクレデンシャルが使われる場合もありますが、攻撃者は他の手段でアクセス権を昇格させ、必要な権限を取得したり、その権限を持つロールを引き受ける能力を獲得したり、現在のクレデンシャルにこの権限を付与する能力を獲得したりすることもできます。これが、認可に対して 最小権限のアプローチ を取ることが、お客様の環境を保護する上で極めて重要である理由です。詳細については、 AWS Identity and Access Management (IAM) ドキュメント と、 組織単位 (OU) 設計および サービスコントロールポリシー (SCP) 実装に関する AWS Organizations のガイダンスをご覧ください。 お客様の環境への影響 アカウントが Organization から離脱させられると、その Organization の一部として継承されていた制限 (破壊的なアクションを防止していた SCP、利用可能な AWS リージョンを制限していたもの、特定の API コールをブロックしていたもの等) が適用されなくなります。また、当該アカウントは一括請求 (Consolidated Billing) の対象外となるため、Organization の請求アラートやコスト異常検知も該当アカウントの活動をカバーしなくなります。 AWS CloudTrail の組織トレイルは離脱したアカウントからのイベント取得を停止し、委任管理者を介して管理されていた Amazon GuardDuty の検出結果も中央のセキュリティアカウントへ流れなくなります。 その結果しばしば発生するのは、Organization が当該アカウントへの可視性を失う一方で、そのアカウント内には引き続き Organization のリソースが残るという状況です。関連する Threat Technique Catalog のエントリを以下に示します。 T1078.A002: Account Root User : 侵害されたルートクレデンシャルを利用した初期アクセス T1078.004: Cloud Accounts : 侵害された IAM クレデンシャルを利用した初期アクセス T1098: Account Manipulation : 制御を維持するための権限昇格とアカウント設定の変更 T1666.A002: Leave AWS Organization : SCP やガバナンスコントロールを回避するため、メンバーアカウントを Organization から離脱させる T1562.008: Disable Cloud Logs : Organization からの離脱後、中央集約型ロギングの可視性が失われる この手口の検知 アカウントが Organization からの離脱を試みると、CloudTrail には少なくとも 2 つの API コールが記録されます。 organizations:AcceptHandshake と organizations:LeaveOrganization です。中央集約型のロギングを構成している場合、これらのイベントが侵害アカウントから観測される最後のイベントとなる可能性があります。Organization からの離脱後、デフォルトではアカウント内のイベントは自身の CloudTrail ログに記録されることになります。アカウントが Organization に参加または離脱する際に関連する CloudTrail イベントを以下に示します。これらのイベントは、AWS Organizations を管理するためにチームが利用する承認済みの運用ワークフローの一部でない限り、調査が必要です。 CloudTrail イベント 意味 LeaveOrganization メンバーアカウントが Organization から離脱しようとしている AcceptHandshake アカウントが別の Organization への参加招待を承諾している InviteAccountToOrganization Organization がアカウントを招待している RemoveAccountFromOrganization 管理アカウントがメンバーアカウントを削除している (メンバー自らが離脱する場合とは異なる) この手口を防ぐための推奨ステップ organizations:LeaveOrganization アクションを拒否する SCP を実装してください。AWS Organizations は この制御の実装に関する詳細なガイダンス を提供しており、具体的な SCP ポリシー JSON や、本番環境および開発環境のアカウントには保護を維持しつつ正当なアカウント移行を許容できる OU 構造の設計に関するアドバイスが含まれています。 SCP は、メンバーアカウント内で IAM ポリシーが許可できる範囲を制限するガードレールとして機能します。AWS Organizations をご利用のすべてのお客様には、この SCP が現在配置されているかを確認し、配置されていない場合には実装に向けた手順を踏むことを強く推奨いたします。この SCP は迅速にデプロイでき、運用上の影響も最小限です。メンバーアカウントを Organization から分離することを慎重に管理・検討するためのプロセスを提供します。 このアクションは、ルートだけでなく organizations:LeaveOrganization 権限を持つあらゆる侵害された IAM プリンシパルから発生し得るため、IAM 権限の最小権限原則は重要な補完的な制御となります。ユーザーやロールがポリシーの追加・削除・変更を行ったり、別のロールを引き受けたり、自身の権限を変更したりできる範囲を制限することで、不正な権限変更が行われる経路を減らすことができます。IAM ポリシーを定期的にレビューし、過度に広範な権限 (特に iam:AttachRolePolicy 、 iam:AttachUserPolicy 、 iam:PutRolePolicy 、および広範な信頼ポリシーを伴う sts:AssumeRole ) を確認することは、侵害されたプリンシパルが実行できる範囲を制限するのに役立ちます。 ルートアカウントのセキュリティは引き続き重要です。ルートの侵害がこのパターンの一般的な侵入経路となるためです。すべてのルートユーザーに対して多要素認証 (MFA) を有効化し、ルートアクセスキーを削除し、メンバーアカウントからルートクレデンシャルを完全に取り除く ルートアクセスの一元管理 を採用することで、リスクの軽減につながります。 今後について 本手口は、私たちが様々なエンゲージメントを通じて目にしている、より広範なテーマを浮き彫りにしています。攻撃者は AWS のガバナンスコントロールがどのように機能するかをますます認識しており、Organization が提供する制御からアカウントを切り離すための意図的な手段を取っています。AWS CloudTrail を無効化する、Amazon GuardDuty ディテクターを削除する、Organization からアカウントを離脱させるといった行為は、いずれも同じ戦略の派生形にあたります。すなわち、本来であれば攻撃者の活動を制約し、お客様による対応を支援するはずのガードレールと可視性から、お客様のアカウントを切り離すというものです。 これを防ぐための制御は本日時点で利用可能であり、実装も簡単です。 AWS Organizations サービスチームのガイダンス から始め、 DenyLeaveOrganizationSCP を実装することをお勧めします。本手口に対して、最も効果が大きく、かつ最も労力の少ない制御です。それ以外にも、OU 構造全体での SCP のカバレッジを見直すこと、すべてのメンバーアカウントでルートクレデンシャルと IAM 権限が適切に保護されていることを確認すること、検知・対応プロセスが本手口を考慮に入れていることを確かめることが、より強固なセキュリティ態勢に貢献します。 Threat Technique Catalog for AWS には、根底にある手口の検知ガイダンスが含まれています。 関連リソース Threat Technique Catalog for AWS – Matrix T1078.A002: Account Root User T1078.004: Cloud Accounts T1098: Account Manipulation T1666.A002: Leave AWS Organization AWS Organizations における不正なアカウント離脱を防止するための重要なセキュリティコントロール メンバーアカウントのルートアクセスを一元管理する AWS Organizations サービスコントロールポリシー Amazon GuardDuty AWS CloudTrail ユーザーガイド 本投稿に関するフィードバックがありましたら、下のコメントセクションにご投稿ください。 著者について Shannon Brazil Shannon は AWS Customer Incident Response Team (CIRT) のセキュリティエンジニアであり、デジタルフォレンジックとクラウドセキュリティ調査を専門としています。コミュニティでは 4n6lady として知られ、セキュリティ教育と次世代の防御者の育成に情熱を注いでいます。 Derek Ramirez Derek は AWS Customer Incident Response Team (CIRT) のセキュリティエンジニアです。サイバーセキュリティと、困難なインシデントレスポンスの課題への対処を支援する AI ツールの構築という、自身が情熱を注ぐ 2 つのことを組み合わせて取り組んでいます。オースティンのダウンタウンを走ったり、ゴルフのショートゲームに取り組んだり、Dallas Cowboys を熱心に応援したりしています。 Richard Billington Richard は AWS Customer Incident Response Team (アクティブなセキュリティイベント中に AWS のお客様をサポートするチーム) のアジア太平洋地域における Sr. Security Engineer です。 翻訳は Security Solutions Architect の 松崎 博昭 が担当しました。

本ブログは 2026 年 4 月 7 日に公開された Amazon Science Blog “ Verifying and optimizing post-quantum cryptography at Amazon ” を翻訳したものです。 自動推論によって、セキュリティ、性能、保守性の要求をどのように両立させるか。 現在、安全なオンライン通信は 公開鍵暗号 によって実現されています。主に RSA と楕円曲線暗号 (ECC) が使われており、その安全性はある計算問題が困難であるという仮定に依存しています。しかし、これらの問題は 従来の コンピュータでは困難と考えられているものの、十分に大規模な量子コンピュータでは扱える可能性があります。「Store now, decrypt later」(今保存して後で復号) 攻撃は、暗号化された情報を傍受しておき、量子コンピュータで復号できるようになるまで保持する攻撃です。こうした攻撃が技術的に実現可能になるよりはるか前から、対策が必要となります。 ポスト量子暗号 (PQC) は、従来のコンピュータ上で動作しながら量子コンピューティングに対しても安全な暗号です。2024 年、米国国立標準技術研究所 (NIST) は 8 年にわたる標準化作業を経て、標準規格 FIPS-203 を公開しました。FIPS-203 では、量子コンピュータからの攻撃に対して安全と考えられている鍵共有メカニズムとして、Module-Lattice-Based Key Encapsulation Mechanism (ML-KEM) が規定されています。 本記事では、Amazon Automated Reasoning Group、AWS Cryptography、そしてオープンソースコミュニティが協力して、ML-KEM のオープンソースかつ形式的に検証された最適化実装をどのように作り上げ、お客様を「Store now, decrypt later」攻撃から最高の保証と最小のコストで保護しているかをご紹介します。 優れた暗号エンジニアリングとは何か? Amazon の Customer Obsession に従い、AWS は暗号ソリューションに取り組む際、次の 3 つの目標を優先します。 お客様のデータのセキュリティ : 暗号は安全に実装することが極めて難しく、わずかな欠陥でもお客様のプライバシーを危険にさらす可能性があるため、万全を期す必要があります お客様の体験 : 暗号には計算コストが伴います。AWS はこれを最小化し、お客様に最小のコストと最良の体験を提供します ソリューションを将来にわたって保守する能力 : 保守に費やす時間が少ないほど、お客様のためにより多くのイノベーションを生み出せます しかし、これらの目標の間にはトレードオフがあります。シンプルなコードは保守も安全な記述も最も簡単ですが、動作が遅くなりがちです。一方、高速なコードは監査が難しく、エラーが起きやすい傾向があります。 自動推論 によって、AWS はこのトレードオフを解消し、安全で、高速で、保守しやすい暗号ソリューションを同時にお客様に提供できます。 なぜ新たな ML-KEM 実装が必要なのか ML-KEM (旧称 Kyber) は実装の観点から十分に研究されています。一方では、 Kyber リファレンスコード が、長年精査されてきたクリーンな C 言語実装を提供しています。他方では、ML-KEM をさまざまな指標やプラットフォーム向けに最適化する方法を記述した数多くの研究論文があります。 2024 年に AWS Cryptography と Amazon Automated Reasoning Group が直面した課題は、リファレンス実装のシンプルさと、研究で明らかになった最適化の可能性を、本番環境で使える単一の実装に組み合わせることでした。 2024 年、AWS Cryptography と Amazon Automated Reasoning Group は、徹底的に精査された ML-KEM リファレンス実装のシンプルさと、研究で明らかになった最適化の可能性を、本番環境で使える単一の実装 mlkem-native にまとめるという課題に取り組みました。 同じ頃、AWS は Linux Foundation の Post-Quantum Cryptography Alliance (PQCA) の創設メンバーとなりました。PQCA は、「標準化過程にあるポスト量子暗号アルゴリズムの高保証ソフトウェア実装の構築を目指すオープンソースプロジェクトの集合」である Post-Quantum Cryptography Package (PQCP) を立ち上げました。 そこで AWS は独自にコードを開発するのではなく、チームメンバーが PQCP に参加し、まもなく mlkem-native を立ち上げました。これは、ML-KEM リファレンス実装と、最適化および形式的検証に関する研究を組み合わせることを目的とした、ML-KEM の高保証・高性能 C 言語実装です。 速く、そして慎重なコーディング mlkem-native のモジュラー設計は、ML-KEM の高レベルロジックをカバーする フロントエンド と、性能が重要なすべてのサブルーチンを担当する バックエンド を組み合わせています。各サブルーチン (SHA3 の基礎となる Keccak 置換や、高速な多項式演算の基礎となる数論変換 (NTT) を含む) には、特定のハードウェア向けにネイティブに記述された、高効率な複数の実装が用意されています。デフォルトの C 言語実装に加えて、mlkem-native は AArch64、x86_64、RISC-V64 向けのアセンブリ/組み込み関数バックエンドを提供しています。 mlkem-native のモジュラー設計は、ML-KEM の高レベルロジックをカバーするフロントエンドと、性能が重要なサブルーチンの複数のハードウェア固有実装からなるバックエンドを組み合わせています。 保守性のために重要なのは、フロントエンドとバックエンドの間のインターフェイスが固定されていることです。新しいターゲットアーキテクチャ向けの最適化を追加する開発者は、バックエンド仕様に従って選択したバックエンド機能を実装し、フロントエンドはそのまま維持します。バックエンド仕様の策定は、見かけほど単純ではないことが分かりました。これについては以下で説明します。 限界を知る メモリ安全性 C プログラミング言語のよく知られた課題は、バッファオーバーフローのリスクです。メモリ領域の指定された境界を超えて書き込むと、データ構造が破壊され、悪意を持って悪用されると非特権コードの実行につながる可能性があります。こうした問題の総称が メモリ安全性 です。Rust のようなメモリ安全な言語は、範囲外アクセスの影響を制限できます (たとえば、未定義動作を示す代わりにパニックする)。しかし、間違いそのものを防ぐわけではありません。 型安全性 もう一つのよく知られた課題は ML-KEM の実装に関するもので、整数オーバーフローのリスク、つまり 型安全性 の側面です。RSA や ECC と同様に、ML-KEM はモジュラー演算に依存しています。モジュラー演算では、演算の結果を特定の数 (ML-KEM の場合は素数 3,329 で、 MLKEM_Q または単に q と表記) で割り、その剰余だけが次に持ち越されます。剰余演算子はパーセント記号 % で表されます。 論理的には、ML-KEM で 2 つの数 x と y を加算または乗算する必要がある場合、( x + y ) % q および ( x * y ) % q を計算する必要があります。たとえば、(294 * 38) % q = 11,172 % q = 1,185 となります。このような「即時」のモジュラー q 演算は、データを「正規」範囲 {0, 1, 2, … , q -1} で表すために常にモジュラー還元を適用するもので、極めて遅くなります。 効率的な ML-KEM 実装では、代わりに「遅延」モジュラー q 演算を使用します。データはできるだけ長くモジュラー還元なしで操作され、最悪の場合のオーバーフローのリスクが生じたときにのみ還元が行われます。さらに、これにより Montgomery 還元のような不完全な還元アルゴリズムが使えるようになります。これは高速ですが、必ずしも完全に還元された出力を返すわけではありません。 ML-KEM の場合、モジュラー q = 3,329 のデータは通常、符号付き 16 ビット整数に格納されます。ML-KEM の数多くの算術ルーチン全体で遅延演算を扱う際には、データの最悪値の境界を追跡し、それらの境界が 16 ビット整数の限界を超える可能性のある箇所にモジュラー還元を挿入することが不可欠です。この領域での小さな間違いは、テストで見逃されることがあります。なぜなら、平均的な境界は最悪値の境界よりはるかに小さい傾向があるためです。そして、本番環境でランダムに表面化することがあります。 バッファ境界、特に算術境界の追跡は、時間がかかり、エラーが起きやすい作業です。たとえば、低レベルの算術関数の出力境界を弱めると、まったく別の関数で稀に算術オーバーフローが発生することがあります。これを手作業で確認するには、緻密なドキュメント作成と熟練した監査担当者が必要なだけでなく、開発が遅くなります。 mlkem-native では、C Bounded Model Checker (CBMC) というツールを使用して、C レベルでメモリ安全性と型安全性を自動的に検証しています。各関数について、機械可読かつ人間可読な契約をソースコードに追加してバッファと算術データの境界を指定し、CBMC にそれらの境界に対してバッファオーバーフローや算術オーバーフローが発生し得ないことを自動的に検証させます。 モジュラー還元の簡単な例を見てみましょう。 void mlk_poly_reduce_c(mlk_poly *r) __contract__( requires(memory_no_alias(r, sizeof(mlk_poly))) assigns(memory_slice(r, sizeof(mlk_poly))) ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q))) { unsigned i; for (i = 0; i < MLKEM_N; i++) __loop__( invariant(i <= MLKEM_N) invariant(array_bound(r->coeffs, 0, i, 0, MLKEM_Q))) { /* Barrett reduction, giving signed canonical representative */ int16_t t = mlk_barrett_reduce(r->coeffs[i]); /* Conditional addition to get unsigned canonical representative */ r->coeffs[i] = mlk_scalar_signed_to_unsigned_q(t); } mlk_assert_bound(r, MLKEM_N, 0, MLKEM_Q); } 関連する部分を一つずつ見ていきましょう。まず、 __contract__( … ) に注目します。簡単に言うと、 memory_no_alias と memory_slice の行は、コードが読み書きできるメモリを指定しています。これはメモリ安全性に関連します。 ensures(array_bound(…)) 句は型安全性に関連しています。これは、関数が戻った時点でデータが区間 [0, 1, …, q ) 内にあることを 保証する ことを指定します。証明では、 __loop__(invariant(…)) があり、ループがこの境界を段階的にどう確立するかを指定しています。 i 番目のイテレーションでは、 i 番目の係数まで成立します。最後に、実装は実質的に mlk_barrett_reduce と mlk_scalar_signed_to_unsigned_q を組み合わせています。CBMC はこれらの内部を見ず、それらの契約に置き換えます。 int16_t mlk_barrett_reduce(int16_t a) __contract__( ensures(return_value > -MLKEM_Q_HALF && return_value < MLKEM_Q_HALF) { ... } int16_t mlk_scalar_signed_to_unsigned_q(int16_t c) __contract__( requires(c > -MLKEM_Q && c < MLKEM_Q) ensures(return_value >= 0 && return_value < MLKEM_Q) ensures(return_value == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q)) { ... } mlk_barrett_reduce がまず対称的な出力区間 ( -q /2, …, q /2) を確立し、次に mlk_scalar_signed_to_unsigned_q がそれを [0,1, …, q ) にマッピングしているのが分かります。この例では、仕様が望ましい形で整合していることを目視で簡単に確認できますが、より複雑な例ではそれほど明確ではありません。いずれにせよ、CBMC が自動的にチェックしてくれます。 速く動かしながら安全を保つ 上述の CBMC 証明は、mlkem-native の C コードに対するメモリ安全性と型安全性を確立します。しかし、mlkem-native の最も性能が重要な部分 (Keccak 置換と数論変換) は、AArch64 と x86_64 向けに手作業で最適化されたアセンブリで実装されています。 mlkem-native のアセンブリ実装に対して、高い性能を維持しつつ保証を得るために、AWS は次の 3 つのコンポーネントを使用しています。アセンブリのスーパーオプティマイザーである SLOTHY、対話型定理証明器である HOL Light、そして HOL Light 上に構築されたアセンブリ用検証基盤である s2n-bignum です。これらを組み合わせることで、開発者がクリーンで保守しやすいアセンブリを記述しつつ、デプロイされるコードが正当性の形式的保証を伴ってピーク性能を達成するワークフローが可能になります。 高性能なアセンブリを手で書くと、根本的なトレードオフが生じます。計算を明確に表現するクリーンで監査可能なコードは遅く、高速なコードは密で、マイクロアーキテクチャ固有で、保守が困難です。SLOTHY はマイクロアーキテクチャ固有の最適化を自動化することで、このトレードオフを解消します。アセンブリプログラムを制約充足問題に変換し、制約ソルバーを使用して最適な命令スケジュールとレジスタ割り当てを見つけ、最適化されたアセンブリを出力します。開発者は計算のロジックを重視したクリーンなコードを書き、SLOTHY が高速なコードを生成します。 AWS は、すべての AArch64 および x86_64 アセンブリルーチンの機能的正当性を、HOL Light と s2n-bignum を使用して証明します。SLOTHY が使用される場所では、特定の命令順序やレジスタ割り当てに依存しないように証明が記述されます。したがって、証明を調整することなく、特定のマイクロアーキテクチャ向けにコードを再最適化できます。この「事後」検証アプローチは、アセンブリで表現された計算の数学的な正しさを、それがどのように生成されたかにかかわらず確立します。特に、SLOTHY は信頼できるコンピューティングベース (TCB) から除外されます。 誠実さを保つ 形式的検証は決して絶対的なものではありません。すべての証明は、形式的なオブジェクト (仕様とモデル) を非形式的な現実世界の要件とシステムに結び付けるものであり、これらの結び付きにはギャップが生じます。形式的仕様は実際に必要なものを捉えているか? 形式的モデルは実際のシステムを忠実に反映しているか? 証明基盤自体は健全か? お客様の信頼を獲得し維持するには、これらの限界について透明性を保つ必要があります。そこで AWS は、 SOUNDNESS.md と題したドキュメントを作成・公開しました。ここでは、mlkem-native で何が証明され、何が仮定され、残存リスクがどこにあるかを、HOL Light 証明で使用されるハードウェアモデルの忠実性、CBMC のより大きな TCB、2 つの検証スタック間の手動の橋渡しに至るまでマッピングしています。各ギャップについて、実施されている緩和策を説明し、今後の作業の概要を示しています。 AWS の目標は完璧を主張することではなく、透明性を通じて信頼を獲得することです。コミュニティの皆様には SOUNDNESS.md を批判的に読み、AWS の前提に異議を唱え、残存するギャップを埋めることにご協力いただければ幸いです。 本番環境への展開 mlkem-native は、AWS サービス全体の安全な通信を支える Amazon のオープンソース暗号ライブラリ AWS-LC に統合されています。この統合では、自動インポーターを使用して mlkem-native のソースコードをアップストリームリポジトリから直接取り込み、AWS-LC が最新の検証済み実装と同期し続けることを保証します。 この統合は手間を最小限に抑えるよう設計されています。mlkem-native のモジュラーアーキテクチャにより、AWS-LC はコアの ML-KEM ロジックをインポートしながら、プラットフォーム固有のコンポーネントには独自の実装を提供できます。たとえば、AWS-LC は mlkem-native の暗号プリミティブを既存の FIPS-202 (SHA-3) 実装にマッピングし、AWS-LC の乱数生成およびメモリゼロ化関数を使用し、必要な場合はペアワイズ一貫性テストなど FIPS モード機能を有効にします。これを可能にしているのは、検証済みコードを変更することなく mlkem-native の API を AWS-LC のインフラストラクチャに橋渡しする薄い互換性レイヤーです。 重要なのは、メモリ安全性と型安全性を証明する CBMC 契約が、インポートされたソースコード内に保持されていることです。プリプロセッサがコンパイルされたバイナリからこれらを削除しますが、ソース内には残り、コードの保証の機械チェック可能なドキュメントとして機能します。これは、実装と共に移動する一種の「生きた証明」です。 さらに、mlkem-native も AWS-LC もオープンソースで寛容なライセンスのため、その利点は AWS の枠を超えて広がります。誰でも mlkem-native を自社のシステムに統合し、同じ性能と保証の組み合わせを得ることができます。形式的検証成果物 (CBMC 契約と HOL Light 証明) はリポジトリの一部であり、関連するすべてのツールはオープンソースであり、セットアップと証明チェックのスクリプトが提供されているため、AWS のセキュリティ主張を独立に検証できます。 インパクト mlkem-native の開発は、自動推論を体系的に適用すれば、暗号エンジニアリングの 3 つの目標 (セキュリティ、性能、保守性) が衝突しないことを示しています。 CBMC は、複雑な算術全体で境界を手動で追跡する作業から AWS を解放し、テストでは見逃されて本番環境でランダムに表面化するエラーを捕捉しました。アノテーションはソースコード内に機械チェック可能なドキュメントとして残り、コードを同時により保守しやすく、より安全にします。HOL Light と s2n-bignum により、AWS は数学的な正当性の確実性を持って積極的なアセンブリ最適化をデプロイできました。SLOTHY により、特定のマイクロアーキテクチャ向けにピーク性能を達成しながら、クリーンで監査可能なコードを書くことができました。そして、証明は最適化に依存しないように記述されているため、検証をやり直すことなくコードのターゲットを変更できます。 その結果、従来の開発で達成できるものよりも、同時により安全で、より高速で、より保守しやすい実装が実現しました。AWS はお客様のセキュリティ、お客様の体験、そして革新する能力の間で妥協しませんでした。自動推論は 3 つすべてを実現したのです。 AWS-LC-FIPS リリース プラットフォーム 処理 3.1 4.0 改善倍率 c7i Keygen 30899 65146 2.1 Encaps 30623 61233 2.0 Decaps 25141 51545 2.0 c7g Keygen 29617 71134 2.4 Encaps 28482 66874 2.3 Decaps 23919 64765 2.3 Amazon の暗号ライブラリ AWS-LC で ML-KEM リファレンス実装から mlkem-native に切り替えた際の性能影響。ML-KEM-768 の性能は c7i および c7g EC2 インスタンスで測定されています。数値は 1 秒あたりの処理数を表します (高いほど良い)。ベースラインは ML-KEM の C リファレンス実装を含む AWS-LC-FIPS 3.1 リリースです。AWS-LC-FIPS 4 リリースは mlkem-native でビルドされています。プラットフォームは Intel(R) Xeon(R) Platinum 8488C を搭載した c7i と、Graviton 3 プロセッサを搭載した c7g です。 謝辞 同僚の John Harrison 氏 (Automated Reasoning Group の senior principal applied scientist) には、HOL Light での AArch64 アセンブリ証明の大部分を提供し、また HOL Light 対話型定理証明器および s2n-bignum 検証基盤の保守を担当いただいたことに感謝します。mlkem-native は AWS だけでなく、オープンソースコミュニティの多くのメンバーが関わる共同作業です。とりわけ、共同保守者である zeroRISC の Matthias Kannwischer 氏に感謝します。彼は AWS と共に mlkem-native を立ち上げ、以来プロジェクトの成功に重要な役割を果たしてきました。 著者について Hanno Becker Hanno Becker は Amazon の Automated Reasoning Group の principal applied scientist です。元 Mbed TLS の開発者で、Arm 上の高性能 (ポスト量子) 暗号に情熱を注いでいます。SLOTHY スーパーオプティマイザーの作者でもあります。 Rod Chapman Rod Chapman は Amazon Web Services (AWS) の senior principal scientist です。 Dusan Kostic Dusan Kostic は Amazon Web Services (AWS) の senior applied scientist です。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

こんにちは。ソリューションアーキテクトの東 健一です。普段はパブリックセクター技術統括本部で中央省庁のお客様の技術支援を担当しており、主にガバメントクラウドや医療 DX に関わるご支援を担当しております。 2026年5月19日（火）に、AWS 目黒オフィスにて「ガバメントクラウドワークショップ 2026 春 ～ AI で実践する開発・モダナイズ・運用 ～」を開催しました。 本ワークショップは、ガバメントクラウドに携わる事業者様を対象に、移行を進める上で必要となる技術を深く学び (Dive Deep)、案件で直面するリアルな課題や他官公庁／自治体の取り組みを共有し、参加者同士の交流を楽しむ (Have Fun) ことを目的とした技術イベントです。 今回のワークショップでは、「 AI を使った開発・モダナイゼーション・運用 」をメインテーマに掲げ、事例セッション・デジタル庁様セッションに加え、参加者の皆様にあらかじめ関心のあるテーマを選択いただいたうえで、手を動かしながら学ぶ 4 つのテーマ別ワークショップを実施しました。当日は会場が満席となり、総勢150名以上の方々にご参加いただく盛況なイベントとなりました。さらに夜の部として、AWS ユーザーコミュニティ「JAWS-UG」の公共分野支部である Gov-JAWS との懇親会を併催し、日中のセッションを振り返りながら参加者同士の交流を深める時間としました。 なお、前回の開催内容について気になる方は下記のブログをご参照ください。 【開催報告】 第2回 自治体事業者向け AWS ガバメントクラウドワークショップ 2025 in 大阪 【開催報告】第三回 中央省庁向け AWS ガバメントクラウドワークショップ イベント概要 本ワークショップは以下のような形で実施しました。 日時 : 2026年5月19日（火）13:00 – 18:30（12:30 受付開始） 懇親会・Gov-JAWS: 18:30 – 21:00 場所 : アマゾン ウェブ サービス ジャパン合同会社 目黒オフィス 参加対象 : ガバメントクラウドに携わる全ての方々 時間 セッション・ワークショップ名 13:00-14:00 中央省庁担当 事業者様登壇 14:00-14:30 自治体担当 事業者様登壇 14:30-15:30 デジタル庁様登壇 15:30-15:40 休憩 15:40-18:30 各テーマに分かれて Workshop 18:30-21:00 懇親会 / Gov-JAWS イベント構成 オープニングおよび事例セッション・デジタル庁セッションを全体で実施した後、参加者の皆様にあらかじめ選択いただいた以下 4 つのテーマに分かれて、各部屋でハンズオン形式のワークショップを実施しました。 AI エージェントを開発する（Strands Agents / AgentCore） AI を使ってシステムをモダナイズする（AWS Transform / Kiro） AI を使ってシステムを開発する（Kiro IDE 実践） AI を使ってシステムを運用する（生成 AI を用いた AWS 環境のトラブルシューティング効率化） 各セッションの概要と発表資料は以下をご覧ください。 事例セッション・デジタル庁セッション ハイライト Step Functions で実現するフルマネージド・ジョブ開発 — ガバメントクラウド開発における 設計／開発・運用時の「理想と現実」のギャップ 発表資料 ： Step Functions で実現する フルマネージド・ジョブ開発（杉元） NTT データ 杉元様より、ジョブ管理ツールを AWS Step Functions を中核に据えてフルマネージドなジョブ機能として作り変えた取り組みについて、設計・開発・運用のリアルな学びとともにご紹介いただきました。「依存関係の表現」「再実行 / リラン」「リトライや補償」「並列実行」「監視・通知」「権限分離」といった “ジョブ管理っぽさ” を、Step Functions のステートマシンとしてどのように実装で落とし込んだかを共有いただきました。 あわせて、移行時に直面した設計／開発時の理想と現実（苦悩）のギャップ、稼働後に見えてきた運用時の理想と現実のギャップを、失敗事例も含めて整理いただきました。ジョブ管理ツールの置き換えを検討している方や、ワークフローを “運用できるジョブ基盤” にしたい方にとって、現実的な設計判断と運用設計の勘所を持ち帰れるセッションとなりました。 Amazon Bedrock で生成 AI 活用サービスをセキュアに構築する方法 発表資料 ： Amazon Bedrock で生成AI活用サービスをセキュアに構築する方法 – Speaker Deck アクロクエストテクノロジー 鈴木様より、 国土交通省様向けにAI書類審査ソリューションを構築支援したご経験 などを踏まえ、AWS の生成 AI サービスである Amazon Bedrock を前提として、どのように基盤モデルのセキュリティ対応を実現するかのポイントをご紹介いただきました。 あわせて、RAG（Retrieval-Augmented Generation）や AI エージェントといった生成 AI 活用サービスを構築する上でのセキュリティ観点を、構成例を交えながら解説いただきました。日本の公共案件で生成 AI を活用する際に求められるセキュリティの考え方が整理されており、これから生成 AI 活用に取り組む事業者様が設計の指針として持ち帰れる実用的な発表内容でした。 自治体ガバメントクラウドにおける生成 AI 活用 NTT 西日本 三浦様より、自治体のお客様向けに生成 AI を導入された取り組みについてご紹介いただきました。AWS が公開している OSS の生成 AI 活用基盤 GenU の閉域オプションをベースに、 Amazon Bedrock AgentCore を活用した独自 AI エージェントの開発を行っているとのお話で、自治体特有のセキュリティ要件を満たしつつ生成 AI 活用を進めるための実践的な設計・構築のポイントを共有いただきました。OSS をベースとしたうえで自社のユースケースに合わせて AgentCore で拡張するアプローチは、これから自治体向けに生成 AI 導入を検討する事業者様にとっても参考になる内容となっておりました。 GCAS ヘルプデスクについて 概要説明および活用方法のご紹介 デジタル庁 加藤様、萬谷様より、ガバメントクラウドにおける GCAS ヘルプデスクの役割と活動についてご紹介いただきました。GCAS ヘルプデスクの概要から、より効果的にご活用いただくための考え方や問い合わせ方法、実際のお問い合わせ事例やフィードバック、CSP (Cloud Service Provider) との連携内容、今後の改善に向けた方針までお話しいただきました。 GCAS ヘルプデスクが単なる問い合わせ窓口にとどまらず、利用者の声をガバメントクラウドの改善につなげる場であるというメッセージは、参加事業者様にとって今後の活用イメージを大きく広げるものとなりました。 ガバメントクラウドにおける生成 AI 利用環境「源内」の構築と展開 デジタル庁 荻原様より、政府職員の業務品質の向上と効率化を実現するために、ガバメントクラウド上に構築・展開している生成 AI 利用環境「 源内 」についてご紹介いただきました。現在、デジタル庁の職員のみならず、全府省庁約 18 万人の政府職員が生成 AI を利用できるよう、大規模実証事業を推進されています。 本セッションでは、ガバメントクラウドにおける「源内」のシステム概要と、大規模展開にあたって考慮した AI 特有の観点についてご説明いただきました。あわせて、行政業務に特化したアプリケーションの取り組みや、オープンソースソフトウェア (OSS) として公開された内容についてもご紹介いただきました。 ガバメントクラウド上での生成 AI 利用の最前線の取り組みを、構築・運用の双方の観点から伺えるセッションとなり、参加事業者様にとっても今後の生成 AI 活用案件に向けた貴重なリファレンスとなりました。 テーマ別ワークショップ Strands Agents, AgentCore を使った AI エージェントのデプロイ（AI エージェントを開発する） ワークショップ資料 ： AI エージェントハンズオン 〜 作って、動かして、体験する 〜 AWS ソリューションアーキテクトの松本より、オープンソースの AI エージェント開発フレームワークである Strands Agents を使ったエージェント開発の体験から、 Model Context Protocol (MCP) を使った AI エージェントの動きの理解、そして AgentCore Runtime を使った AI エージェントのデプロイまでを、一連のハンズオンとして体験いただきました。 さらに後半では、AWS 公式 GitHub で公開しているサンプル実装である RAPID （生成 AI を活用した書類審査ソリューション）と Moca （マルチエージェントオーケストレーションのサンプル）を実際にお試しいただき、業務適用イメージを具体化していただきました。実装から本番デプロイ、さらにユースケース特化型のサンプル実装までをエンドツーエンドで体験できる内容となり、生成 AI を活用したサービス開発の第一歩として手応えを感じていただけたワークショップとなりました。 Kiro IDE 実践ワークショップ（AI を使ってシステムを開発する） ワークショップ資料 ： Kiro IDE 実践ワークショップ AWS ソリューションアーキテクトの葉山より、生成 AI の概要解説からスタートし、生成 AI を使った開発体験、Kiro を活用した開発業務の効率化までを体験いただきました。仕様駆動開発（Spec-Driven Development）の考え方に基づき、要件定義からコード生成までを Kiro でどのように実現するかをハンズオンで学んでいただきました。「すぐにでも自分の業務で試したい」という声を多くいただいたワークショップとなりました。 生成 AI を用いた AWS 環境のトラブルシューティング効率化（AI を使ってシステムを運用する） ワークショップ資料 ： 生成AIを用いたAWS環境のトラブルシューティング効率化ワークショップ ワークショップ補足資料 ： 生成 AI を用いた AWS 環境のトラブルシューティング – Speaker Deck AWS ソリューションアーキテクトの東より、AWS 上に構築したシステムにおいてトラブルシューティングを生成 AI を用いて効率化するための手法をご紹介し、ハンズオンとして体験いただきました。ガバメントクラウドで活用できる手法・サービスを紹介しつつ、一般の AWS 環境でも活用可能な手法も併せてお試しいただける内容となり、運用業務の効率化に向けた具体的な打ち手を持ち帰っていただけました。 AWS Transform, Kiro を使ったモダナイゼーション（AI を使ってシステムをモダナイズする） AWS ソリューションアーキテクトの今坂より、AI エージェントによるレガシーコードの分析・バージョンアップグレード計画の自動生成を体験いただいた後、AI エージェントを活用したバージョンアップグレードを実際に体験いただきました。「これまで人手で時間をかけていたモダナイゼーション作業が、AI エージェントの活用でここまで自動化できるのか」という驚きとともに、自社案件への適用イメージを持ち帰っていただけたワークショップとなりました。 ※ ワークショップ資料については「Kiro IDE 実践ワークショップ」と同じコンテンツをベースに実施しております。 Gov-JAWS ワークショップと併せて、 Gov-JAWS の活動も行われました。Gov-JAWS は、AWS のユーザーコミュニティ「 JAWS-UG 」の支部として、公共分野における AWS 利用に焦点を当てた新しいコミュニティです。政府や自治体が進める公共分野のクラウド利用に関連する知識やノウハウを共有するための場として設立されました。 イベント当日は夜の部として Gov-JAWS 第 5 回 Meet Up が開催され、懇親会と併せて多くの参加者が交流を深めました。このコミュニティを通じて、今後も公共分野でのクラウド活用に関する情報共有と横のつながりの拡大が期待されています。 詳細は Gov-JAWS 側のページをご覧ください。 まとめ 今回のガバメントクラウドワークショップ 2026 春では、「AI エージェント開発」「モダナイゼーション」「AI 駆動開発」「AI による運用効率化」という生成 AI を軸とした 4 つのテーマに加え、ジョブ基盤の実装事例、生成 AI のセキュアな構成、自治体システム標準化の取り組み、GCAS ヘルプデスクの活用といった、ガバメントクラウドに携わる事業者様にとって直近で必要となるテーマを幅広く取り扱いました。 ご参加いただいた皆様におかれましては、お忙しい中ご足労いただき誠にありがとうございました。また、ご登壇いただいた NTT データ様、アクロクエストテクノロジー様、NTT 西日本様、デジタル庁様にも、貴重な知見をご共有いただきましたことを心より御礼申し上げます。 AWS では、今後もガバメントクラウドに携わる事業者様向けのワークショップを継続して開催してまいります。次回開催のご案内をお待ちください。 ガバメントクラウドに関するお問い合わせ AWS の公共チームではガバメントクラウド相談窓口を設けております。ガバメントクラウド利用全般に関するお問い合わせについて、担当の営業およびソリューションアーキテクトがご回答いたします。ぜひご活用ください。 https://aws.amazon.com/jp/government-education/worldwide/japan/gov-cloud-advisory-site/ 著者について 東 健一 アマゾン ウェブ サービス ジャパン合同会社のソリューションアーキテクト。パブリックセクター技術統括本部に所属し、主にガバメントクラウドや医療 DX 、コンテナワークロードに関する案件の技術支援に取り組んでいる。