初めてブログを書きました。キクと申します。 普段はPower Platform関連の業務対応をしているエンジニアです。 今回は私がPower Automateを触り始めたころに苦戦したフローについて解説します。その内容は、

Amazon Bedrock の API キーの正体は IAM のサービス固有認証情報です。short-term と long-term の違い、既定ポリシーが許す範囲、そしてアクセスキー流出時に攻撃者が長期キーを発行する連鎖とその防ぎ方までを IAM の観点から整理しました。

本ブログは 2026 年 8 月 11 日に公開された Amazon Science Blog “ A decade of mathematical certainty: Reflections on the Automated Reasoning Group ” を翻訳したものです。 Automated Reasoning Group の設立から 10 年。数学的論理は学術研究の領域を越え、お客様の数百万のワークロードを守る本番サービスにまで広がりました。これは、システムが単に「おそらく正しい」だけでなく、「正しいと証明できる」ものになり得ることを示しています。 2016 年、Amazon の小さな研究チームが Automated Reasoning Group (ARG) の発足とともに、その存在を世界に向けて発信しました。掲げたビジョンは大胆なものでした。数学的論理を用いて AWS のシステムをテストするだけでなく、正しく動作することを数学的な確実性をもって証明する、というものです。 それから 10 年。ARG は、形式的検証の進歩によってこれまで解決困難だった問題を AWS の規模で緩和できるのかを模索する段階から、AWS のセキュリティと信頼性への取り組みの根幹を成すシステムを構築する段階へと進みました。ARG の本番サービスは、1 日あたり数十億件のクエリを処理しています。 本記事では、最先端の形式的検証とプログラム解析の技術を Amazon 特有の課題にどう適用してきたかを振り返ります。この取り組みの原動力となったのは、現実世界のセキュリティとインフラストラクチャの問題を、AWS の規模で数学的な厳密さをもって解決できるという確信でした。実際、当時研究していたようなツールは、Intel や NASA では既に成果を上げていました。ただ、これらの技術がここまで広範に適用できるようになるとは、十分に予測できていませんでした。 デモから大規模な本番環境へ 2016 年に第 1 回 ARG Demo Day を開催したとき、AWS Security に向けていくつもの野心的なプロジェクトを紹介しました。それぞれが、同じ根本的な問い、すなわち「自分たちのシステムが安全かつ正しいことを数学によってどう証明できるのか」に対する異なるアプローチでした。その日に示された答えは、2026 年の今も AWS とお客様にとって重要な役割を果たし続けるシステムの土台となっています。 Sean McLaughlin は「Automatic tools for reasoning about virtual private clouds (VPC)」と題したプレゼンテーションを行いました。VPC ネットワークの拡大に伴い、設定ミスやセキュリティ脆弱性を特定できる自動推論ソリューションへの需要が高まっていると指摘したうえで、その答えとして示したのが「 Tiros というツール で、簡単に言えば、ネットワークに関する質問に答えてくれるもの」でした。 Tiros は、 Amazon Inspector のネットワークセキュリティ分析機能の基盤となりました。Amazon Inspector は、クラウドでアプリケーションを構築する数百万のお客様にご利用いただいています。Tiros は AWS 内部でも、多くの AWS サービスにおけるコンプライアンス認証の確認やセキュリティ不変条件の遵守チェックを自動化する用途で使われています。現在では、Amazon Inspector と Reachability Analyzer の両方を支えています。この取り組みからは Zelkova も派生しました。Zelkova は 自動推論 を用いて、ポリシーとそれが将来もたらす結果を分析します。 S3 Block Public Access や IAM Access Analyzer をはじめ、数多くのツールが Zelkova を基盤としています。 同様に、その日には、重要なインフラストラクチャを対象とする詳細な自動解析の活用をテーマにしたプレゼンテーションも行われました。これが、TLS ハンドシェイクの正しさや、暗号、ストレージ、仮想化のコードが備えるその他の性質を証明する取り組みへとつながりました。 紹介した小規模なプロジェクトの中にも、その規模をはるかに超える影響をもたらしたものがあります。価値の高いインフラストラクチャに対する演繹的検証の取り組みを発表した当時、その適用範囲は主に暗号プロトコルの最も深い部分に限られていました。しかし今日、その重要性は飛躍的に高まっています。これを後押ししたのが、証明支援システム (proof assistant) の台頭です。証明支援システムとは、ユーザーが形式的な証明を作成するのを助ける自動化ツールで、自動推論 (AR) チームの senior principal scientist である Leo de Moura が作成した Lean などがあります。AWS は現在、こうしたツールを言語モデルと組み合わせることで、より多くの、そしてはるかに大規模なシステムの証明を見つけられるようになりました。実際、 Nitro Isolation Engine について発表した証明 は、まさにそれを裏付けるものです。これは、AWS のポリシーインタープリターの証明や、暗号基盤の正しさを証明する近年の取り組みの基礎にもなっています。 お客様が信頼を寄せる数学的保証 この 10 年間で、ARG の研究プロトタイプは、数百万の AWS のお客様が毎日利用するサービスへと発展しました。 IAM Access Analyzer は Zelkova を利用して、USAA や GoTo といったお客様がリソースへの意図しないアクセスを特定できるよう支援します。セキュリティポリシーが正しく設定されていることをただ期待するのではなく、お客様はポリシーが実際に何を許可しているのかを、数学的な証明という形で確認できます。 2016 年にデモを行った Tiros をベースに構築された Reachability Analyzer は、パケットを 1 つも送信することなく、ネットワークの接続性を把握できるよう支援します。設定をテストするのではなく、考えられるすべてのネットワーク経路を数学的に分析し、宛先に到達できるかどうか、到達できない場合はどのコンポーネントが妨げているのかを示します。 Amazon Bedrock Guardrails の 自動推論チェック は、生成 AI に数学的な検証をもたらします。この機能は、モデルの応答が定義されたポリシーに準拠していることを形式論理で検証し、AI のハルシネーションの防止に役立ちます。検証精度は最大 99% に達します。 これらのお客様向けサービスには共通の基盤があります。いずれも 充足可能性モジュロ理論 (satisfiability modulo theories、SMT) ソルバーなどの自動推論技術を用いてシステムの動作に関する数学的保証を提供し、従来のテストで到達できる範囲をはるかに超えています。 クラウドを支えるインフラストラクチャの正しさの証明 お客様向けのツールは自動推論の実用的な価値を示すものですが、最も困難な取り組みの一部は AWS 内部のインフラストラクチャに向けられてきました。数百万のワークロードが依存しているため、正しさが不可欠なシステムです。 AWS は自動推論を用いて、次に挙げるものをはじめ、インフラストラクチャの多くの部分について正しさを証明してきました。 AWS Nitro Isolation Engine s2n-bignum などの暗号実装 AWS データセンターで動作するブートコード S3 などのストレージシステム とりわけ野心的だったプロジェクトでは、1 秒あたり 10 億回の API コールを処理する認可エンジン全体の正しさを証明し、シームレスに置き換えました。仕様と証明を用い、新しいエンジンを数千兆件に及ぶ本番環境の認可判定に対して検証したのです。 こうした内部検証の取り組みは、クラウドインフラストラクチャの最も基礎的な層に対しても、自動推論が数学的確実性をもたらせることを示しています。 予想外の発見 この 10 年の取り組みでおそらく最も意外だったのは、自動推論はシステムをより安全にするだけでなく、多くの場合、より効率的で保守しやすいものにするという発見です。検証のために厳密な仕様を書く必要が生じると、チームはより単純で洗練された解決策に気付くことがよくあります。 その理由の一つは、自動推論によって可能になる、システム全体を対象としたアプローチにあります。自動推論は、特定のシナリオにおけるシステムの動作を検証することに主眼を置くのではなく、論理を用いて 起こり得るあらゆる シナリオでの動作を検証します。考えられるすべての入力シナリオとその失敗のしかたを洗い出すのではなく、システムがどのように動作すべきかを定義し、その動作に必要な条件を特定します。そして、それらの条件が真であることを数学的証明によって検証します。つまり、システムそれ自体が正しいことを検証できるのです。 この発見は、数学的な厳密さと実践的なエンジニアリングは対立するものではなく、互いに補い合うものだという確信を裏付けました。形式的検証に求められる規律は、そうでなければ見えないままだった単純化の機会をしばしば浮かび上がらせます。 エージェンティック AI を支える基盤の構築 10 年前に始めた研究によって、AWS は AI 開発の次の時代に向けた独自の強みを備えることになりました。分散システムや重要なコードの検証で培った成果は、いまや AI が生成したコードの検証に直接活かせる土台となっています。一方、AWS ポリシーや VPC ネットワークの設定ミスに関する研究は、AI が生成したコンテンツの正しさを検証するのに役立っています。 この進化は、近年のいくつかのローンチに表れています。 Amazon Bedrock Guardrails の自動推論チェック は、深い専門知識を必要とするツールから、ビルダーが毎日使うサービスに直接組み込まれた機能へと歩を進めた、重要な節目です。 Amazon Bedrock AgentCore の Policy は、自動推論を用いてエージェントのアクションに明確な境界を設定し、エージェントが自律的に動作しながらも定められたコンプライアンスの境界内にとどまるようにします。チームは自然言語で、エージェントがアクセスできるツールとデータを指定できます。 AgentCore Gateway と統合すれば、システムはミリ秒単位でポリシーをチェックします。 エージェンティックな開発環境である Kiro では、 要件分析機能 をリリースしました。この機能は自動推論を用いて、コードを書く前にソフトウェア要件に矛盾、あいまいさ、抜け漏れがないことを証明し、コードの正確性を高め、後々のデバッグの繰り返しを防ぎます。Kiro を開発しているチーム自身も、機能を公開する前に、その機能を実装する AI 生成コードが正しく動作するかを自動推論で確認しています。 AI エージェントがより自律的になり、より複雑なタスクを担うようになるほど、その動作に関する数学的保証は決定的に重要になります。AI エージェントが形式仕様を備えたシステムへのコード変更を提案すれば、そのシステムは数学的証明に照らして変更を自動的に検証できます。自動推論は、強力であるだけでなく、安全性と信頼性を証明できる AI システムを構築する道筋をもたらします。 10 年にわたるコラボレーション この取り組みは、築き上げてきた優秀なチームと、重要なインフラストラクチャの保護を AWS に託してくださったお客様なしには実現できませんでした。AWS 全体で、各チームが自動推論の能力を拡大し続けています。 Senior principal scientist の Daniel Kroening が率いる Annapurna のチームは、ハードウェア検証を前進させています。Senior applied scientist の Nadia Labai は、自然言語を形式的な数学的証明へ変換することを AI システムに学習させる自動形式化 (auto-formalization) の研究を切り開いています。Principal applied scientist の Tristan Ravitch が率いる AWS Security のチームは、AWS と Amazon の全アカウントにわたるデータフローを自動的に追跡する Peri をローンチしました。サービスチーム側でのオンボーディングは一切不要です。 これらの取り組みによって、AWS は自動推論の次の 10 年を、最初の 10 年と同じくらい、あるいはそれ以上に変革的なものにする態勢を整えています。 証明してきたこと 10 年を経て、これまで達成してきたことに大きな喜びを感じています。設定エラーの防止から AI システムの動作に関する数学的保証の提供まで、自動推論はあらゆる層で測定可能な価値をもたらすことを証明してきました。そして、数学的な厳密さと実践的なエンジニアリングが手を携えて、お客様が実際に抱える課題を大規模に解決できることを示してきました。 2016 年の最初の Demo Day から今日に至るまでの道のりは、学術的な進歩をお客様が日々頼りにするサービスへと変えていくという AWS の姿勢を体現しています。数学的確実性を通じて信頼の基盤を築いてきました。その基盤は、AI イノベーションの次の 10 年を進むうえで欠かせないものとなるでしょう。 次の 10 年に向けて。 著者について Byron Cook Amazon の vice president 兼 distinguished scientist である Byron Cook は、形式的検証分野のリーダーです。SAT、SMT、記号モデル検査への貢献と、それらを生物システム、コンピュータオペレーティングシステム、プログラミング言語、セキュリティへ応用したことで知られています。Amazon での Byron の自動推論の取り組みは、クラウドにおけるより高い水準の保証と、新しいお客様向け機能をもたらしました。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。