Crate cedar_policy_symcc

Expand description

§Symbolic Cedar Compiler (SymCC)

With this library, you can

Compile Cedar policies to logical constraints in SMT-LIB.
Formally verify a number of useful properties about your Cedar policies with concrete counterexamples.

Our symbolic compiler and verifiers have been formally modeled and verified in Lean to guarantee trustworthy verification results.

SymCC currently supports formally verifying the following properties:

Policy never errors (CedarSymCompiler::check_never_errors).
Policy set always allows (CedarSymCompiler::check_always_allows).
Policy set always denies (CedarSymCompiler::check_always_denies).
Policy set subsumption (CedarSymCompiler::check_implies).
Policy set equivalence (CedarSymCompiler::check_equivalent).
Policy set disjointness (CedarSymCompiler::check_disjoint).

For each of them, we also have the CedarSymCompiler::check_*_with_counterexample counterparts that produce a counterexample (a synthesized request and entity store) if the property is not true.

§Setup

To get started, first download or compile the cvc5-1.3.1 SMT solver. The following example assumes that you have set the following environment variable:

CVC5=<path to cvc5 1.3.1 executable>

§Example

To verify that a policy set does not always allow every well-formed request:

use tokio;
use std::str::FromStr;
use cedar_policy::{Schema, PolicySet, Authorizer, Decision};
use cedar_policy_symcc::{solver::LocalSolver, CedarSymCompiler, SymEnv, WellTypedPolicies};

#[tokio::main]
async fn main() {
    // Parse Cedar schema
    let schema = Schema::from_cedarschema_str(r#"
        entity User;
        entity Document { owner: User };
        action view appliesTo {
            principal: [User],
            resource: [Document]
        };
    "#).unwrap().0;

    // Parse Cedar policy set
    let policy_set = PolicySet::from_str(r#"
        permit(principal, action == Action::"view", resource)
        when { resource.owner == principal };
    "#).unwrap();

    // Initialize the symbolic compiler
    let cvc5 = LocalSolver::cvc5().unwrap();
    let mut compiler = CedarSymCompiler::new(cvc5).unwrap();

    // Iterate through all request environments and check the property
    for req_env in schema.request_envs() {
        // Encode the request environment symbolically
        let sym_env = SymEnv::new(&schema, &req_env).unwrap();

        // Validate/type check the policy set
        let typed_policies = WellTypedPolicies::from_policies(&policy_set, &req_env, &schema).unwrap();

        // Verify that `policy_set` does not always allow any request
        let always_denies = compiler.check_always_allows(&typed_policies, &sym_env).await.unwrap();
        assert!(!always_denies);

        // Similar to above, but returns a counterexample (a synthesized request
        // and entity store) which is denied by the policy set.
        let cex = compiler.check_always_allows_with_counterexample(&typed_policies, &sym_env).await.unwrap().unwrap();
        let resp = Authorizer::new().is_authorized(&cex.request, &policy_set, &cex.entities);
        assert!(resp.decision() == Decision::Deny);
    }
}

To learn more about what you can do with SymCC, see the documentation of the CedarSymCompiler type.

§Development

To build and test this crate, run the following commands from the root of the repository:

cargo build -p cedar-policy-symcc
CVC5=<absolute path to cvc5 1.3.1 executable> cargo test -p cedar-policy-symcc

Structure of this crate:

symcc is the core library. It maps directly to the Lean model.
lib.rs is the frontend for symcc, and does not directly correspond to the Lean, but it provides an interface in terms of cedar-policy types rather than cedar-policy-core types.

Modules§

bitvec: Implementation of BitVec.
err: All error types in SymCC.
ext: Extension values in SymCC.
extension_types: Implementations of various extension values.
op: Various super::term::Term operations allowed in super::term::Term::App.
solver: A simple interface to an SMT solver.
solver_pool: A pool of warm CVC5 solver processes for reusing across queries.
term: A simply typed IR to which we reduce Cedar expressions during symbolic compilation.
term_factory: Utility functions to construct Terms.
term_type: Definitions of term types.
type_abbrevs: Various type abbreviations used throughout SymCC.

Structs§

CedarSymCompiler: Cedar symbolic compiler, which takes your policies and schemas and converts them to SMT queries to perform various verification tasks such as checking if a policy set always allows/denies, if two policy sets are equivalent, etc.
CompiledPolicy: Represents a symbolically compiled policy. This can be fed into various functions on CedarSymCompiler for efficient solver queries (that don’t have to repeat symbolic compilation).
CompiledPolicySet: Represents a symbolically compiled policyset. This can be fed into various functions on CedarSymCompiler for efficient solver queries (that don’t have to repeat symbolic compilation).
CompiledSchema: A Schema paired with its precomputed [SymEntities].
Env: A concrete environment recovered from a SymEnv.
Interpretation: An interpretation extracted from an SMT model consists of
SymEnv: Symbolic representation of a request environment.
WellFormedAsserts: Well-formed assertions generated by the symbolic compiler.
WellTypedPoliciesDeprecated: Validated and well-typed policy set. Similar to WellTypedPolicy but for policy sets.
WellTypedPolicyDeprecated: Validated and well-typed policy.

Enums§

ResetMode: Controls how the (reset) that starts each solver query is written into the SMTLib script.

Traits§

SmtLibScript: Abstraction layer to write output in the SMTLib2 format.

Functions§

always_allows_asserts: Generate the WellFormedAsserts for the check_always_allows() operation, without actually calling a solver.
always_denies_asserts: Generate the WellFormedAsserts for the check_always_denies() operation, without actually calling a solver.
always_matches_asserts: Generate the WellFormedAsserts for the check_always_matches() operation, without actually calling a solver.
disjoint_asserts: Generate the WellFormedAsserts for the check_disjoint() operation, without actually calling a solver.
equivalent_asserts: Generate the WellFormedAsserts for the check_equivalent() operation, without actually calling a solver.
implies_asserts: Generate the WellFormedAsserts for the check_implies() operation, without actually calling a solver.
matches_disjoint_asserts: Generate the WellFormedAsserts for the check_matches_disjoint() operation, without actually calling a solver.
matches_equivalent_asserts: Generate the WellFormedAsserts for the check_matches_equivalent() operation, without actually calling a solver.
matches_implies_asserts: Generate the WellFormedAsserts for the check_matches_implies() operation, without actually calling a solver.
never_errors_asserts: Generate the WellFormedAsserts for the check_never_errors() operation, without actually calling a solver.
never_matches_asserts: Generate the WellFormedAsserts for the check_never_matches() operation, without actually calling a solver.

Type Aliases§

Asserts: Type of assertions (i.e., a list of Terms).