Like any cloud provider, AWS has umpteen access-control systems for different services. Customers building applications on those services need to manage permissions and authorize user actions.
Whether that's which accounts an online banking user has access to, which photos and albums someone can see on a photo sharing tool, or who can see job titles or salary details in an HR system, it’s fundamentally the same problem. But usually authorising a user and checking if they have access to a specific resource is intertwined with the application logic, making it hard to adopt the policy-as-code approach.
Instead of hoping you build every authorisation sequence to be correct, efficient, and performant (as well as making users learn every different system and hoping they get their policies right each time), Cedar is an open-source language for writing and verifying authorization policies with a small, formally verified engine you can add to any application.
Designed to balance expressiveness, performance, and the ability to analyse policies, Cedar started as a research project drawing on everything AWS had learned about identity and access management as well as familiar role-based and attribute-based access control (RBAC and ABAC) approaches to create a policy language and engine for the Amazon Verified Permissions authorization service, which customers can use to control access to their own applications.
“Our research scientists were looking at how to build a policy system that’s mathematically provable, applying formal methods to software,” AWS principal engineer Phil Estes told The Stack. They also wanted to make it reusable.
“What if we built an engine, and the checking capability that could be formally proven, separate, so that people could just plug that into applications, and it's written in Rust and has all these performance guarantees and formal methods guarantees,” Estes said.
The language and engine are useful for far more than AWS services: "Anywhere I need authorization or I need to define an actor, an action and a resource – anything with RBAC or accessed based control for what an actor can do or not do – anywhere you need to make those decisions, Cedar fits really well.”
