SymCert: Verifying SMT-Based Policy Analyses

Abstract

Cedar is a popular authorization language designed to support sound and complete policy analysis by reduction to SMT. But building these analyses is error-prone: subtle encoding mistakes can silently compromise soundness or completeness, and are hard to catch through testing alone. Cedar’s high-assurance development process therefore requires writing and maintaining formal proofs of correctness for each new analysis. This paper presents SymCert, a framework implemented in Lean for building verified SMT-based analyses of Cedar policies. SymCert provides a verified symbolic compiler and authorizer for reducing policies to SMT formulas, a hierarchy enforcer for ensuring well-formedness of counterexamples, and a counterexample extractor for converting infinite SMT models into finite Cedar inputs, which is essential for proving analysis completeness. To make verification practical, we develop a modular proof approach that decomposes symbolic compiler correctness into two general properties, reducibility and interpretability, yielding reusable lemmas that simplify proofs across all components. We evaluate SymCert by verifying five analyses used in a Cedar analysis service at Amazon Web Services. Modeling and proving these analyses took just one work day, resulting in efficient executable models that service developers use for prototyping and differential random testing of production code. We demonstrate SymCert’s maintainability through three extensions to support new Cedar features, requiring only modest effort (4 to 8 days each) thanks to our modular proof approach.