形式手法特論：SMT ソルバで解く認可ポリシの静的解析 #kernelvm / Kernel VM Study Tsukuba No3

Kernel/VM 探検隊@つくば No3 で使用したスライドです。

Transcript

1. 形式手法特論 SMTソルバで解く 認可ポリシの静的解析 #kernelvm チェシャ猫 (@y_taka_23) Kernel/VM 探検隊@つくば No3 (20th Mar. 2026)
2. 卒業式といえば SMT ソルバ
3. 我々は「幼年期の終り」にいる
4. 生成 AI 時代の仕様記述 • 仕様を「記述すること」への重心の移動 ◦ AI はそれらしい実装を高速・大量に生成できる ◦ 明示されたコンテキスト外の事情は汲んでくれない • 今後は仕様の「検証可能性」がより問われる時代に ◦ まずい実装を機械的に弾ける、白黒が決まる仕様 ◦ リッチな型システムや静的解析の利用
5. 理解は全てに先立つ そして理解とは記述である
6. Cedar Policy Language https://github.com/cedar-policy
7. 認可エンジン Cedar • AWS 製の認可判定エンジン ◦ Principal / Action / Resource + α でポリシを記述 ◦ リクエストに対し許可 or 拒否を返す • いわばジェネリック IAM 的な立ち位置 ◦ Rust で実装され、OSS として公開されている ◦ マネージド版の Amazon Verified Permissions も
9. 持ち主が操作主
10. 持ち主が操作主 拡張子が .png private でない
11. 閲覧操作 持ち主が操作主 拡張子が .png 許可 private でない
12. 構造化・リファクタリングも可能
14. 持ち主が操作主 拡張子が .png private なら拒否
15. 「リファクタリング」？
16. リファクタリングとは 観測可能な挙動を保つ変更のこと！
17. Cedar Analysis による解析 • 複雑なポリシは最終的な結果が分かりづらい ◦ デプロイ前に「検証可能性」が欲しい • Cedar では静的解析ツールが提供されている ◦ ふたつのポリシ間に強弱の違いがあるか？ ◦ 自明・冗長なポリシがないか？ ◦ 許可を拒否で上書きして潰していないか？
19. 一つ目の方が許可範囲が広い
20. Cedar Analysis の特徴 • リクエストを与えずとも、ポリシのみで検査 ◦ 単体テストと違い具体的なテストケースが不要 ◦ 真に「任意のリクエスト」を検査する全称形の仕様 • 内部では SMT ソルバが使用されている ◦ 比較するポリシを SMT エンコード ◦ 一方で Allow、他方で Deny となるリクエストを探索
22. 最終的な assert 条件は 「t10 と t12 が等しくない」
23. 最終的な assert 条件は 「t10 と t12 が等しくない」 t10 は「t4 または t9」
24. 最終的な assert 条件は 「t10 と t12 が等しくない」 t10 は「t4 または t9」 t4 は「t0 と t3 が等しい」
25. 最終的な assert 条件は 「t10 と t12 が等しくない」 t10 は「t4 または t9」 t4 は「t0 と t3 が等しい」 t3 は t2 の owner (R1_a1)
26. 最終的な assert 条件は 「t10 と t12 が等しくない」 t10 は「t4 または t9」 t4 は「t0 と t3 が等しい」 t0 はリクエストの principal t3 は t2 の owner (R1_a1) t2 はリクエストの resource
27. t4
28. Cedar: A new language for expressive, fast, safe, and analyzable authorization J. W. Cutler et al. (OOPSLA 2024) https://doi.org/10.1145/3649835
29. Cedar 式から Option 付き SMT 式への コンパイル規則
30. 地味に厄介な in 演算子 • リソースの包含関係は in で記述できる ◦ 未解釈関数として SMT エンコード • 推移性・非巡回性を制約として SMT に伝えたい ◦ しかし全称量化を許すと SMT の決定性が失われる • 判定問題に対して必要十分な有限制約集合を生成 ◦ このエンコードの健全性・完全性が論文の貢献
32. 操作対象が term フォルダに含まれる term フォルダが shared フォルダに含まれる shared フォルダが 操作主アカウントに含まれる
34. t24は team が shared に含まれるなら shared の祖先は team の祖先でもある
35. （人間の仕事じゃねぇ〜）
36. だからこそ機械が理解する形で 仕様が定式化される意味がある
37. 本日のまとめ • 仕様記述の「検証可能性」の重要性 • 認可エンジン Cedar ◦ IAM と同様、Principal / Action / Resource で指定 • Cedar Analysis ◦ ポリシの意味を静的に検査できる ◦ 内部では SMT ソルバで充足可能性を検査
38. Solve Smart Policies With SMT Solvers! Presented By チェシャ猫 (@y_taka_23)