Documentation

Cedar.Thm.Authorization.PolicySlice

This file contains definitions relevant to slicing.

source
def Cedar.Thm.IsSoundPolicySlice (req : Spec.Request) (entities : Spec.Entities) (slice policies : Spec.Policies) :
Prop

A policy slice is a subset of a collection of policies. This slice is sound for a given request and entities if every policy in the collection that is not in the slice is also not satisfied with respect to the request and entities, and doesn't produce an error when evaluated.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Cedar.Thm.sound_slice_transitive {r : Spec.Request} {es : Spec.Entities} {slice₁ ps slice₂ : Spec.Policies} :
    IsSoundPolicySlice r es slice₁ ps → IsSoundPolicySlice r es slice₂ slice₁ → IsSoundPolicySlice r es slice₂ ps
    source
    def Cedar.Thm.IsSoundPolicySliceFalseDef (req : Spec.Request) (entities : Spec.Entities) (slice policies : Spec.Policies) :
    Prop

    Alternate definition of soundness for policy slicing. Rather than showing that a policy doesn't evaluate to true or error, we can show that it does evaluate to false.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Cedar.Thm.is_sound_policy_slice_def_equiv {req : Spec.Request} {entities : Spec.Entities} {slice policies : Spec.Policies} :
      IsSoundPolicySlice req entities slice policies ↔ IsSoundPolicySliceFalseDef req entities slice policies
      source
      def Cedar.Thm.IsSoundPolicyBound (bound : Slice.PolicyBound) (policy : Spec.Policy) :
      Prop

      A bound is sound for a given policy if the bound is satisfied for every request and entities for which the policy is satisfied or for which the policy produces an error.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cedar.Thm.IsSoundBoundAnalysis (ba : Slice.BoundAnalysis) :
        Prop

        A bound analysis is sound if it produces sound bounds for all policies.

        Equations
        Instances For
          source
          theorem Cedar.Thm.sound_policy_slice_is_equisatisfied (effect : Spec.Effect) {request : Spec.Request} {entities : Spec.Entities} {slice policies : Spec.Policies} :
          IsSoundPolicySlice request entities slice policies → List.filterMap (fun (x : Spec.Policy) => Spec.satisfiedWithEffect effect x request entities) slice ≡ List.filterMap (fun (x : Spec.Policy) => Spec.satisfiedWithEffect effect x request entities) policies
          source
          theorem Cedar.Thm.satisfiedPolicies_eq_for_sound_policy_slice (effect : Spec.Effect) {request : Spec.Request} {entities : Spec.Entities} {slice policies : Spec.Policies} :
          IsSoundPolicySlice request entities slice policies → Spec.satisfiedPolicies effect slice request entities = Spec.satisfiedPolicies effect policies request entities
          source
          theorem Cedar.Thm.sound_policy_slice_is_equierror {request : Spec.Request} {entities : Spec.Entities} {slice policies : Spec.Policies} :
          IsSoundPolicySlice request entities slice policies → List.filter (fun (x : Spec.Policy) => Spec.hasError x request entities) slice ≡ List.filter (fun (x : Spec.Policy) => Spec.hasError x request entities) policies
          source
          theorem Cedar.Thm.errorPolicies_eq_for_sound_policy_slice {request : Spec.Request} {entities : Spec.Entities} {slice policies : Spec.Policies} :
          IsSoundPolicySlice request entities slice policies → Spec.errorPolicies slice request entities = Spec.errorPolicies policies request entities