Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

How We Built Cedar: A Verification-Guided Approach

Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, Andrew Wells

TL;DR

This paper introduces verification-guided development (VGD) as a practical approach to building high-assurance software by combining readable Lean models with mechanized proofs, differential random testing (DRT) to align production Rust code with the model, and property-based testing (PBT) for unmodeled parts. Applied to Cedar, a policy language for expressive, fast, and safe authorization, VGD yields strong correctness guarantees while maintaining development agility, evidenced by the discovery of four validator bugs and twenty-one additional issues via DRT and PBT. The authors argue that VGD strikes a favorable balance between formal verification benefits and maintainability compared with purely Lean-based or Rust-only strategies, and demonstrate the approach with open-source tooling and large-scale testing. The work highlights the practical impact of combining formal methods with targeted testing to drive design improvements, reliability, and trust in security-critical systems.

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.

How We Built Cedar: A Verification-Guided Approach

TL;DR

This paper introduces verification-guided development (VGD) as a practical approach to building high-assurance software by combining readable Lean models with mechanized proofs, differential random testing (DRT) to align production Rust code with the model, and property-based testing (PBT) for unmodeled parts. Applied to Cedar, a policy language for expressive, fast, and safe authorization, VGD yields strong correctness guarantees while maintaining development agility, evidenced by the discovery of four validator bugs and twenty-one additional issues via DRT and PBT. The authors argue that VGD strikes a favorable balance between formal verification benefits and maintainability compared with purely Lean-based or Rust-only strategies, and demonstrate the approach with open-source tooling and large-scale testing. The work highlights the practical impact of combining formal methods with targeted testing to drive design improvements, reliability, and trust in security-critical systems.

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.
Paper Structure (12 sections, 2 figures, 4 tables)

This paper contains 12 sections, 2 figures, 4 tables.

Table of Contents

  1. Introduction
  2. The Cedar Policy Language
  3. Lean Models and Proofs
  4. A human-readable specification
  5. Proofs of properties
  6. Differential Random Testing
  7. Input generation
  8. Properties to test
  9. Experience
  10. Related Work
  11. Conclusion
  12. Trophy and Anti-Trophy Cases

Figures (2)

  • Figure 1: Cedar policies for TinyTodo
  • Figure 2: DRT workflow