Trillions of Formally Verified Authorizations a Day! (Keynote)

To control access to their data and resources, AWS users write policies that express fine-grained permissions. An authorization engine evaluates these policies trillions of times a day to determine if access is allowed. The authorization engine is a critical part of the security, availability, and correctness of AWS. To raise the bar in the security and correctness of this engine, we replaced it with a formally verified one. It was absolutely critical that users were not impacted by the change. Over a period of months and over quadrillion tests, we gathered data on the impact, and deployed the new verified engine. And then what happens? Come to the talk to find out.