Documentation

Cedar.Thm.SymbolicCompilation

This file defines the top-level correctness properties for the symbolic compiler. We show the encoding is sound and complete with respect to the concrete semantics of Cedar. That is, the symbolic semantics both overapproximates (soundness) and underapproximates (completeness) the concrete semantics. #

source
theorem Cedar.Thm.compile_is_sound {x : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term.Outcome εnv} :
εnv.WellFormedFor x → env.WellFormedFor x → env∈ᵢεnv → SymCC.compile x εnv = Except.ok t.term → ∃ (o : Spec.Outcome Spec.Value), o∈ₒt ∧ Spec.evaluate x env.request env.entities ∼ o

Let x be a Cedar expression, env a concrete evaluation environment (request and entities), εnv a symbolic environment, and t the outcome of compiling x to a Term with respect to εnv.

Let x and env be a well-formed input to the concrete evaluator, i.e., env.WellFormedFor x. This means that the entity store env.entities has no dangling entity references, and all entity references that occur in x and env.request are included in env.entities.

Let x and εnv be a well-formed input to the symbolic compiler, i.e., εnv.WellFormedFor x. This means that the symbolic entity store εnv.entities has no dangling (undefined) entity types or references; all term types contained in εnv.entities represent valid Cedar types; and all entity references that occur in x and εnv.request are valid according to εnv.entities.isValidEntityUID.

Let εnv represent a set of concrete environments that includes env, i.e., env ∈ᵢ εnv. We relate concrete structures to their symbolic counterparts via interpretations, which map from term variables and uninterpreted functions to literals. For example, env ∈ᵢ εnv if there exists a well-formed interpretation I such that env ∼ εnv.interpret I are equivalent according to the sameness relation ∼. Note that we can't use equality here, because interpreting a symbolic structure with respect to an Interpretation produces a literal symbolic structure (without any unknowns), which is then compared to the corresponding concrete structure using a suitable sameness relation.

Given the above, the soundness theorem says that the output of the concrete evaluator on x and env is contained in the set of concrete outcomes represented by the output of the symbolic compiler on x and εnv. We state soundness in terms of Outcomes rather than Results because the symbolic compiler does not distinguish between different kinds of errors---only between normal and erroring executions.

source
theorem Cedar.Thm.compile_is_complete {x : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term.Outcome εnv} {o : Spec.Outcome Spec.Value} :
εnv.WellFormedFor x → SymCC.compile x εnv = Except.ok t.term → o∈ₒt → ∃ (env : Spec.Env), env.WellFormedFor x ∧ env∈ᵢεnv ∧ Spec.evaluate x env.request env.entities ∼ o

Let x be a Cedar expression and εnv a symbolic environment, where x and εnv are a well-formed input to the symbolic compiler, i.e., εnv.WellFormedFor x.

Let t the outcome of compiling x to a Term with respect to εnv, and o a concrete outcome represented by t.

Then, the completeness theorem says that there exists a concrete environment env represented by εnv such that x and env are well-formed inputs to the concrete evaluator and evaluating x against env produces the outcome o.

source
theorem Cedar.Thm.isAuthorized_is_sound {ps : Spec.Policies} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term.Outcome εnv} :
εnv.WellFormedForPolicies ps → env.WellFormedForPolicies ps → env∈ᵢεnv → SymCC.isAuthorized ps εnv = Except.ok t.term → ∃ (decision : Spec.Decision), decision∈ₒt ∧ Spec.isAuthorized env.request env.entities ps ∼ decision

Let ps be Cedar policies, env a concrete evaluation environment (request and entities), εnv a symbolic environment, and t the term resulting from symbolically authorizing ps with respect to εnv, i.e., SymCC.isAuthorized ps εnv = .ok t.

Let ps and env be a well-formed input to the concrete authorizer, i.e., env.WellFormedForPolicies ps. This means that the entity store env.entities has no dangling entity references, and all entity references that occur in ps and env.request are included in env.entities.

Let ps and εnv be a well-formed input to the symbolic authorizer, i.e., εnv.WellFormedForPolices ps. This means that the symbolic entity store εnv.entities has no dangling (undefined) entity types or references; all term types contained in εnv.entities represent valid Cedar types; and all entity references that occur in ps and εnv.request are valid according to εnv.entities.isValidEntityUID.

Let εnv represent a set of concrete environments that includes env, i.e., env ∈ᵢ εnv. We relate concrete structures to their symbolic counterparts via interpretations, which map from term variables and uninterpreted functions to literals. For example, env ∈ᵢ εnv if there exists a well-formed interpretation I such that env ∼ εnv.interpret I are equivalent according to the sameness relation ∼. Note that we can't use equality here, because interpreting a symbolic structure with respect to an Interpretation produces a literal symbolic structure (without any unknowns), which is then compared to the corresponding concrete structure using a suitable sameness relation.

Given the above, the soundness theorem says that the decision of the concrete authorizer on ps and env is contained in the set of concrete decisions represented by the output of the symbolic authorizer on ps and εnv. We state soundness in terms of Decisions rather than Responses because the symbolic authorizer computes only decision (and not the extra diagnostics contained in a concrete Response).

source
theorem Cedar.Thm.isAuthorized_is_complete {ps : Spec.Policies} {εnv : SymCC.SymEnv} {t : SymCC.Term.Outcome εnv} {decision : Spec.Decision} :
εnv.WellFormedForPolicies ps → SymCC.isAuthorized ps εnv = Except.ok t.term → decision∈ₒt → ∃ (env : Spec.Env), env.WellFormedForPolicies ps ∧ env∈ᵢεnv ∧ Spec.isAuthorized env.request env.entities ps ∼ decision

Let ps be Cedar policies and εnv a symbolic environment, where ps and εnv are a well-formed input to the symbolic authorizer, i.e., εnv.WellFormedForPolicies ps.

Let t the outcome of symbolically authorizing ps with respect to εnv, and d a concrete authorization decision represented by t.

Then, the completeness theorem says that there exists a concrete environment env represented by εnv such that ps and env are well-formed inputs to the concrete authorizer and authorizing os against env produces the decision d.

source
theorem Cedar.Thm.compile_well_typed {tx : Validation.TypedExpr} {Γ : Validation.TypeEnv} :
Γ.WellFormed → TypedExpr.WellTyped Γ tx → ∃ (t : SymCC.Term), SymCC.compile tx.toExpr (SymCC.SymEnv.ofEnv Γ) = Except.ok t ∧ SymCC.Term.WellFormed (SymCC.SymEnv.ofEnv Γ).entities t ∧ t.typeOf = (SymCC.TermType.ofType tx.typeOf).option

For any well-typed expression tx in a well-formed environment Γ (which can be produced by Cedar's type checker), the symbolic compiler should never fail and produce a term t that is well-formed and has the type TermType.ofType tx.typeOf.

source
def Cedar.Thm.IsOption (tty : SymCC.TermType) :
Prop
Equations
Instances For
    source
    def Cedar.Thm.OptionTyped (t : SymCC.Term) :
    Prop
    Equations
    Instances For
      source
      theorem Cedar.Thm.compile_ok_implies_option {x : Spec.Expr} {εnv : SymCC.SymEnv} {t : SymCC.Term} :
      SymCC.compile x εnv = Except.ok t → ∃ (tty : SymCC.TermType), t.typeOf = tty.option

      Weaker result than compile_well_typed, but requiring weaker hypotheses:

      If compile on any expression (not necessarily well-typed) produces .ok t, then t must have option type