Formally Verified Cloud-Scale Authorization

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 10<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">15</sup> production samples prior to deployment. Our approach demonstrates how formal verification can be effectively applied to evolve critical legacy software at scale.

Authors

Institutions

Publication Details

Published
2025-04-26
DOI
https://doi.org/10.1109/icse55347.2025.00166
Citations
1
Primary Topic
Cloud Data Security Solutions
Type
article
Field-Weighted Citation Impact
3.25
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

Formally Verified Cloud-Scale Authorization

Yongwei Yuan, Michael W. Whalen, Clément Pit-Claudel, Sean McLaughlin et al.
1 citations
Cloud Data Security Solutions
3.25
article

Formally Verified Cloud-Scale Authorization

Yongwei Yuan, Michael W. Whalen, Clément Pit-Claudel, Sean McLaughlin, Mikaël Mayer, R. F. Willems, Songshan Sam Huang, Jakob Rath, Jean-Baptiste Tristan, Mike Rapoport, Dominik Wagner, Aaron Tomb, Tao Xiang, Daniel Schoepe, Michael Hicks, Neha Rungta, Jaco Geldenhuys, Sorawee Porncharoenwase, Giles Reger, Joshua Cohen, Matthias Schlaipfer, K. Rustan M. Leino, Lucas K. Wagner, Emina Torlak, Robin Salkeld, Serdar Taşiran, Florian Rabe, Anjali Joshi, Junyoung Jang, M. Heck, Christian Roux, Georges-Axel Jaloyan, Ruijie Fang, Aleks Chakarov, Akhilesh Mritunjai, Johanna Schwartzentruber, Tae Joon Byun, Hira Taqdees Syeda
article en
1 citations

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 10<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">15</sup> production samples prior to deployment. Our approach demonstrates how formal verification can be effectively applied to evolve critical legacy software at scale.

TU Wien (AT), The University of Melbourne (AU), Princeton University (US), Purdue University West Lafayette (US), Amazon (Germany) (DE), McGill University (CA), The University of Texas at Austin (US)
Openalex Percentile: Top 8%
Cloud Data Security Solutions
3.25
DOISourceOpenAlex
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.