2024/07/01 by Craig Disselkoen, Disselkoen, Craig, Aaron Eline +22 · 1 citation
Engineering · #FOS: Computer and information sciences #Software Engineering (cs.SE) #Tunneling and Rock Mechanics
paper · pdf · doi:10.48550/arxiv.2407.01688
openalex publication_date 2024/07/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This paper presents verification-guided development (VGD), a software engineering process we used to build Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves writing an executable model of the system and mechanically proving properties about the model; writing production code for the system and using differential random testing (DRT) to check that the production code matches the model; and using property-based testing (PBT) to check properties of unmodeled parts of the production code. Using VGD for Cedar, we can build fast, idiomatic production code, prove our model correct, and find and fix subtle implementation bugs that evade code reviews and unit testing. While carrying out proofs, we found and fixed 4 bugs in Cedar's policy validator, and DRT and PBT helped us find and fix 21 additional bugs in various parts of Cedar.