自动化推理与差分测试构建Cedar授权策略语言
Cedar是一种新的授权策略语言，被某中心的验证权限和验证访问托管服务使用，并已公开发布。开发者可以使用Cedar编写策略，为其应用程序指定细粒度权限。应用程序通过调用Cedar的授权引擎来授权访问请求。由于Cedar策略与应用程序代码分离，因此可以独立编写、更新、分析和审计。
为确保Cedar的授权决策正确，采用称为验证引导开发的两部分过程。首先，使用自动化推理证明Cedar组件形式化模型的重要正确性属性。其次，使用差分随机测试显示模型与生产代码匹配。
Cedar入门
Cedar是一种用于编写和执行自定义应用程序授权策略的语言。策略语法类似于自然语言，定义主体（谁）可以对资源（什么）执行操作（什么动作）以及在什么条件下（何时）。
以TinyTodo应用为例，该应用使用Cedar控制访问权限。示例策略包括：
- 策略1：允许资源所有者执行任何操作。
- 策略2：允许编辑者或读者获取列表。
- 策略3：禁止实习生创建新列表。
当应用程序需要强制执行访问时，只需向Cedar授权引擎发出请求。引擎根据Cedar策略和相关应用程序数据评估请求，返回允许或拒绝决策。
构建可信Cedar
采用验证引导开发过程确保Cedar授权引擎做出正确决策。该过程包括两部分：
- 使用Dafny验证感知编程语言对Cedar授权引擎和验证器进行建模，利用Dafny的内置自动化推理能力证明代码满足各种安全和安全属性。
- 使用差分随机测试（DRT）确认Rust编写的生产实现与Dafny模型行为匹配。生成数百万个多样化输入，馈送到模型和生产代码中。如果两个版本始终产生相同输出，则高度确信实现与模型匹配。
证明Cedar授权属性
Cedar授权算法默认安全设计，具有两个关键属性：
- 显式允许：权限仅由单个允许策略授予，不会因错误或默认获得。
- 禁止覆盖允许：任何适用的禁止策略总是拒绝访问，即使有允许策略允许。
授权引擎评估请求时，将应用程序请求参数代入策略变量，收集满足的禁止和允许策略到不同集合中，然后做出决策。
使用Dafny函数对授权引擎建模，并利用Dafny的自动化推理能力陈述和证明显式允许和禁止覆盖允许属性。通过错误版本代码示例说明Dafny如何帮助发现错误，并展示修正后的代码。
使用Cedar Dafny模型证明了多种属性，最重要的证明是Cedar验证器（确认策略与应用程序数据模型一致）是健全的：如果验证器接受策略，评估策略应永远不会导致某些类别的错误。在Dafny中进行此证明时，发现了验证器设计中的几个细微错误并予以纠正。
Dafny模型不仅对自动化推理有用，对手动推理也有帮助。Dafny代码比Rust实现更易阅读，作者授权器的Dafny模型代码行数约为生产代码的六分之一。
差分随机测试
证明Cedar Dafny模型属性后，通过DRT提供证据表明这些属性也适用于生产代码。使用cargo fuzz随机测试框架生成数百万输入（访问请求、伴随数据和策略），并发送到Dafny模型引擎和Rust生产引擎。如果两个版本决策一致，则一切正常；如果不一致，则发现错误。
有效使用DRT的主要挑战是通过生成有用和多样化输入确保必要的代码覆盖率。纯随机生成会错过大量核心评估逻辑，并过度索引错误处理代码。为解决此问题，编写了几个输入生成器，生成相互一致的策略、数据和请求，同时产生使用Cedar关键语言结构的策略。目前，每晚运行DRT六小时，执行约1亿次测试。
在Cedar开发过程中使用DRT发现了模型与生产代码之间的差异角落案例，使其成为重要工具。例如，发现使用的Rust IP地址操作包中存在错误；Dafny模型暴露了包解析IP地址的问题。由于错误在外部包中，在代码中修复问题，同时等待上游修复。还发现了Cedar策略解析器、授权器处理缺失应用程序数据以及应用程序数据命名空间前缀解释中的细微错误。
了解更多
本文讨论了Cedar授权策略语言的验证引导开发过程。在该过程中，使用Dafny编程语言对Cedar语言组件建模，并利用Dafny的自动化推理能力证明属性。通过差分随机测试检查Cedar生产代码是否与Dafny模型匹配。此过程在开发过程中揭示了几个有趣错误，并增强了Cedar授权引擎做出正确决策的信心。
可查看GitHub上的Cedar Dafny模型和差分测试代码，了解更多关于Dafny和Cedar服务的信息。