diff --git a/docs/multi-tenant-relay.md b/docs/multi-tenant-relay.md index debfddd6c..4a936cb79 100644 --- a/docs/multi-tenant-relay.md +++ b/docs/multi-tenant-relay.md @@ -571,13 +571,47 @@ load-bearing *backstop*. stops a B-stamped token authorizing over an A-host stops a B-host AUTH registering into A. Its in-relay counterpart is I5's open-community branch (`AuthenticateOpenCommunity`, mutation M10). +- **S9 (Operator-plane provisioning confinement).** Runtime community + provisioning (`POST /operator/communities`) is the one admitted surface whose + *effect* spans tenants: it creates a community, binds its host, and + bootstraps or rotates that community's owner. Its authority is the + deployment-level `RELAY_OPERATOR_PUBKEYS` allowlist + (`crates/buzz-relay/src/api/operator.rs`), never a `relay_members` role — + deployment-root authority, documented as such on the endpoint. Three lemmas: + `provisioning_requires_operator_authorization` (every owner + bootstrap/rotation — the plane's only membership effect, emitted by both the + provision and the converge/rotate path — names an operator-registered key; + there is deliberately **no** compromise disjunct, because compromising an + operator's secret does not put a new key on the allowlist, so the claim + holds unconditionally); `provision_accepts_only_operator_signed_payload` + (the accepted `(host, owner)` pair is exactly a pair the named operator + signed — the NIP-98 payload hash over the JSON body is what forces this, so + a captured `Authorization` header can only *replay* the same pair, which is + the documented idempotent convergence, never *re-target* it); and + `rotation_confined_to_host_community` (an owner rotation lands only in the + community bound to the request's host — the request names a host, never a + community id, the same single-witness framing as S5/S6 via + `RotationResolved(owner, used_comm, host, host_comm)`). The payload-binding + lemma pins the PR #1657 review finding that `buzz-auth`'s NIP-98 + verification treats the `payload` tag as *optional* if absent: + `MUTATION_Provision_Unsigned_Body` models exactly that gap (operator signs + without the payload hash; relay accepts body fields from the wire unbound) + and falsifies the lemma, so requiring the payload tag on this endpoint is a + conformance obligation, not a nicety. `Create_Community` remains the + trusted startup-seed path (`ensure_configured_community` at boot); the S9 + theorems quantify over the provisioning action facts, so they constrain the + protocol path without pretending the config path is adversarial. Each Tamarin lemma is paired with an exists-trace sanity lemma (the honest protocol can run), the Tamarin analog of the mutation test. -**Verification status.** S1–S8 are **machine-verified green** on -Tamarin 1.12.0 / Maude 3.5.1 — the full selected run verifies all 32 lemmas in -~12s with zero `analyzed` failures. S1/S2: `token_confinement`, +**Verification status.** S1–S9 are **machine-verified green** on +Tamarin 1.12.0 / Maude 3.5.1 — the full selected run verifies all 38 lemmas in +~141s with zero `analyzed` failures. (The step counts and wall-clock figures +below are from earlier, smaller revisions of the model; each addition enlarges +the search space for the pre-existing lemmas — e.g. +`other_community_key_compromise_does_not_authorize` closes at 486 steps in the +current run versus 147 pre-S9 — but every lemma still closes.) S1/S2: `token_confinement`, `cross_community_use_attempts_are_not_authorized`, the two `minted_*_channels_match_stamp` lemmas, `token_stamp_matches_mint`, `cross_community_mint_yields_no_token_for_that_request`, and the @@ -620,6 +654,23 @@ S8 (open-community AUTH confinement): `open_auth_registration_confined_to_host_c (5 steps) proving a legitimate open-community registration is producible, so the confinement lemma is non-vacuous; its in-relay counterpart is the M10 open-AUTH stamp mutation, confirmed red in TLA+ (a 2-state `Inv_AdmissionFence` violation). +S9 (operator-plane provisioning): `provisioning_requires_operator_authorization` +(6 steps), `provision_accepts_only_operator_signed_payload` (7 steps), and +`rotation_confined_to_host_community` (2 steps — the S5/S6 single-witness +framing, so a counterexample is one rule instance), with three exists-trace +probes (`executable_provision`, 12 steps; `executable_rotate`, 10 steps; and +`executable_rotate_after_provision`, 12 steps — the create-then-converge +lifecycle end to end, proving a rotate on an already-bound host lands in the +community the original provision bound). All three S9 mutations are confirmed +red: `MUTATION_Provision_Unsigned_Body` (the payload tag omitted, so the signed +NIP-98 event binds URL/method/freshness but not the JSON body — the PR #1657 +review finding) falsifies `provision_accepts_only_operator_signed_payload` with +an 8-step trace; `MUTATION_Provision_Any_Client` (the `RELAY_OPERATOR_PUBKEYS` +gate replaced by "any valid signature") falsifies +`provisioning_requires_operator_authorization` with an 8-step trace; and +`MUTATION_Rotate_Ignore_Host` (the rotation applied to a community other than +the host's binding — the operator-plane confused deputy) falsifies +`rotation_confined_to_host_community` with a 12-step trace. The S5 confinement lemma was deliberately framed to keep its mutation *cheaply* refutable. An earlier framing joined two action facts @@ -700,6 +751,31 @@ Each axiom is *admitted* per deployment, not assumed universally: token under the deployment's routing/storage shape (and that the seen-set TTL covers the full ±60 s window). A failing test or an unmet gate rejects the deployment. +- **P-HOST-APPEND (operator plane)** — the host→community map is **append-only**: + a host, once bound, is never re-pointed to a different community. Admitted by + `ensure_configured_community`'s upsert + (`crates/buzz-db/src/lib.rs`): `INSERT ... ON CONFLICT (lower(host)) DO UPDATE + SET host = EXCLUDED.host RETURNING id` — a second request for an + already-bound host returns the *same* community id and only refreshes the + host's stored casing; there is no code path (startup seeding or + `POST /operator/communities`) that changes an existing binding's community. + This is the assumption that lets the TLA+ model keep `HostCommunity` a + *constant* function per checked segment (runtime provisioning appends a new + host↦community pair, which is a fresh constant assignment for subsequent + behavior — never a mutation of an existing one), so every TLC result over the + fixed `HostA/HostB/HostBad` harness remains valid across provisioning events + without remodeling `HostCommunity` as a variable. Tamarin imports the same + assumption as the `UniqueHostBinding` restriction and discharges the operator + plane's authorization obligations as S9 (three lemmas + three confirmed-red + mutations). Two further conformance obligations ride on this surface: the + NIP-98 `payload` tag MUST be required (not merely verified-if-present) on + `POST /operator/communities`, since `MUTATION_Provision_Unsigned_Body` shows + an optional payload tag lets a captured `Authorization` header be raced with + a swapped JSON body on the one endpoint that mints tenancy; and + `RELAY_OPERATOR_PUBKEYS` must be checked against the *signer* of the NIP-98 + event, never inferred from the body or connection. A migration lint asserting + no `UPDATE communities SET host` path (mirroring P-RESOLVE's + channel-immutability lint) admits the append-only axiom structurally. ## Prior Art @@ -831,14 +907,16 @@ as label-flow non-interference is, to our knowledge, new for a Nostr relay. actors, and ids explodes the space; symmetry + bounded observations keep the core isolation surface exhaustively checkable. - **`docs/spec/MultiTenantAuth.spthy`** — the Tamarin authorization model. Run: - `tamarin-prover --prove docs/spec/MultiTenantAuth.spthy`. All 32 lemmas (S1–S8) - verify green (Tamarin 1.12.0 / Maude 3.5.1, ~12 s) — each safety lemma paired with + `tamarin-prover --prove docs/spec/MultiTenantAuth.spthy`. All 38 lemmas (S1–S9) + verify green (Tamarin 1.12.0 / Maude 3.5.1, ~141 s) — each safety lemma paired with a verified exists-trace sanity lemma, and the documented mutations (`MUTATION_Use_Token_Claimed_Community` for S1, the S3 bad-accept and S4 splice-as-append mutations, `MUTATION_Use_Token_ChannelLess_Ignore_Host` for S5's host fence, `MUTATION_Use_Token_Ignore_Host` for S6's channel-bearing - host/channel-agreement fence, and `MUTATION_Admit_Ignore_Community` for S7's - NIP-43 admission confinement) confirmed red. The 32 lemmas include the + host/channel-agreement fence, `MUTATION_Admit_Ignore_Community` for S7's + NIP-43 admission confinement, and the three S9 operator-plane mutations — + `MUTATION_Provision_Unsigned_Body`, `MUTATION_Provision_Any_Client`, + `MUTATION_Rotate_Ignore_Host`) confirmed red. The 38 lemmas include the open-community AUTH pair added with the host-scoped-open-auth surfaces: `open_auth_registration_confined_to_host_community` (2 steps) proves an open-community auto-registration commits to the host-resolved community and never @@ -849,12 +927,13 @@ as label-flow non-interference is, to our knowledge, new for a Nostr relay. full lemma list, the S5/S6 single-witness framing, and the corrected `other_community_key_compromise_does_not_authorize` vacuity fix. - **Machine-check hygiene.** S1–S8 lemmas close by two distinct shapes. + **Machine-check hygiene.** S1–S9 lemmas close by two distinct shapes. **Rule-shape closure** means the lemma's conclusion follows by unification on a single rule's action multiset: `token_confinement`, `audit_append_advances_same_community_head`, `channelless_use_confined_to_host_community` (the S5 single-witness fact), - `channelbearing_use_agrees_with_host` (the S6 single-witness fact), and + `channelbearing_use_agrees_with_host` (the S6 single-witness fact), + `rotation_confined_to_host_community` (the S9 single-witness fact), and the S2 supporting set (`minted_token_channels_match_stamp`, `minted_request_channels_match_stamp`, `token_stamp_matches_mint`). These are well-formedness guards on the model's @@ -869,9 +948,13 @@ as label-flow non-interference is, to our knowledge, new for a Nostr relay. **Substantive closure** requires cross-rule reasoning over persistent-fact invariance (`cross_community_mint_yields_no_token_for_that_request`, `leaked_token_blast_radius_contained`, - `cross_community_use_attempts_are_not_authorized`), linear-fact lifecycle + `cross_community_use_attempts_are_not_authorized`, + `provisioning_requires_operator_authorization`), linear-fact lifecycle (`cross_community_audit_splice_attempt_is_not_append`), or signed-preimage - unification (`system_event_acceptance_requires_same_community_key_or_compromise`). + unification (`system_event_acceptance_requires_same_community_key_or_compromise`, + `provision_accepts_only_operator_signed_payload` — the S9 payload-binding + claim, which needs both the operator's signature over the payload hash and + the allowlist premise). Tamarin proves both kinds identically; the distinction is for reviewer hygiene, not a weakened theorem claim. This paragraph is prose-only to preserve the `.spthy` byte hash above. @@ -999,7 +1082,7 @@ The model's obligations map to concrete code seams: red — so admit-into-A-then-act-in-B is a *caught* escape, not an invisible one. On the authorization side, NIP-43 member-list events are signed and accepted per-community in Tamarin (`Community_Signs_NIP43_MemberList` / - `Relay_Accepts_NIP43_MemberList`, `MultiTenantAuth.spthy:403`/`:413`), and + `Relay_Accepts_NIP43_MemberList`, `MultiTenantAuth.spthy:427`/`:437`), and `nip43_admission_confined_to_signing_community` proves B's signing key can never admit a pubkey into A (Theorem S7). diff --git a/docs/spec/MultiTenantAuth.spthy b/docs/spec/MultiTenantAuth.spthy index 02a0a94a9..c8c763ba8 100644 --- a/docs/spec/MultiTenantAuth.spthy +++ b/docs/spec/MultiTenantAuth.spthy @@ -472,6 +472,264 @@ rule Relay_Accepts_NIP43_MemberList: // Expected mutation result: `nip43_admission_confined_to_signing_community` // goes red. +// ============================================================================ +// S9: Deployment-operator community provisioning (POST /operator/communities) +// ============================================================================ +// +// PR #1657 adds a deployment-operator HTTP plane that can create a community +// (and its host mapping) at runtime and bootstrap/rotate that community's +// owner. This is intentionally the ONLY admitted surface whose effect spans +// tenants: its authority is the deployment-level RELAY_OPERATOR_PUBKEYS +// allowlist (`!OperatorKey`), never a `relay_members` role. `Create_Community` +// above remains the CONFIG/STARTUP seeding path (ensure_configured_community +// at boot — trusted by deployment, not by protocol); this section models the +// runtime protocol path, so its theorems quantify over the provisioning +// action facts, not over `CommunityCreated`. +// +// Wire shape: one NIP-98-signed POST whose signed preimage includes the +// payload hash over the JSON body (host, owner). The payload binding is +// load-bearing — see MUTATION_Provision_Unsigned_Body below, which models the +// real "NIP-98 payload tag optional" gap (kalvin's review finding #1 on +// PR #1657) and falsifies the S9 lemmas. +// +// Create-vs-rotate is decided by DB state, exactly like the endpoint: the +// SAME signed request provisions when the host is unbound and converges +// (owner bootstrap/rotation) when it is already bound. A replayed create can +// therefore only re-assert the SAME (host, owner) it signed — benign +// convergence, the documented idempotency — because the payload binds both. + +rule Register_Operator: + [ Fr(~sk_op) ] + --[ + OperatorRegistered(pk(~sk_op)) + ]-> + [ + !OperatorKey(pk(~sk_op)), + !OperatorSecret(pk(~sk_op), ~sk_op), + Out(pk(~sk_op)) + ] + +rule Compromise_Operator_Key: + [ !OperatorSecret(op, sk) ] + --[ + OperatorKeyCompromised(op) + ]-> + [ Out(sk) ] + +// The operator signs a provision request for a fresh host. The signed +// preimage commits to the payload hash h() alongside URL, +// method, and freshness — the NIP-98 payload-tag discipline made mandatory. +// `OperatorAuthorizedProvision` is the single authorization witness both +// relay rules (provision + rotate) are checked against: it names the exact +// (host, owner) the operator signed. +rule Operator_Sends_Provision_Request: + [ !OperatorSecret(op, sk), !ClientPublic(owner), Fr(~host), Fr(~url), Fr(~time) ] + --[ + OperatorAuthorizedProvision(op, ~host, owner), + ProvisionRequested(op, ~host, owner) + ]-> + [ + Out( + < 'operator_provision', + op, + ~url, + 'POST', + ~time, + ~host, + owner, + sign(< 'kind27235_operator', op, ~url, 'POST', ~time, h(< ~host, owner >) >, sk) + > + ), + Out(~host) + ] + +// The operator signs the same request shape for an ALREADY-BOUND host: the +// endpoint converges (bootstrap_owner re-runs), which rotates the community +// owner. Deployment-root authority, documented as such on the endpoint. +rule Operator_Sends_Rotate_Request: + [ !OperatorSecret(op, sk), !HostCommunity(host, comm), !ClientPublic(owner), + Fr(~url), Fr(~time) ] + --[ + OperatorAuthorizedProvision(op, host, owner), + RotateRequested(op, host, owner) + ]-> + [ + Out( + < 'operator_provision', + op, + ~url, + 'POST', + ~time, + host, + owner, + sign(< 'kind27235_operator', op, ~url, 'POST', ~time, h(< host, owner >) >, sk) + > + ) + ] + +// Provision path: the host has no existing binding, so the upsert inserts a +// fresh community, binds the host, and bootstraps the owner. The signature is +// verified against the payload hash recomputed over the RECEIVED body — an +// adversary who swaps host/owner in transit fails verification (P-SIG). +// The relay checks the sender against `!OperatorKey` — the model's +// RELAY_OPERATOR_PUBKEYS allowlist. A registered client key is NOT sufficient +// (see MUTATION_Provision_Any_Client). +rule Relay_Provisions_Community: + [ In(< 'operator_provision', op, url, 'POST', time, host, owner, sig >), + !OperatorKey(op), + Fr(~comm), Fr(~sk_comm) ] + --[ + Eq(verify(sig, < 'kind27235_operator', op, url, 'POST', time, h(< host, owner >) >, op), true), + CommunityProvisioned(~comm, host, op), + ProvisionAccepted(op, host, owner), + OwnerBootstrapped(owner, ~comm, host, op), + HostBound(host, ~comm) + ]-> + [ + !Community(~comm), + !CommunitySigningKey(~comm, ~sk_comm), + !HostCommunity(host, ~comm), + AuditHead(~comm, 'genesis'), + !Admitted(owner, ~comm) + ] + +// Converge/rotate path: the host is already bound, so the upsert is a no-op +// on the community row and bootstrap_owner (re)runs for that SAME community. +// The effect is confined to the host's bound community — the request names a +// host, never a community id (see MUTATION_Rotate_Ignore_Host). +rule Relay_Rotates_Owner: + [ In(< 'operator_provision', op, url, 'POST', time, host, owner, sig >), + !OperatorKey(op), + !HostCommunity(host, comm) ] + --[ + Eq(verify(sig, < 'kind27235_operator', op, url, 'POST', time, h(< host, owner >) >, op), true), + OwnerRotated(owner, comm, host, op), + OwnerBootstrapped(owner, comm, host, op), + RotationResolved(owner, comm, host, comm) + ]-> + [ !Admitted(owner, comm) ] + +// Idempotency / append-only host map, imported as a restriction: a host is +// bound to at most one community, ever. Grounded in the implementation: +// `ensure_configured_community` upserts `ON CONFLICT (lower(host)) DO UPDATE +// SET host = EXCLUDED.host RETURNING id` — a second request for the same host +// returns the SAME community id and never re-points the host. This is the +// same append-only assumption the TLA+ model's header states for keeping +// `HostCommunity` a constant-per-segment function; here it excludes traces +// where a replayed provision would mint a second community for a bound host +// (the real relay converges instead — the rotate rule above is that path). +restriction UniqueHostBinding: + "All host c1 c2 #i #j. + HostBound(host, c1) @ i & HostBound(host, c2) @ j ==> #i = #j" + +// MUTATION_Provision_Unsigned_Body (DO NOT ENABLE in the real model): the +// real-world gap this pins is kalvin's finding #1 on PR #1657 — NIP-98 +// verification treats the payload tag as OPTIONAL, so an operator client that +// omits it produces a signature binding only URL/method/freshness, and anyone +// who captures the Authorization header can race it with a swapped JSON body. +// Modeled as the pair: the operator signs WITHOUT the payload hash, and the +// relay accepts the body fields from the wire unbound. +// +// rule MUTATION_Operator_Signs_Without_Payload: +// [ !OperatorSecret(op, sk), !ClientPublic(owner), Fr(~host), Fr(~url), Fr(~time) ] +// --[ +// OperatorAuthorizedProvision(op, ~host, owner), +// ProvisionRequested(op, ~host, owner) +// ]-> +// [ +// Out(< 'operator_provision_nopayload', op, ~url, 'POST', ~time, ~host, owner, +// sign(< 'kind27235_operator_nopayload', op, ~url, 'POST', ~time >, sk) >), +// Out(~host) +// ] +// +// rule MUTATION_Relay_Provisions_Unbound_Body: +// [ In(< 'operator_provision_nopayload', op, url, 'POST', time, host, owner, sig >), +// !OperatorKey(op), +// Fr(~comm), Fr(~sk_comm) ] +// --[ +// Eq(verify(sig, < 'kind27235_operator_nopayload', op, url, 'POST', time >, op), true), +// CommunityProvisioned(~comm, host, op), +// ProvisionAccepted(op, host, owner), +// OwnerBootstrapped(owner, ~comm, host, op), +// HostBound(host, ~comm) +// ]-> +// [ +// !Community(~comm), !CommunitySigningKey(~comm, ~sk_comm), +// !HostCommunity(host, ~comm), AuditHead(~comm, 'genesis'), +// !Admitted(owner, ~comm) +// ] +// +// Expected mutation result: `provision_accepts_only_operator_signed_payload` +// goes red — the adversary intercepts the unsigned-body message, substitutes +// its own (host, owner), and the relay emits ProvisionAccepted for a pair the +// operator never authorized. Confirmed: falsified with an 8-step trace on +// Tamarin 1.12.0 / Maude 3.5.1 (see docs/multi-tenant-relay.md §Mechanized +// Verification). + +// MUTATION_Provision_Any_Client (DO NOT ENABLE in the real model): the relay +// authorizes provisioning from ANY registered client key instead of the +// operator allowlist — the RELAY_OPERATOR_PUBKEYS gate replaced by "any valid +// signature". Modeled by swapping the `!OperatorKey(op)` premise for +// `!ClientPublic(op)` in Relay_Provisions_Community (clients can sign the +// operator preimage with their own key; only the allowlist premise stops the +// relay accepting it). +// +// rule MUTATION_Client_Signs_Provision: +// [ !ClientSecret(op, sk), !ClientPublic(owner), Fr(~host), Fr(~url), Fr(~time) ] +// --[ ClientSignedProvision(op, ~host, owner) ]-> +// [ +// Out(< 'operator_provision', op, ~url, 'POST', ~time, ~host, owner, +// sign(< 'kind27235_operator', op, ~url, 'POST', ~time, h(< ~host, owner >) >, sk) >), +// Out(~host) +// ] +// +// rule MUTATION_Relay_Provisions_For_Any_Client: +// [ In(< 'operator_provision', op, url, 'POST', time, host, owner, sig >), +// !ClientPublic(op), +// Fr(~comm), Fr(~sk_comm) ] +// --[ +// Eq(verify(sig, < 'kind27235_operator', op, url, 'POST', time, h(< host, owner >) >, op), true), +// CommunityProvisioned(~comm, host, op), +// ProvisionAccepted(op, host, owner), +// OwnerBootstrapped(owner, ~comm, host, op), +// HostBound(host, ~comm) +// ]-> +// [ +// !Community(~comm), !CommunitySigningKey(~comm, ~sk_comm), +// !HostCommunity(host, ~comm), AuditHead(~comm, 'genesis'), +// !Admitted(owner, ~comm) +// ] +// +// Expected mutation result: `provisioning_requires_operator_authorization` +// goes red — a mere registered client (never OperatorRegistered, never +// compromised as an operator) mints a community. Confirmed: falsified with an +// 8-step trace on Tamarin 1.12.0 / Maude 3.5.1. + +// MUTATION_Rotate_Ignore_Host (DO NOT ENABLE in the real model): the relay +// applies the owner rotation to a community OTHER than the request host's +// binding — the operator-plane confused deputy (effect escapes the named +// host). The real rule's `!HostCommunity(host, comm)` premise pins the +// effect; this mutation re-binds it to an arbitrary community. +// +// rule MUTATION_Relay_Rotates_Owner_Other_Community: +// [ In(< 'operator_provision', op, url, 'POST', time, host, owner, sig >), +// !OperatorKey(op), +// !HostCommunity(host, host_comm), +// !Community(other_comm) ] +// --[ +// Eq(verify(sig, < 'kind27235_operator', op, url, 'POST', time, h(< host, owner >) >, op), true), +// Neq(host_comm, other_comm), +// OwnerRotated(owner, other_comm, host, op), +// OwnerBootstrapped(owner, other_comm, host, op), +// RotationResolved(owner, other_comm, host, host_comm) +// ]-> +// [ !Admitted(owner, other_comm) ] +// +// Expected mutation result: `rotation_confined_to_host_community` goes red — +// the single RotationResolved witness carries used_comm # host_comm in one +// rule instance (same single-witness framing as S5/S6). Confirmed: falsified +// with a 12-step trace on Tamarin 1.12.0 / Maude 3.5.1. + // ============================================================================ // Independent per-community audit chains // ============================================================================ @@ -684,6 +942,44 @@ lemma cross_community_audit_splice_attempt_is_not_append: CrossCommunityAuditSpliceAttempt(commA, commB, prevA, prevB, forged) @ i ==> not (Ex #j. AuditAppended(commA, prevB, forged) @ j)" +// S9: every owner bootstrap/rotation — the operator plane's only effect, +// emitted by BOTH the provision and the rotate rule — names an +// operator-allowlisted key. Registration (`!OperatorKey`) is the +// RELAY_OPERATOR_PUBKEYS gate; there is intentionally NO compromise +// disjunct: compromising an operator's secret does not put a new key on the +// allowlist, so the claim holds unconditionally. Enabling +// MUTATION_Provision_Any_Client (relay accepts any registered client key) +// falsifies this. +lemma provisioning_requires_operator_authorization: + "All owner comm host op #i. + OwnerBootstrapped(owner, comm, host, op) @ i + ==> (Ex #j. OperatorRegistered(op) @ j & #j < #i)" + +// S9 payload binding: an accepted provision's (host, owner) pair is exactly a +// pair the named operator signed — the payload hash h() in the +// NIP-98 preimage is what forces this. An adversary who captures the +// Authorization material can replay it (benign convergence, same pair) but +// cannot re-target it. The disjunct admits operator-key compromise, after +// which the adversary can sign arbitrary pairs itself. Enabling +// MUTATION_Provision_Unsigned_Body (payload tag omitted — kalvin's finding #1 +// on PR #1657) falsifies this. +lemma provision_accepts_only_operator_signed_payload: + "All op host owner #i. + ProvisionAccepted(op, host, owner) @ i + ==> (Ex #j. OperatorAuthorizedProvision(op, host, owner) @ j & #j < #i) + | (Ex #k. OperatorKeyCompromised(op) @ k & #k < #i)" + +// S9 confinement: an owner rotation lands in exactly the community bound to +// the request's host. Same single-witness framing as the S1-host lemmas: the +// rotate rule emits one RotationResolved(owner, used_comm, host, host_comm) +// fact carrying both the community actually mutated and the host's binding, +// so a counterexample is one rule instance. Enabling +// MUTATION_Rotate_Ignore_Host falsifies this fast. +lemma rotation_confined_to_host_community: + "All owner used_comm host host_comm #i. + RotationResolved(owner, used_comm, host, host_comm) @ i + ==> used_comm = host_comm" + // Reachability / anti-vacuity probes. lemma executable_token_leak: exists-trace @@ -745,4 +1041,26 @@ lemma executable_open_auth_registration: exists-trace "Ex pk comm host #i. OpenCommunityAutoRegistered(pk, comm, host) @ i" +// S9 anti-vacuity probes: the operator plane's provision and rotate paths are +// both reachable, so the S9 safety lemmas are not vacuously true. +lemma executable_provision: + exists-trace + "Ex op host owner #i #j. + OperatorAuthorizedProvision(op, host, owner) @ i + & ProvisionAccepted(op, host, owner) @ j + & #i < #j" + +lemma executable_rotate: + exists-trace + "Ex owner comm host op #i. OwnerRotated(owner, comm, host, op) @ i" + +// A rotate on an already-bound host lands in the community the ORIGINAL +// provision bound — the create-then-converge lifecycle end to end. +lemma executable_rotate_after_provision: + exists-trace + "Ex comm host op op2 owner2 #i #j. + CommunityProvisioned(comm, host, op) @ i + & OwnerRotated(owner2, comm, host, op2) @ j + & #i < #j" + end diff --git a/docs/spec/MultiTenantRelay.tla b/docs/spec/MultiTenantRelay.tla index 007100529..7c98f8e2f 100644 --- a/docs/spec/MultiTenantRelay.tla +++ b/docs/spec/MultiTenantRelay.tla @@ -133,6 +133,22 @@ InitialChannelOwners == [ch \in Channels |-> \* NoCommunity sentinel (an unmapped/unknown host) -> the connection fails closed \* and no channel-less write may derive a community from it. This is the upstream \* of ResolveTenant: ctx.community is *derived* from the host, never free-chosen. +\* +\* Stated assumption (P-HOST-APPEND): HostCommunity is a CONSTANT-per-segment +\* function even though the operator plane (POST /operator/communities) can +\* provision new communities at runtime. The host map is append-only — +\* ensure_configured_community's upsert (ON CONFLICT (lower(host)) DO UPDATE +\* SET host = EXCLUDED.host RETURNING id) returns the SAME community id for an +\* already-bound host and no code path re-points an existing binding — so a +\* provisioning event only extends the function's domain with a fresh +\* host |-> community pair. Every behavior TLC checks over the fixed +\* HostA/HostB/HostBad harness therefore remains valid across provisioning: +\* new hosts are new constant assignments for subsequent behavior, never +\* mutations of the bindings modeled here. The authorization obligations of +\* the operator plane itself (allowlist gate, payload binding, rotation +\* confinement) live in the Tamarin model (MultiTenantAuth.spthy S9, with the +\* append-only assumption imported as the UniqueHostBinding restriction); see +\* docs/multi-tenant-relay.md SS-Conformance (P-HOST-APPEND). HostCommunity == [h \in Hosts |-> CASE h = HostA -> CommA [] h = HostB -> CommB