Title: AWS re:Inforce 2024 - Proving the correctness of AWS authorization (IAM401)

Insights:

• Seamless Transition to New Authorization Engine: AWS launched a new authorization engine that operates one billion times per second, replacing the old one without any noticeable impact on customers or service teams. This transition was likened to changing an airplane engine mid-flight without passengers noticing.
• Automated Reasoning: The new engine's success is attributed to automated reasoning, which uses algorithms to construct and audit proofs in mathematical logic, ensuring the correctness of complex digital systems.
• Proofs and Their Importance: Proofs, like the Pythagorean theorem, provide a foundational truth that can be built upon. In AWS's case, proofs ensure that the authorization engine evaluates policies correctly, providing higher confidence in security.
• IAM Architecture: IAM (Identity and Access Management) is a globally distributed system with two main components: policy management and distribution, and a runtime client library for authentication and authorization.
• Authorization Engine: The core of IAM's runtime client library is the authorization engine, which evaluates requests against policies to allow or deny access. This engine has been proven correct through automated reasoning.
• Security and Customer Obsession: AWS's motivation for this rigorous proof process stems from their commitment to security and customer satisfaction, aiming to make changes with greater confidence and speed.
• Development and Validation Process: The development process involved specifying, implementing, and validating the authorization engine using the Daphne programming language. Validation included extensive unit testing, fuzzing, and running the new engine in shadow mode to compare results with the old engine.
• Performance Improvements: The new authorization engine is 65% faster than its predecessor, achieved through aggressive optimizations validated by automated reasoning.
• Cedar and Amazon Verified Permissions: AWS also developed Cedar, an open-source, proven correct authorization language for custom applications, and Amazon Verified Permissions, a service that manages Cedar policies.

Quotes:

• "We changed the engine on an airplane while it was in flight and the passengers didn't even notice that it had happened."
• "Automated reasoning is the application of proofs, the same approach to building proofs that you learned in high school geometry, scaled up with algorithms and tooling to enable reasoning about larger complex digital systems."
• "This proof gives you greater confidence that we're correctly evaluating policies because this proof applies to all possible inputs into the authorization engine."
• "We want to continue to make changes to this very important algorithm, but we want to do it with more confidence and greater speed."
• "We implemented something called shadow mode across AWS authorization... We found around 100 million mismatches per day."
• "Our new authorization engine is 65% faster than its predecessor without changing its behavior."
• "Cedar is a proven correct authorization language that you can use in your applications."
• "Amazon Verified Permissions gives you that system for Cedar."