WebUI Protected Ingress Lanes Proposal

The capOS-served remote-session-web-ui service admits every accepted connection through one pre-identity ledger of record (WebUiIngressLedger in demos/remote-session-web-ui/src/lib.rs). That ledger already models an anonymous public lane and a protected reserve, but the live serve loop feeds only the anonymous lane, because the service has exactly one listener capability and no transport provenance from which to select a protected admission. This document selects the concrete topology that gives protected authority its own non-forgeable provenance and defines the accounting invariants that keep the three lanes separate and independently abuse-bounded.

This is an accepted design record, not an implementation: it is the selected production direction for the WebUI ingress lanes. The topology and invariants gate the follow-up implementation tasks listed at the end; no protected lane is fed by the live serve loop today.

It is cross-linked from Remote Session UI Security (the parent web-security posture, whose “Health and recovery admission” and “Auth-endpoint rate limiting and lockout” sections state the lane requirement this document makes concrete), the Resource Governance taxonomy (the accepted current-state authority for ingress accounting), and the Cloud Deployment proposal (which owns the provider-terminated public ingress the public lane sits behind).

Problem

Behind a provider load balancer many browsers collapse onto one backend peer address, forwarded headers are trustworthy only from an explicitly admitted proxy range, and any internet client can request any public path, including GET /healthz. Therefore:

• The public /healthz route is anonymous input and cannot stand in for a protected health authority. Its route name must not select protected capacity.
• A shared peer address, a Host/Origin/X-Forwarded-* header, or a request path is a caller-supplied signal, not authority. Selecting a protected lane from any of them is forgeable and is rejected by this design.
• Local recovery/setup progress and a cloud provider’s liveness probe both need bounded, deterministic progress that ordinary public traffic — including a /healthz flood — can never consume. Deterministic progress requires distinguishable authority.

The failure mode this design forecloses is inferring protected authority from shared peer identity or ordinary public traffic, then granting it protected reserve capacity.

Selected Topology: One Listener Capability Per Lane

The lane an admission belongs to is a property of which listener capability accepted the connection, resolved at accept time before any request bytes are parsed. The service holds one distinct TcpListenAuthority capability per lane, each named in its boot CapSet and each reachable only over a transport the other lanes’ clients cannot reach:

Each listener capability is minted to the service from the manifest, exactly as ui_listener is today (capset.get_client(b"ui_listener") in demos/remote-session-web-ui/src/main.rs). A lane whose listener capability is absent from the CapSet is simply not served: the service binds and accepts only the lanes it was granted, and a manifest that authors no protected listener gets today’s anonymous-only behavior byte-for-byte. This makes protected authority additive and fail-closed — absence of the capability is absence of the lane, never a silent downgrade of a public admission into a protected one.

Distinct-object binding is mandatory, not implied by distinct names

Distinct CapSet names do not by themselves prove distinct authority: a manifest that aliases one endpoint or one underlying listener object under two names would let a public connection accepted on the shared object be labeled protected, defeating the whole design. The lane labeling therefore fails closed on ambiguous grants. Two enforcement points, both required:

• Manifest construction invariant. The public, local-health, and provider-health listener grants must resolve to structurally distinct listener/transport objects bound to distinct transports. A manifest that binds two lane listeners to the same object, port, or endpoint is invalid.
• Boot-time distinct-object check. At startup, before accepting on any lane, the service verifies that the granted lane listeners are pairwise distinct objects (distinct capability identity, not merely distinct names) and refuses to serve — failing the boot closed with a diagnostic — on a duplicate or ambiguous grant. A lane is served only after its listener is proven distinct from every other served lane’s listener.

This mechanical check is what turns “distinct listener capability” into a non-forgeable selector rather than a naming convention. It is asserted by proof 1 (positive lane selection) and, in its negative form, by an aliased-grant refusal added to the proof matrix.

Why capability provenance, not port-in-header or path

The provenance is the accepted socket’s originating listener capability, which the service resolves locally. It is not a port number echoed in a header, a forwarded original-destination field, or a path prefix — all of which cross the public frontend and are attacker-controlled. A distinct kernel-minted TcpListenAuthority cannot be forged by a public client because the public client never holds it and never reaches the transport it fronts. This is the “non-bypassable listener/transport provenance” the resource-governance admission rule requires (rule 2 in Resource Governance).

Rejected alternatives

• Single listener, lane inferred from request path/header/peer. Rejected: every selector crosses the load balancer and is forgeable; a /healthz or X-Forwarded-For flood would reach protected reserve. This is the exact ambiguous shared-peer inference the task forbids.
• Single listener, lane inferred from source CIDR. Rejected as the sole selector: a CIDR is defense-in-depth and a reachability restriction, not authority (Resource Governance, “Identity and Pre-Authentication Work”). It may narrow who can reach a protected listener, but it does not select the lane. Behind a shared LB peer it collapses entirely.
• One listener, protected requests carry a shared secret/bearer token. Not selected for this iteration: it introduces a pre-identity secret to custody, compare in constant time, and rotate, and still shares the anonymous lane’s accept/parse budget. A distinct transport is simpler and strictly fail-closed. A reviewed upstream admission token remains the documented path for deterministic remote guarantees beyond a local transport, but it is a separately reviewed trust boundary, not this lane-selection mechanism.

Per-Lane Accounting Invariants

All three lanes share the one process-lifetime WebUiIngressLedger, so a single min(structural, quota)-validated IngressProfile still bounds aggregate memory. Each lane draws its slots from a lane-private reserve carved from that profile; opportunistic borrowing never crosses into a protected reserve. The invariants below are stated per lane using the existing ledger vocabulary (request → move-only IngressReservation → complete/cancel, typed IngressOverload → 429/503).

Charge (admission)

• Public anonymous. Charge TCP accept, request parsing, failed-cookie rejection, unauthenticated response bytes, and /healthz before any identity is read, against the anonymous lane’s IngressFootprint (worst-case in-flight request + retained response bytes). This is today’s live behavior (charge_ingress_admission requests IngressLane::Anonymous). A successful later login never retroactively charges already-spent anonymous work to the resulting session (the separate SessionBudgetLedger owns post-auth credit).
• Local health / recovery. Charge against a lane-private reserve the anonymous lane can never consume. Recovery/setup work is admitted here only because it arrived on the local listener capability, giving it a deterministic progress bound the public lane cannot.
• Provider health. Charge a small fixed footprint sized for a bounded liveness probe (status line + tiny body). The provider-health footprint is deliberately minimal; this lane performs no login, no session lookup, and no recovery, so it never touches the credential-hash path.

Zero-footprint admission is invalid on every lane: a lane whose effective capacity would read zero fails the profile validation closed (IngressProfileError), never silently as one or unbounded.

Lane-specific route/method allowlist (fail-closed dispatch). Passing the resolved lane to charge_ingress_admission is necessary but not sufficient: the footprint and abuse claims above hold only if a connection admitted on a protected lane cannot reach the general request handler and request a large asset or a login route. The lane therefore selects, in the single route descriptor table, a bounded per-lane operation allowlist; a request outside the lane’s allowlist is a bounded typed denial, not a fall-through to the common handler. Concretely:

• The provider-health lane serves only the bounded health handler (the minimal liveness response). Login, session, asset-bundle, ACME, and manual routes are not in its allowlist and fail closed; the lane thus structurally cannot reach the credential-hash path or an asset that would undercharge its fixed footprint.
• The local-health/recovery lane serves only the bounded recovery/setup and local-status operations, with its own explicit allowlist; public application and asset routes are not in it.
• The public anonymous lane keeps today’s full public route set (HTML, static assets, JSON API, /healthz, ACME http-01).

Route descriptors default to denial, so a route absent from a lane’s allowlist is denied without special-casing. This is asserted by a per-lane route-scope negative in the proof matrix.

Deadline

Every admitted ticket carries one absolute deadline set from the monotonic clock at admission and preserved across partial progress and retry (the ledger already rejects a request already at or past its deadline with DeadlineExceeded → 503). A lost clock fails admission closed on every lane, exactly as the live serve loop’s other clock reads do.

• Public anonymous deadlines are the ordinary bounded serve deadline; no lane gets a longer deadline by virtue of being protected.
• Local health / recovery keeps the same absolute-deadline discipline; its determinism comes from reserved capacity and distinguishable authority, not from an unbounded or longer deadline.
• Provider health uses a short deadline matched to a liveness probe; a probe that cannot complete promptly is refused rather than parked.

Dispatch (selection)

The ledger’s select_next is a work-conserving fair arbiter over admitted-but- undispatched tickets. The slot pool is partitioned so that non-starvation is structural — enforced by admission arithmetic — rather than by a revocation or preemption mechanism the ledger does not have.

Slot partition (no borrowing across a private reserve). The effective application slots split into one private reserve per protected lane plus a shared general pool:

general_pool = effective_application_slots - sum(all protected-lane reserves)

• Each protected lane’s own admissions draw first from that lane’s private reserve, then from the general pool.
• Anonymous admissions and any opportunistic protected borrowing draw only from the general pool, never from any lane’s private reserve.
• A private reserve is therefore never consumed by another lane: it is not “revocable-borrow-only,” it is simply not borrowable. IngressProfile::validate fails closed unless sum(reserves) < effective_application_slots (the generalized ReserveLeavesNoAnonymousCapacity check), so the general pool is always non-empty and every protected lane retains its floor no matter how the other lanes or the anonymous lane load the general pool.
• Every enabled protected lane must have a non-zero reserve. A reserve of zero is valid only for a lane that is disabled (its listener capability ungranted). An enabled protected lane with a zero reserve would rely entirely on the contested general pool and have no deterministic progress floor — defeating the reason it is protected — so validate fails closed on an enabled lane whose reserve is zero. This keeps “deterministic protected progress” honest: a lane advertised as protected always has a floor the general-pool contention cannot erase.

This makes cross-protected-lane non-starvation a counting invariant: lane A saturating the general pool cannot touch lane B’s reserve, so lane B always reaches its reserved floor. Deterministic protected progress rests on this counting property, not on preempting an in-flight reservation.

Cross-lane arbitration. When several lanes have ready tickets competing for general-pool slots, selection is deterministic and starvation-free:

• A lane with an unused private-reserve slot dispatches from its own reserve first; that dispatch never competes for the general pool.
• Contention for the general pool is resolved by the work-conserving fair, aging/arrival-aware arbiter across all lanes with ready general-pool tickets — not a fixed lane priority, so no lane (protected or anonymous) can indefinitely starve another’s general-pool progress. Queue position and reconnect churn confer no privilege (Resource Governance honest contract).
• Within a lane, selection is fair and aging/arrival-aware.

Current state. In the live loop every admitted ticket owns a serving slot at admission time (admission only when a slot is free), so there is no pending-over-slots queue yet and select_next is inert; the partition and cross-lane arbitration become load-bearing only once the accepted-socket lifecycle decouples admission from an immediately owned slot (the webui-accepted-socket-lifecycle-no-global-quiesce dependency).

Release

Every IngressReservation is move-only and released exactly once on its issuing ledger — on complete for a fully served response or cancel for timeout, cancellation, close, or error — and completed + cancelled == admitted holds as a ledger identity. This is lane-independent: the reservation records its lane, and releasing on the wrong ledger is a debug-asserted no-op, so a protected release can never remove a like-numbered anonymous ticket or desynchronize byte accounting. The single structural release site the live serve loop already relies on (Progress::Finished slot-clear) extends unchanged to protected lanes: each protected connection holds its reservation for its lifetime and releases at the same one site.

Overload

Overload is per lane and typed, never authentication:

• Lane-pool / per-connection saturation → 429. A lane’s own slot pool full (LanePoolFull) or one connection over its per-connection bound (PerConnectionLimit) is the caller doing too much on that lane.
• Aggregate / byte-budget / deadline exhaustion → 503. The shared aggregate backstop, the shared in-flight byte budget, or an expired deadline is the service temporarily out of admitted capacity.
• Protected non-escalation. Anonymous-lane saturation returns anonymous overloads and can never convert into consumption of a protected reserve: a 429/503 on the public lane leaves the local-health and provider-health reserves untouched by construction, because the anonymous lane’s effective ceiling excludes those reserves.
• Provider-health / local-health abuse. Occupancy, in-flight bytes, and absolute deadlines bound concurrent work, and denial on a protected lane is a fixed-size counter bump, not a per-attempt record. Concurrency bounds alone do not bound cumulative work: a peer that can reach a protected listener and complete short requests back to back would otherwise consume unbounded cumulative CPU/network over time. Each protected lane therefore also carries a bounded, replenishable per-lane accept/request rate budget (a token ledger refilled at a fixed rate); a request over the current budget is a bounded typed overload (429), not queued work. This is what backs the claim that a protected lane cannot be turned into an amplifier or an unbounded work source; the abuse proof asserts both the occupancy bound and the sustained-rate bound. Where a lane’s reachability makes a sustained-rate budget unnecessary (for example a strictly loopback-only local lane), the design records that the claim there is occupancy/deadline-bounded only, rather than implying a rate bound it does not enforce.

Saturation is observable through the bounded fixed-size IngressCounters (admitted_anonymous, admitted_protected, the overload_* family, completed, cancelled, high_water_slots); the design adds per-protected- lane admit/overload counters so provider-health and local-health saturation are independently visible in the quiescent evidence line.

Mapping to Current Manifest Profiles and Serve-Loop Symbols

• Ledger and profile. WebUiIngressLedger, IngressProfile, IngressLane, IngressFootprint, IngressOverload, IngressReservation, IngressCounters in demos/remote-session-web-ui/src/lib.rs. Today IngressLane has Anonymous and ProtectedControl; this design splits the protected side into two lanes — local-health/recovery and provider-health — each with its own reserve field, replacing the single protected_reserve_slots with per-lane reserves while preserving the ReserveLeavesNoAnonymousCapacity fail-closed check against the sum of reserves.
• Live profile. WEB_UI_LIVE_INGRESS_PROFILE and INGRESS_PROFILE / WEB_UI_CONNECTION_SLOTS in demos/remote-session-web-ui/src/main.rs. The live profile currently forces protected_reserve_slots = 0 precisely because no listener can feed a protected lane; introducing the distinct listeners is what lets the reserve be restored (the doc comment at WEB_UI_LIVE_INGRESS_PROFILE already records this as the restore condition).
• Admission site. charge_ingress_admission requests IngressLane::Anonymous for every connection. The implementation follow-up passes the lane resolved from the accepting listener capability instead of a hard-coded Anonymous, and it is the only place a lane is chosen.
• Manifest policy. The ingress_* inert-Endpoint marker caps parsed in evaluate_service_capset_policy (per webui-ingress-manifest-profile-binding, done) select the policy quotas over the code’s fixed structural maxima. This design adds per-lane reserve markers (e.g. ingress_local_health_reserve, ingress_provider_health_reserve) so an operator tightens or enlarges a protected reserve within the pool without recompiling, with the same fail-closed validation and boot readback. The structural maxima stay code-owned and non-manifest-tunable.
• CapSet listener grant. capset.get_client(b"ui_listener") extends to the proposed ui_local_listener and ui_provider_health_listener names; each is optional, and its absence disables exactly that lane.
• Deployment surface. The public listener sits behind the provider-terminated HTTPS ingress owned by Cloud Deployment; the local and provider- health listeners are bound to transports the public frontend does not route to (loopback/admin interface for local; an out-of-band probe port for provider health).

Deployment Consequences

• The public frontend / LB target group routes only the public listener’s port. The provider-health probe target and the local admin origin are configured out of band and are never members of the public routable set; otherwise the distinct-transport guarantee collapses and the design’s core invariant is void.
• A provider whose health check can only reach the public LB port does not get a protected lane — it consumes anonymous /healthz like any other client, and that is the honest, documented outcome. A protected provider-health lane exists only when the provider probe can be pointed at the distinct transport.
• Firewall/security-group rules restrict the local and provider-health transports to their intended origins as defense in depth; that restriction is reachability narrowing, not the lane selector.
• No TLS key or certificate material, provider resource id, public address, or firewall rule name is emitted as browser-readable state or in any local/QEMU proof evidence line, consistent with the existing web-ui secret-handling contract.

QEMU and Deployment Proofs

The following proofs gate the implementation follow-ups. They extend the existing make run-cloud-prod-remote-session-web-ui-l4 L4 harness and the host-tested ledger, and each must be a real assertion, not an observed is_err():

1. Lane selection by provenance (positive). With all three listener capabilities granted, a connection accepted on each listener is charged to the matching lane; the quiescent kernel evidence line reports non-zero admitted on each lane it was fed. Proven in QEMU by driving the local and provider-health listeners from in-guest clients on their distinct transports.
2. Public-lane non-escalation (negative). A /healthz flood and a concurrent asset-connection flood on the public listener drive anonymous 429/503, and the evidence line shows the local-health and provider-health reserves were never admitted into (admitted_local_health = 0, admitted_provider_health = 0) while the anonymous lane saturated. This is the core abuse proof: public saturation cannot reach protected reserve.
3. Protected-lane abuse bound. A flood on each protected listener returns that lane’s own typed overload and bumps only its fixed counters. A rate-budgeted lane does not grow unbounded cumulative work; a rate-exempt strictly-loopback lane bounds only concurrent work (occupancy / deadline), and its cumulative work is bounded by the trusted local origin that is the only thing able to reach it, not by the lane — which is why the rate exemption is admissible only for such a lane. It does not starve the other protected lane’s reserved floor, and — since protected admissions may use the shared general pool — the anonymous lane keeps fair, starvation-free general-pool progress under the arbitration contract, not zero impact. Asserts the concurrency bound (occupancy / in-flight bytes / deadline, plus the per-connection bound on the protected listener); for a lane whose configured policy carries a sustained-rate budget, also asserts the sustained-rate bound (back-to-back short requests over the per-lane rate budget return 429 rather than doing unbounded cumulative work). For a lane explicitly exempted from the rate budget (a strictly loopback local lane), this proof asserts only the occupancy / deadline bounds, matching the exemption recorded in the overload section.
4. Route-scope negative. A connection admitted on a protected listener that requests a route outside that lane’s allowlist (a login, asset-bundle, or large route on the provider-health lane) receives a bounded typed denial and never reaches the common handler or the credential-hash path.
5. Absent-authority and aliased-grant fail-closed. A manifest that grants no protected listener capability boots byte-identically to today’s anonymous-only service (no protected lane bound, admitted_protected* stay zero). A manifest that aliases two lane listeners onto the same object/port is refused at the boot-time distinct-object check with a diagnostic — proving absence or ambiguity of authority is absence of the lane, never a silent protected admission.
6. Forgery negative. A public-listener request bearing a crafted Host/Origin/X-Forwarded-*/path that names the protected port or route is charged to the anonymous lane and never selects a protected reserve — asserting the selector is the accepting capability, not any request field.
7. Release balance across lanes. Mixed public + protected load reaches a quiescent completed + cancelled == admitted, outstanding == 0, release_balanced = true evidence line, extending the existing exact-once release assertion to the multi-lane case.

Deployment proof (separately authorized, no unattended spend): once a distinct provider-health transport is authorized in the cloud posture, a live proof that the provider probe reaches the provider-health listener while the public LB port serves anonymous traffic, and that the public port cannot reach the provider-health lane. This depends on the on-hold cloud-gce-public-self-hosted-webui-ingress-tls authorization and is not part of the local design/proof scope.

Follow-Up Implementation Tasks

These are the implementation slices this design gates. They are recorded here with proposed dependencies and conflict domains; task creation with the operator-owned ready control fields (hazards, validation, write_scope) is an operator step.

1. webui-multi-lane-ingress-listeners (behavior). Split IngressLane into Anonymous, LocalHealth, ProviderHealth; replace the single protected reserve with per-lane reserves, the generalized sum(reserves) < effective_slots validation plus the enabled-lane-needs-non-zero-reserve check, and the general-pool/private-reserve admission arithmetic; add the boot-time distinct-object listener check (fail closed on an aliased/ambiguous grant); resolve the lane from the accepting listener capability in charge_ingress_admission; bind the distinct ui_local_listener / ui_provider_health_listener CapSet grants; add the per-lane route/method allowlist in the route descriptor table and the per-lane accept/request rate budget; add per-lane counters and evidence fields.
   • Depends on: webui-ingress-ledger-live-serve-loop-wiring (done, live anonymous ledger), webui-accepted-socket-lifecycle-no-global-quiesce (on-hold — needed for real per-lane dispatch over slots).
   • Conflict domains: path:demos/remote-session-web-ui/src/lib.rs, path:demos/remote-session-web-ui/src/main.rs, resource:web-ui-ingress-ledger.
2. webui-multi-lane-manifest-reserves (behavior). Add the per-lane reserve ingress_* marker caps and their fail-closed resolution/readback; extend the manifest profiles for the focused and cloudboot manifests.
   • Depends on: task 1, webui-ingress-manifest-profile-binding (done).
   • Conflict domains: path:demos/remote-session-web-ui/src/main.rs, path:schema/capos.capnp (if a marker shape changes), resource:web-ui-manifest-ingress-policy.
3. webui-multi-lane-abuse-proof-matrix (behavior / harness-hardening). Implement proofs 1–7 above over the L4 harness and host tests, including the route-scope, aliased-grant, public non-escalation, and forgery negatives.
   • Depends on: tasks 1 and 2.
   • Conflict domains: path:tools/qemu-remote-session-self-served-ui-harness.sh (the L4 assertion harness), path:demos/remote-session-web-ui/src/lib.rs (host tests), resource:web-ui-l4-proof.
4. webui-provider-health-deployment-proof (behavior, separately authorized). The live provider-health-transport deployment proof.
   • Depends on: tasks 1–3, cloud-gce-public-self-hosted-webui-ingress-tls (on-hold, operator authorization).
   • Conflict domains: resource:cloud-gce-public-webui-ingress.

The related on-hold sibling behavior tasks webui-independent-browser-sessions, webui-accepted-socket-lifecycle-no-global-quiesce, and remote-session-gateway-concurrent-admission-deadlines remain prerequisites for the load-bearing multi-lane dispatch and concurrency-above-four throughput proofs; this design does not unblock them.

Design Grounding

• Resource Governance — the accepted ingress-accounting taxonomy, the admission-order rule requiring non-bypassable transport provenance for a protected reserve, and the current WebUI enforcement matrix.
• Remote Session UI Security — the parent web-security posture; its “Health and recovery admission” and “Auth-endpoint rate limiting and lockout” sections state the requirement this document makes concrete.
• Cloud Deployment — owns the provider-terminated public ingress and the deployment surface the public lane sits behind.
• demos/remote-session-web-ui/src/lib.rs and src/main.rs — the live ledger, profile, and serve-loop admission site the design maps onto.

Relevant Research

• Capability Systems Survey — the cross-system grounding for selecting authority by an unforgeable capability (the accepting listener object) rather than by an ambient, caller-supplied signal, which is the core of this design’s lane selector.

No other docs/research/ file applies. The remaining design content — HTTP overload semantics (429/503), load-balancer peer/forwarded-header trust, and per-lane admission accounting — is grounded in the accepted in-tree taxonomy (Resource Governance) and the existing implemented ledger, not in an external-system report, so no further external-design grounding is required.