This file contains verify* functions that use the Cedar symbolic compiler, authorizer, and hierarchy enforcer to generate a list of Asserts. These are boolean terms whose conjunction is unsatisfiable if and only if the verified property holds.

@[reducible, inline]

abbrev Cedar.SymCC.Asserts : Type

Equations

• Cedar.SymCC.Asserts = List Cedar.SymCC.Term

def Cedar.SymCC.verifyEvaluate (φ : Term → Term) (p : Spec.Policy) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff the evaluation of p, represented as a Term of type .option .bool, satisfies φ on all inputs drawn from εnv. See also verifyNeverErrors, verifyAlwaysMatches, and verifyNeverMatches.

Equations

• Cedar.SymCC.verifyEvaluate φ p εnv = do let t ← Cedar.SymCC.compile p.toExpr εnv Except.ok ((Cedar.SymCC.enforce [p.toExpr] εnv).elts ++ [Cedar.SymCC.Factory.not (φ t)])

def Cedar.SymCC.verifyEvaluatePair (φ : Term → Term → Term) (p₁ p₂ : Spec.Policy) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff the evaluation of p₁ and p₂, represented as Terms of type .option .bool, satisfy φ on all inputs drawn from εnv. See also verifyMatchesImplies, verifyMatchesEquivalent, and verifyMatchesDisjoint.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyIsAuthorized (φ : Term → Term → Term) (ps₁ ps₂ : Spec.Policies) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff the authorization decisions produced by ps₁ and ps₂, represented as Terms of type .bool, satisfy φ on all inputs drawn from εnv. See also verifyAlwaysAllows, verifyAlwaysDenies, verifyImplies, verifyEquivalent, and verifyDisjoint.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyNeverErrors (p : Spec.Policy) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff p does not error on any input in εnv. If the asserts are satisfiable, then there is some input in εnv on which p errors.

Equations

• Cedar.SymCC.verifyNeverErrors p εnv = Cedar.SymCC.verifyEvaluate Cedar.SymCC.Factory.isSome p εnv

def Cedar.SymCC.verifyAlwaysMatches (p : Spec.Policy) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff p matches all inputs in εnv. If the asserts are satisfiable, then there is some input in εnv which p doesn't match.

Equations

• Cedar.SymCC.verifyAlwaysMatches p εnv = Cedar.SymCC.verifyEvaluate (fun (x : Cedar.SymCC.Term) => Cedar.SymCC.Factory.eq x (⊙Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool true))) p εnv

def Cedar.SymCC.verifyNeverMatches (p : Spec.Policy) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff p matches no inputs in εnv. If the asserts are satisfiable, then there is some input in εnv which p does match.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyMatchesEquivalent (p₁ p₂ : Spec.Policy) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff p₁ and p₂ match exactly the same set of inputs in εnv.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyMatchesImplies (p₁ p₂ : Spec.Policy) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff p₁ matching implies that p₂ matches, for every input in εnv. In other words, for every request where p₁ matches, p₂ also matches.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyMatchesDisjoint (p₁ p₂ : Spec.Policy) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff there is no input in εnv that is matched by both p₁ and p₂. In other words, the sets of inputs matched by p₁ and p₂ are disjoint. If this query is satisfiable, then there is at least one input that is matched by both p₁ and p₂.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyMatchesDisjoint.disjoint (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.verifyMatchesDisjoint.disjoint t₁ t₂ = Cedar.SymCC.Factory.not (Cedar.SymCC.Factory.and t₁ t₂)

def Cedar.SymCC.verifyImplies (ps₁ ps₂ : Spec.Policies) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff the authorization decision of ps₁ implies that of ps₂ for every input in εnv. In other words, every input allowed by ps₁ is allowed by ps₂.

Equations

• Cedar.SymCC.verifyImplies ps₁ ps₂ εnv = Cedar.SymCC.verifyIsAuthorized Cedar.SymCC.Factory.implies ps₁ ps₂ εnv

def Cedar.SymCC.verifyAlwaysAllows (ps : Spec.Policies) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff ps allows all inputs in εnv.

Equations

• Cedar.SymCC.verifyAlwaysAllows ps εnv = Cedar.SymCC.verifyImplies [Cedar.SymCC.verifyAlwaysAllows.allowAll] ps εnv

def Cedar.SymCC.verifyAlwaysAllows.allowAll : Spec.Policy

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyAlwaysDenies (ps : Spec.Policies) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff ps denies all inputs in εnv.

Equations

• Cedar.SymCC.verifyAlwaysDenies ps εnv = Cedar.SymCC.verifyImplies ps [] εnv

def Cedar.SymCC.verifyEquivalent (ps₁ ps₂ : Spec.Policies) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff ps₁ and ps₂ produce the same authorization decision on all inputs in εnv.

Equations

• Cedar.SymCC.verifyEquivalent ps₁ ps₂ εnv = Cedar.SymCC.verifyIsAuthorized Cedar.SymCC.Factory.eq ps₁ ps₂ εnv

def Cedar.SymCC.verifyDisjoint (ps₁ ps₂ : Spec.Policies) (εnv : SymEnv) : Result Asserts

Returns asserts that are unsatisfiable iff there is no input in εnv that is allowed by both ps₁ and ps₂. This checks that the authorization semantics of ps₁ and ps₂ are disjoint. If this query is satisfiable, then there is at least one input that is allowed by both ps₁ and ps₂.

Equations

• Cedar.SymCC.verifyDisjoint ps₁ ps₂ εnv = Cedar.SymCC.verifyIsAuthorized Cedar.SymCC.verifyDisjoint.disjoint ps₁ ps₂ εnv

def Cedar.SymCC.verifyDisjoint.disjoint (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.verifyDisjoint.disjoint t₁ t₂ = Cedar.SymCC.Factory.not (Cedar.SymCC.Factory.and t₁ t₂)