diff --git a/formal/Ceremony.lean b/formal/Ceremony.lean index eddbe8a..770cddb 100644 --- a/formal/Ceremony.lean +++ b/formal/Ceremony.lean @@ -1,2 +1,3 @@ import Ceremony.P0.Authority +import Ceremony.P0.Boundary import Ceremony.P1.SignedObject diff --git a/formal/Ceremony/P0/Boundary.lean b/formal/Ceremony/P0/Boundary.lean new file mode 100644 index 0000000..0493bd9 --- /dev/null +++ b/formal/Ceremony/P0/Boundary.lean @@ -0,0 +1,192 @@ +/- + Ceremony Suite — Enforcement boundary & the two-stream composition (P0) + + Mechanizes the "OCAP two-stream sequencing" decision + (knowledge/board/2026-07-16_ocap-two-streams-sequencing-DECIDED.md) AGAINST + the frozen algebra of `Authority.lean`. It exists to answer one question with + a proof rather than prose: + + Does deciding "brush-first / ceremony-in-parallel, L3-gated brush default, + fall back to safe-subset when no fence" VIOLATE the ratified v0.3.1 spec? + + The load-bearing sub-decision under test (verbatim from the board note): + + "Brush is the confined default WHERE an L3 fence is actively enforcing; + fall back to safe-subset's structural refusal when L3 is unavailable." + + RESULT (what the theorems below establish): + • The L3-gate is NOT a new law and NOT a fourth Authority axis. It is the + existing `Effect` meet, driven by an *enforceable ceiling* the active + fence supplies (ADR 0002 I9/I10 "never overclaim"; only L3 sees inside a + spawned binary). `boundaryVerdict = attenuate desired (fence ceiling)`. + • The safe-subset fallback is FORCED, not a bolt-on policy: it is exactly + what the honest (non-overclaiming) brush verdict reduces to under + `advisory` (`fallback_is_forced`). + • Stream A (brush enforces `Caveats`) and Stream B (ceremony proves + `Authority`) COMPOSE: projection to the enforced carrier is a meet- + homomorphism (`proj_effect_meet`) — the ADR 0020 D7 "siblings, not two + competing models" claim, mechanized. So enforcement can never grant above + what the authority algebra permits; layered-parallel converges. + + It imports only `Ceremony.P0.Authority` and introduces no new operation over + it. That IS the confirmation: the sequencing is *inside* the frozen system. + + The temporal half — a fence that DROPS between grant and exec must not fail + open (spec I4, "checked at the moment it executes") — is modeled separately + in `formal/tla/EnforcementGate.tla`. +-/ +import Ceremony.P0.Authority +namespace Ceremony.P0 + +/-! ### The enforcement fence — ADR 0002 I9/I10 `sandbox_kind`, NOT a new axis + +`Fence` is *enforcement strength* (is a kernel L3 fence active right now?), a +distinct concept from the `Assurance` axis (how strongly the human is present). +It is deliberately NOT lifted into `Authority` as a fourth coordinate: it does +not decide *what/how-present/how-long*; it bounds only *what the boundary can +faithfully enforce*, which lands on `Effect` via the meet below. -/ +inductive Fence + | advisory -- NoopSandbox: L1/L2 cannot see inside a spawned binary (I10) + | kernel -- Landlock / seatbelt / AppContainer actively confining +deriving DecidableEq, Repr + +/-- A shell request, abstracted to the one bit the decision turns on: does it + use dynamic constructs (`$(…)`, pipes, `eval`) whose containment only a + kernel fence can provide? `dynamic = false` is structurally safe. -/ +structure Request where + dynamic : Bool +deriving DecidableEq, Repr + +/-! ### The two engines -/ + +/-- safe-subset engine: STRUCTURAL refusal of dynamic constructs — least + authority by construction, fence-independent (it never runs `$(…)`). -/ +def safeSubset (q : Request) : Effect := + if q.dynamic then .deny else .allow + +/-- brush engine, stated as its *honest* verdict (ADR 0002 I9: never report an + advisory run as confined). Under `kernel` the op is confined ⇒ honest + `allow`. Under `advisory` a dynamic op cannot be confined, so running it and + calling it confined would OVERCLAIM ⇒ the honest verdict is `deny` + (fail-closed, I5/L3); a static op is structurally safe regardless. -/ +def brushHonest (f : Fence) (q : Request) : Effect := + match f, q.dynamic with + | .kernel, _ => .allow + | .advisory, true => .deny + | .advisory, false => .allow + +/-- The DECIDED rule: brush is the default WHERE a kernel fence enforces; else + fall back to safe-subset's structural refusal. -/ +def boundaryVerdict (f : Fence) (q : Request) : Effect := + match f with + | .kernel => brushHonest .kernel q + | .advisory => safeSubset q + +/-! ### The board decision is exactly the honest brush verdict -/ + +/-- **The safe-subset fallback is FORCED, not bolted on.** Under `advisory`, the + honest brush verdict *is* safe-subset's — so "fall back to safe-subset when + L3 is unavailable" is derived from the no-overclaim rule (I9), not an + independent policy knob. -/ +theorem fallback_is_forced (q : Request) : + brushHonest .advisory q = safeSubset q := by + rcases q with ⟨d⟩; cases d <;> rfl + +/-- The DECIDED rule and the honest brush verdict are the same function; the + "default + fallback" phrasing is one thing, not two. -/ +theorem boundaryVerdict_eq_honest (f : Fence) (q : Request) : + boundaryVerdict f q = brushHonest f q := by + cases f + · exact (fallback_is_forced q).symm -- advisory: safeSubset = brushHonest advisory + · rfl -- kernel: definitional + +/-! ### It is an attenuation in the FROZEN algebra — no new operation + +The user's desired effect is `allow` (they want to run the command). `allow` is +the top of `Effect`, so meeting the desired effect with the fence's enforceable +ceiling recovers exactly the verdict: the decision is `Effect.meet`, nothing +new. -/ + +/-- the enforceable-effect ceiling the fence supplies for this request. -/ +def enforceableCeiling (f : Fence) (q : Request) : Effect := boundaryVerdict f q + +theorem allow_is_effect_top (e : Effect) : Effect.meet .allow e = e := by + cases e <;> rfl + +/-- **The boundary decision is a meet.** It attenuates the desired `allow` by + the fence's enforceable ceiling — the frozen `Effect.meet`, no bespoke op. -/ +theorem boundaryVerdict_is_attenuation (f : Fence) (q : Request) : + boundaryVerdict f q = Effect.meet .allow (enforceableCeiling f q) := by + simp only [enforceableCeiling, allow_is_effect_top] + +/-! ### Lifted to `Authority`: the fence bounds ONLY `Effect` + +The boundary ceiling is `⊤` on Assurance and Scope (the fence says nothing about +human presence or duration) and the enforceable effect on `Effect`. Minting a +grant is `attenuate request boundaryCeiling` — the frozen product meet. -/ + +/-- the fence ceiling as an `Authority`: enforceable on `Effect`, `⊤` elsewhere. -/ +def boundaryCeiling (f : Fence) (q : Request) : Authority := + ⟨boundaryVerdict f q, .hardware, .durable⟩ + +/-- what the gate actually mints: the request attenuated by the fence ceiling. -/ +def mintedGrant (req : Authority) (f : Fence) (q : Request) : Authority := + attenuate req (boundaryCeiling f q) + +/-- **Never more than requested** — a direct corollary of `meet_le_left`. -/ +theorem minted_le_request (req : Authority) (f : Fence) (q : Request) : + mintedGrant req f q ≤ᴬ req := + meet_le_left req (boundaryCeiling f q) + +/-- **Never above what the fence can enforce (I9, in the product).** The minted + authority is ⊑ the boundary ceiling on every axis — a corollary of + `meet_le_right`. An advisory boundary therefore cannot mint an + effect its fence would only *advise*. -/ +theorem minted_le_enforceable (req : Authority) (f : Fence) (q : Request) : + mintedGrant req f q ≤ᴬ boundaryCeiling f q := + meet_le_right req (boundaryCeiling f q) + +/-- **Fail-closed on the unenforceable case (L3/I5).** A containment-needing + request under no kernel fence mints `deny` on the effect axis — the exact + structural refusal safe-subset gives, reached here through the meet, for + ANY request ceiling. This is the honesty guarantee the L3-gate rests on. -/ +theorem advisory_dynamic_grant_is_deny (req : Authority) (q : Request) + (h : q.dynamic = true) : + (mintedGrant req .advisory q).effect = Effect.deny := by + rcases req with ⟨e, a, s⟩ + simp only [mintedGrant, attenuate, boundaryCeiling, boundaryVerdict, safeSubset, + h, Authority.meet, Effect.meet] + cases e <;> rfl + +/-! ### The two streams compose — projection is a meet-homomorphism (ADR 0020 D7) + +Stream A enforces the effect carrier (`Caveats`, ADR 0002 — bridle *depends on* +it and MUST NOT reinvent it, I3). Stream B proves `Authority`. The projection +`Authority.effect` carries the product meet to the axis meet definitionally, so +whenever ceremony attenuates authority, the effect brush enforces attenuates in +lockstep. Layered-parallel converges: enforcement is the ⊓-image of the proof, +never a divergent second model. -/ + +/-- **The convergence theorem.** Projection to the enforced carrier commutes + with the meet: `(a ⊓ b).effect = a.effect ⊓ b.effect`. Stream B's + attenuation, projected onto what Stream A enforces, *is* Stream A's + attenuation. -/ +theorem proj_effect_meet (a b : Authority) : + (a ⊓ b).effect = Effect.meet a.effect b.effect := rfl + +/-- Same homomorphism on the other two axes — the product really is + coordinatewise, so no axis can smuggle in amplification. -/ +theorem proj_assurance_meet (a b : Authority) : + (a ⊓ b).assurance = Assurance.meet a.assurance b.assurance := rfl +theorem proj_scope_meet (a b : Authority) : + (a ⊓ b).scope = Scope.meet a.scope b.scope := rfl + +/-! ### Summary the gate can quote + +`boundaryVerdict = attenuate allow (fence ceiling)` (frozen meet), the fallback +is forced by I9, minting never exceeds request or enforceable ceiling, dynamic- +under-advisory fails closed, and enforcement is the meet-homomorphic image of +the proven authority. No new law; no fourth axis. The sequencing lives INSIDE +the v0.3.1 freeze. -/ + +end Ceremony.P0 diff --git a/formal/README.md b/formal/README.md index 36177ca..f3fbe26 100644 --- a/formal/README.md +++ b/formal/README.md @@ -17,10 +17,12 @@ it builds in seconds. | Path | Covers | Origin | |---|---|---| | `Ceremony/P0/Authority.lean` | **P0 authority algebra** — the product meet-lattice `Effect × Assurance × Scope`, attenuation (L4), no-fail-open (OB-9/OB-12), order-independence (L1). 25 theorems, 0 `sorry`. | P0 (this suite) | +| `Ceremony/P0/Boundary.lean` | **the OCAP two-stream sequencing, mechanized** — the L3-gated brush default proven to be an `Effect` attenuation in the frozen algebra (no new law/axis); safe-subset fallback *forced* by I9; enforcement = meet-homomorphic image of authority (streams converge). Confirms the [DECIDED board note](../../../knowledge/board/2026-07-16_ocap-two-streams-sequencing-DECIDED.md). | P0 (this suite) | | `Ceremony/P1/SignedObject.lean` | **P1 signed-object contracts** — profile/algorithm allowlist (`TrustedProfile`), canonical encoding injectivity, the universal `SignaturePreimage` binding profile/codec/domain/store/thread/body/cid/signer (OB-13), genesis. | PR #233 (GPT-5/Codex) | | `Gate.lean` + `formalGate` exe | the proof-escape gate: rejects `sorry` / omitted modules. | PR #233 | | `Tests/P1Counterexamples.lean`, `Tests/SignedObjectContracts.lean` | negative + contract tests (Lean-level conformance). | PR #233 | | `tla/CeremonyStore.tla` | **P2 store** — CAS append + anti-rollback state machine; invariants map to PO-2/2a/2c + OB-15/16. Check with TLC. | P2 (this suite) | +| `tla/EnforcementGate.tla` | **the L3-gate under a fence that DROPS over time** — temporal half of `Boundary.lean`. `NoAdvisoryDynamicExec` holds iff the fence is re-checked at exec (I4). TLC PASSES with `CheckAtExec=TRUE`, exhibits the TOCTOU trace with `FALSE` (two `.cfg`s next to it). | P0 (this suite) | ## Why this shape diff --git a/formal/tla/.gitignore b/formal/tla/.gitignore new file mode 100644 index 0000000..675bb7a --- /dev/null +++ b/formal/tla/.gitignore @@ -0,0 +1,5 @@ +# TLC model-checker run artifacts (scratch) +states/ +*_TTrace_*.tla +*_TTrace_*.bin +*.st diff --git a/formal/tla/EnforcementGate.tla b/formal/tla/EnforcementGate.tla new file mode 100644 index 0000000..e0d0704 --- /dev/null +++ b/formal/tla/EnforcementGate.tla @@ -0,0 +1,98 @@ +-------------------------- MODULE EnforcementGate -------------------------- +(* + Ceremony Suite — the L3-gate under a fence that CHANGES over time (P0). + Temporal companion to formal/Ceremony/P0/Boundary.lean, which proves the + *static* case (the L3-gated brush default is an attenuation in the frozen + algebra, no new law/axis). This module discharges the one genuinely-new + obligation the sequencing decision introduces: + + the "OCAP two-stream sequencing" board note makes brush the confined + default WHERE a kernel fence is active. But a fence can DROP between the + moment a dynamic op is authorized and the moment it executes (kernel + module unload, container reconfig, policy change). Spec I4 requires the + check "at the moment it executes" — NOT cached from grant time. + + The model makes that requirement falsifiable. `CheckAtExec` toggles the two + designs: + + CheckAtExec = TRUE -> re-check the CURRENT fence at exec (I4-faithful). + CheckAtExec = FALSE -> trust the fence observed at grant time (the bug). + + Invariant NoAdvisoryDynamicExec: no containment-needing op ever actually runs + while the fence is advisory (I9 "never overclaim" / I5 fail-closed, over + time). TLC result: + + CheckAtExec = TRUE -> []Inv holds (the sequencing is safe). + CheckAtExec = FALSE -> TLC exhibits the fence-drop TOCTOU counterexample + (authorize under kernel -> FenceDown -> Exec runs + advisory). This is the design the gate must NOT use. + + So: the L3-gated brush default is spec-faithful IFF enforcement re-checks the + fence at exec. That conditional IS the confirmation — and names the exact + thing Stream A must implement. +*) +EXTENDS Naturals + +CONSTANT CheckAtExec \* TRUE = I4-faithful (re-check at exec); FALSE = cache grant-time fence + +VARIABLES + fence, \* "advisory" | "kernel" : the CURRENT enforcement strength + grantFence, \* "none" | "advisory" | "kernel" : fence seen when the pending dynamic op was authorized + advisoryDynamicRan \* BOOLEAN : did a containment-needing op ever actually run under an advisory fence? + +vars == << fence, grantFence, advisoryDynamicRan >> + +Fences == { "advisory", "kernel" } + +TypeOK == + /\ fence \in Fences + /\ grantFence \in (Fences \cup { "none" }) + /\ advisoryDynamicRan \in BOOLEAN + +Init == + /\ fence \in Fences + /\ grantFence = "none" + /\ advisoryDynamicRan = FALSE + +\* The fence strength can change under our feet at any time. +FenceDown == fence = "kernel" /\ fence' = "advisory" /\ UNCHANGED << grantFence, advisoryDynamicRan >> +FenceUp == fence = "advisory" /\ fence' = "kernel" /\ UNCHANGED << grantFence, advisoryDynamicRan >> + +\* Authorize a containment-needing (dynamic) op. Per the L3-gate, a dynamic op +\* is authorized only where a kernel fence is currently active; we record the +\* fence observed at grant time. +AuthorizeDynamic == + /\ grantFence = "none" + /\ fence = "kernel" + /\ grantFence' = fence + /\ UNCHANGED << fence, advisoryDynamicRan >> + +\* Execute the pending dynamic op. The gate consults either the current fence +\* (I4-faithful) or the cached grant-time fence (the bug), per CheckAtExec. It +\* proceeds only if that fence reads "kernel". `advisoryDynamicRan` records what +\* ACTUALLY happened at the kernel — which depends on the CURRENT fence, not the +\* one the gate consulted. +ExecDynamic == + /\ grantFence # "none" + /\ LET checked == IF CheckAtExec THEN fence ELSE grantFence + IN checked = "kernel" \* the gate lets it through + /\ advisoryDynamicRan' = (advisoryDynamicRan \/ (fence = "advisory")) + /\ grantFence' = "none" + /\ UNCHANGED fence + +Next == FenceDown \/ FenceUp \/ AuthorizeDynamic \/ ExecDynamic + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------ +\* Invariant: a containment-needing op never actually runs advisory (I9/I5 over +\* time). Holds under CheckAtExec = TRUE; TLC finds a counterexample under FALSE. +NoAdvisoryDynamicExec == advisoryDynamicRan = FALSE + +Inv == TypeOK /\ NoAdvisoryDynamicExec + +\* Config: to see it PASS, run with CheckAtExec <- TRUE and check Inv. +\* To see the TOCTOU bug, run with CheckAtExec <- FALSE (Inv will fail with a +\* trace: AuthorizeDynamic; FenceDown; ExecDynamic). +THEOREM SafeWhenCheckedAtExec == (CheckAtExec = TRUE) => (Spec => []Inv) +============================================================================= diff --git a/formal/tla/EnforcementGate_cacheGrantFence.cfg b/formal/tla/EnforcementGate_cacheGrantFence.cfg new file mode 100644 index 0000000..cc3d76e --- /dev/null +++ b/formal/tla/EnforcementGate_cacheGrantFence.cfg @@ -0,0 +1,7 @@ +\* THE BUG: trust the fence observed at grant time. TLC MUST report a violation +\* of NoAdvisoryDynamicExec (trace: AuthorizeDynamic; FenceDown; ExecDynamic). +\* This is the design Stream A must NOT ship; it documents the obligation. +\* Run: java -cp tla2tools.jar tlc2.TLC -config EnforcementGate_cacheGrantFence.cfg EnforcementGate.tla +SPECIFICATION Spec +CONSTANT CheckAtExec = FALSE +INVARIANT Inv diff --git a/formal/tla/EnforcementGate_checkAtExec.cfg b/formal/tla/EnforcementGate_checkAtExec.cfg new file mode 100644 index 0000000..e1bd328 --- /dev/null +++ b/formal/tla/EnforcementGate_checkAtExec.cfg @@ -0,0 +1,5 @@ +\* I4-FAITHFUL: re-check the current fence at exec time. Inv MUST hold. +\* Run: java -cp tla2tools.jar tlc2.TLC -config EnforcementGate_checkAtExec.cfg EnforcementGate.tla +SPECIFICATION Spec +CONSTANT CheckAtExec = TRUE +INVARIANT Inv