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.

翻译：本文提出验证导向开发（VGD），这是一种我们用于构建Cedar的软件工程流程。Cedar是一种新型策略语言，旨在实现表达性强、快速、安全且可分析的授权。采用VGD开发系统包括：编写系统的可执行模型并机械验证模型属性；编写系统生产代码，并利用差分随机测试（DRT）验证生产代码与模型的一致性；以及采用基于属性的测试（PBT）检验生产代码中未建模部分的特性。通过将VGD应用于Cedar，我们构建了高效地道的生产代码，证明了模型的正确性，并发现并修复了那些逃过代码审查和单元测试的隐蔽实现缺陷。在验证过程中，我们发现并修复了Cedar策略验证器中的4个错误，而DRT和PBT则帮助我们在Cedar各模块中额外发现并修复了21个错误。