This paper presents verification-guided development (VGD), a software development process that we used to develop Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves two activities: (1) writing a readable, executable model of the system and proving mechanically-verified properties about it; and (2) writing production code for the system, using extensive differential random testing (DRT) to check that the production code's behavior matches that of the model, and property-based testing (PBT) to check properties of unmodeled components of the production code. Using VGD for Cedar has been beneficial: we are able to build fast, idiomatic production code and find and fix bugs during the development phase: when carrying out proofs we found and fixed four soundness bugs in Cedar's policy validator, and when carrying out DRT and PBT we found and fixed 21 bugs in the Cedar parser, evaluator, authorizer, and validator.

[ http ]

@inproceedings{disselkoen24vgd,
  title = {How We Built Cedar: A Verification-Guided Approach},
  author = {Craig Disselkoen and Aaron Eline and Shaobo He and Kyle Headley and Michael Hicks and Kesha Hietala and John Kastner and Anwar Mamat and Matt McCutchen and Neha Rungta and Bhakti Shah and Emina Torlak and Andrew Wells},
  booktitle = {Proceedings of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE)},
  note = {Industry papers track},
  year = 2024,
  month = jul
}

This file was generated by bibtex2html 1.99.