Theorem Catalog

33 proved · 0 sorry · 33 total

Condition Key Evaluation (IamExplainer.Condition)

SCPs, Permission Boundaries, and RCPs (IamExplainer.Layers)

End-to-End IAM Authorization Proofs (IamExplainer.Proofs)

Policy Evaluation Semantics (Seclib.Domain.PolicySem)

Action and Resource Pattern Matching (Seclib.Prim.Glob)

Statement Combining — Deny Overrides (Seclib.Prim.Rule)

Dependency Graph

Nodes: 🟢 proved, 🟡 sorry, ⚪ definition.

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) :

Seclib.Prim

— ⚪ definition

instance · source

instance : ToString Tri where

Seclib.Prim.Context

Request — ⚪ definition

structure · source

Vendor-neutral authorization request and evaluation context. No cloud provider noun appears in this module.

structure Request where

CondContext — ⚪ definition

structure · source

structure CondContext where

mkContext — ⚪ definition

def · source

def mkContext (j : Json) : Except String CondContext

CondContext.lookup — ⚪ definition

def · source

def CondContext.lookup (ctx : CondContext) (key : String) : Option Json

Seclib.Prim.Finding

Severity.toString — ⚪ definition

def · source

def Severity.toString : Severity → String
  | .critical => "critical"
  | .high     => "high"
  | .medium   => "medium"
  | .low      => "low"

— ⚪ definition

instance · source

instance : ToString Severity

Evidence — ⚪ definition

structure · source

structure Evidence where

Fix — ⚪ definition

structure · source

structure Fix where

Finding — ⚪ definition

structure · source

structure Finding where

Seclib.Prim.Glob

toLowerStr — ⚪ definition

def · source

Vendor-neutral case folding, glob pattern matching, and string lemmas. No cloud provider noun appears in this module.

def toLowerStr (s : String) : String

matchPatternGo — ⚪ definition

def · source

def matchPatternGo (ps vs : List Char) : Bool

matchPattern — ⚪ definition

def · source

def matchPattern (pattern : String) (value : String) : Bool

ciEq — ⚪ definition

def · source

def ciEq (s₁ s₂ : String) : Bool

ciEq_toLowerStr — 🟢 proved

theorem · source

theorem ciEq_toLowerStr (s s' : String) (h : ciEq s s' = true) :
    toLowerStr s = toLowerStr s'

matchPatternGo_literal_eq — 🟢 proved

theorem · source

theorem matchPatternGo_literal_eq (ps vs : List Char)
    (hno_star : '*' ∉ ps) (hno_q : '?' ∉ ps)
    (h : matchPatternGo ps vs = true) :
    ps = vs

matchPattern_literal_mp — 🟢 proved

theorem · source

theorem matchPattern_literal_mp (p s : String)
    (hno_star : '*' ∉ p.toList) (hno_q : '?' ∉ p.toList)
    (h : matchPattern p s = true) :
    ciEq p s = true

matchPattern_cs_literal_eq — 🟢 proved

theorem · source

theorem matchPattern_cs_literal_eq (p s : String)
    (hno_star : '*' ∉ p.toList) (hno_q : '?' ∉ p.toList)
    (h : matchPattern p s = true) : p = s

toLower_eq_star — 🟢 proved

theorem · source

theorem toLower_eq_star (c : Char) (h : c.toLower = '*') : c = '*'

toLower_eq_question — 🟢 proved

theorem · source

theorem toLower_eq_question (c : Char) (h : c.toLower = '?') : c = '?'

Seclib.Prim.Rule

Rule — ⚪ definition

structure · source

Vendor-neutral authorization primitives: Rule, appliesOf, denyOverrides. No cloud provider noun appears in this module.

structure Rule where

denyOverridesRules — ⚪ definition

def · source

def denyOverridesRules (rules : List Rule) : Bool

denyOverrides_remove_allow_narrows — 🟢 proved

theorem · source

Lemma 1: Removing an allow rule narrows access

theorem denyOverrides_remove_allow_narrows (rules : List Rule) (i : Nat)
    (hi : i < rules.length) (hallow : (rules[i]).decision = .allow)
    (h : denyOverridesRules (rules.eraseIdx i) = true) :
    denyOverridesRules rules = true

denyOverrides_add_deny_narrows — 🟢 proved

theorem · source

Lemma 2: Adding a deny narrows

theorem denyOverrides_add_deny_narrows (rules : List Rule) (i : Nat)
    (hi : i < rules.length) (hdeny : (rules[i]).decision = .deny)
    (h : denyOverridesRules rules = true) :
    denyOverridesRules (rules.eraseIdx i) = true

conj_narrows — 🟢 proved

theorem · source

Lemma 3: Conjunction of evaluation gates never widens access

theorem conj_narrows (a b : Bool) (h : a && b = true) : a = true ∧ b = true

appliesOf_unknown_conservative — 🟢 proved

theorem · source

Lemma 4: Unknown applicability is conservative

theorem appliesOf_unknown_conservative (rules rules_noCtx : List Rule)
    (hlen : rules.length = rules_noCtx.length)
    (hpair : ∀ j (hj : j < rules.length),
      (rules_noCtx[j]'(hlen ▸ hj)).decision = (rules[j]).decision ∧
      (rules_noCtx[j]'(hlen ▸ hj)).sat = (rules[j]).sat ∧
      ((rules_noCtx[j]'(hlen ▸ hj)).applicability = .t ∨
       (rules_noCtx[j]'(hlen ▸ hj)).applicability = .u) ∧
      ((rules_noCtx[j]'(hlen ▸ hj)).applicability = .t →
       (rules[j]).applicability = .t))
    (h : denyOverridesRules rules = true) :
    denyOverridesRules rules_noCtx = true

IamExplainer.Checks

checkAdminEquiv — ⚪ definition

def · source

def checkAdminEquiv (s : Statement) : List Finding

checkServiceWildcard — ⚪ definition

def · source

def checkServiceWildcard (s : Statement) : List Finding

checkResourceWildcard — ⚪ definition

def · source

def checkResourceWildcard (s : Statement) : List Finding

checkNotAction — ⚪ definition

def · source

def checkNotAction (s : Statement) : List Finding

checkNotResource — ⚪ definition

def · source

def checkNotResource (s : Statement) : List Finding

checkPassRole — ⚪ definition

def · source

def checkPassRole (s : Statement) : List Finding

evaluate — ⚪ definition

def · source

def evaluate (p : Policy) : List Finding

IamExplainer.Condition

CondWarning — ⚪ definition

structure · source

structure CondWarning where

CondKeyVal — ⚪ definition

structure · source

structure CondKeyVal where

CondOp — ⚪ definition

structure · source

structure CondOp where

decodeCondBlocks — ⚪ definition

def · source

def decodeCondBlocks (cond : Option Json) : CondBlocks × List CondWarning

evalCond_noContext_tu — 🟢 proved

theorem · source

theorem evalCond_noContext_tu (blocks : CondBlocks) :
    (evalCond noContext blocks).1 = .t ∨ (evalCond noContext blocks).1 = .u

evalCond_noContext_T_imp — 🟢 proved

theorem · source

theorem evalCond_noContext_T_imp (blocks : CondBlocks) (ctx : CondContext)
    (h : (evalCond noContext blocks).1 = .t) :
    (evalCond ctx blocks).1 = .t

IamExplainer.Emit

Need — ⚪ definition

structure · source

structure Need where

Needs — ⚪ definition

structure · source

structure Needs where

Transform — ⚪ definition

structure · source

structure Transform where

Residual — ⚪ definition

structure · source

structure Residual where

Withheld — ⚪ definition

structure · source

structure Withheld where

EmitReport — ⚪ definition

structure · source

structure EmitReport where

hasWildcard — ⚪ definition

def · source

def hasWildcard (s : String) : Bool

allNeedResourcesExact — ⚪ definition

def · source

def allNeedResourcesExact (stmt : Statement) (ns : List Need) : Bool

touchingResources — ⚪ definition

def · source

def touchingResources (stmt : Statement) (ns : List Need) : List String

emitFixed — ⚪ definition

def · source

def emitFixed (p : Policy) (ns : Needs) : Policy × EmitReport

parseNeeds — ⚪ definition

def · source

def parseNeeds (input : String) : Except String Needs

stmtToJson — ⚪ definition

def · source

def stmtToJson (s : Statement) : Json

policyToJson — ⚪ definition

def · source

def policyToJson (p : Policy) : Json

IamExplainer.Grants

CondState.toString — ⚪ definition

def · source

def CondState.toString : CondState → String
  | .t => "T"
  | .f => "F"
  | .u => "U"
  | .none_ => "NONE"

— ⚪ definition

instance · source

instance : ToString CondState

Grant — ⚪ definition

structure · source

structure Grant where

stmtGrants — ⚪ definition

def · source

def stmtGrants (ctx : Context) (condCtx : CondContext) (s : Statement) : List Grant

grants — ⚪ definition

def · source

def grants (ctx : Context) (condCtx : CondContext) (p : Policy) : List Grant

grantToJson — ⚪ definition

def · source

def grantToJson (g : Grant) : Json

IamExplainer.Layers

Layers — ⚪ definition

structure · source

structure Layers where

LayerVerdict — ⚪ definition

structure · source

structure LayerVerdict where

LayerResult — ⚪ definition

structure · source

structure LayerResult where

evalLayers — ⚪ definition

def · source

def evalLayers (req : Request) (ctx : CondContext) (layers : Layers)
    (rcpServices : List String) (kind : DocKind) : LayerResult

noLayers — ⚪ definition

def · source

def noLayers : Layers

validateScp — ⚪ definition

def · source

def validateScp (p : Policy) : Option String

validateRcp — ⚪ definition

def · source

def validateRcp (p : Policy) : Option String

evalLayers_noLayers_blocked — 🟢 proved

theorem · source

theorem evalLayers_noLayers_blocked (req : Request) (ctx : CondContext)
    (rcpSvcs : List String) (kind : DocKind) :
    (evalLayers req ctx noLayers rcpSvcs kind).blocked = []

evalLayers_blocked_noContext_empty — 🟢 proved

theorem · source

theorem evalLayers_blocked_noContext_empty (req : Request) (ctx : CondContext)
    (layers : Layers) (rcpSvcs : List String) (kind : DocKind)
    (h : (evalLayers req ctx layers rcpSvcs kind).blocked = []) :
    (evalLayers req noContext layers rcpSvcs kind).blocked = []

IamExplainer.Match

matchResourcePattern — ⚪ definition

def · source

def matchResourcePattern (pattern : String) (resource : String) : Bool

IamExplainer.Policy

— ⚪ definition

instance · source

instance : ToJson Effect where

— ⚪ definition

instance · source

instance : FromJson Effect where

Statement — ⚪ definition

structure · source

structure Statement where

ParseWarning — ⚪ definition

structure · source

structure ParseWarning where

— ⚪ definition

instance · source

instance : ToJson ParseWarning where

parseStatement — ⚪ definition

def · source

def parseStatement (j : Json) (idx : Nat) : Except String (Statement × List ParseWarning)

Policy — ⚪ definition

structure · source

structure Policy where

parsePolicy — ⚪ definition

def · source

def parsePolicy (input : String) : Except String (Policy × List ParseWarning)

IamExplainer.Principal

PrincipalType.toString — ⚪ definition

def · source

def PrincipalType.toString : PrincipalType → String
  | .aws => "AWS"
  | .federated => "Federated"
  | .service => "Service"
  | .canonicalUser => "CanonicalUser"
  | .wildcard => "Wildcard"

— ⚪ definition

instance · source

instance : ToString PrincipalType

Principal — ⚪ definition

structure · source

structure Principal where

isBareAccountId — ⚪ definition

def · source

def isBareAccountId (s : String) : Bool

normPrincipal — ⚪ definition

def · source

def normPrincipal (s : String) : Principal

parsePrincipals — ⚪ definition

def · source

def parsePrincipals (j : Json) : List Principal

Principal.isRoot — ⚪ definition

def · source

def Principal.isRoot (p : Principal) : Bool

Principal.accountId — ⚪ definition

def · source

def Principal.accountId (p : Principal) : Option String

Scope.toString — ⚪ definition

def · source

def Scope.toString : Scope → String
  | .sameAccount => "SAME_ACCOUNT"
  | .inOrg       => "IN_ORG"
  | .crossOrg    => "CROSS_ORG"
  | .pub         => "PUBLIC"
  | .federated   => "FEDERATED"
  | .service     => "SERVICE"
  | .unverified  => "UNVERIFIED"

— ⚪ definition

instance · source

instance : ToString Scope

Context — ⚪ definition

structure · source

structure Context where

condOrgIds — ⚪ definition

def · source

def condOrgIds (cond : Option Json) : List String

scopeOf — ⚪ definition

def · source

def scopeOf (ctx : Context) (p : Principal) (cond : Option Json) : Scope

DocKind.toString — ⚪ definition

def · source

def DocKind.toString : DocKind → String
  | .identity => "IDENTITY"
  | .trust    => "TRUST"
  | .resource => "RESOURCE"
  | .mixed    => "MIXED"

— ⚪ definition

instance · source

instance : ToString DocKind

detectKind — ⚪ definition

def · source

def detectKind (stmts : List Statement) : DocKind

IamExplainer.Proofs

Policy.removeStmt — ⚪ definition

def · source

Soundness theorems: policy transforms (T1-T3) and emitFixed can only narrow access, never grant new permissions. All theorems are universally quantified over the condition context.

def Policy.removeStmt (p : Policy) (i : Nat) : Policy

iamSem — ⚪ definition

def · source

def iamSem : PolicySem Statement Request CondContext where

removeAllow_narrows — 🟢 proved

theorem · source

theorem removeAllow_narrows (p : Policy) (i : Nat)
    (hi : i < p.statements.length)
    (heff : (p.statements[i]'hi).effect = .allow)
    (req : Request) (ctx : CondContext)
    (h : allows (p.removeStmt i) req ctx = true) :

matchPattern_ci_congr — 🟢 proved

theorem · source

theorem matchPattern_ci_congr (p s s' : String)
    (h : matchActionPattern p s = true) (heq : ciEq s s' = true) :
    matchActionPattern p s' = true

stmtGrantsAction_ci_congr — 🟢 proved

theorem · source

theorem stmtGrantsAction_ci_congr (st : Statement) (ℓ a : String)
    (h : stmtGrantsAction st ℓ = true) (heq : ciEq ℓ a = true) :
    stmtGrantsAction st a = true

stmtGrantsAction_narrow — 🟢 proved

theorem · source

theorem stmtGrantsAction_narrow (s new_stmt : Statement)
    (hnew_notactions : new_stmt.notActions = none)
    (hnew_actions : ∃ acts, new_stmt.actions = some acts ∧

allows_replaceAllow_mono — 🟢 proved

theorem · source

theorem allows_replaceAllow_mono (p : Policy) (i : Nat) (hi : i < p.statements.length)
    (heff : (p.statements[i]).effect = .allow)
    (new_stmt : Statement) (hnew_eff : new_stmt.effect = .allow)
    (hnew_res : new_stmt.resources = (p.statements[i]).resources)
    (hnew_notres : new_stmt.notResources = (p.statements[i]).notResources)
    (hnew_cond : new_stmt.condition = (p.statements[i]).condition)
    (hgrants : ∀ a, stmtGrantsAction new_stmt a = true → stmtGrantsAction (p.statements[i]) a = true)
    (req : Request) (ctx : CondContext)
    (h : allows { p with statements

narrowActions_narrows — 🟢 proved

theorem · source

theorem narrowActions_narrows
    (p : Policy) (i : Nat)
    (hi : i < p.statements.length)
    (heff : (p.statements[i]).effect = .allow)
    (new_stmt : Statement)
    (hnew : new_stmt.effect = .allow)
    (hnew_notactions : new_stmt.notActions = none)
    (hnew_actions : ∃ acts, new_stmt.actions = some acts ∧

allows_replace_stmt_mono — 🟢 proved

theorem · source

Generalized statement replacement mono

theorem allows_replace_stmt_mono (p : Policy) (i : Nat) (hi : i < p.statements.length)
    (heff : (p.statements[i]).effect = .allow)
    (new_stmt : Statement) (hnew_eff : new_stmt.effect = .allow)
    (hnew_cond : new_stmt.condition = (p.statements[i]).condition)
    (hmono : ∀ req, stmtMatches new_stmt req = true → stmtMatches (p.statements[i]) req = true)
    (req : Request) (ctx : CondContext)
    (h : allows { p with statements

narrowResources_narrows — 🟢 proved

theorem · source

NEW: narrowResources_narrows (T3)

theorem narrowResources_narrows
    (p : Policy) (i : Nat)
    (hi : i < p.statements.length)
    (heff : (p.statements[i]).effect = .allow)
    (new_stmt : Statement) (hnew_eff : new_stmt.effect = .allow)
    (hnew_act : new_stmt.actions = (p.statements[i]).actions)
    (hnew_notact : new_stmt.notActions = (p.statements[i]).notActions)
    (hnew_cond : new_stmt.condition = (p.statements[i]).condition)
    (hnew_notres : new_stmt.notResources = none)
    (hnew_res : ∃ rlist, new_stmt.resources = some rlist ∧

emitFixed_narrows — 🟢 proved

theorem · source

theorem emitFixed_narrows (p : Policy) (ns : Needs)
    (hns : ∀ n ∈ ns.needs, '?' ∉ n.action.toList ∧ '*' ∉ n.action.toList)
    (req : Request) (ctx : CondContext)
    (h : allows (emitFixed p ns).1 req ctx = true) :
    allows p req ctx = true

grants_complete — 🟢 proved

theorem · source

Grants completeness and no-context conservatism

theorem grants_complete (p : Policy) (req : Request) (ctx : CondContext)
    (h : allows p req ctx = true) :

allows_nocontext_conservative — 🟢 proved

theorem · source

theorem allows_nocontext_conservative (p : Policy) (req : Request) (ctx : CondContext)
    (h : allows p req ctx = true) :

layers_narrow — 🟢 proved

theorem · source

Layer theorems: layered evaluation only narrows access.

theorem layers_narrow (p : Policy) (req : Request) (ctx : CondContext)
    (layers : Layers) (rcpSvcs : List String) (kind : DocKind)
    (h : (allowsLayered p req ctx layers rcpSvcs kind).allowed = true) :
    allows p req ctx = true

layer_add_monotone — 🟢 proved

theorem · source

theorem layer_add_monotone (p : Policy) (req : Request) (ctx : CondContext)
    (rcpSvcs : List String) (kind : DocKind)
    (h : allows p req ctx = true) :
    (allowsLayered p req ctx noLayers rcpSvcs kind).allowed = true

layered_nocontext_conservative — 🟢 proved

theorem · source

theorem layered_nocontext_conservative (p : Policy) (req : Request) (ctx : CondContext)
    (layers : Layers) (rcpSvcs : List String) (kind : DocKind)
    (h : (allowsLayered p req ctx layers rcpSvcs kind).allowed = true) :
    (allowsLayered p req noContext layers rcpSvcs kind).allowed = true

IamExplainer.Report

Counts — ⚪ definition

structure · source

structure Counts where

countFindings — ⚪ definition

def · source

def countFindings (fs : List Finding) : Counts

Report — ⚪ definition

structure · source

structure Report where

buildReport — ⚪ definition

def · source

def buildReport (findings : List Finding) (warnings : List ParseWarning) : Report

reportToJson — ⚪ definition

def · source

def reportToJson (r : Report) : Json

renderText — ⚪ definition

def · source

def renderText (r : Report) : String

IamExplainer.XAChecks

condHasKey — ⚪ definition

def · source

def condHasKey (cond : Option Json) (key : String) : Bool

checkXA — ⚪ definition

def · source

def checkXA (ctx : Context) (kind : DocKind) (s : Statement) : List Finding

xaWarnings — ⚪ definition

def · source

def xaWarnings (ctx : Context) (s : Statement) : List ParseWarning

Main

CliOpts — ⚪ definition

structure · source

structure CliOpts where

parseOpts — ⚪ definition

def · source

def parseOpts (args : List String) : CliOpts

loadAccounts — ⚪ definition

def · source

def loadAccounts (path : String) : IO (List String)

buildContext — ⚪ definition

def · source

def buildContext (opts : CliOpts) : IO Context

runExplain — ⚪ definition

def · source

def runExplain (opts : CliOpts) : IO UInt32

loadCondContext — ⚪ definition

def · source

def loadCondContext (opts : CliOpts) : IO CondContext

runGrants — ⚪ definition

def · source

def runGrants (opts : CliOpts) : IO UInt32

loadLayerDoc — ⚪ definition

def · source

def loadLayerDoc (path : String) : IO (Policy × List ParseWarning)

rcpServicesPath — ⚪ definition

def · source

def rcpServicesPath : String

loadRcpServices — ⚪ definition

def · source

def loadRcpServices : IO (List String)

runCan — ⚪ definition

def · source

def runCan (opts : CliOpts) : IO UInt32

runEmitFixed — ⚪ definition

def · source

def runEmitFixed (opts : CliOpts) : IO UInt32

main — ⚪ definition

def · source

def main (args : List String) : IO UInt32