対象とする聴衆のレベル

• Intermediate: 分野の基礎知識を持っている

セッションのテーマ

• 導入事例
• 理論

セッションの概要

本セッションでは、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 実装、そしてサービス化された機能をそれぞれ参照しつつ解説します。