This file defines a simple policy slicing algorithm that is based on policy scopes. For proofs of correctness, see Cedar.Thm.PolicySlice.

structure Cedar.Slice.PolicyBound : Type

A policy bound consists of optional principal and resource entities.

• principalBound : Option Spec.EntityUID
• resourceBound : Option Spec.EntityUID

def Cedar.Slice.inSomeOrNone (uid : Spec.EntityUID) (opt : Option Spec.EntityUID) (entities : Spec.Entities) : Bool

Equations

• Cedar.Slice.inSomeOrNone uid (some uid') entities = Cedar.Spec.inₑ uid uid' entities
• Cedar.Slice.inSomeOrNone uid none entities = true

def Cedar.Slice.satisfiedBound (bound : PolicyBound) (request : Spec.Request) (entities : Spec.Entities) : Bool

A bound is satisfied by a request and store if the request principal and resource fields are descendents of the corresponding bound fields (or if those bound fields are none).

Equations

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

@[reducible, inline]

abbrev Cedar.Slice.BoundAnalysis : Type

A bound analysis takes as input a policy and returns a PolicyBound.

Equations

• Cedar.Slice.BoundAnalysis = (Cedar.Spec.Policy → Cedar.Slice.PolicyBound)

def Cedar.Slice.BoundAnalysis.slice (ba : BoundAnalysis) (request : Spec.Request) (entities : Spec.Entities) (policies : Spec.Policies) : Spec.Policies

A bound-based slicing algorithm takes as input a bound analysis, request, entities, and policies, and filters out the policies whose bound is not satisfied by the request and entities.

Equations

• ba.slice request entities policies = List.filter (fun (policy : Cedar.Spec.Policy) => Cedar.Slice.satisfiedBound (ba policy) request entities) policies

def Cedar.Slice.scopeAnalysis (policy : Spec.Policy) : PolicyBound

Scope-based bound analysis extracts the bound from the policy scope.

Equations

• Cedar.Slice.scopeAnalysis policy = { principalBound := policy.principalScope.scope.bound, resourceBound := policy.resourceScope.scope.bound }