How We Built Cedar: A Verification-Guided Approach
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909240373805056 |
|---|---|
| author | Disselkoen, Craig Eline, Aaron He, Shaobo Headley, Kyle Hicks, Michael Hietala, Kesha Kastner, John Mamat, Anwar McCutchen, Matt Rungta, Neha Shah, Bhakti Torlak, Emina Wells, Andrew |
| author_facet | Disselkoen, Craig Eline, Aaron He, Shaobo Headley, Kyle Hicks, Michael Hietala, Kesha Kastner, John Mamat, Anwar McCutchen, Matt Rungta, Neha Shah, Bhakti Torlak, Emina Wells, Andrew |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_01688 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | How We Built Cedar: A Verification-Guided Approach Disselkoen, Craig Eline, Aaron He, Shaobo Headley, Kyle Hicks, Michael Hietala, Kesha Kastner, John Mamat, Anwar McCutchen, Matt Rungta, Neha Shah, Bhakti Torlak, Emina Wells, Andrew Software Engineering 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. |
| title | How We Built Cedar: A Verification-Guided Approach |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2407.01688 |