自動推論と差分テストでCedarをどう構築したか (2023)
本記事では、アマゾンが開発したポリシー記述言語「Cedar」の構築プロセスを解説する。Cedarの正確性とセキュリティを担保するため、自動推論技術と差分テスト（differential testing）を組み合わせた独自の手法を採用。開発チームは形式的検証と実践的テストを融合させることで、高信頼なアクセス制御システムを実現した。
背景メモ
• CedarはAmazonが開発したオープンソースのアクセス制御（IAM）ポリシー言語。AWSのIAMポリシーの課題（複雑さ・バグの混入しやすさ）を解決する目的で設計された。
• "自動推論（automated reasoning）"とは、プログラムやポリシーが正しく振る舞うことを数学的に検証する技術。AmazonはZ3やAWS Provable Securityなどの自動証明ツールを社内で多数開発している。
• "差分テスト（differential testing）"とは、同じ入力に対して複数の実装を実行し、結果の違いからバグを発見する手法。Cedarでは、新実装と参照実装をランダムテストで比較している。
• Cedarは2022年にオープンソース化され、AWS Verified Permissionsやその他アプリケーションで利用可能。Dafnyという形式検証言語で仕様が記述され、安全性の高いポリシー評価が可能。
• 本記事は、Cedarの内部でどのようにフォーマル検証が活用されているか、エンジニアリングの具体的手法を解説したもの。セキュリティ・権限管理に興味がある読者にとって、言語設計と検証技術の交差点を理解するうえで重要な事例。