AWS と定理証明 〜ポリシー言語 Cedar 開発の舞台裏〜 #fp_matsuri / FP Matsuri 2025

関数型まつり 2025 で使用したスライドです。

本セッションでは、AWS によって定理証明支援系 Lean を用いて開発されたポリシー記述言語 Cedar について、定理証明の役割や実サービスとの接続に焦点を当てて解説します。

Web サービスのセキュリティを考える上で、権限管理の設計は不可欠です。Cedar は AWS の IAM と同様、許可ルールと拒否ルールを組み合わせてポリシーを定義することで、リクエストに応じて許可もしくは拒否を返します。また、カスタム型を含むスキーマ定義が可能で、型検査も行われます。Cedar は OSS として公開されている他、マネージドサービスが Amazon Verified Permissions として利用可能です。

Cedar 開発の鍵のひとつとなったのが、定理証明支援系 Lean です。Cedar には操作的意味論が定義されており、「ポリシーの評価は必ず停止する」「拒否ルールは許可ルールに優先する」といった認可エンジンとしての仕様や、型システムの健全性について Lean で証明が行われています。また、認可エンジンとしてのスケーラビリティを実現するために、Cedar はポリシー内で判定に関係する部分のみを抽出する slice と呼ばれる最適化を実装しており、その健全性も Lean により証明されています。

もう一つのポイントは定理証明から実装への接続です。多くの定理証明支援系では実行可能なプログラムの抽出が可能ですが、実システムへの適用ではパフォーマンスやエコシステムが課題となりがちです。このギャップを乗り越えるため、Cedar では認可エンジン自体は Rust で開発し、Rust による実装と Lean による証明済み実装の両方に同じランダム入力を与えて出力の一致を確認する手法が採用されています。

Cedar は、定理証明が AWS という巨大システムの中で活用されている点で非常に特徴的なプロダクトです。本セッションでは、このような実世界との接続について、論文、OSS 実装、そしてサービス化された機能をそれぞれ参照しつつ解説します。

プロポーザル：https://fortee.jp/2025fp-matsuri/proposal/8bb407b5-5df3-48bb-a934-0ca6ca628c9a
補足記事：https://ccvanishing.hateblo.jp/entry/2025/06/17/225129

Transcript

1. AWSと定理証明 ポリシー言語 Cedar 開発の舞台裏 #fp_matsuri #fp_matsuri_a チェシャ猫 (@y_taka_23) 関数型まつり 2025 (15th June 2025)
2. 本日お話ししたいこと • AWS で実際に使用されている定理証明 ◦ 世界でも有数の複雑な巨大 Web システム ◦ さらに認可というクリティカルな分野 • どんな仕様が定理証明で保証されているのか ◦ 教科書的な練習問題ではあまり実感できない ◦ 実際の「使いどころ」を実感していただきたい
3. 形式手法 in クソデカ・リアルワールド Web システム
4. 組織横断的な認可処理の課題 • アプリ開発チームの苦労 ◦ 似たような判定を各チームで再発明 ◦ 実装は別だが概念としては一貫している必要性 • セキュリティ / CCoE チームの苦労 ◦ セキュリティ統制的にガードレールを敷きたい ◦ 実装は別なので統一したチェックが困難
5. PDP と PEP • Policy Decision Point（PDP） ◦ ポリシー言語に基づきアクセス要求を評価 ◦ 許可（Allow）または拒否（Deny）を判定 • Policy Enforcement Point（PEP） ◦ PDP に判断を仰いで実際のアクセス制御を行う ◦ Web アプリでは API Gateway やバックエンド実装
6. Cedar Policy Language https://github.com/cedar-policy
7. Cedar: A new language for expressive, fast, safe, and analyzable authorization J. W. Cutler et al. (OOPSLA 2024) How we built Cedar: A verification-guided approach C. Disselkoen et al. (FSE 2024) https://doi.org/10.1145/3649835 https://doi.org/10.1145/3663529.3663854
8. 例：写真共有アプリの認可 • ユーザの写真に対する操作を許可 / 禁止したい • 所属関係による条件 ◦ ユーザが所属するグループに対して許可 ◦ 写真が所属するアルバムに対して許可 • 所属関係によらないアドホックな条件 ◦ 写真の所有者はデフォルトで許可
9. Cedar によるポリシー記述 • 効果は permit（許可）または forbid（禁止） ◦ 複数該当する場合は forbid が優先 • 三つ組を基本としてルールを記述 ◦ Principal：alice が（操作の主体） ◦ Action：写真を閲覧する（操作の内容） ◦ Resource：photo01.jpg を（操作の対象）
10. ポリシーの基本形 permit ( principal == PhotoApp::User::"alice", action == PhotoApp::Action::"viewPhoto", resource == PhotoApp::Photo::"photo01.jpg" ); forbid ( principal == PhotoApp::User::"bob", action == PhotoApp::Action::"viewPhoto", resource == PhotoApp::Photo::"photo02.jpg" );
11. Amazon Verified Permissions • AWS マネージド版の Cedar エンジン ◦ PDP は単一障害点なので管理したくない ◦ 各種言語の AWS SDK でアクセス可能 • Amazon Cognito とも連携可能 ◦ 認証：Cognito User Pool ◦ 認可：AWS Verified Permissions https://aws.amazon.com/jp/verified-permissions/
12. Lean Theorem Prover https://github.com/leanprover
13. Lean による証明 • 定理証明支援系と呼ばれるツールの一種 ◦ いわば「証明付きの関数型言語」 • 型に乗せられる情報量が非常に多い ◦ 数学的な命題を型で表し、コンパイル時に検査 ◦ 命題 P の証明を受け取って、それを使用して 別の命題 Q の証明を返すといった関数が定義できる
14. Cedar での Lean 利用規模 • Lean で 7,387 行、そのうち証明が 5,714 行（約 77 %） • 他の定理証明プロジェクトと比較してコンパクト ◦ CompCert：Coq 約 42,000 行 ◦ seL4：Isabelle 約 200,000 行 • 証明により発見された仕様バグ 4 件、実装バグ 21 件 • 現在進行形で新しい証明が追加されている https://doi.org/10.1145/3663529.3663854
15. Cedar の設計方針 • 表現力：典型的なポリシー設計のユースケースをカバー • 安全性：認可処理の正確性、ポリシー定義ミスの防止 • 応答速度：ポリシー数に対して速度劣化しづらい • 解析可能性：人間だけでなく機械にとっても解釈しやすい
16. 表現力 1. Expressivity
17. RBAC と ABAC • Role-Based Access Control (RBAC) ◦ Principal の所属関係に基づく認可 ◦ Cedar では Resource もグループ化可能 • Attribute-Based Access Control (ABAC) ◦ エンティティの属性（フィールド）に基づく認可 ◦ Cedar ではユーザが自由に属性を定義できる
18. RBAC 的なポリシー permit ( principal in PhotoApp::UserGroup::"team01", action == PhotoApp::Action::"viewPhoto", resource in PhotoApp::Album::"album01" );
19. ABAC 的なポリシー permit ( principal, action == PhotoApp::Action::"viewPhoto", resource ) when { resource has owner && resource.owner == principal };
20. どうやって判定結果を与えるのか？
21. 【ポリシーの Small-step 操作的意味論】 エンティティが μ、リクエストが σ であるとき 式 e を式 e’ に書き換えてよい
22. Fig 6. https://doi.org/10.1145/3649835
23. 評価規則の正しさを保証する上で
24. Lean Theorem Prover https://github.com/leanprover
25. Lean で証明されている基本性質 • 判定手続きは無限ループにならず必ず停止する • forbid は permit に優先し、両方あれば拒否が勝つ • 許可されるならば明示的な permit が最低一つ存在 • 明示的な permit が存在しない場合、拒否される • ポリシーの重複や順序は判定結果に影響を与えない
26. 定理：拒否は許可に優先する theorem forbid_trumps_permit (request : Request) (entities : Entities) (policies : Policies) : (∃ (policy : Policy), policy ∈ policies ∧ policy.effect = .forbid ∧ satisfied policy request entities) → (isAuthorized request entities policies).decision = .deny := by ...
27. 安全性 2. Safety
28. スキーマによるバリデーション • 記述言語としての汎用性はエラーの温床 ◦ エンティティ名も属性名もユーザ定義 ◦ Undefined 属性を参照すると予期せぬ結果を招く • Cedar は組み込みのバリデーション機能をサポート ◦ ポリシーとは別に JSON Schema を定義できる ◦ 違反したポリシーは登録時に弾かれる
29. "Photo": { "shape": { "type": "Record", "attributes": { "owner": { "type": "Entity", "name": "User", "required": true } } }, "memberOfTypes": ["Album"] }
30. バリデーションの正体は型検査
31. 【ポリシーの型付け規則】 ケイパビリティが α の下で、 エンティティとリクエストの組が Γ であるとき、 式 e には型 τ とケイパビリティ ε が付く
32. ケイパビリティ？
33. Fig 7.(a) https://doi.org/10.1145/3649835
34. Fig 7.(a) https://doi.org/10.1145/3649835 ケイパビリティ {e.f} = 式が true に評価されるために 存在しなければならないフィールド
35. 型システムの正しさを保証する上で
36. Lean Theorem Prover https://github.com/leanprover
37. 定理：型検査の健全性 theorem typecheck_is_sound (policy : Policy) (env : Environment) (t : CedarType) (request : Request) (entities : Entities) : RequestAndEntitiesMatchEnvironment env request entities → typecheck policy env = .ok t → (∃ (b : Bool), EvaluatesTo policy.toExpr request entities b) := by ...
38. 応答速度 3. Latency
39. Slice によるパフォーマンス改善 • Policy Slice ◦ リクエストに対して無関係なポリシーを除外 ◦ 判定に関わる (Principal, Resource) の組をキーに • Level-based Entity Slice ◦ ポリシーに対して無関係なエンティティを除外 ◦ フィールドを辿る必要がある深さを予め調べておく
40. 他 OSS とのパフォーマンス比較 • Rego < OpenFAG << Cedar • 特に Cedar はエンティティ数に対して速度劣化しづらい Fig 14. https://doi.org/10.1145/3649835
41. 最適化の正しさを保証する上で
42. Lean Theorem Prover https://github.com/leanprover
43. 定理：Policy Slice は認可判断を保つ theorem isAuthorized_eq_for_sound_policy_slice (req : Request) (entities : Entities) (slice policies : Policies) : IsSoundPolicySlice req entities slice policies → isAuthorized req entities slice = isAuthorized req entities policies := by ...
44. 解析可能性 4. Analyzability
45. Symbolic Compiler (ongoing) • Allow / Deny とは別に、ポリシー自体の性質を検査 ◦ 例：ポリシー P1 と P2 はお互い等価か？ ◦ 例：ポリシー P1 はデッドコードか？ • SMT ソルバを利用して検査 ◦ ポリシーを SMT エンコーディング ◦ 「P1 と P2 の結果が異なる」が SAT なら非等価
46. 【SMT による表示的意味論】 エンティティを SMT 化したものが M、 リクエストを SMT 化したものが Γ のとき、 式 e は SMT 式 ê にエンコーディングされる
47. Fig 10. https://doi.org/10.1145/3649835
48. エンコードの正しさを保証する上で
49. Lean Theorem Prover https://github.com/leanprover
50. Lean で証明されている性質 • 型検査を通ったポリシーは SMT エンコード可能 • φ :=「ê1 と ê2 の true / false が一致」と表すと、 以下の 2 条件は同値 ◦ エンティティ階層が有限 DAG かつ not φ が UNSAT ◦ 任意の妥当なエンティティとリクエストに対して、 e1 と e2 の Allow / Deny 判定は常に一致
51. 定理：SMT エンコードの健全性 theorem compile_is_sound {x : Expr} {env : Env} {εnv : SymEnv} {t : Term.Outcome εnv} : εnv.WellFormedFor x → env.WellFormedFor x → env ∈ᵢ εnv → compile x εnv = .ok t → ∃ (o : Outcome Value), o ∈ₒ t ∧ evaluate x env.request env.entities ∼ o := by ...
52. 実システムを開発・運用する上で
53. Rust https://github.com/rust-lang/rust
54. Lean じゃない！
55. Verification–Guided Development • 実プロダクトとしての Cedar は Rust 製 ◦ Lean だけではエコシステムが貧弱 ◦ Rust だけでは検証のためのオーバヘッドが大きい • Lean 7,387 行に対して Rust は 67,542 行もある • Differential Random Test (DRT) ◦ 両者に同じランダム入力を与え、結果を比較
56. DRT による CI フロー リクエスト + エンティティ + ポリシー 証明済み実装 プロダクト実装 cargo-fuzz Allow / Deny Allow / Deny 一致？ Fail リリース Pass
57. 本日のまとめ • Cedar は意味論が与えられたポリシー言語 ◦ 評価 / 型付け / SMT エンコーディング ◦ 各種の性質は Lean で証明されている • Lean と Rust との橋渡し ◦ Cedar 自体の実装は Rust 製 ◦ Differential Random Testing で両者を比較
58. Implement Your Policies! Presented By チェシャ猫 (@y_taka_23)