Harden WebBFF and deployment release behavior

Model fail-closed cross-replica session renewal and implement owner-fenced refresh, transient observer handling, logout fencing, and graceful shutdown. Remove chart-owned Ingress while retaining qualification-owned external routing.
2026-07-20 17:09:26 +09:00 · 2026-07-20 17:09:26 +09:00 · 414b380516
commit 414b380516
parent ffa65018ed
5 changed files with 980 additions and 136 deletions
--- a/docs/protocol/WebSessionRenewal.cfg
+++ b/docs/protocol/WebSessionRenewal.cfg
@ -0,0 +1,20 @@
+SPECIFICATION FairSpec
+
+CHECK_DEADLOCK FALSE
+
+CONSTANTS
+    Replicas = {r1, r2}
+    NoReplica = NoReplica
+    AllowTakeover = FALSE
+    AllowAmbiguousRelease = FALSE
+    ObserverDestroysOwned = FALSE
+
+INVARIANTS
+    TypeOK
+    ProviderRefreshSerialized
+    CommitIsOwnerFenced
+    ObserverPreservesOwnedRenewal
+
+PROPERTIES
+    TerminalSessionIsPermanent
+    EventuallyTerminal
--- a/docs/protocol/WebSessionRenewal.tla
+++ b/docs/protocol/WebSessionRenewal.tla
@ -0,0 +1,276 @@
+------------------------ MODULE WebSessionRenewal ------------------------
+EXTENDS Naturals, FiniteSets, TLC
+
+\* This protocol covers one WebSession refresh-token generation. Provider refresh
+\* is external and cannot observe or honor the store's ownership fence.
+
+CONSTANTS
+    Replicas, NoReplica,
+    AllowTakeover, AllowAmbiguousRelease, ObserverDestroysOwned
+
+ASSUME
+    /\ Replicas # {}
+    /\ NoReplica \notin Replicas
+    /\ AllowTakeover \in BOOLEAN
+    /\ AllowAmbiguousRelease \in BOOLEAN
+    /\ ObserverDestroysOwned \in BOOLEAN
+
+Active    == "Active"
+Renewed   == "Renewed"
+Destroyed == "Destroyed"
+SessionStates == {Active, Renewed, Destroyed}
+
+Up   == "Up"
+Down == "Down"
+ReplicaStates == {Up, Down}
+
+Idle            == "Idle"
+Submitted       == "Submitted"
+ProviderUnknown == "ProviderUnknown"
+Returned        == "Returned"
+CommitUnknown   == "CommitUnknown"
+Committed       == "Committed"
+RequestStates ==
+    {Idle, Submitted, ProviderUnknown, Returned, CommitUnknown, Committed}
+
+AccessValid   == "AccessValid"
+AccessExpired == "AccessExpired"
+AccessStates == {AccessValid, AccessExpired}
+
+NoObservation   == "NoObservation"
+UsedCurrent     == "UsedCurrent"
+Unavailable     == "Unavailable"
+ObservedSignout == "ObservedSignout"
+Observations ==
+    {NoObservation, UsedCurrent, Unavailable, ObservedSignout}
+
+VARIABLES
+    sessionState, owner, replicaState, requestState, committedBy,
+    accessState, observation, observerDestroyedOwned
+
+vars ==
+    <<sessionState, owner, replicaState, requestState, committedBy,
+      accessState, observation, observerDestroyedOwned>>
+
+Init ==
+    /\ sessionState = Active
+    /\ owner = NoReplica
+    /\ replicaState = [r \in Replicas |-> Up]
+    /\ requestState = [r \in Replicas |-> Idle]
+    /\ committedBy = NoReplica
+    /\ accessState = AccessValid
+    /\ observation = NoObservation
+    /\ observerDestroyedOwned = FALSE
+
+Acquire(r) ==
+    /\ sessionState = Active
+    /\ owner = NoReplica
+    /\ replicaState[r] = Up
+    /\ requestState[r] = Idle
+    /\ owner' = r
+    /\ UNCHANGED
+        <<sessionState, replicaState, requestState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+Submit(r) ==
+    /\ sessionState = Active
+    /\ owner = r
+    /\ replicaState[r] = Up
+    /\ requestState[r] = Idle
+    /\ requestState' = [requestState EXCEPT ![r] = Submitted]
+    /\ UNCHANGED
+        <<sessionState, owner, replicaState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+ProviderOutcomeUnknown(r) ==
+    /\ requestState[r] = Submitted
+    /\ requestState' = [requestState EXCEPT ![r] = ProviderUnknown]
+    /\ UNCHANGED
+        <<sessionState, owner, replicaState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+Return(r) ==
+    /\ requestState[r] = Submitted
+    /\ replicaState[r] = Up
+    /\ requestState' = [requestState EXCEPT ![r] = Returned]
+    /\ UNCHANGED
+        <<sessionState, owner, replicaState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+CommitOutcomeUnknown(r) ==
+    /\ sessionState = Active
+    /\ owner = r
+    /\ requestState[r] = Returned
+    /\ requestState' = [requestState EXCEPT ![r] = CommitUnknown]
+    /\ UNCHANGED
+        <<sessionState, owner, replicaState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+Commit(r) ==
+    /\ sessionState = Active
+    /\ owner = r
+    /\ requestState[r] = Returned
+    /\ sessionState' = Renewed
+    /\ owner' = NoReplica
+    /\ requestState' = [requestState EXCEPT ![r] = Committed]
+    /\ committedBy' = r
+    /\ UNCHANGED
+        <<replicaState, accessState, observation, observerDestroyedOwned>>
+
+ExpireOwnership(r) ==
+    /\ AllowTakeover
+    /\ sessionState = Active
+    /\ owner = r
+    /\ requestState[r] # Idle
+    /\ owner' = NoReplica
+    /\ UNCHANGED
+        <<sessionState, replicaState, requestState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+ReleaseAfterAmbiguousOutcome(r) ==
+    /\ AllowAmbiguousRelease
+    /\ sessionState = Active
+    /\ owner = r
+    /\ requestState[r] \in {ProviderUnknown, CommitUnknown}
+    /\ owner' = NoReplica
+    /\ UNCHANGED
+        <<sessionState, replicaState, requestState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+Crash(r) ==
+    /\ replicaState[r] = Up
+    /\ replicaState' = [replicaState EXCEPT ![r] = Down]
+    /\ UNCHANGED
+        <<sessionState, owner, requestState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+DestroyAfterOwnerCrash(r) ==
+    /\ sessionState = Active
+    /\ owner = r
+    /\ replicaState[r] = Down
+    /\ sessionState' = Destroyed
+    /\ owner' = NoReplica
+    /\ UNCHANGED
+        <<replicaState, requestState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+ConfirmRenewalFailure(r) ==
+    /\ sessionState = Active
+    /\ owner = r
+    /\ requestState[r] \in
+        {Submitted, ProviderUnknown, Returned, CommitUnknown}
+    /\ sessionState' = Destroyed
+    /\ owner' = NoReplica
+    /\ UNCHANGED
+        <<replicaState, requestState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+ExpireAccessToken ==
+    /\ sessionState = Active
+    /\ accessState = AccessValid
+    /\ accessState' = AccessExpired
+    /\ UNCHANGED
+        <<sessionState, owner, replicaState, requestState, committedBy,
+          observation, observerDestroyedOwned>>
+
+ObserveValidToken ==
+    /\ sessionState = Active
+    /\ accessState = AccessValid
+    /\ observation' = UsedCurrent
+    /\ UNCHANGED
+        <<sessionState, owner, replicaState, requestState, committedBy,
+          accessState, observerDestroyedOwned>>
+
+ObserveExpiredOwnedRenewal ==
+    /\ sessionState = Active
+    /\ accessState = AccessExpired
+    /\ owner # NoReplica
+    /\ observation' = Unavailable
+    /\ UNCHANGED
+        <<sessionState, owner, replicaState, requestState, committedBy,
+          accessState, observerDestroyedOwned>>
+
+ObserveExpiredAndDestroy ==
+    /\ sessionState = Active
+    /\ accessState = AccessExpired
+    /\ \/ owner = NoReplica
+       \/ ObserverDestroysOwned
+    /\ sessionState' = Destroyed
+    /\ owner' = NoReplica
+    /\ observation' = ObservedSignout
+    /\ observerDestroyedOwned' = (owner # NoReplica)
+    /\ UNCHANGED
+        <<replicaState, requestState, committedBy, accessState>>
+
+Logout ==
+    /\ sessionState = Active
+    /\ sessionState' = Destroyed
+    /\ owner' = NoReplica
+    /\ UNCHANGED
+        <<replicaState, requestState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+ExpireSession ==
+    /\ sessionState = Active
+    /\ sessionState' = Destroyed
+    /\ owner' = NoReplica
+    /\ UNCHANGED
+        <<replicaState, requestState, committedBy,
+          accessState, observation, observerDestroyedOwned>>
+
+Next ==
+    \/ \E r \in Replicas : Acquire(r)
+    \/ \E r \in Replicas : Submit(r)
+    \/ \E r \in Replicas : ProviderOutcomeUnknown(r)
+    \/ \E r \in Replicas : Return(r)
+    \/ \E r \in Replicas : CommitOutcomeUnknown(r)
+    \/ \E r \in Replicas : Commit(r)
+    \/ \E r \in Replicas : ExpireOwnership(r)
+    \/ \E r \in Replicas : ReleaseAfterAmbiguousOutcome(r)
+    \/ \E r \in Replicas : Crash(r)
+    \/ \E r \in Replicas : DestroyAfterOwnerCrash(r)
+    \/ \E r \in Replicas : ConfirmRenewalFailure(r)
+    \/ ExpireAccessToken
+    \/ ObserveValidToken
+    \/ ObserveExpiredOwnedRenewal
+    \/ ObserveExpiredAndDestroy
+    \/ Logout
+    \/ ExpireSession
+
+Spec == Init /\ [][Next]_vars
+FairSpec == Spec /\ WF_vars(ExpireSession)
+
+TypeOK ==
+    /\ sessionState \in SessionStates
+    /\ owner \in Replicas \cup {NoReplica}
+    /\ replicaState \in [Replicas -> ReplicaStates]
+    /\ requestState \in [Replicas -> RequestStates]
+    /\ committedBy \in Replicas \cup {NoReplica}
+    /\ accessState \in AccessStates
+    /\ observation \in Observations
+    /\ observerDestroyedOwned \in BOOLEAN
+
+SubmittedRefreshes ==
+    {r \in Replicas : requestState[r] # Idle}
+
+ProviderRefreshSerialized ==
+    Cardinality(SubmittedRefreshes) <= 1
+
+CommitIsOwnerFenced ==
+    committedBy # NoReplica =>
+        /\ sessionState = Renewed
+        /\ requestState[committedBy] = Committed
+
+ObserverPreservesOwnedRenewal ==
+    ~observerDestroyedOwned
+
+TerminalSessionAction ==
+    sessionState \in {Renewed, Destroyed} =>
+        sessionState' = sessionState
+
+TerminalSessionIsPermanent == [][TerminalSessionAction]_vars
+
+EventuallyTerminal ==
+    <>(sessionState \in {Renewed, Destroyed})
+
+=============================================================================
--- a/docs/spec/architecture.md
+++ b/docs/spec/architecture.md
@ -22,6 +22,7 @@ Terms in this glossary are stable identifiers for use across Remora documentatio
 | `WebClient` | The browser-based user interface for submitting and managing jobs. |
 | `WebBFF` | The same-origin confidential OAuth client and token-mediating backend for `WebClient`. |
 | `WebSession` | Ephemeral server-side OAuth session state addressed by an opaque browser cookie. |
+| `WebSessionProtocol` | The TLA+ specification defining distributed browser-session renewal semantics and their safety and liveness properties. |
 | `API` | The authenticated service interface for job submission, status, cancellation, history, and deletion. |
 | `Worker` | A stateless process that executes attempts and reports progress and outcomes. |
 | `IdentityProvider` | The external authority for user identity, administrative roles, and storage authorization scopes. |
@ -35,9 +36,14 @@ Terms in this glossary are stable identifiers for use across Remora documentatio

 ## Scope

-This document is authoritative for Remora's product requirements, system boundaries, major components, result representation and access contract, and allocation of responsibilities below the abstraction of `JobProtocol`. It intentionally does not define implementation-level technology choices.
+This document is authoritative for Remora's product requirements, system boundaries, major components, result representation and access contract, and allocation of responsibilities below the protocol models' abstractions. It intentionally does not define implementation-level technology choices.

-[`Remora.tla`](../protocol/Remora.tla) is the authoritative `JobProtocol`. This document references its symbols without restating their definitions or actions; where they overlap, the model controls. Concrete frameworks, libraries, wire formats, mutable API descriptions, and deployment choices are outside the scope of this specification.
+[`Remora.tla`](../protocol/Remora.tla) is the authoritative `JobProtocol`, and
+[`WebSessionRenewal.tla`](../protocol/WebSessionRenewal.tla) is the authoritative
+`WebSessionProtocol`. This document references their symbols without restating
+their definitions or actions; where they overlap, the models control. Concrete
+frameworks, libraries, wire formats, mutable API descriptions, and deployment
+choices are outside the scope of this specification.

 ## Problem Statement

@ -108,7 +114,7 @@ flowchart TD

 - `WebBFF` uses the OAuth authorization-code flow as a confidential client with Proof Key for Code Exchange and nonce validation. OAuth and OpenID Connect remain the only user-authentication path.
 - Access tokens, refresh tokens, and ID tokens remain inside `WebBFF` and its protected `WebSession` store. Browser JavaScript receives only an authorization snapshot and a CSRF value.
- The browser carries a random session identifier in a host-only `__Host-` cookie with `Secure`, `HttpOnly`, `SameSite=Strict`, and `Path=/`. Authentication creates both the session identifier and CSRF value. Token renewal rotates the identifier while retaining the CSRF value for in-flight same-session requests; an identity change invalidates the session.
+- The browser carries a random session identifier in a host-only `__Host-` cookie with `Secure`, `HttpOnly`, `SameSite=Strict`, and `Path=/`. Authentication creates both the session identifier and CSRF value. The authorization callback rotates the identifier before establishing the authenticated session. Renewal and concurrent-observer behavior refine `WebSessionProtocol`. An identity change invalidates the session.
 - `WebSession` state is stored under a deployment-specific, WebBFF-only namespace in `CoordinationStore`. Its lifetime is bounded by the provider session and token lifetimes. Loss, expiry, unreadable state, or failed renewal destroys the local session and requires authentication again.
 - Unsafe same-origin requests require the current session CSRF value in a request header. `WebBFF` also rejects unsafe requests with an absent or foreign `Origin` or a cross-site Fetch Metadata classification. SameSite cookies are defense in depth rather than the sole CSRF control.
 - Browser API requests use a same-origin BFF route. `WebBFF` removes browser credentials and forwarding headers, injects the current access token, preserves idempotency keys and response status, and never retries an unsafe application request.
@ -267,9 +273,9 @@ flowchart TD
 ## Responsibility Boundaries

 - [`docs/protocol`](../protocol/) is authoritative for distributed state and coordination semantics, including safety and liveness invariants.
- This architecture specification is authoritative for components, trust boundaries, externally visible behavior, and responsibility allocation below the model's abstraction, and must conform to `JobProtocol` where they overlap.
- Implementations may optimize storage layout but must refine `JobProtocol` behavior and preserve its linearization points.
- Mutable implementation contracts and documentation select technologies, wire shapes, and mappings from architectural components. They are not normative over `JobProtocol` or this specification.
+- This architecture specification is authoritative for components, trust boundaries, externally visible behavior, and responsibility allocation below the models' abstractions, and must conform to the applicable protocol where they overlap.
+- Implementations may optimize storage layout but must refine the applicable protocol behavior and preserve its linearization points.
+- Mutable implementation contracts and documentation select technologies, wire shapes, and mappings from architectural components. They are not normative over the protocol models or this specification.
 - Deployment configuration supplies service credentials and endpoints, configures allowed source reachability, and provides infrastructure-level egress enforcement.
 - Deployment configuration reserves and protects Remora's internal target namespace, excludes it from independent lifecycle deletion, and establishes either exclusive write ownership or immutable version addressing.
 - Deployment configuration selects secret-store topology and policies while preserving the application-level grant-bound credential-resolution contract.
--- a/docs/spec/deployment.md
+++ b/docs/spec/deployment.md
@ -40,7 +40,9 @@ application and NetworkPolicy CIDR allowances.
 Containers run non-root with read-only roots, dropped capabilities, resource
 limits, and no service links. Worker temporary storage is bounded.

-TLS ingress redirects HTTP to HTTPS and emits HSTS. The WebBFF session cookie
+The chart exposes ClusterIP Services and does not own north-south routing.
+Deployments attach Gateway API `HTTPRoute` resources outside the chart and
+enforce HTTPS redirection and HSTS at that boundary. The WebBFF session cookie
 is always `Secure`; unencrypted origins are unsupported outside loopback test
 environments.

--- a/docs/spec/testing.md
+++ b/docs/spec/testing.md
@ -34,4 +34,4 @@ Package runners may create additional namespaced fixtures and fault injectors ne

 Automated backend tests use cluster-local service discovery. Tests of Keycloak or ZITADEL issuer behavior use the `dnsPolicy` and `dnsConfig` pattern in [`fixture-consumer-sample`](../../tests/kind/sample/job.yaml.in) so discovery URLs and token issuers have one identity from every participating pod.

-Port forwarding is for interactive diagnostics only and is not an acceptance-test transport. Ingress is introduced by deployment and system qualification, where routing is itself under test; substrate test components do not install an ingress controller merely to reach fixture services.
+Port forwarding is for interactive diagnostics only and is not an acceptance-test transport. System qualification owns an external routing fixture around the chart Services; substrate test components do not install a routing controller merely to reach fixture services.