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 a cloud-scale 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 10¹5 production samples prior to deployment.

Our approach demonstrates how formal verification can be effectively applied to evolve critical legacy software at scale.

@inproceedings{chakarov25awsauth,
  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 Clement Pit-Claudel and Sorawee Porncharoenwase and Marianna Rapoport 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 Jean-Baptiste Tristan and Emina Torlak and Lucas Wagner and Michael W. Whalen and Remy Willems and Tongtong Xiang and Tae Joon Byun and Joshua 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 = {Proceedings of the International Conference on Software Engineering (ICSE)},
  year = 2025,
  month = apr
}

This file was generated by bibtex2html 1.99.