How We Built Cedar: A Verification-Guided Approach

TL;DR

This paper introduces verification-guided development (VGD), a process combining formal proofs, differential random testing, and property-based testing to build a secure, efficient policy language called Cedar, ensuring correctness and bug detection.

Contribution

The paper presents VGD as a novel integrated approach for developing secure policy languages, demonstrating its effectiveness through the construction of Cedar.

Findings

Proved the correctness of Cedar’s model.

Detected and fixed 25 bugs in Cedar's implementation.

Enhanced reliability and security of Cedar through combined testing and formal verification.

Abstract

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.