"We want to assure developers that Cedar’s authorization decisions will be correct. To provide that assurance, we follow a two-part process we call verification-guided development when we’re working on Cedar. First, we use automated reasoning to prove important correctness properties about formal models of Cedar’s components. Second, we use differential random testing to show that the models match the production code."
If you like that angle I think you’d really like the part of this talk https://www.youtube.com/watch?v=k6pPcnLuOXY from Emina Torlak, goes into how they were able to have duel implementations to get both performance and formal correctness.
Congratulations on the OSS launch! Was it always in the cards to open source Cedar?
I'm excited to see you've found a way to bring verification that exists in non-policy-based authorization solutions to Cedar. Was that functionality the driving factor that made the team create something new instead of leveraging the widely adopted Rego/OPA[0] stack for policy?
It looks like this talk[1] briefly covers why you made Cedar, but I'd be eager to hear more about the trade-offs in design, because other policy languages are leveraging decades of formal research on Datalog.
Disclosure: I work on SpiceDB[2], an authorization database inspired by Google's Zanzibar system[3], but I wouldn't say Cedar is directly competitive as SpiceDB is not a policy-based system.
I agree with you re:"I wouldn't say Cedar is directly competitive as SpiceDB" - I think Zanzibar and SpiceDB in particular can work well together with Cedar / OPA. By syncing SpiceDB via OPAL[0] into edge nodes with Cedar-agents[1].
I tried Cedar out for a small research project when it was first announced, and it felt incredibly clumsy compared to what I could have done in OPA. That was probably 8-9 months ago, so things may have changed.
Really exciting to see this and the recent renewed interest in more expressive ACL systems re: policy and (alternatively) relational access control.
The pedigree of Cedar is also really interesting to me, coming from the angle that Torlak was previously part of the UNSAT group @ Washington, and was the developer of Rosette. I was hoping there might be a semantic description of Cedar using Rosette as well! Maybe writing one would be a good challenge...
"We want to assure developers that Cedar’s authorization decisions will be correct. To provide that assurance, we follow a two-part process we call verification-guided development when we’re working on Cedar. First, we use automated reasoning to prove important correctness properties about formal models of Cedar’s components. Second, we use differential random testing to show that the models match the production code."