こんにちは、チェシャ猫です。
先日開催された関数型まつりで、AWS によって開発されたポリシー言語 Cedar と、その開発に使用された定理証明支援系 Lean について登壇してきました。公募 CFP 枠です。
（TODO: 録画が公開されたら貼る）
前回登壇との関係
Cedar については、チェシャ猫自身が少し前、PHPerKaigi 2025 でも登壇しています。
前回と今回では、扱っている題材は同じですが、想定しているターゲットや興味の方向性が少し異なります。今回の登壇では Lean が保証している意味論的な定理や開発フローなど「Cedar がどのように設計・開発されたか」に焦点を当てた一方、前回はユーザ側の立場で「Cedar をどのように使うか」に焦点を当てた内容になっています。
AWS での構成例や Slice のアルゴリズムなど、今回オミットされた内容もあるので、もしよろしければこちらも併せてご覧ください。
質問への回答
当日、会場では 25 分間の枠を全てプレゼンで使い切ってしまったのですが、ありがたいことにその後の休憩時間や Twitter でいくつか質問をいただいています。
#fp_matsuri #fp_matsuri_a
— ちぇっちぇ (@Chen__TS) 2025年6月15日
単一障害点なのはそうと思いつつ、AWS 側ならそれでどれだけの可用性があるのだろう....？
この質問は、自分では思いつかなかったのですが確かに良い着眼点だと思います。ドキュメントによれば、可用性が 99.9% を下回ると返金の対象になるようです。
ポリシー複雑に書けるけど、爆発しそう。そういうときこそ、拒否が優先されるのがいいのかな #fp_matsuri #fp_matsuri_a
— よんた (@keita44_f4) 2025年6月15日
はい、第一には複雑になったときに安全側に倒す、というのが目的です。Cedar の特徴として挙げた「安全性」の一環でもあります。
さらに言うならば、ポリシーを設計・定義する主体が分散している、というのも背景の一つです。ポリシー言語自体の動機として、個々のサービスを担当する個々のチームがポリシーを定義しても統一的に管理可能である、という点が挙げられます。仮に、拒否されていたものが許可で上書きできる場合、統制用の禁止ポリシーを定義しても個々のチームがそれを無効化することができてしまいます。拒否が優先する設計はこれを嫌ったものと見ることができます。
ちなみに、Lean で示されている定理「ポリシーの重複や評価順は結果に影響を与えない」にも同じ背景があります。また、これらの性質は IAM にも共通しています。基本的な思想として Cedar は、認可管理の対象が原則 AWS リソースに限られる IAM を、ユーザがアプリ用にも使えるように汎用化したものと考えて良いでしょう。
本筋とは関係ないけど、LeanもSwiftみたいに . でデータ構築子を引っ張ってこれる？ #fp_matsuri #fp_matsuri_a
— mod_poppo@技術書典18す06 (@mod_poppo) 2025年6月15日
はい、その通りです。この .ok は、.ok と .error からなる直和型 Except の値コンストラクタです。Except.ok x の形で書くのが正式ですが、推論できる場合は省略しても大丈夫です。
CIは何分ぐらいで通るんだろ#fp_matsuri #fp_matsuri_a
— エヌユル (@ncaq) 2025年6月15日
今回紹介した二本目の論文には以下のような記述があり、数分のオーダで証明の検査を含めた Lean コンパイルが通るようです。実際の CI では Rust 側のビルドやテストも含めて実行する必要があるのでこれよりはかなり長くなるとは思いますが、いずれにせよ証明が CI 速度上のボトルネックになることはなさそうです。
Our Lean proofs are fast to verify, and the models are fast to execute. It takes about 3 minutes to check all proofs and compile models for execution.
余談ですが、これはモデル検査とは対照的です。モデル検査は常に状態爆発との戦いであり、多くのモデル検査器では、状態を圧縮したり効率的に枝刈りを行ったりといった最適化がボトルネックになります。
「正しい実装」と「実用的な実装」の間で違いがないことを乱数ベースで検証するのは、「乱数によって生成された入力がコーナーケースをうまく突いてくれるか」という問題をクリアする必要があるので、単に「乱数でテストします」だけだとツッコミの余地がある気がする。
— mod_poppo@技術書典18す06 (@mod_poppo) 2025年6月15日
これは非常に鋭く、正しい指摘です。libfuzzer を用いることで未実行パスを重点的にテストするという基本方針の他、さらに論文中では、2 種類の生成戦略を併用していることが述べられています。
一つは型指向 (type-directed) 生成で、まずスキーマを生成した後、それに併せてエンティティとポリシーを生成する方法です。完全にランダムに生成した場合はほとんどの入力がエラーケースになってしまいますが、スキーマを先に確定させることで明らかにナンセンスなデータの生成を抑制します。
しかしこれだけでは、逆にバリデーションエラーになるような経路がテストできず、また when の条件が即値の true や false に偏りすぎる傾向があったようです。そこで Cedar の開発では、when に限って不整合を許容してバリエーションをつけるような生成も行なっています。
さらに論文中では、非常に生成確率が低かったことにより DRT で見逃されたバグについても触れられています。このバグは Cedar のポリシー評価器が無限ループに陥って停止しないというもので、「DRT では発見できなかった、Lean の停止性判定によって検出されたバグの例」として挙げられています。
