如何通过自动化推理和差分测试构建Cedar

Cedar是一种新型授权策略语言，被某机构的验证权限服务和验证访问托管服务所采用。开发者可以使用Cedar编写策略，为其应用程序指定细粒度权限。应用程序通过调用Cedar的授权引擎来授权访问请求。由于Cedar策略独立于应用程序代码，因此可以独立编写、更新、分析和审计。

确保Cedar的可信度

为确保Cedar授权引擎做出正确决策，采用了名为“验证引导开发”的两阶段流程：

1. 使用Dafny验证感知编程语言对Cedar组件进行建模，通过自动化推理证明安全属性
2. 通过差分随机测试验证Rust实现与Dafny模型的一致性

Cedar授权属性证明

Cedar授权算法默认具备以下安全属性：

• 显式许可：权限仅通过许可策略授予，不会因错误或默认获得
• 禁止优先：任何适用的禁止策略都会拒绝访问，即使存在允许策略

通过Dafny函数建模授权引擎，使用谓词和引理形式化这些属性。例如，在纠正错误的实现后，Dafny成功证明了“显式许可”属性：

function method isAuthorized(): Response {
    var f := forbids();
    var p := permits();
    if f == {} && p != {} then
        Response(Allow, p)
    else
        Response(Deny, f)
}

差分随机测试实践

使用cargo fuzz框架生成数百万个输入（访问请求、数据和策略），同时发送给Dafny模型和Rust实现进行对比测试。为确保代码覆盖率，开发了多个输入生成器，保证策略、数据和请求的一致性。目前每晚运行6小时差分测试，执行约1亿次测试。

技术成果

该开发流程发现了多个关键问题：

• IP地址解析库的bug
• 策略解析器的细微错误
• 应用数据处理和命名空间解析问题

Dafny模型仅占生产代码1/6的代码量，为开发者和工具实现者提供了更清晰的技术参考。通过形式化验证和差分测试的结合，显著提升了Cedar授权引擎的可靠性。
更多精彩内容 请关注我的个人公众号 公众号（办公AI智能小助手）或者 我的个人博客 https://blog.qife122.com/
公众号二维码

对安全感兴趣的朋友可以关注我的安全公众号（网络安全技术点滴分享）
公众号二维码