Seclib.Domain.PolicySem

PolicySem — ⚪ definition

structure · source

Vendor-neutral policy evaluation: deny-overrides semantics. All definitions and theorems are parameterized over a PolicySem instance. No cloud provider, ARN, IAM, or vendor-specific concept appears in this module.

structure PolicySem (S R Ctx : Type) where

denyOverrides — ⚪ definition

def · source

def denyOverrides (sem : PolicySem S R Ctx) (stmts : List S) (req : R) (ctx : Ctx) : Bool

removeAllow — 🟢 proved

theorem · source

removeAllow: removing an Allow statement narrows access

theorem removeAllow (sem : PolicySem S R Ctx) (stmts : List S) (i : Nat)
    (hi : i < stmts.length) (heff : sem.effect (stmts[i]'hi) = .allow)
    (req : R) (ctx : Ctx)
    (h : denyOverrides sem (stmts.eraseIdx i) req ctx = true) :
    denyOverrides sem stmts req ctx = true

narrow_narrows — 🟢 proved

theorem · source

narrow_narrows: replacing a statement with one that matches fewer requests narrows access. Unifies narrowActions and narrowResources.

theorem narrow_narrows (sem : PolicySem S R Ctx)
    (stmts : List S) (i : Nat) (hi : i < stmts.length)
    (heff : sem.effect (stmts[i]) = .allow)
    (new_s : S) (hnew_eff : sem.effect new_s = .allow)
    (hnew_cond : ∀ c, sem.condEval c new_s = sem.condEval c (stmts[i]))
    (hmono : ∀ req, sem.sat new_s req = true → sem.sat (stmts[i]) req = true)
    (req : R) (ctx : Ctx)
    (h : denyOverrides sem (stmts.set i new_s) req ctx = true) :
    denyOverrides sem stmts req ctx = true

filterMap_narrows — 🟢 proved

theorem · source

theorem filterMap_narrows (sem : PolicySem S R Ctx)
    (stmts : List S) (f : S → Option S) (req : R) (ctx : Ctx)
    (h_deny : ∀ s ∈ stmts, sem.effect s = .deny → f s = some s)
    (h_mono : ∀ s s', s ∈ stmts → f s = some s' → sem.effect s = .allow →

nocontext_conservative — 🟢 proved

theorem · source

nocontext_conservative: if allowed under any context, allowed under noCtx

theorem nocontext_conservative (sem : PolicySem S R Ctx)
    (stmts : List S) (req : R) (ctx : Ctx)
    (h : denyOverrides sem stmts req ctx = true) :
    denyOverrides sem stmts req sem.noCtx = true

grants_complete — 🟢 proved

theorem · source

grants_complete: if allowed, an Allow statement exists that matches

theorem grants_complete (sem : PolicySem S R Ctx)
    (stmts : List S) (req : R) (ctx : Ctx)
    (h : denyOverrides sem stmts req ctx = true) :