Access Control is key to securing the increasing amount of data stored, processed and exchanged today. Users and legislation demand privacy, organizations require confidentiality and business continuity, and more and more data is exchanged between business entities through APIs. However, there is no standard for access control, no lingua franca to let two different systems understand how exchanged data should be protected, and it’s near-impossible to query a system for “what resources do I have access to?” or “who has access to this resource?”. Furthermore, just as configuration changes as a major source of outages, policy changes are hard to reason about, as the intricacies of real-world systems makes it demanding to see if the old policy is the same as the new one, leading to risk aversion or outages.

In this lightning talk, we’ll cover how access control policies can be distilled down to Mathematics, and thus analyzed through the lens of logic. Given this, one can formally verify that a changed policy is exactly the same as the old one, or at least, doesn’t let bad things happen (e.g. allow public access to any resource). Two different systems can verify their implementations of a policy to be equal. Finally, querying the policies for who can do what becomes possible. The best of all is that all of this can be done today, using open source tooling, using the Cedar Policy project.