How we built Cedar with automated reasoning and differential testing (2023)
Amazon describes how it built Cedar, a policy language for access control, using automated reasoning to formally verify correctness and differential testing to compare against a reference implementation. The approach helped catch subtle bugs early and ensure the language's safety and reliability before release.
Background
Cedar is Amazon's open-source policy language and authorization engine (similar to AWS's own IAM but more general-purpose). It lets developers write fine-grained rules about who can do what to which resources — e.g., "Alice can read files in ProjectX" — and then enforce those rules in their apps. The blog explains how Amazon built Cedar using two rigorous testing techniques: automated reasoning (mathematically proving that the policy engine behaves correctly in all edge cases) and differential testing (running the same policies through different implementations and checking that they agree). This matters because authorization bugs are a common source of security breaches, and traditional testing often misses subtle logical errors in permission rules.