本記事は、AWS re:Invent 2025に現地参加し、Level 500のセッションを聴講した内容についての紹介です。
▲ 実際のセッション会場の様子。満席で立ち見が出るほどの盛況でした！
はじめに
AWS re:Inventとは
AWS re:Inventは、AWSが開催する技術カンファレンスで、サービスアップデートから設計・運用・セキュリティ、研究寄りの深掘りまで幅広いセッションが提供されます。
Level 500の位置づけ
AWS re:Inventにおけるセッションは、対象者や技術的な深さによってレベル分けされています。
Level 500は、先端技術の研究者やスペシャリスト向けのセッションです。
| セッションレベル | 概要 |
|---|---|
| 100 (Foundational) | AWSサービスの概要や基本的なユースケースを学ぶ初学者向け |
| 200 (Intermediate) | 一般的なユースケースにおける設計、デプロイ戦略などを紹介 |
| 300 (Advanced) | アーキテクチャの詳細な設計や、具体的なベストプラクティスを紹介 |
| 400 (Expert) | より複雑な課題解決、高度なトラブルシューティングを紹介 |
| 500 (Distinguished) | 先端研究、理論的基盤、および新興技術がどのように実装に接続されているかを紹介 |
今回のセッション INV505
本記事では、数あるLevel 500セッションの中で「INV505で学んだ“仕組み（研究→実装）”」に絞って、噛み砕いて紹介します。
| 項目 | 内容 |
|---|---|
| セッション名 | IAM Access Analyzer from Research Paper to Reality (INV505) |
| 概要 | 理論計算機科学の研究成果が、実際のAWSセキュリティサービスにどう反映されているかを紹介 |
| 講演者 | Andrew Gacek (Senior Principal Applied Scientist, Amazon) |
| 形式/レベル | Chalk talk (Interactive) / Level 500 – Distinguished |
想定読者
- AWSの概要は知っている（少なくともIAMポリシーを触ったことがある）
- AWSサービスの裏側の仕組みに興味がある
1. TL;DR（本記事のまとめ）
INV505の学びを整理すると次の3点に集約されます。
- 問いの転換：IAMポリシー検証は「この設定は正しいか？」ではなく、「結局、だれが、どの条件なら通れるのか？」に問いを置き換えると上手くいく
- 良い検出結果の3条件：検出結果は「見落とさない(Sound)」「言い過ぎない(Precise)」「多すぎない(Compact)」の3つを同時に満たす必要がある
- 2つのコア技術：その条件を両立するために、「Stratified Abstraction（段階的な分割）」と「AWS Zelkova（数学的証明による検証エンジン）」が裏側で連携している
この記事で得られること
- 基礎研究を実際のサービスに落とし込む実践例を知ることができる
- IAM Access Analyzerというセキュリティサービスの裏側の仕組みが分かる
- 学術論文を読む際のハードルが少し下がる
2. 背景：IAMポリシーが引き起こす「論理パズル」の難しさ
IAMポリシーにおいて、Allow / Deny / Condition が一つでも組み合わさると、途端に「結局どの条件でアクセスが通るのか」を追うのが困難になります。人間にとって直感的な「ビジネス上の要件」であっても、IAMのJSONに落とし込んだ瞬間に難解な論理パズルに化けてしまうからです。
INV505のセッション内では、「S3バケットのアクセス制御」を例に、次のような要件が示されました
- 要件1（Allow）：原則として、自社の本番VPC（VPC-A）と開発VPC（VPC-B）からはアクセスを許可したい。
- 要件2（Allow）：また、データ連携のため親会社の組織（Org-O2）からのアクセスも特別に許可したい。
- 要件3（Deny）：ただし、開発VPC（VPC-B）には協力会社のメンバーもいるため、開発VPCからのアクセスは「自社の組織（Org-O1）」だけに制限したい。（＝VPC-B かつ OrgがO1ではない場合は拒否する）
やりたいことは分かります。しかし、これをIAMポリシーとして実装した場合、「このポリシーの挙動を完全に把握している」 と自信を持って言えるでしょうか？
ぱっと見で「許可」「拒否」と即答するのは難しくないでしょうか？
少しでも評価順序（明示的Denyの優先等）や否定条件を見落とすと、重大なセキュリティインシデントに繋がります。
このように、IAMの仕様（Denyの強さ、条件の相互作用など）が絡むと、人間の脳だけでアクセス許可を漏れなく判定するのは至難の業です。
そこで頼りになるのが、AWSが提供する推論ツール IAM Access Analyzer です。
ここからは、このツールがどうやって先ほどの「論理パズル」を解読しているのかに迫ります。
3. アプローチの転換：問いを変えると見えてくるもの
通常、IAMポリシーの検証ツールを作ろうとすると「このポリシーの設定は正しいですか？」というエラーチェック機能を想像するかもしれません。しかし、これに対するAWSのアプローチは違います。
「正しい/誤り」は判定できない
なぜなら、“正しさ”は組織のビジネスインテント（意図）によって変わるからです。
例えば「世界中の誰からでもアクセス可能（Public Read）」という設定は、コーポレートサイトの画像バケットであれば「正しい」ですが、社内秘の顧客データバケットであれば「情報漏洩（誤り）」になります。ツールがビジネスの背景まで汲み取って断定することはできません。
そこで、問いを置き換える
INV505では、ツール側が答えるべき「問い」を次のように定義し直しました。
「このポリシーは正しいですか？」ではなく
「このポリシーにより、結局だれが、どの条件なら通れますか？」
IAM Access Analyzer は「この設定は間違いです！」とアラートを出すのではなく、「現在、外部のアカウント〇〇（誰）から特定のIPアドレス（条件）からアクセスできる状態になっていますよ」という客観的な事実（アクセス経路の検出結果） だけを列挙して教えてくれます。
人間はそれを見て、最終的に「よし、意図通りだ」または「設定ミスだ、直そう」という判断をすることができます。
以降の章では、この「客観的な事実」を人間が使える品質にまで高めるためのアルゴリズムについて紹介します。
4. 良い検出結果（要約）に必要な3つの条件
IAM Access Analyzerが返す「〜の条件で通れます」という検出結果が実用に耐えうるためには、次の3つの相反する条件を満たす必要があります（INV505より）。
-
見落とさない（Sound / 安全性）
本当は外部からアクセス可能なのに「安全です」と見逃してしまうのが一番危険です。 -
言い過ぎない（Precise / 正確性）
「もしかすると全員アクセスできるかもしれません」というような、おおざっぱすぎる警告ばかり出されると、オオカミ少年状態になり人間が判断に使うことができなくなります。 -
多すぎない（Compact / 簡潔性）
だからといってIPアドレスや条件の組み合わせを「100万パターンのリスト」で長々と羅列されても、人間は結局読まなくなります。
これを一言で言うと 「漏れがなくて、正確で、短い検出結果を作れ」 という非常にハードルが高い要求になります。
この相反する条件を同時に満たすために考案された手法が、次章の「Stratified Abstraction」です。
5. 良い検出結果を生み出す工夫：Stratified Abstraction
どうすれば「見落とさない」「言い過ぎない」「多すぎない」を満たす検出結果を出せるのでしょうか。そのためのアルゴリズムが「Stratified Abstraction（階層的抽象化）」です。
2章で出した「S3バケットのアクセス制御パズル」を使って、アルゴリズムの動きを追ってみましょう。
2章のおさらい
あのパズルには、3つの要件が混ざっていました。
- 要件① Allow：本番VPC（VPC-A） または 開発VPC（VPC-B） なら許可
- 要件② Allow：親会社Org（O2） なら許可
- 要件③ Deny：開発VPC（VPC-B） かつ 自社Org（O1）以外 なら拒否
この掛け合わせを、人間が直感的に扱える形に落とし込んでいくのがこのアルゴリズムの狙いです。
図解：アルゴリズムの動き
処理のポイント
- 最初はざっくり見積もる：まずは大枠で捉えることで見落とし（漏れ）を防ぎます。
- 必要な区画だけを割る：最初から全条件を細かく掛け合わせると処理がパンクしてしまうため、「ここでは大雑把すぎて結論が出せない」と分かった境界（VPCやOrganizationなど）から順番に分割します。
- 整理して短くする：最終的な結果が出揃った後、意味が被っている条件を統合して、人間が読みやすい長さに要約します。
6. 「本当に通れるの？」を数学的に確かめるエンジン：AWS Zelkova
5章の通り、条件を徐々に「区画」に分割していくと、ある疑問にぶつかります。
「それで、この区画（例：開発VPC（VPC-B）かつ 親会社Org（O2））の中に、実際にAllowになるリクエストは存在するの？」
これを人間の代わりに確かめてくれるのが、AWSの裏側で動いている検証エンジン AWS Zelkova（ゼルコバ） です。
"通れる例"を探し出す
IAM Access Analyzer側から見ると、AWS Zelkovaは「この区画で通れる例はある？」と聞くための問い合わせ先（検証エンジン） になります。すべてのIPアドレスやユーザーのパターンを総当たりでチェックするわけではありません。
IAMポリシーには、IPアドレス帯、ワイルドカードを含んだ文字列、日時など、複雑な条件が混在しています。
AWS Zelkovaは、これらIAMポリシーの条件を 「数学の方程式」として論理式に変換 します。そして、SMT（Satisfiability Modulo Theories） と呼ばれる理論計算機科学の仕組みを活用して、次のように判定します。
-
Q：この方程式をすべて満たす具体例（リクエスト）は存在するか？
- Yes（例が見つかった）: この区画にはアクセスできるパターンが存在する！
- No（例が見つからない）: 絶対にアクセスできない！（数学的に証明された）
2つの技術の「役割分担」
ここまでのお話を要約すると、それぞれ以下の役割を担って動いていることが分かります。
-
IAM Access Analyzer
Stratified Abstractionで問題を適切な粒度に切り分けて整理し、人間に分かりやすい検出結果をまとめるマネージャー。 -
AWS Zelkova
IAM Access Analyzerから渡された条件式に対して、「通れる例は存在するか」を正確に解いて白黒つける数学のスペシャリスト。
7. 裏側を支える1979年の基礎研究「Nelson-Oppen」
6章で「AWS Zelkovaという数学のスペシャリストが白黒つける」と説明しましたが、ここにはもう1つ厄介な問題が隠れています。
それは、IAMポリシーの条件が 「IPアドレス（CIDR）」「ワイルドカードを含む文字列」「日時」といった、まったくルールの違う要素の寄せ集めであるという点です。
「異なる専門家」をどう連携させるか？
AWS Zelkovaの中にはそれぞれの条件に特化した個別の「判定器」が入っていますが、それらを別々に動かすだけでは複雑な条件の掛け合わせは解けません。
そこで、この性質の異なる複数の判定器を互いに協調（連携）させ、1つの全体的な答えを出すために、Nelson-Oppenの結合手法（1979年） という枠組みが使われています。
Research to Realityの体現
アルゴリズムの深入りは避けますが、セッションINV505においてこの手法が言及されたとき、エンジニアとして深い感銘を受けました。
なぜなら、「1979年に発表された理論計算機科学の基礎研究が、約半世紀の時を超えて、AWSという現代の巨大クラウドの最前線のセキュリティを支えている」 からです。これこそまさに、セッションのタイトルである「Research to Reality（研究から実装へ）」を完璧に体現するエピソードだと感じました。
8. おまけ：INV505で印象に残った論文の読み方
INV505では内容そのものだけでなく、研究論文の読み方も強調されていました。職業柄論文を読むので、ここが非常に参考になりました。
前提：論文は小説でも、テストが出されるわけでもない
- 最初から最後まで読まなくてもよい
- 分からないところは飛ばしてよい
3-Pass
論文の3つのパス（段階的な読み方）です。論文ごとにすべて行う必要はなく、目的に応じて「1st Passだけ」などで止めても問題ないとのことでした。
- 1st Pass（見極め）
- タイトル・図・見出し・評価の章だけをざっと見て「自分にとって読む価値があるか」を判断する。
- 2nd Pass（全体像）
- 具体的にどういう「問題設定」をして、どういう「狙い（アプローチ）」で解こうとしているかを掴む。
- 3rd Pass（深掘り）
- 自分の実装などに必要なときだけ、数式の「定義」や詳細な「アルゴリズム」をじっくり追う。
INV505内では、本記事でも解説したアルゴリズムの元論文である「Stratified abstraction of access control policies（CAV 2020）」を題材にして、この3-Passをどう適用するかが説明されていました。
▲ 対象の論文に対して3つのパス（読み方の深度）をどう割り当てるかを示したスライド
「全部理解できないといけない」と思い込むより、目的に応じて読み方を変える、というメッセージが印象的でした。
9. まとめ
- IAM Access Analyzerは「このポリシーは正しいか？」ではなく「だれが、どの条件なら通れるのか？」への問いを置き換えてポリシーを検証します
- 良い検出結果には「見落とさない」「言い過ぎない」「多すぎない」が必要です
- それを両立する工夫が Stratified Abstractionというアルゴリズムでした
- その裏側にはAWS Zelkovaという1979年の基礎研究を利用した仕組みがあり、「区画ごとに通れる例が存在するか」を確かめています
- 論文は全部読むのではなく、目的に応じて読み方を変えることが重要です
10. おわりに
AWS re:InventのLevel 500セッションは蓋を開けてみると 「私たちが普段使っているブラックボックスなマネージドサービスの裏側で、どんな理論が動いているのか」 を垣間見ることができる非常にエキサイティングな場所でした。
特に1979年の基礎研究が、現代のクラウドサービスを構築する上で利用されているというのは非常に興味深かったです。
クラウドサービスを「使う視点」だけでなく、「作る側の視点や理論」から見つめ直すことができるLevel 500のセッション。皆さんも機会があれば、ぜひ一度足を運んでみてはいかがでしょうか。
最後まで読んでいただき、ありがとうございました！