Models and proofs of correctness for permissions queries algorithms

[john-h-kastner-aws]

A permissions query algorithm is an procedure for enumerating resources with a specific type that a principal is authorized to access.

For each algorithm, this PR proves that a resources is listed if and only if it has the expected type and access is in fact allowed.

Specifically, the two main theorems are

theorem resource_scan_correct (n : Nat) (schema : Schema) (req : ResourcesForPrincipalRequest) (entities : Entities) (policies : Policies) (r : EntityUID) :
    validateWithLevel policies schema n = .ok () →
    schema.validateWellFormed = .ok () →
    validateRequest schema (req.req r) = .ok () →
    validateEntities schema entities = .ok () →
    (r ∈ scanResourcesForPrincipal n schema req entities policies ↔
    (r ∈ entities ∧ r.ty = req.resourceType ∧ (isAuthorized (req.req r) entities policies).decision = .allow))

theorem discretionary_resource_for_principal_correct :
  arePoliciesDiscretionary ps = true →
    (r ∈ discretionaryResourcesForPrincipal pq es ps ↔ (r.ty = pq.resourceType ∧ (isAuthorized (pq.req r) es ps).decision = .allow))

[cdisselkoen]

these three lines, which check whether the policy could possibly apply to resourceType, could

• be factored out into a separate def since they're repeated three times in this file
• be further optimized to consider policies with resource is in the scope (my understanding is these have .bound none, but we could exclude some of them)

[john-h-kastner-aws]

I think the current code is the clearest way to implement the intended algorithm

[Copilot]

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.