# Multi-Tenant Buzz Relay: A Formal Specification
`draft`
## Abstract
This document specifies the data and authorization model that lets one shared
Postgres instance, served by N stateless relay processes, host M independent
**communities** without one community observing or acting on another, and gives
a formal proof of its safety properties. It proves two families of property:
**isolation** — a community is *non-interfering* with every other community
across the relay's logical interface (query results, authorization decisions,
emitted errors, and audit-chain contents) — and **authorization soundness** — no
credential, signature, or forged event lets an actor cross a community boundary.
Today a Buzz relay *process* is the security boundary: one `DATABASE_URL`, one
relay keypair, one relay-global `relay_members` table, with `channel_id` (the
`h` tag) as the only sub-relay locality. The model proven here demotes the relay
process to stateless compute and elevates a new **community** entity to the
tenant/security boundary, carried as a `community_id` on every scoped row. That
move collapses a process-level boundary into a row-level one. The contribution of
this document is the formal characterization that the collapse loses nothing —
proven *relative to* explicitly stated axioms about Postgres row-level security,
Schnorr/NIP-98, a collision-resistant hash, and the relay's own
`channel_id → community_id` resolution.
The architecture is not novel as a *pattern*: row-level multi-tenancy with a
discriminator column and row-level security (RLS) is established practice (see
§Prior Art). The contribution is the **formal treatment** — stating tenant
isolation as non-interference encoded as a label-flow invariant (not a
`WHERE community_id = $1` predicate), mechanizing it (TLA+ for the
concurrency/serving model, Tamarin for the authorization protocol under a
Dolev-Yao adversary), and gating every invariant on a mutation test so the proof
is non-vacuous.
## Scope and Non-Goals
This specification proves **safety** ("nothing bad happens"). It deliberately
does **not** prove:
- **Liveness or performance.** That a query meets a latency budget, or that a hot
partition does not throttle, is empirical — characterized by the perf rig, not
by theorem.
- **Postgres's internal correctness.** RLS enforcement, MVCC snapshot isolation,
and `ON CONFLICT DO NOTHING` semantics are trusted and stated as axioms
(§Axioms). We prove our *composition* on top of them; we do not reprove them.
- **Cryptographic primitives.** Schnorr signature unforgeability (BIP-340), the
NIP-98 request binding, and second-preimage resistance of the event-id hash are
the Tamarin model's equational theory, not reproven.
- **Physical-resource isolation.** Communities share an id space, time
partitions, a connection pool, and a CPU. The proof covers the *logical*
interface; bandwidth-limited physical channels are a named, explicit carve-out
(§Isolation Boundary, class C1).
- **Above-the-interface client leakage.** The proof boundary is the relay's
observational interface. If a client (a multi-tenant UI, an NIP-19 `nevent`
share, a screenshot, a leaked log) surfaces a user's own event ids from
community A while that user is also a member of B, the user then holds an A-id
out-of-band and can probe the existence oracle from a B connection. The
composite-index closure (A-RLS-5) means the probe still reveals nothing — B's
write at that id is a fresh `(community_id, id)` key — but we name this surface
explicitly: closing it for any *weaker* index shape is above the interface and
is the client's obligation, not the relay's.
Stating this boundary is part of the claim. "Provably isolated" without naming
the trust boundary does not survive scrutiny; "isolation is machine-checkable
relative to these stated axioms, with every shared logical channel either closed
in-model or closed by a named axiom" does.
## System Model
A **community** `C` is the tenant/security boundary. It owns: a set of channels,
a membership relation, a signing keypair, a token namespace, workflows, an audit
hash chain, and the messages scoped to it. A community is a durable row in a
`communities` table; creating one is an INSERT, never DDL.
The shared store holds three tiers:
- One **canonical message log** `L`: an append-only table keyed by
`(community_id, created_at, id)`. Every message carries the `community_id` of
the community it belongs to. Append is idempotent
(`ON CONFLICT (community_id, created_at, id) DO NOTHING`).
- A **tenant-scoped control plane**: relational, ACID tables — `channels`,
`channel_members`, `api_tokens`, `workflows`, audit entries — each carrying
`community_id`, kept relational because authorization needs synchronous current
state.
- **Disposable projections**: mentions, thread metadata, reactions, full-text
search — each `community_id`-keyed, rebuildable from `L`, never authoritative.
A **relay process** is stateless compute. It owns no community data; any process
can serve any community, and N processes share the store.
A **connection** is bound to an **actor** (a pubkey, authenticated via NIP-42 on
WebSocket or via a NIP-98-minted bearer token on REST). Every connection
operation is evaluated under a **TenantContext** `⟨community_id, actor⟩`. The
`community_id` is **resolved by the relay**, never read from the client-supplied
`h` tag or claimed community. For a **channel-bearing** operation it is the
community of the channel the operation names (`resolve : channel_id →
community_id`, an indexed lookup the relay owns under the same transaction
snapshot as the operation), and the connection's **host** must agree with it —
an A-host presenting a B-channel event is rejected fail-closed, never acted on as
B. For a **channel-less** operation (profiles, DMs,
long-form, status, read-state, lists — no `h` tag) it is the community bound to
the connection's **host** at establishment (`resolve_host : host → community_id`,
lifting today's per-relay URL identity up to the community); an unmapped host
binds to no community and the connection is rejected fail-closed. The composed
resolver is `ResolveTenant(req, event)` (see P-RESOLVE-HOST).
Two operation classes act on the store:
- **Serve(ctx, q)** — a read (REQ / REST GET, including direct `ids` lookup,
`#e`/`#a` tag filters, metadata/member discovery, and projection reads). Returns
rows and derived results matching `q`, confined to `ctx.community_id`.
- **Accept(ctx, e)** — a write (EVENT / REST POST). Appends `e` to `L` (or mutates
control-plane state) under `ctx.community_id`, after an authorization decision
over current control-plane state.
A community is either **allowlisted** or **open**. An allowlisted community admits
actors only via a signed NIP-43 member list (§Authorization, S7); an **open**
community (one with no member-pubkey allowlist) auto-registers any authenticated
npub on AUTH — but the registration is stamped to the **host-resolved** community,
never a client-claimed one, so "open" widens *who* may join, never *which*
community they join. Two further control-plane writes are first-class: **channel
creation** stamps a fresh channel atomically from `HostCommunity[host]` (the client
supplies no community id, and the stamp is immutable thereafter), and **no-`#h`
reads** — the kinds-only feed read and the `#e`-only aux read (reactions, edits,
deletes, thread metadata) — resolve their community from the connection's host and
are gated on host-community admission like every other channel-less operation.
These surfaces are modeled, not asserted: see §Isolation (I5) and
§Authorization (S5/S8).
**The resolved `community_id` is the sole tenant authority.** The `h` tag on a
wire event is a *routing hint* a client asserts; it is never the commit point of
tenancy. This is the **confused-deputy** hazard (Hardy 1988): the relay holds
broad authority over a shared DB, and a client supplies an ambient name; if the
relay acts on its broad authority under the client's name, the client escapes its
community. The defense is capability discipline — authority is bound to the
*resolved object* `(community_id, channel_id, capabilities)`, never to a
caller-supplied tag. The model treats the `h` tag as adversary-controlled and
proves it is not load-bearing (Theorem I2 / S1).
## Isolation Boundary
Tenant isolation is stated as **non-interference**: for any two executions equal
on community B's inputs and initial B-visible state, B's observable outputs are
equal regardless of community-A-only actions (Goguen–Meseguer 1982; the
concurrent variant is observational determinism). A `WHERE community_id = $1`
row-return invariant is only *one projection* of this theorem — it implies
nothing about timing, errors, uniqueness collisions, projection rebuild, or the
auth gate. Two execution traces cannot be expressed directly in TLA+; the
standard tractable encoding is a **label-flow invariant**: every state element
(message row, membership, projection cell, in-flight query, emitted error, audit
entry) carries the community label it originated from, and the single-run safety
invariant is *"no high-labeled value ever flows into a low-labeled observation."*
This encoding forces enumeration of every state element's label, which is what
catches the projection-rebuild and error-surface channels that a predicate hides.
Shared channels split into two classes:
**(C1) Bandwidth-limited physical channels — declared, out of scope.** Buffer
cache, autovacuum, planner statistics, partition right-edge throughput, and
connection-pool tail latency are shared. A co-tenant can measure these as timing;
the channel is bandwidth-bounded and orthogonal to the threat model
(cross-tenant data leak, privilege escalation, audit forgery). We declare this
class as git-on-s3 declares physical pack pruning: named, with a deferred future
bandwidth bound. **We do not claim timing non-interference.**
**(C2) Logical channels — in scope, enumerated, each closed.** These are *not*
carve-outs; a B-scoped connection can observe them at the interface, so each must
be closed in-model or by a named axiom:
1. **Event-id existence oracle.** `INSERT … ON CONFLICT DO NOTHING` on the
content-hash id: a B-writer observing zero rows affected learns *some* tenant
wrote that id. Closed by **A-RLS-5** (§Axioms): the uniqueness constraint is
composite over `(community_id, …, id)`, so a B-scoped write at an id A already
holds gets a *fresh* key, not a conflict — B's rows-affected count is a
function of B's own state alone, never A's. **A_HASH** is the *supporting*
axiom: it additionally rules out the adversarial-search variant (B cannot
*find* a fresh event hashing to a chosen id). Note the residual: A_HASH says
nothing about ids B already *knows* out-of-band (NIP-19 `nevent` shares,
multi-tenant client UIs that surface a user's own ids across communities) —
that exposure is closed by the composite index, not the hash, and any
above-the-interface client surface that leaks a user's A-ids while they are
also in B is a named residual in §Scope and Non-Goals, not a relay-closed channel.
2. **Constraint-violation error surface.** Postgres errors can leak constraint
names, conflicting tuples, and columns. Closed by a fixed **sanitized error
alphabet** and the structural obligation that the relay emits only errors from
that alphabet (an implementation code-fence, proven relative to it).
3. **Projection rebuild path.** A rebuild touches every community's events by
construction. Closed by the invariant that rebuild writes server-side
projection tables only and **never serves rows** to a tenant-scoped
connection; a tenant query concurrent with a rebuild sees its own rows or none.
4. **Unauthenticated global surface.** The NIP-11 relay information document at
`/` is unauthenticated and tenant-unscoped by construction; no B-scoped
connection, no `c.scope`, no label exists, so the labeling invariant does not
reach it. Closed by a **typed-input code-fence**: the doc-build function
consumes only relay-static configuration types — no database handle, no tenant
context, no audit service. Today `RelayInfo::build`
(`crates/buzz-relay/src/nip11.rs:122`) takes only static inputs and
`nip11_facts` (`:176`) reads only `state.config`/`state.relay_keypair`, so the
surface is clean — but by *current code*, not by the proof; adding a
`total_events` counter is one `&PgPool` argument away and the labeling
invariant catches none of it. This is the same enforcement class as the Σ_err
alphabet (C2.2) — a typed constraint at a seam, lintable over `build`'s
signature — but disjoint: Σ_err governs *what symbols leave on authenticated
paths*, C2.4 governs *what state populates unauthenticated paths*. Any future
unauthenticated relay-level endpoint (NIP-66 monitoring, health probes that
expose counters) lives under C2.4 by default.
The numeric COUNT (NIP-45) and EOSE cardinality channels are deliberately *not*
on this list: they are closed by the same label propagation as event rows (a
count is `|{B-labeled rows matching the filter}|`), so they belong in the typed
interface, not as distinct C2 mechanisms. The C2 list is the index of *distinct
closure mechanisms* — A_HASH, the Σ_err alphabet, the rebuild behavioral
invariant, and the C2.4 typed-input fence — not the index of channels.
**(C3) Historical writes after revocation — declared, out of scope.** The
admission fence (I5, `Inv_AdmissionFence`) governs **current** capability: it
proves that no membership or channel-less read capability survives for an actor
not currently admitted to that community. Revocation (`RevokeMember`) removes the
current `admittedMembers` row and therefore the capability, but it does *not*
relabel or delete rows the actor wrote while admitted — those historical writes
retain their original community label and remain present. This is sound and
intended: the property we mechanize is "current membership and read capability
track current admission," not "writes are retroactively un-admitted." We declare
this as C1 declares physical timing: named, with retroactive-write redaction left
to an operator data-lifecycle surface outside the isolation model. **We do not
claim historical writes are revoked when a member is revoked.**
### The typed observational interface
The non-interference theorem is stated *over an interface*: the exclusive set of
observations a **B-scoped connection** (one whose *resolved* community is B) can
make. Enumerating this set is load-bearing — a `WHERE community_id = $1` invariant
silently omits cardinality, error, status-code, and global-document channels.
**Any observation not in this set is either C1 (declared) or a model violation.
There is no third category.** Each entry below names its code seam so the TLA+
model, the Tamarin model, and the red-team audit reference the same surface.
**O.WS — WebSocket transport** (`crates/buzz-relay/src/protocol.rs:180-215`). The
relay emits exactly these client-bound messages:
- **`O.WS.EVENT(sub_id, event)`** — a delivered Nostr event. Its `content` is
high-labeled at the row's community; `e`/`p`/`q` tag references inherit the
row's label (they may *name* globally-existing ids, but the row reaches B only
if B-labeled).
- **`O.WS.EOSE(sub_id)`** — end-of-stored-events. The *count* of preceding events
is the cardinality of B-visible rows matching the filter; it must be a function
only of B-labeled state.
- **`O.WS.OK(event_id, accepted, message)`** — write ack. `event_id` echoes the
submission (benign); `accepted` is a function of (validity, signature, resolved
scope, dedup) over B-labeled state only; `message` is drawn from the sanitized
alphabet `Σ_err` (the C2.2 seam — the current `String` type admits any value).
- **`O.WS.NOTICE` / `O.WS.CLOSED`** — out-of-band and sub-termination strings;
same `Σ_err` constraint (`connection.rs:307,326`).
- **`O.WS.AUTH(challenge)`** — NIP-42 challenge; a fresh nonce, function of relay
randomness only, never of any tenant's writes.
- **`O.WS.COUNT(sub_id, n)`** — NIP-45 count (`protocol.rs:213`). `n` is a numeric
channel: even under row confinement, a count touching non-B rows leaks A's
cardinality. The rule: `n` is the count of B-labeled rows matching the filter,
full stop.
**O.REST — HTTP API surface.**
- **`O.REST.BODY`** — JSON response: row content, projection results, and audit
entries (`crates/buzz-audit/src/service.rs:get_entries`) must all be B-labeled.
- **`O.REST.META`** — status code, headers, structured error envelope. The status
code is itself observable: `IngestError::{Rejected,AuthFailed,Internal}` →
`400/401|403/500` (`handlers/ingest.rs:138-146`) must be a function of
{request, B-labeled state}, never of A's state.
**O.AUTH — auth verdict.** The Boolean "did this pass the gate," observable via
`O.WS.OK.accepted` and `O.REST.META.status`. It is a function of (submitted
credentials, server-side resolution `channel_id → community`, B-labeled
membership/token/policy state). The *claimed* community never appears in this
function — only the *resolved* one. (Theorem S1.)
**O.AUDIT — audit chain.** `get_entries(scope=B)` returns only B-chain entries;
`verify_chain(scope=B)` is decidable from B-labeled entries alone; compromise of
A's chain key does not affect B's. (Theorem S4.)
**O.NIP11 — relay info document (`/`).** Global and unauthenticated, so by
construction it *cannot* be tenant-labeled — therefore its content must be a
function of relay-static configuration only. `supported_nips` is fine;
`total_events` would be a cross-tenant leak.
Everything outside this set is **C1** (wall-clock latency, buffer-cache hit rate,
planner choice, autovacuum, partition right-edge throughput, pool saturation,
memory/fd/scheduler effects — declared, bandwidth-bounded) or **closed by axiom**
(the `INSERT … ON CONFLICT DO NOTHING` id-existence oracle at `event.rs:151`,
closed by A_HASH).
### Label-propagation rules
The labeling discipline that makes non-interference a *single-run* safety
invariant (every state element carries a community label; the invariant is "no
high-labeled value flows into a low observation"):
- **L1 — Source label.** Every event row carries `community_id`, set by the
server-side resolver at insert time via `ResolveTenant`. For a **channel-bearing**
event the label is `resolve(channel_id)`; for a **channel-less** event
(`kind:0` profiles, `1059` DMs, `30023`/`30174`/`30315`/`30078`, lists —
`channel_id = NULL`) the label is the connection's host-bound community
`resolve_host(connection.host)`, with the token stamp required to *agree* (never
to *supply* it). The `h` tag is **not** the label source, and neither is the
client-claimed community. (Resolution is a fence — see P-RESOLVE and
P-RESOLVE-HOST.)
- **L2 — Projection inheritance.** Each projection row (`event_mentions`,
`thread_metadata`, `reactions`, FTS) inherits its source event's label; rebuild
= replay of labeled source rows, so rebuilds preserve labels by construction.
- **L3 — Audit partitioning.** N independent chains, one per community label;
community-scoped writers only; no cross-chain reference, no global "latest" head.
- **L4 — Auth-verdict label.** The allow/deny verdict carries the **resolved**
community label, never the **claimed** one.
- **L5 — Token stamp.** A NIP-98 token has exactly one community stamp, assigned
at mint from the resolved channel set; a mint resolving to >1 community is
rejected fail-closed (S2). The token's label *is* its stamp.
- **L6 — Connection scope.** A connection has exactly one resolved community at a
time, **bound from its host** (`resolve_host(connection.host)`) at establishment
before any handler runs; re-scoping requires a new connection to a different
host; all its observations inherit that scope. An unmapped host binds to no
community and is rejected fail-closed (P-RESOLVE-HOST), never defaulted.
- **L7 — Error label.** A finite, statically-declared alphabet `Σ_err` governs the
*authenticated, tenant-scoped* WS error surface: every `O.WS.OK.message`,
`O.WS.NOTICE`, and `O.WS.CLOSED` is drawn from it (the 9 NIP-01-reachable
prefixes — `auth-required`, `restricted`, `invalid`, `duplicate`, `pow`,
`rate-limited`, `blocked`, `error`, `frame-too-large`). Emitting a non-`Σ_err`
string is a structural code violation (the C2.2 code-fence — a lint, not a model
property). Today `RelayError::Database(#[from] buzz_db::DbError)` (`error.rs:11`)
is the seam. The *unauthenticated/REST* error surface (`not-found`,
`bad-request`) is a **distinct fence** — C2.4's typed-input constraint, not
`Σ_err` — because it has no tenant scope and no label, so it sits outside the
labeling invariant entirely. One Rust enum may back both for ergonomics, but the
model treats them as two alphabets closed by two mechanisms.
- **L8 — No injection.** Per L7, A-labeled state cannot influence *which* `Σ_err`
symbol B observes.
In one line: *for every reachable state `s`, every B-scoped connection `c`, and
every observation `o ∈ O.* ∪ Σ_err` emitted to `c`, `o` is a deterministic
function of (B-labeled state in `s`, `c`'s request history, relay-static config);
no A-labeled element is an input to `o`.* This is what the TLA+ model encodes —
strictly stronger than row-equality, because it forces enumeration of every
observation channel above.
## Axioms
The proof holds *relative to* the following. Each is a documented property of
Postgres / the crypto primitives, and a testable assumption admitted per
deployment (§Conformance).
### Row-level security (the fail-closed backstop)
Postgres RLS is fail-closed **only** under specific configuration (PostgreSQL
manual, "Row Security Policies"). We state the configuration as obligations:
- **(A-RLS-1)** Every queryable tenant-bearing table has RLS enabled with a
restrictive policy `community_id = current_setting('app.community_id')::uuid`,
and no permissive policy that admits cross-tenant rows.
- **(A-RLS-2)** The relay's request role is non-superuser, `NOBYPASSRLS`, and not
the table owner unless `FORCE ROW LEVEL SECURITY` is set (owners and `BYPASSRLS`
roles bypass policies).
- **(A-RLS-3)** `app.community_id` is set transaction-locally (`SET LOCAL`) before
any query and cleared at transaction end. Pooled connections must not retain or
combine tenant context across requests.
- **(A-RLS-4)** `SECURITY DEFINER` and `leakproof`/user-defined functions in the
request path are audited as part of the trusted boundary: a `leakproof`
function may be evaluated *ahead of* the RLS check, and a `SECURITY DEFINER`
function can read data unavailable to the caller.
- **(A-RLS-5)** Uniqueness and foreign-key constraints include `community_id`, so
a conflict outcome or a dangling reference cannot reveal or reach another
community.
A query that fails to set `app.community_id` matches the policy predicate over
NULL → no rows, never all rows. This is what makes a missed *application*
predicate fail closed rather than leak (Theorem I4).
### Concurrency, crypto, and resolution
- **(P-APPEND)** `INSERT … ON CONFLICT (community_id, created_at, id) DO NOTHING`
commits a row iff no row with that key exists; concurrent appends are
serializable under MVCC; a committed row is never silently overwritten; a read
sees a consistent snapshot.
- **(P-SIG)** An actor cannot produce a valid Schnorr signature (BIP-340) for a
pubkey whose secret key it does not hold. A NIP-98 event's `u`/`method`/
`payload` tags bind it to exactly one HTTP request and are non-transferable to a
different request.
- **(P-RESOLVE)** `resolve : channel_id → community_id` is a total function over
existing channels, computed from control-plane state under the operation's
transaction snapshot. A channel belongs to exactly one community
(`channels.community_id` NOT NULL); resolution never returns a community a
channel does not belong to. **A channel's community is set at creation and never
reassigned: `channels.community_id` is immutable after insert.** Both mechanized
models encode this — Tamarin as the persistent `!ChannelCommunity` fact
(`MultiTenantAuth.spthy:51`, once-true-always-true), TLA+ as the
`ChannelCommunity` CONSTANT function (`MultiTenantRelay.tla:107`). Any future
re-tenanting would be a separate axiomatic admission with its own audit
discipline and re-verification of S1/S2 (and I1–I5).
- **(P-RESOLVE-HOST)** `resolve_host : host → community_id ∪ {⊥}` is the upstream
binding for **every** connection, lifting today's per-relay URL identity one
level up to the community. A connection's community is `resolve_host(host)`,
fixed at establishment; the URL the client connects to *is* the selector,
exactly as a relay URL is today. `ResolveTenant(req, event)` composes the two:
if the event has an `h` tag, require `resolve(h) = resolve_host(host)` (the
host/channel **agreement** fence — an A-host presenting a B-channel event is a
confused deputy on the host axis and is rejected fail-closed, never acted on as
B) and store that community; if it has none, store
`community_id = resolve_host(host), channel_id = NULL`. Two fences hold for both
paths. **Fail-closed:** a host/channel disagreement (incl. an unmapped host
resolving to `⊥`, which can never equal a real channel community) is rejected
generically (`auth-required`/`restricted`), never bound to a default tenant —
`resolve_host` is partial and the absence/disagreement of a binding is a reject,
not a fallback. **Host wins:** a NIP-98 token's community stamp (L5) must *agree
with* the host-derived community; a token that disagrees is rejected, so the
confused-deputy fence (I2) is intact with authority binding to the host-resolved
object. Tamarin encodes this as the persistent `!HostCommunity` fact
(`MultiTenantAuth.spthy`): the channel-less use rule fires only when token stamp
and host community coincide (witness `ChannelLessResolved`, lemma
`channelless_use_confined_to_host_community`), and the **channel-bearing** use
rule fires only when the channel mapping and the host community coincide (witness
`ChannelBearingResolved(tok, used_comm, host, host_comm)`, lemma
`channelbearing_use_agrees_with_host` asserting `used_comm = host_comm`). TLA+
encodes it as the `HostCommunity` resolver (with a `⊥` sentinel for unmapped
hosts) and an `Inv_HostBindingFence` invariant quantifying over **every** accepted
write — channel-bearing and channel-less — *and* every observable duplicate/no-op
outcome, that its stored community equals its originating host's mapping. The
duplicate/no-op path carries the same obligation because it is client-observable
write surface (the `Duplicate` result exposes the scoped existence/conflict rows):
an A-host presenting a B-channel id is fenced before any conflict lookup, so it
cannot learn whether that id exists in B. At N = 1 this is byte-identical to
today: one host → the one community, every connection lands there, nothing
client-observable changes.
- **(A_HASH)** The event id `sha256(canonical event)` is second-preimage
resistant: an actor cannot find a distinct event hashing to a chosen id. (NIP-01
already relies on this; we cite it the way git-on-s3 cites its CAS axiom.)
- **(P3)** *NIP-98 mint freshness.* A NIP-98 mint event (kind:27235) is accepted
at most once. The implementation enforces this with two checks: a `created_at`
within ±60s of server time (`buzz-auth/src/nip98.rs:77-83`,
`TIMESTAMP_TOLERANCE_SECS = 60`) **and** a seen-set keyed on event id
(`buzz-relay/src/api/bridge.rs::check_nip98_replay`), whose cache TTL (120s,
`state.rs:407`) is 2× the window so a mint valid at either edge stays tracked
for the full window. The Tamarin model abstracts the window as a fresh nonce on
`~time` (`MultiTenantAuth.spthy:91`), which over-approximates the
implementation by treating every mint as structurally unique; the spthy comment
at `:84-86` references this obligation as "P3."
P-RESOLVE is the load-bearing *application* assumption for channel-bearing events
and P-RESOLVE-HOST is its channel-less counterpart — together the fence the
`h`-tag and claimed-community adversary cannot circumvent. A-RLS-1..5 are the
load-bearing *backstop*.
## Safety Theorems
### Isolation (mechanized in TLA+)
- **NI (Non-interference, master).** For every reachable state and every B-scoped
observation, the observed value is a function only of B-labeled state — no
high-labeled value flows into a low-labeled observation. I1–I5 are the specific
flows it rules out, each independently mutation-tested non-vacuous.
- **I1 (Read confinement).** Every row a `Serve` returns — including direct-id and
`#e`/`#a` lookups — is `ctx.community`-labeled.
- **I2 (Resolution fence).** `ctx.community = resolve(channel_id)` for
channel-bearing events and `resolve_host(host)` for channel-less ones, never the
`h` tag, the claimed community, or the token stamp; an adversary `h = C' ≠
resolve = C` cannot widen what is served or accepted. The **host axis** is fenced
on both paths: a channel-less write over host A cannot land in community B, and a
channel-bearing op over host A on a B-channel is rejected rather than acted on as
B — including the **duplicate/no-op outcome**, so an A-host cannot use a B-channel
id-conflict result as a cross-tenant existence oracle (`Inv_HostBindingFence`
quantifies over accepted writes *and* recorded duplicates, making "default to C",
"A-host drives a B-channel insert", and "A-host probes a B-channel duplicate"
caught mutations, not invisible ones).
- **I3 (Write non-loss & no cross-contamination).** Every accepted append commits
under the resolved label and no other; no committed message is lost or
overwritten; two communities appending the same event id land as two rows under
distinct labels (cross-community id collision is not a write conflict).
- **I4 (Fail-closed backstop).** A dropped application predicate yields ∅ under
A-RLS, and NI still holds; removing the RLS guard makes the dropped predicate
produce a cross-label row — proving RLS load-bearing, not decorative.
- **I5 (Admission fence).** Channel membership and channel-less read capability
exist only for actors admitted to *that* community. The NIP-43 allowlist is the
`admittedMembers` relation keyed on `(community, actor)`; `AddMembership` and
every channel-less read are gated on `IsAdmitted(c, a)`, and `Inv_AdmissionFence`
quantifies over every membership *and* every recorded channel-less read,
requiring same-community admission on both — the channel-less branch additionally
binding `HostCommunity[host] = community`, so the host axis is fenced here too.
The same gate covers the **open-community** and **no-`#h`-read** surfaces: an
open community auto-registers an authenticated npub into the host-resolved
community (`AuthenticateOpenCommunity` recording an `authRegistration`), and the
kinds-only **feed read** (`ReadHostFeedRows`) and `#e`-only **aux read**
(`ReadHostAuxRows`) each record a witness only when the actor is `IsAdmitted` to
the host community — `Inv_AdmissionFence` quantifies over those witness sets too,
so an actor admitted only in B can neither open-register into A nor read A's
no-`#h` feed/aux. **Channel creation** (`CreateChannel`) stamps a fresh channel
from `HostCommunity[host]` and `Inv_ChannelCommunityImmutable` proves that stamp
is never re-labeled — creation is an in-relay analog of S2's
resolve-then-immutable discipline. The fence is about **current**
capability: it is mutation-tested non-vacuous by
M9 (re-keying the membership/read gate to any-community admission), which goes red
on both a membership trace and a channel-less-read trace, and by M10–M13 (the
open-AUTH, channel-create, feed-read, and aux-read stamp/gate mutations), each
confirmed red — proving an admit-into-A then act-in-B escape is caught rather than
invisible on every one of these surfaces. (See C3 for the explicit
historical-write carve-out.)
### Authorization soundness (mechanized in Tamarin, Dolev-Yao adversary)
- **S1 (Token confinement).** A token accepted for a B-resolved operation was
minted with stamped community B; a token stamped A never authorizes in B. A
*leaked* token authorizes within its own community (blast radius is not zero and
we do not pretend otherwise) but never another — containment, proven.
- **S2 (Mint integrity).** A token exists only as the output of a NIP-98 mint by
the holder of `owner_pubkey`'s key (P-SIG); it carries exactly one stamped
community; a mint whose channel set spans two communities yields no token.
S2's trace-level mint-rejection closure relies on P-RESOLVE's totality,
single-valuedness, **and immutability**: the Tamarin model encodes immutability
via persistent-fact semantics (`!ChannelCommunity`), without which a
retag-then-replay — reject a cross-community `req`, retag a channel, replay the
original mint bytes (same `req` hash) — would mint a token for a request S2
declares unmintable. This is the structural analog of A-RLS-5's
`UNIQUE (community_id, id)` clause for I1: both turn stable scope into the
disjointness witness.
- **S3 (Signing-key non-confusion + containment).** A community-B-signed system
event (NIP-29 `39000`/`39001`/`39002`) is never accepted as an authentic
community-A event, even when group ids collide; compromise of B's signing key
does not let the adversary forge A's events.
- **S4 (Audit-chain unforgeability + containment).** No splice, reorder, or forge
in community A's hash chain; compromise of B's chain does not break A's — N
independent chains, N independent guarantees.
- **S5 (Channel-less host confinement).** A channel-less authorization (profiles,
DMs, long-form, lists — no `h` tag) is confined to the community bound to the
connection's **host**, not the token's stamp: host wins. The token must agree
with the host community or the request is rejected; a B-stamped token presented
over an A-host never authorizes for B. This is I2's host counterpart, mechanized
as `channelless_use_confined_to_host_community`,
`channelless_token_agrees_with_host`, and `host_token_mismatch_not_authorized`.
- **S6 (Channel-bearing host/channel agreement).** A channel-*bearing*
authorization is confined to the community bound to the connection's **host**:
the host and the channel mapping must agree. An A-host presenting a B-channel
event never authorizes as B — the host axis of the confused-deputy fence, which
the prior model proved only on the channel axis (claimed-community ignored). This
closes the cross-tenant escape over a wildcard host route where the channel
mapping alone would have been authoritative. Mechanized as
`channelbearing_use_agrees_with_host` (the single-witness `ChannelBearingResolved`
fact asserting `used_comm = host_comm`).
- **S7 (NIP-43 admission confinement).** A community's member-list (NIP-43)
admission is confined to the community whose signing key signed it: B's signing
key can never admit a pubkey into A. Modeled as a parallel rule pair —
`Community_Signs_NIP43_MemberList` mints the signed list and
`Relay_Accepts_NIP43_MemberList` re-verifies the signature against
`!CommunitySigningKey(comm, sk)`, so `comm` is bound by unification to the
resolved community (the same confused-deputy discipline as the S5/S6 host
fence), emitting persistent `!Admitted(pk, comm)`.
`nip43_admission_confined_to_signing_community` proves the confinement; the
commented `MUTATION_Admit_Ignore_Community` (the dual of S6's
`MUTATION_Use_Token_Ignore_Host`) falsifies it, confirming the green is
non-vacuous. This is the authorization-world half of the same admission property
TLA+'s I5 proves in the in-relay world: `!Admitted(pk, comm)` /
`MemberAdmitted(pk, comm)` ⇔ `admittedMembers`/`IsAdmitted(c, a)` — one property,
two worlds (Tamarin proves the admission *event* per-community unforgeable, TLA+
proves the resulting capability in-relay scoped).
- **S8 (Open-community AUTH confinement).** When a community carries no NIP-43
member-pubkey allowlist it is **open**: any authenticated npub auto-registers on
AUTH. The registration is still confined to the **host-resolved** community —
`Authenticate_To_Open_Community` stamps the registration from the connection's
host binding, never a client-supplied selector, so "open" relaxes the *gate* on
membership without relaxing the *boundary* it lands in. Mechanized as
`open_auth_registration_confined_to_host_community` (a host-bound npub registers
only into its host's community), with the exists-trace witness
`executable_open_auth_registration` proving a legitimate open registration is
producible so the confinement lemma is non-vacuous. This is S5/S6's host-binding
discipline applied to the admission *event*: the same confused-deputy fence that
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).
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`,
`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
`leaked_token_blast_radius_contained` / `leaked_token_can_authorize_within_its_community`
containment pair, with `MUTATION_Use_Token_Claimed_Community` confirmed red
(`falsified — found trace`). S3:
`system_event_acceptance_requires_same_community_key_or_compromise` (21 steps) and
`other_community_key_compromise_does_not_authorize` (147 steps). S4:
`audit_append_advances_same_community_head` (2 steps) and
`cross_community_audit_splice_attempt_is_not_append` (1 step). S5 (channel-less
host confinement): `channelless_use_confined_to_host_community` (2 steps),
`channelless_token_agrees_with_host` (3 steps), and
`host_token_mismatch_not_authorized` (6 steps), each paired with an exists-trace
probe (`executable_host_bound`, `executable_channelless_use`,
`executable_host_token_mismatch_attempt`). The S5 mutation
`MUTATION_Use_Token_ChannelLess_Ignore_Host` (the relay reading the token's stamp
and ignoring the host binding — the B-token-on-A-host confused deputy) is
confirmed red: it falsifies `channelless_use_confined_to_host_community` in 3.3s
with a 13-step trace. Each safety lemma is
paired with a verified exists-trace sanity lemma, and the S3/S4 mutations are
confirmed red: the bad-accept-with-other-community-key mutation falsifies both S3
lemmas (5 / 16 steps) and the splice-as-append mutation falsifies the S4 splice
lemma (8 steps). S6 (channel-bearing host/channel agreement):
`channelbearing_use_agrees_with_host` (2 steps), with the
`MUTATION_Use_Token_Ignore_Host` mutation (the relay resolving a channel-bearing
op from the channel mapping while ignoring the host binding — the A-host-on-a-
B-channel confused deputy) confirmed red: it falsifies
`channelbearing_use_agrees_with_host` in 2.6s with a 14-step trace. S7 (NIP-43
admission confinement): `nip43_admission_confined_to_signing_community` (19 steps)
and `other_community_key_compromise_does_not_admit` (79 steps), with the
exists-trace probe `executable_member_admitted` (7 steps) proving a legitimate
admission is producible — so the confinement lemma is non-vacuous, not trivially
true over an unreachable premise. The S7 mutation `MUTATION_Admit_Ignore_Community`
(the relay minting `!Admitted` for a community other than the one whose key
signed — the admission-side confused deputy, the dual of S6's
`MUTATION_Use_Token_Ignore_Host`) is confirmed red: it falsifies
`nip43_admission_confined_to_signing_community` in 1.57s with a 7-step trace.
S8 (open-community AUTH confinement): `open_auth_registration_confined_to_host_community`
(2 steps), paired with the exists-trace witness `executable_open_auth_registration`
(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).
The S5 confinement lemma was deliberately framed to keep its mutation
*cheaply* refutable. An earlier framing joined two action facts
(`ChannelLessAuthorized` ⋈ `HostBoundFor`) on a shared host; the proof verified,
but the *mutation refutation* did not terminate — Tamarin chased which
`HostBoundFor` instance applied for a given host across both the real and mutated
rules. The fix emits a single combined witness
`ChannelLessResolved(tok, used_comm, host, host_comm)` from the authorizing rule
(in the real rule both communities are the same variable), so the confinement
lemma is a single-fact assertion `used_comm = host_comm` and the mutation that
breaks it is a one-rule-instance counterexample. The proof dropped to 2 steps and
the mutation falsifies in 3.3s — the same "make the bad case structurally cheap to
exhibit" discipline as the S1 claimed-community mutation.
The S3/S4 round corrected one vacuity bug in the committed
`1e7fb042…aceaacf24` artifact: `other_community_key_compromise_does_not_authorize`
bound `Neq(commA, commB)` to the *same* timepoint as `CommunityKeyCompromised(commB)`,
but no rule emits `Neq` at the compromise point, so that premise was unsatisfiable —
the lemma verified vacuously and asserted nothing. (Independently confirmed: an
exists-trace probe of the old premise returns `no trace found`.) The fix decouples
the inequality onto a separate witness timepoint `#k`; a new exists-trace lemma
`executable_other_key_compromise_plus_system_accept` (16 steps, verified) proves the
corrected premise is satisfiable, so the 147-step proof is non-vacuous. This is the
same hygiene class as F1/F3/F4 — an artifact relying on a fact the model never makes
reachable — but caught inside a safety lemma's premise rather than a comment. That
fix predates this milestone's host-binding additions and is carried forward
unchanged in the current `.spthy`.
## Conformance
Each axiom is *admitted* per deployment, not assumed universally:
- **A-RLS-1..5** are admitted by a startup/CI assertion suite: enumerate every
tenant-bearing table and assert RLS enabled + restrictive policy present; assert
the request role is `NOBYPASSRLS` and non-owner-or-FORCE; assert no
`SECURITY DEFINER` function in the request path reads tenant tables without
re-establishing context; assert every unique/FK constraint includes
`community_id`. A failing assertion rejects the deployment.
- **P-RESOLVE** is admitted by the `channels.community_id NOT NULL` constraint
plus a test that `resolve` is read under the operation's snapshot, plus a
migration lint asserting `channels.community_id` is never mutated after insert
(no `UPDATE`/`ALTER`/drop-recreate). A failing lint rejects the deployment.
- **P-SIG / A_HASH** are the standard Nostr crypto assumptions; admitted by using
the audited libraries the rest of Buzz uses.
- **P3** is admitted by the NIP-98 handler enforcing *both* timestamp-range
validation and the seen-event-id check (`check_nip98_replay`) before any mint.
Two structural gates make the seen-set sound, and both are conformance checks
because the implementation is silent if either is violated:
1. **Capacity vs. rate.** The seen-set is bounded (capacity 10,000, TTL 120 s
= 2× the ±60 s window). It must satisfy `capacity ≥ peak NIP-98 RPS × 120 s`
(≈ 83 RPS sustained at the current capacity); above that, LRU eviction can
release an entry while its signed `created_at` is still inside the window,
and a replay slips through.
2. **Per-pod scope.** The seen-set is `Arc<AppState>`-scoped, not cross-pod, so
the same replayed event reaching two pods succeeds once on each. P3 therefore
requires *either* NIP-98 mints be pod-sticky on `event_id` *or* the seen-set
be shared across pods (e.g. Redis with the same atomic insert-if-absent
semantics and TTL ≥ 120 s). The chart default (`replicaCount: 1`) satisfies
this gate today; the shipped HA examples (`replicaCount: 3` in
`deploy/charts/buzz/examples/argocd-app.yaml:27` and
`deploy/charts/buzz/examples/flux-helmrelease.yaml:35`) are
P3-non-conforming as shipped unless the operator adds one of:
- **(a)** an ingress annotation hashing upstream selection on a header stable
across replays — `nginx.ingress.kubernetes.io/upstream-hash-by:
"$http_authorization"` works for today's NIP-98 HTTP path, since the signed
event rides in `Authorization: Nostr <base64>` (`bridge.rs:34-46`) and is
bit-identical across replays. Two caveats keep this from being the
recommended fix: it couples replay-stickiness to literal-byte-identity of
the auth header (any future header normalization — whitespace, casing,
base64 padding — silently breaks it), and it does not extend to any mint
path that moves off HTTP (a WS mint has no Authorization header to hash on).
- **(b)** a shared seen-set backed by a store with atomic insert-if-absent and
TTL ≥ 120 s (e.g. Redis, already present in the HA chart for git-pubsub).
**This is the recommended path** — no new infra surface and none of (a)'s
fragility.
A regression test asserts a replayed mint within the window yields a single
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.
## Prior Art
The *pattern* (discriminator column + RLS) is established; the *formal treatment*
as label-flow non-interference is, to our knowledge, new for a Nostr relay.
- **Goguen & Meseguer, "Security Policies and Security Models" (IEEE S&P 1982)** —
the origin of non-interference; the theorem shape ("A's actions do not affect
B's observations"), with "community" for "security domain."
- **Sabelfeld & Myers, "Language-Based Information-Flow Security" (IEEE JSAC
2003)** — the canonical label-based IFC survey; its declassification discipline
is the model for our named C1 carve-out.
- **Jean Yang et al., "Precise, Dynamic Information Flow for Database-Backed
Applications" (arXiv:1507.03513, Jacqueline)** and **Parker, Vazou, Hicks,
"LWeb" (arXiv:1901.07665)** — the closest formal analogs: label-based per-row
policy over a real relational store with a *mechanized* non-interference proof.
They justify "RLS is a backstop axiom; the theorem is the composition."
- **Hardy, "The Confused Deputy" (ACM SIGOPS OSR 1988)** and **Miller et al.,
"Capability Myths Demolished" (HPL-2003-222)** — the resolution-as-capability
framing: bind authority to the resolved object, not the caller-supplied name.
- **NIP-29 (relay-based groups)** — confirms the relay is authoritative and group
ids are not globally unique security domains; supports per-community signing
keys and per-community audit chains, and motivates S3's "non-confusable even
when group ids collide."
- **`fiatjaf/relay29`** — empirical prior art: isolation logic lives across read
filters, direct-id lookups, metadata generation, in-memory state rebuilds, and
`previous`-tag validation, not just insert/select predicates. The reason
`Serve` must model the full observable surface, not just channel reads.
- **PostgREST / PostGraphile** — converge on the transaction-local-context fence
(A-RLS-3); real systems install request-local identity into the DB transaction
and let policies authorize. (See `RESEARCH/MULTITENANT_ISOLATION_PRIOR_ART.md`
for citations and local checkout line references.)
## Mechanized Verification
- **`docs/spec/MultiTenantRelay.tla` + `.cfg`** — the TLA+ isolation model. Run:
`java -cp tla2tools.jar tlc2.TLC -config MultiTenantRelay.cfg MultiTenantRelay.tla`.
On the core finite harness (2 communities × 4 channels, 2 message ids, 1 actor,
1 worker, 2 audit values, bounded observation set, symmetry over the permutable
model-value sets) TLC **completes exhaustively**: *Model checking completed. No
error has been found.* — 472,530,528 states generated, 16,226,016 distinct, 0 left
on queue, depth 13 (8 workers, ~5m). The distinct-state count grew from the
pre-host-binding baseline (4,350,464 → 5,091,328 with channel-less host binding →
5,621,760 with channel-bearing host/channel agreement → 9,232,992 with the
`admittedMembers` allowlist, `channelLessReads` capability rows, and the
`AdmitMember`/`RevokeMember` actions → 16,226,016 with the open-community AUTH
auto-registration, server-stamped channel creation, and the no-`#h` host
feed/aux read paths) precisely because the
channel-less write path, the fail-closed unmapped-host path, the
channel-bearing host/channel-agreement (and its fail-closed disagreement) path,
the admit/revoke/gated-membership/gated-read paths, and now the
open-AUTH/channel-create/feed-read/aux-read paths
are genuinely reachable — new behavior, not dead code. Threading the host through
the duplicate/no-op path adds reachable fail-closed transitions without new
distinct states: only the agreeing host can produce a
recorded duplicate, so the host on that path is fully determined; layering the
admission gate, then the open-AUTH/channel-create/feed/aux surfaces on top, is the
growth to the figures above (admit-then-act, revoke-then-act-fails, gated
reads/joins, open-community auto-registration, server-stamped creation, and the
two host-fenced no-`#h` read shapes multiply the reachable space). That each new
surface is reachable rather than dead is pinned by four intentionally-false
reachability probes (`Probe_OpenAuthRegistration_Unreachable`,
`Probe_CreatedChannel_Unreachable`, `Probe_HostFeedRead_Unreachable`,
`Probe_HostAuxRead_Unreachable`): each asserts the corresponding witness set stays
empty, so each must go red if its action fires — and all four do (open AUTH and
channel-create at 2 states; host feed and host aux at 3 states, via open AUTH then
read). A vacuously-passing new conjunct over an unfireable action is therefore
ruled out, not assumed. Non-vacuity of the
invariants themselves is shown by thirteen mutations (M1–M13), each
confirmed to produce a counterexample: substituting the unscoped direct-by-id
lookup (`UnscopedDirectIdRows`, the `get_accessible_channel_ids` landmine) →
`Safety` violated at depth 4; widening the sanitized-error label to all
communities (the raw-error leak) → `Safety` violated at depth 2; the
global-id conflict key (M3: `WriteDuplicate` keyed on `id` alone via
`GlobalConflictRows`, the missing-`community_id`-in-the-unique-index footgun)
→ `Safety` violated at depth 3, with a B-scoped `WriteResult` observation
carrying `labels |-> {commA}` (the existence-oracle leak C2.1 closes); the
host-default-tenant mutation (a channel-less write from an unmapped host landing
in a default community instead of failing closed) → `Inv_HostBindingFence`
violated at depth 2, the counterexample exhibiting `hostBad` writing into
`commA`; the **M8** host/channel-agreement mutation (`WriteInsert` dropping
the agreement fence so an A-host op on a B-channel is accepted) →
`Inv_HostBindingFence` violated by a 2-state trace (`Init → WriteInsert`); and the
**M8-duplicate** mutation (`WriteDuplicate` dropping the same fence so an A-host
can probe a B-channel id-conflict) → `Inv_HostBindingFence` violated by a 3-state
trace (`Init → WriteInsert → WriteDuplicate`), the counterexample exhibiting a
foreign-host duplicate record whose stored community ≠ its host's mapping (the
existence oracle the duplicate path would otherwise reopen); and the **M9**
global-allowlist mutation (re-keying the admission gate from same-community
`IsAdmitted(c, a)` to any-community `AdmittedInAnyCommunity(a)`) →
`Inv_AdmissionFence` violated in two surfaces: a 5-state membership trace
(`Init → WriteInsert → WriteInsert → AdmitMember(commA, alice) →
AddMembership(commB/chanB1, alice)`) where alice, admitted to A, joins B's
channel through the global hole; and a 4-state channel-less-read trace
(`Init → WriteInsert → AdmitMember(commB, alice) →
ReadMessageRows(commA, NoChannel, hostA)`). The two M9 variants prove both the
`AddMembership` gate and the channel-less-read gate are independently
load-bearing, not just one. The four newest surfaces — open-community AUTH
auto-registration, server-stamped channel creation, and the two no-`#h` host
read shapes (kinds-only feed, `#e`-only aux) — are each held by their own
confirmed-red mutation: the **M10** open-AUTH stamp mutation (the relay stamping
an open-community auto-registration into a default/claimed community instead of
`HostCommunity[host]`) → `Inv_AdmissionFence` violated by a 2-state trace
(`Init → AuthenticateOpenCommunity(hostB stamps commA)`), catching an
`authRegistration` whose host maps elsewhere; the **M11** channel-create stamp
mutation (a fresh channel stamped into a default/claimed community rather than
the host's) → `Inv_HostBindingFence`/`Inv_ChannelCommunityImmutable` violated by a
2-state trace (`Init → CreateChannel(hostB stamps commA)`); the **M12** feed
global-admission mutation (re-keying the `ReadHostFeedRows` admission guard from
same-community `IsAdmitted(c, a)` to relay-global `GloballyAdmitted(a)`) →
`Inv_AdmissionFence` violated by a 3-state trace
(`Init → AdmitMember(commB, alice) → ReadHostFeedRows(hostA)`), so an actor
admitted only in B cannot read A's no-`#h` feed; and the **M13** aux
global-admission mutation (the same guard re-key on `ReadHostAuxRows`) →
`Inv_AdmissionFence` violated by a 3-state trace
(`Init → AdmitMember(commB, alice) → ReadHostAuxRows(hostA)`). M10–M13 confirm the
open-AUTH/create/feed/aux fences are load-bearing, not decorative — the same
"every new conjunct earns a confirmed red" contract as M1–M9. (To reproduce M12/M13,
the substitution that trips `Inv_AdmissionFence` is the action's admission *guard*
(`IsAdmitted(c, a)` → `GloballyAdmitted(a)` in `ReadHostFeedRows`/`ReadHostAuxRows`),
not the row-set helper alone, since the invariant quantifies over the recorded
`feedReads`/`auxReads` witnesses rather than the returned row set — the `.tla`
helper comments call this out.) The host-fence and new-surface
figures above are counterexample **trace lengths** (the error-trace state count),
which unlike TLC's run-dependent "depth of complete graph search" total are
reproducible from the printed error trace. The
`h`-tag mutation is the same shape (I2). The config is deliberately a
fast non-vacuity harness, not the full deployment scale — widening workers,
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
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
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
a client-claimed one, and its exists-trace witness
`executable_open_auth_registration` (5 steps) proves a legitimate open-community
registration is producible, so the confinement lemma is non-vacuous. See
§Authorization soundness for the
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.
**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
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
action labels; the substantive security claim is carried by the corresponding
rule design and mutation (for example, `MUTATION_Use_Token_Claimed_Community`
falsifies `token_confinement` when authorization is rewritten to use a claimed
community, `MUTATION_Use_Token_ChannelLess_Ignore_Host` falsifies
`channelless_use_confined_to_host_community` when the relay reads the token
stamp instead of the host binding, and `MUTATION_Use_Token_Ignore_Host`
falsifies `channelbearing_use_agrees_with_host` when the relay resolves a
channel-bearing op from the channel mapping while ignoring the host).
**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_audit_splice_attempt_is_not_append`), or signed-preimage
unification (`system_event_acceptance_requires_same_community_key_or_compromise`).
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.
## Implementation Correspondence
The model's obligations map to concrete code seams:
- **P-RESOLVE / I2** — `resolve(channel_id)` must be the *only* source of
`ctx.community_id`; the `h` tag is never written into tenancy. Today there is no
community layer; `channel_id` is the only locality.
- **P-RESOLVE (immutability) / S2** — `channels.community_id` must be immutable
after insert. No migration may `UPDATE channels SET community_id = …`,
`ALTER TABLE channels … community_id …`, or drop-and-recreate the column without
an explicit re-admission of P-RESOLVE and re-verification of S1/S2. This is the
load-bearing assumption behind S2's trace-level mint-rejection (a retag-then-
replay breaks it) and behind the TLA `ChannelCommunity` CONSTANT; it is
invisible to both the labeling invariant and the Tamarin lemmas (the proofs
would silently weaken, not fail), so it is enforced by a migration lint — the
same gate-on-the-migration class as the C2.1 composite-index and C2.4
`RelayInfo::build` signature lints.
- **I1 / I4** — every DB entry point takes `TenantContext` and `SET LOCAL
app.community_id`; the unscoped `get_accessible_channel_ids()`
(`crates/buzz-db/src/channel.rs:545-560`, which unions every open channel in the
DB) must not exist in any tenant-scoped path. RLS is the backstop.
- **C2.1 / A-RLS-5** — the message-uniqueness constraint must be composite over
`(community_id, …, id)`, never `UNIQUE (id)` alone. This is the closure for the
existence-oracle (M3 goes red at depth 3 under a global key). It is one bad
migration away from breaking and is invisible to the labeling invariant, so it
is enforced by the conformance schema assertion (§Conformance: "every unique/FK
constraint includes `community_id`") — the same gate-on-the-migration class as
the C2.4 `RelayInfo::build` signature lint.
- **S3 / S4** — the relay keypair becomes a per-community signing key
(`communities.signing_key`), distinct from relay-instance identity; the single
global audit chain (`crates/buzz-audit/src/service.rs`) becomes N per-community
chains `AuditEntry(community, seq, prev, hash)`.
- **P3 / S2** — the NIP-98 mint freshness obligation the Tamarin model abstracts
as a fresh `~time` nonce is carried by two code seams: the ±60s window in
`crates/buzz-auth/src/nip98.rs:77-83` and the event-id seen-set
`check_nip98_replay` in `crates/buzz-relay/src/api/bridge.rs:76-94`, called
before every mint (`bridge.rs:181`, `:254`, `:514`). The seen-set
(`state.nip98_seen`, `state.rs:249`/`:407`) is the structural analog of the
model's nonce: it makes a replayed mint within the window non-fresh, so the
implementation matches the "every mint is structurally unique" world the model
proves S2 in. This correspondence is deployment-conditional: today's in-process
moka cache carries P3 for the chart default (`replicaCount: 1`) and for any
deployment that routes all mints for the same event id to the same pod, but the
shipped HA examples (`replicaCount: 3`) do **not** carry P3 as shipped because
there is no sticky routing and no shared seen-set. HA conformance requires a
Redis/shared-store seen-set with atomic insert-if-absent and TTL ≥ 120 s
(recommended), or a header-stable sticky-routing layer — see §Conformance (P3)
for the two operator options and the caveats on the routing workaround.
- **C2.2** — the client-facing error path must map all DB errors to a fixed
sanitized alphabet; no `sqlx::Error::to_string()` reaches a tenant connection.
- **C2.4** — the NIP-11 builder `RelayInfo::build`
(`crates/buzz-relay/src/nip11.rs:122`) must keep its relay-static-only signature
(no `&PgPool`, no tenant context, no audit service); a signature lint enforces
the typed-input fence on the unauthenticated `/` surface.
- **P-RESOLVE-HOST / row-zero conformance** — every externally reachable
relay-global surface consumes the host-derived `TenantContext` before reading
or mutating tenant data. This is the implementation seam for NIP-11/community
relay identity, NIP-98/API-token REST calls, media upload/serve, git Smart
HTTP, workflow webhooks/schedules/manual triggers, search, presence, and Redis
fan-out. Tokens, signed NIP-98 `u` URLs, webhook ids, workflow ids, repo names,
media hashes, and event ids are subordinate names; none may select a community
that disagrees with the request host.
- **NIP-11 / S3** — tenant-observable relay identity is per-community. Static
software/version fields may be operator-global, but `self`/relay-signed group,
membership, audit, and system events use the community signing key. The
unauthenticated info path may reveal facts about the addressed host/community
only; unknown hosts fail closed generically rather than returning another
community's info document.
- **API tokens / P3** — `api_tokens` is a community-scoped namespace. Token hash
lookup, channel claims, scopes, revocation, and NIP-98 replay checks are
evaluated under `(community_id, token_hash/event_id)`. HA deployments require a
shared atomic seen-set keyed by community and NIP-98 event id, or an explicitly
admitted sticky/single-replica deployment; otherwise S2's freshness premise is
not carried in production.
- **Search / C2.1** — the Postgres FTS index (the `events.search_tsv` generated
column, backed by a GIN index) is shared infrastructure, not a shared result
space. Searchable rows carry `community_id`, and every search query filters by
`community_id` so the FTS predicate is BitmapAnd-ed with the community-leading
btree filters; a hit never crosses tenants and refetch by hit id is
`(community_id, event_id)`. The channel-less scope (`ChannelScope::ChannelLessOnly`,
formerly the `__global__` sentinel) means channel-less within one community,
never operator-global.
- **Redis / subscription refinement** — Redis pub/sub keys, presence keys, typing
keys, cache invalidation channels, and local-echo dedup labels include
community context in any shared multi-tenant deployment. The safe shape is
`buzz:{community}:channel:{channel_id}`,
`buzz:{community}:presence:{pubkey}`, and
`buzz:{community}:typing:{channel_id}`. The current unprefixed keys are
admissible only for the degenerate single-community deployment or physically
isolated Redis.
- **Media / Blossom** — raw blob bytes may remain content-addressed and
operator-deduplicated, but descriptors, upload authorization, quotas, audit
rows, and any future read policy are community-scoped. A media hash collision or
pre-existing blob in another community must not become an existence oracle via
metadata, status code, quota accounting, or audit output.
- **Git / NIP-34** — git Smart HTTP resolves the repository namespace from the
host-derived community before consulting owner/repo names, branch protection,
NIP-34 repo announcements, manifests, or object-store pointers. Pointer keys
include community (for example `repos/{community}/{owner}/{repo}/pointer`);
pack/object CAS may be shared only below community-scoped refs/manifests and
authorization metadata.
- **Workflows / system events** — workflow definitions, runs, approval hashes,
webhook/manual trigger routes, cron scheduling, and relay-signed workflow events
inherit `community_id`. A workflow id or approval token hash alone is never a
lookup key. Trigger evaluation sees events in the same community only, and
schedule coordination must preserve that label across pods.
- **Relay membership / pubkey admission** — relay membership, pubkey allowlist,
and archived identities are community-global admission facts. The portable
value is the pubkey; the stored membership/archive fact is
`(community_id, pubkey, ...)`. No deployment-global user gate is
tenant-observable unless it is modeled as a separate operator surface. This is
no longer asserted-only: the `(community_id, pubkey)` admission key and the
*absence* of a deployment-global gate are both mechanized. TLA+ carries the
allowlist as the `admittedMembers` relation
(`MultiTenantRelay.tla:149`), keyed on `[community, actor]`; `IsAdmitted(c, a)`
(`:317`) gates `AddMembership` and every channel-less read, and
`Inv_AdmissionFence` proves no membership or channel-less read capability
survives that is not same-community-admitted (Theorem I5). The
deployment-global gate is exactly mutation M9: replacing `IsAdmitted(c, a)`
with the any-community `AdmittedInAnyCommunity(a)` (`:324`) makes the model go
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
`nip43_admission_confined_to_signing_community` proves B's signing key can
never admit a pubkey into A (Theorem S7).
### Subscription-pipeline abstraction
The mechanized models abstract one structural seam: the **subscription
pipeline** (`REQ → register → match → fan-out → access-filter → EVENT/EOSE`).
The TLA+ isolation model represents this pipeline as the synchronous `Read*`
actions, indexed by `(worker, actor, community, channel)`; it has no
`sub_id`, no `Register`, no `Match`, no `FanOut`, no `EOSE`, no filter state.
This is sound — the model proves `Inv_LabelPropagation` over the **aggregate**
row-set delivered to a B-scoped worker, and the prose observational interface
(§The typed observational interface) presents the same property over
**per-sub streams**. The refinement from aggregate to per-stream is *coarser
than the interface, not wrong* — but it is not mechanized, and it is closed
here, by code-fence and obligation, against the implementation.
**Governing rule.** Every observation kind enumerated in §The typed
observational interface must either (i) be discharged by a TLA+ invariant or
Tamarin lemma, or (ii) appear by name in this subsection with a code-fence
and a closure obligation. New observation kinds added to §The typed
observational interface require a new entry here in the same commit. This
rule is what surfaced F1 (A_HASH closure mis-attribution) and F2 (the
subscription-pipeline abstraction itself).
#### G1 — establishment (`crates/buzz-relay/src/handlers/req.rs:79-204`)
A `REQ` from a connection authenticated under pubkey *p* and token *t*
registers a subscription only after:
1. `accessible_channels ← get_accessible_channel_ids_cached(p)` (`:79`) —
the DB-derived UUID set the connection's pubkey is a member of.
2. If *t* carries a `channel_ids` claim, intersect with it (`:88-90`). This
is the one-token-one-community enforcement at the WS surface.
3. `extract_channel_id_from_filters(filters)` (`:92`, body at `:795-822`)
returns `Some(uuid)` **only if every filter pins the same `#h=<uuid>`**;
any mixed-`#h` or missing-`#h` filter yields `None`, routing the
subscription to the global indexes (tests at `:1045-1083`).
4. Channel-scoped path: if the returned `ch_id ∉ accessible_channels`,
re-confirm via `is_member` against the DB (`:112`); on `Ok(false)` or
`Err(_)` emit `CLOSED "restricted: …"` (`:127-132`).
5. Global path (`channel_id = None`): per-filter p/engram/author gates must
hold against *p* (`:144-167`); otherwise `CLOSED`.
6. Only then is `sub_registry.register_scoped(...)` called. Direct `register`
calls are confined to test setup; production subscription registration goes
through the community-scoped API in `req.rs`.
#### G2 — delivery (`crates/buzz-relay/src/handlers/event.rs:59-113`)
Every candidate from `sub_registry.fan_out` passes through
`filter_fanout_by_access` before any `send_to`. The function (`:59`) and its
doc comment (`:117-124`) state the invariant: *a registered subscription is
never sufficient for delivery — delivery always revalidates access on the
sending pod*. Three checks, in order:
- **Author-only kinds** (`:70-83`) — filter to recipients whose
`pubkey_for_conn` equals the event author.
- **Channel visibility** (`:85-97`) — `channel_visibility_cached(channel_id)`.
Non-private → pass through; `"private"` → continue. **Lookup error →
`return Vec::new()`** (`:91-96`): visibility short-circuit, fail-closed
for the whole fan-out. The cache discipline at `state.rs:560-568` caches
only `"private"`, so a stale entry can only over-restrict (≤10s), never
leak.
- **Membership** (`:99-111`) — `is_member_cached(channel_id, pubkey)` per
recipient; `Ok(false)` or `Err(_)` drops that recipient.
#### Non-mechanized obligations
The following obligations close the per-sub stream properties the TLA+
`Inv_LabelPropagation` does not reach. Each names its code-fence and the
gates (G1, G2) that carry the closure.
1. **EOSE cardinality.** The count of events preceding `O.WS.EOSE(sub_id)`
must equal `|{m ∈ messages : matches(m, F) ∧ m ∈ ResolvedScope(conn)}|`,
where `F` is the sub's declared filter set. Delivery: `req.rs:281`
(per-event `EVENT` send); EOSE emission: `req.rs:292`. Closure: G1
admits the subscription only with a `ResolvedScope(conn)`-consistent
filter set, and G2 drops any candidate not in `ResolvedScope(conn)` at
delivery; the EOSE count is therefore the sum of events that passed
both gates.
2. **EOSE → late-EVENT temporal pairing.** No `O.WS.EVENT(sub_id, …)`
delivered after the sub's EOSE may reveal state withheld by G2 during
the historical dump. Closure: G2 re-validates visibility and membership
on every live fan-out, against the same `ResolvedScope(conn)` predicate
used at EOSE time. The **primary closure is the visibility
short-circuit at `event.rs:91-96`** — a transient DB error during the
late-EVENT window returns an empty fan-out for the whole event, not a
relaxed predicate; the per-recipient membership branch at
`event.rs:107-110` is the secondary backstop.
3. **`sub_id` reuse and collisions.** The `sub_id` namespace is
**per-connection, not global**. Cross-connection collisions are
structurally impossible: `SubRegistry.subs` is keyed
`entry(conn_id).or_default().insert(sub_id, …)` (`subscription.rs:66-69`)
and every index entry stores `(conn_id, sub_id)`. Same-connection reuse
(`REQ` with `sub_id="x"` superseding a prior `sub_id="x"`) is closed by
`subscription.rs::register` calling `remove_subscription(conn_id, &sub_id)`
at `:64` before re-insert, and by the new subscription re-running G1
against the connection's current `ResolvedScope(conn)`.
## Summary
One shared Postgres, one canonical `community_id`-keyed message log, stateless
relay workers, a relational tenant-scoped control plane, and disposable
tenant-scoped projections — with isolation stated as label-flow non-interference
(TLA+), authorization soundness stated as trace lemmas under a Dolev-Yao
adversary (Tamarin), every shared logical channel enumerated and closed, and
every invariant mutation-tested. Safety is machine-checkable relative to the RLS,
crypto, and resolution axioms, each admitted per deployment by a conformance gate.