Soundness of batched authorization: if the batched authorizer reaches a definitive decision, that decision agrees with the concrete authorizer.
theorem
Cedar.Thm.evaluatePolicy_ok_implies_env_some
{schema : Validation.Schema}
{p : Spec.Policy}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{r : Spec.Residual}
:
theorem
Cedar.Thm.evaluatePolicy_ok_implies_requestMatchesEnvironment
{schema : Validation.Schema}
{p : Spec.Policy}
{req : Spec.Request}
{r : Spec.Residual}
{pes : TPE.PartialEntities}
:
TPE.evaluatePolicy schema p req.asPartialRequest pes = Except.ok r →
∀ (env : Validation.TypeEnv),
schema.environment? req.asPartialRequest.principal.ty req.asPartialRequest.resource.ty req.asPartialRequest.action = some env →
Validation.requestMatchesEnvironment env req = true
theorem
Cedar.Thm.evaluatePolicy_ok_implies_well_formed_env
{schema : Validation.Schema}
{p : Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{r : Spec.Residual}
{pes : TPE.PartialEntities}
:
TPE.evaluatePolicy schema p req.asPartialRequest pes = Except.ok r →
schema.validateWellFormed = Except.ok () →
Validation.validateEntities schema es = Except.ok () →
∃ (env : Validation.TypeEnv), schema.environment? req.asPartialRequest.principal.ty req.asPartialRequest.resource.ty
req.asPartialRequest.action = some env ∧ InstanceOfWellFormedEnvironment req es env
If evaluatePolicy succeeds on a concrete request, and the schema and entities
pass validation, then InstanceOfWellFormedEnvironment holds for the
environment determined by the schema and request.
def
Cedar.Thm.ResidualPoliciesEquivAndWellTyped
(env : Validation.TypeEnv)
(policies : List Spec.Policy)
(residuals : List TPE.ResidualPolicy)
(req : Spec.Request)
(es : Spec.Entities)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cedar.Thm.equiv_well_typed_implies_equiv
{env : Validation.TypeEnv}
{policies : List Spec.Policy}
{residuals : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
(h : ResidualPoliciesEquivAndWellTyped env policies residuals req es)
:
ResidualPoliciesEquiv policies residuals req es
theorem
Cedar.Thm.residuals_equiv_preserved
{env : Validation.TypeEnv}
{policies : List Spec.Policy}
{residuals : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
(h_sound : ResidualPoliciesEquivAndWellTyped env policies residuals req es)
(h_wf : InstanceOfWellFormedEnvironment req es env)
(h_ref : RequestAndEntitiesRefine req es req.asPartialRequest pes)
:
ResidualPoliciesEquivAndWellTyped env policies
(List.map
(fun (rp : TPE.ResidualPolicy) =>
{ id := rp.id, effect := rp.effect, residual := TPE.evaluate env rp.residual req.asPartialRequest pes })
residuals)
req es
theorem
Cedar.Thm.batched_authorize_loop_equiv
{loader : TPE.EntityLoader}
{iters : Nat}
{policies : List Spec.Policy}
{residuals : List TPE.ResidualPolicy}
{req : Spec.Request}
(es : Spec.Entities)
{current_store : TPE.PartialEntities}
{env : Validation.TypeEnv}
:
EntityLoader.WellBehaved es loader →
ResidualPoliciesEquivAndWellTyped env policies residuals req es →
RequestAndEntitiesRefine req es req.asPartialRequest current_store →
InstanceOfWellFormedEnvironment req es env →
∃ (rps : List TPE.ResidualPolicy), TPE.batchedAuthorizeLoop env residuals req loader current_store iters = TPE.isAuthorizedFromResiduals rps ∧ ResidualPoliciesEquivAndWellTyped env policies rps req es
The loop's response is isAuthorizedFromResiduals of a list still equivalent to the policies.
theorem
Cedar.Thm.batched_authorize_loop_decision_agrees
{loader : TPE.EntityLoader}
{iters : Nat}
{policies : List Spec.Policy}
{residuals : List TPE.ResidualPolicy}
{req : Spec.Request}
(es : Spec.Entities)
{current_store : TPE.PartialEntities}
{env : Validation.TypeEnv}
{d : Spec.Decision}
:
EntityLoader.WellBehaved es loader →
ResidualPoliciesEquivAndWellTyped env policies residuals req es →
RequestAndEntitiesRefine req es req.asPartialRequest current_store →
InstanceOfWellFormedEnvironment req es env →
(TPE.batchedAuthorizeLoop env residuals req loader current_store iters).decision = some d →
(Spec.isAuthorized req es policies).decision = d
The loop's decision agrees with concrete authorization.
theorem
Cedar.Thm.evaluatePolicies_equiv_and_well_typed
{schema : Validation.Schema}
{policies : List Spec.Policy}
{rps : List TPE.ResidualPolicy}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{env : Validation.TypeEnv}
:
List.Forall₂
(fun (p : Spec.Policy) (rp : TPE.ResidualPolicy) =>
TPE.ResidualPolicy.mk p.id p.effect <$> TPE.evaluatePolicy schema p preq pes = Except.ok rp)
policies rps →
schema.environment? preq.principal.ty preq.resource.ty preq.action = some env →
InstanceOfWellFormedEnvironment req es env →
RequestAndEntitiesRefine req es preq pes → ResidualPoliciesEquivAndWellTyped env policies rps req es