我们如何利用自动推理和差异测试构建Cedar（2023）
这篇文章介绍了亚马逊科学家如何结合自动推理和差异测试两种技术来构建 Cedar 策略引擎。自动推理用于形式化验证系统行为，而差异测试则帮助发现实现中的不一致性。通过这一组合方法，团队确保了 Cedar 的可靠性和正确性，为云安全策略管理提供了坚实的基础。
背景速读
- Cedar 是亚马逊开发的一款开源策略语言（policy language），用于在 AWS 服务和应用程序中精细控制访问权限。它类似于 AWS IAM 的策略语言，但设计为更通用、可嵌入任何系统。
- 本文介绍了亚马逊如何将"自动化推理"（automated reasoning，即使用数学证明来验证软件行为）与"差分测试"（differential testing，即对比多个实现以确保行为一致）结合，来构建 Cedar 的验证引擎。
- 这背后的关键背景：亚马逊内部长期使用形式化方法（formal methods）来验证关键安全系统。该团队曾在 AWS 的 IAM 策略引擎上应用自动化推理，发现了数百个难以通过传统测试发现的 bug。
- 论文于 2023 年发表在 ACM SIGPLAN 的 OOPSLA 会议上，属于编程语言和软件工程领域的顶级会议。作者团队来自亚马逊的 Automated Reasoning Group（ARG），该团队也开发了 AWS 的 Zelkova、S3 的 Bucket 策略验证等工具。