Formally Verified Cloud-Scale Authorization
Abstract
All critical systems must evolve to meet the needs of a growing and diversifying user base. But supporting that evolution is challenging at increasing scale: Maintainers must find a way to ensure that each change does only what is intended, and will not inadvertently change behavior for existing users. This paper presents how we addressed this challenge for the Amazon Web Services (AWS) authorization engine, invoked 1 billion times per second, by using formal verification. Over a period of four years, we built a new authorization engine, one that behaves functionally the same as its predecessor, using the verification-aware programming language Dafny. We can now confidently deploy enhancements and optimizations while maintaining the highest assurance of both correctness and backward compatibility. We deployed the new engine in 2024 without incident and customers immediately enjoyed a threefold performance improvement. The methodology we followed to build this new engine was not an off-the-shelf application of an existing verification tool, and this paper presents several key insights: 1) Rather than prove correct the existing engine, written in Java, we found it more effective to write a new engine in Dafny, a language built for verification from the ground up, and then compile the result to Java. 2) To ensure performance, debuggability, and to gain trust from stakeholders, we needed to generate readable, idiomatic Java code, essentially a transliteration of the source Dafny. 3) To ensure that the specification matches the system's actual behavior, we performed extensive differential and shadow testing throughout the development process, ultimately comparing against 1015production samples prior to deployment. Our approach demonstrates how formal verification can be effectively applied to evolve critical legacy software at scale.
BibTeX
@inproceedings{Chakarov-al:ICSE25,
author = {Aleks Chakarov and
Jaco Geldenhuys and
Matthew Heck and
Michael Hicks and
Sam Huang and
Georges{-}Axel Jaloyan and
Anjali Joshi and
K. Rustan M. Leino and
Mikael Mayer and
Sean McLaughlin and
Akhilesh Mritunjai and
Cl{\'{e}}ment Pit{-}Claudel and
Sorawee Porncharoenwase and
Florian Rabe and
Marianna Rapoport and
Giles Reger and
Cody Roux and
Neha Rungta and
Robin Salkeld and
Matthias Schlaipfer and
Daniel Schoepe and
Johanna Schwartzentruber and
Serdar Tasiran and
Aaron Tomb and
Emina Torlak and
Jean{-}Baptiste Tristan and
Lucas G. Wagner and
Michael W. Whalen and
Remy Willems and
Tongtong Xiang and
Taejoon Byun and
Joshua M. Cohen and
Ruijie Fang and
Junyoung Jang and
Jakob Rath and
Hira Taqdees Syeda and
Dominik Wagner and
Yongwei Yuan},
title = {Formally Verified {Cloud-Scale} Authorization},
booktitle = {ICSE},
pages = {2508--2521},
publisher = {{IEEE}},
year = {2025},
}