Select multi-process SC architecture and align protocol model
Promote Host Coordinator + Runtime Supervisor + attached runsc as the product architecture in the specification, and extend the TLA+ model with generation-scoped identities, multi-role durable intent, network readiness, prepared-lower lease, and connectivity-helper ownership. TLC-checked; trim product prose that the model now owns.
This commit is contained in:
parent
697aada29e
commit
518c0ad531
1 changed files with 614 additions and 246 deletions
|
|
@ -1,12 +1,18 @@
|
|||
# Lazaret Specification
|
||||
|
||||
This document is the normative product specification for Lazaret. It defines the
|
||||
problem, stable vocabulary, architecture, and requirements. The
|
||||
[TLA+ application protocol model](protocol/Lazaret.tla) defines lifecycle and
|
||||
communication semantics. Current implementation strategy, experimental results,
|
||||
and historical rationale live in the development journal (local checkout:
|
||||
[journal index](journal/00_INDEX.md), including the
|
||||
[implementation plan](journal/implementation-plan.md)).
|
||||
This document is the normative product specification for Lazaret.
|
||||
|
||||
### Document authority
|
||||
|
||||
| Document | Authoritative for |
|
||||
| :--- | :--- |
|
||||
| This specification | Product north star, trust model, stable vocabulary and identifiers, below-abstraction architecture, and product requirements |
|
||||
| [TLA+ application protocol model](protocol/Lazaret.tla) and [TLC config](protocol/Lazaret.cfg) | Protocol lifecycle, communication semantics, publication, registration, escalation, recovery, and checked invariants |
|
||||
| Development journal | Implementation strategy, experiments, and historical rationale (local checkout: [journal index](journal/00_INDEX.md), [implementation plan](journal/implementation-plan.md)) |
|
||||
|
||||
This specification does **not** restate the protocol state machine. If a product
|
||||
requirement needs a protocol rule the model does not yet express, either extend
|
||||
the model or state that the requirement is outside the current model abstraction.
|
||||
|
||||
## 1. Problem Statement
|
||||
|
||||
|
|
@ -32,9 +38,11 @@ human-in-the-loop host escalation path.
|
|||
The following components are trusted:
|
||||
|
||||
- The developer and host operating system.
|
||||
- The Lazaret CLI and the domain's Session Coordinator.
|
||||
- The Lazaret CLI and the domain's Session Coordinator (Host Coordinator, Runtime
|
||||
Supervisor, and attached runsc client).
|
||||
- Host configuration selected by the developer.
|
||||
- The Network Sidecar and the policy given to it by Lazaret.
|
||||
- Domain network-policy installation and connectivity helpers under Runtime
|
||||
Supervisor ownership, and the policy Lazaret installs for the Domain.
|
||||
|
||||
The following components are untrusted:
|
||||
|
||||
|
|
@ -66,22 +74,34 @@ implementation plan, logs, and user interfaces.
|
|||
| :--- | :--- |
|
||||
| **Agent Profile** | A developer-selected host configuration describing an agent image and its granted storage, network, environment, and escalation capabilities. |
|
||||
| **Agent Workspace** | The canonical host project directory mounted read-write at `/workspace` in the Agent Sandbox. |
|
||||
| **Agent Sandbox** | The rootless gVisor container in which an agent and its child processes execute. One sandbox is shared by all Client Sessions in a Domain. |
|
||||
| **Agent Sandbox** | The rootless gVisor container in which an agent and its child processes execute. One sandbox is shared by all Client Sessions in a Domain. gVisor sentry, gofer, and guest processes are the sandbox, not the Session Coordinator. |
|
||||
| **Agent Sandbox ID** | A runtime-unique identifier assigned to one Agent Sandbox instance and bound to its Domain protocol identity. |
|
||||
| **Client CLI ID** | A runtime-unique identifier assigned to one host Lazaret CLI process. It is authenticated as a protocol identity and bound to one Client Session. |
|
||||
| **Client Session** | One active host Lazaret CLI process and the interactive or non-interactive command it attaches to the Agent Sandbox. |
|
||||
| **Session ID** | A cryptographically random identifier unique to one Client Session. |
|
||||
| **Session Anchor** | Ephemeral session credentials that bind protocol messages to a registered Session ID and route them to the owning host CLI. |
|
||||
| **Session Coordinator** | The ephemeral host process that exclusively owns and coordinates a Domain's runtime resources and Client Sessions. |
|
||||
| **Session Coordinator ID** | A runtime-unique identifier assigned to one Session Coordinator instance and bound to its Domain protocol identity. |
|
||||
| **Session Coordinator** | The logical Domain role that exclusively owns and coordinates a Domain generation's runtime resources and Client Sessions. It is realized by exactly three constitutive processes: Host Coordinator, Runtime Supervisor, and attached runsc client. |
|
||||
| **Session Coordinator ID** | A runtime-unique identifier for the logical Session Coordinator as a protocol peer, authenticated on the Host Coordinator face. Generation scoping and stale-credential refuse follow the protocol model. |
|
||||
| **Host Coordinator** | The constitutive Session Coordinator process that runs in the host user and mount namespaces. It is the protocol face: Domain lock, durable state store, Session PTY masters, escalation mailbox and routing, publication and session admission, and lifetime authority over the Runtime Supervisor. |
|
||||
| **Runtime Supervisor** | The constitutive Session Coordinator process that runs in the Domain generation's user, mount, and network namespaces under a Host Coordinator lifetime lease. It owns supervised filesystem and network resources for the generation, arms the parent-death edge to attached runsc, and launches the attached runsc client. |
|
||||
| **Attached runsc** | The constitutive Session Coordinator process that is the non-detached `runsc` client child of the Runtime Supervisor. It supplies the causal coupling edge to the complete Agent Sandbox. |
|
||||
| **Domain** | The shared runtime and persistent-state scope for one `(Agent Profile, canonical Agent Workspace)` pair. |
|
||||
| **Domain ID** | A deterministic identifier derived from the Agent Profile name and canonical Agent Workspace path. It namespaces Domain resources but is not an authentication credential. |
|
||||
| **Domain generation** | One attempt to prepare, publish, operate, and tear down or recover a Domain's transient runtime resources under a single Session Coordinator instance and durable generation identity. |
|
||||
| **Domain Root** | The host-only directory containing persistent state and metadata for one Domain. |
|
||||
| **Network Sidecar** | The trusted, shell-less gateway container that establishes the Domain's network policy before the Agent Sandbox starts. |
|
||||
| **Network Sidecar ID** | A runtime-unique identifier assigned to the Network Sidecar instance owned by a Domain. |
|
||||
| **Network Sidecar** | The logical Domain network-policy role for one Domain generation: derived-policy application, enforcement network-namespace preparation, connectivity-helper supervision, and network readiness attestation. Under the selected architecture this role is realized on the Runtime Supervisor-owned install path (with a supervised connectivity helper). It is not a constitutive Session Coordinator process and need not be a separate OS process. The Agent Sandbox never holds network-administration capability. |
|
||||
| **Network Sidecar ID** | Protocol component identifier for the Domain generation's Network Sidecar role instance (not a Runtime Supervisor or connectivity-helper process id, and not a filesystem path). Generation scoping follows the protocol model. |
|
||||
| **Connectivity helper** | The supervised process that provides user-space connectivity for the Domain enforcement network namespace. Production uses `slirp4netns`. Ownership and lease coupling follow the protocol model; process identity is product recovery material, not the Network Sidecar ID. |
|
||||
| **Derived network policy** | The generation-bound policy document Lazaret derives from trusted host configuration (default and profile allow/deny prefixes, DNS reachability, address-family disposition). Only derived policy is installed; the Agent Sandbox never supplies policy. |
|
||||
| **Network readiness fingerprint** | Product encoding of protocol network readiness: a cryptographic digest over Domain ID, generation, configuration fingerprint, Network Sidecar ID, derived-policy digest, and enforcement network-namespace identity material. |
|
||||
| **Prepared lower** | A Lazaret-owned immutable root filesystem tree materialised from the selected base image. Content is identified by a prepared-artifact identity. |
|
||||
| **Prepared-artifact ID** | A Lazaret-assigned identity for one immutable prepared-lower tree (content-addressed or otherwise unique among prepared lowers under the Storage Root). |
|
||||
| **Prepared-lower lease** | Product binding of a Domain generation to a prepared-artifact ID for State Anchor use (not a container-engine mount refcount). Lease lifecycle follows the protocol model. |
|
||||
| **Durable intent** | Protocol durable intent that Lazaret intends to create or has created a named external resource for a Domain generation (see protocol model). |
|
||||
| **Publication** | Protocol publication of a Domain generation for Client Session registration and service (see protocol model). |
|
||||
| **Git Sentry** | The protective mount layout that preserves bidirectional workspace and Git access while preventing writes to the host's default Git hooks and repository configuration. |
|
||||
| **Ignored Workspace State** | Domain-scoped sandbox-local storage presented at Git-ignored Agent Workspace paths instead of exposing the corresponding host content. |
|
||||
| **State Anchor** | The Domain-scoped persistent writable filesystem layer merged over selected paths from the sandbox base image. |
|
||||
| **State Anchor** | The Domain-scoped persistent writable filesystem layer merged over selected paths from the sandbox base image prepared lower. |
|
||||
| **Trust Anchor** | The ephemeral Domain-scoped certificate authority used to authenticate role-bound Lazaret protocol identities. |
|
||||
| **Protocol Identity** | An authenticated binding of a component role, Agent Profile, Domain ID, and runtime component ID. Identifiers name components but do not authenticate them by themselves. |
|
||||
| **Escalation Client** | The Lazaret-provided executable through which a sandboxed process requests a host action. |
|
||||
|
|
@ -97,19 +117,21 @@ implementation plan, logs, and user interfaces.
|
|||
### 3.1 System Boundaries
|
||||
|
||||
```mermaid
|
||||
flowchart LR
|
||||
flowchart TB
|
||||
subgraph Host[Trusted host]
|
||||
CLI[Client CLI]
|
||||
Config[Host configuration]
|
||||
HostWorkspace[Agent Workspace]
|
||||
Coordinator[Session Coordinator]
|
||||
State[State Anchor]
|
||||
Gateway[Network Sidecar]
|
||||
HC[Host Coordinator]
|
||||
RS[Runtime Supervisor]
|
||||
Runsc[Attached runsc]
|
||||
State[State Anchor / FUSE]
|
||||
Net[Network policy + connectivity helper]
|
||||
Mailbox[Escalation Mailbox]
|
||||
HostExec[Approved host process]
|
||||
end
|
||||
|
||||
subgraph Sandbox[Untrusted Agent Sandbox - rootless runsc]
|
||||
subgraph Sandbox[Untrusted Agent Sandbox - rootless gVisor]
|
||||
Agent[Agent and child processes]
|
||||
Workspace[/workspace mount]
|
||||
Escalate[Escalation Client]
|
||||
|
|
@ -117,60 +139,102 @@ flowchart LR
|
|||
|
||||
Config --> CLI
|
||||
HostWorkspace <--> Workspace
|
||||
CLI <--> Coordinator
|
||||
Coordinator --> State
|
||||
Coordinator --> Gateway
|
||||
Coordinator <--> Mailbox
|
||||
CLI <--> HC
|
||||
HC --> RS
|
||||
RS --> Runsc
|
||||
Runsc --> Sandbox
|
||||
RS --> State
|
||||
RS --> Net
|
||||
HC <--> Mailbox
|
||||
Agent <--> Workspace
|
||||
Agent --> Escalate
|
||||
Escalate <--> Mailbox
|
||||
Coordinator --> HostExec
|
||||
Agent --> Gateway
|
||||
Gateway --> Network[Permitted destinations]
|
||||
HC --> HostExec
|
||||
Agent --> Net
|
||||
Net --> Network[Permitted destinations]
|
||||
```
|
||||
|
||||
The logical Session Coordinator for a Domain generation is the composition of the
|
||||
Host Coordinator, Runtime Supervisor, and attached runsc client. The Host
|
||||
Coordinator is the sole protocol and session face for Client CLIs. The Runtime
|
||||
Supervisor owns generation-bound runtime namespaces and supervised resources. The
|
||||
attached runsc client is the non-detached causal edge to the Agent Sandbox.
|
||||
|
||||
The Agent Sandbox uses gVisor's application-kernel isolation under rootless
|
||||
Podman. Rootless operation limits the host authority of the runtime, while gVisor
|
||||
operation. Lazaret owns sandbox lifetime through the Session Coordinator process
|
||||
chain; an external container engine does not own the Domain's Agent Sandbox.
|
||||
Rootless operation limits the host authority of runtime helpers, while gVisor
|
||||
interposes a separate userspace kernel between untrusted processes and the host
|
||||
kernel. The Network Sidecar is a separate trusted component and is not part of the
|
||||
untrusted agent environment.
|
||||
kernel. Network policy installation and connectivity helpers are trusted and are
|
||||
not part of the untrusted agent environment.
|
||||
|
||||
Lazaret is daemonless: it does not require a persistent global Unix service or
|
||||
cross-Domain runtime authority that survives independently of Domain generations.
|
||||
Active Domains have per-generation and per-session processes whose authority is
|
||||
scoped by Domain ID, generation, configuration fingerprint, role identity, and
|
||||
exact physical ownership. Bootstrap recovery for a Domain is initiated by a host
|
||||
Lazaret CLI invocation for that Domain, not by a resident scheduler.
|
||||
|
||||
### 3.2 Domain and Session Lifecycle
|
||||
|
||||
The Session Coordinator is the single owner of a Domain's Agent Sandbox, Network
|
||||
Sidecar, State Anchor, host-only sockets, Escalation Mailbox, and active-session
|
||||
registry. Concurrent CLI processes for the same Domain join the existing
|
||||
coordinator and attach separate Client Sessions to the shared sandbox. Different
|
||||
Domains never share these resources.
|
||||
One logical Session Coordinator exclusively owns a Domain generation's Agent
|
||||
Sandbox, Network Sidecar resources, State Anchor mounts, host-only sockets,
|
||||
Escalation Mailbox, durable generation state, and active-session registry.
|
||||
Concurrent CLI processes for the same Domain join the published Host Coordinator
|
||||
and attach separate Client Sessions to the shared sandbox. Different Domains never
|
||||
share these resources.
|
||||
|
||||
The first Client Session starts the Domain. The coordinator prepares persistent
|
||||
state, establishes network policy, starts the Agent Sandbox, and then accepts the
|
||||
session. When no Client Sessions remain, it tears down transient resources while
|
||||
retaining Domain-scoped persistent state.
|
||||
An exclusive non-blocking Domain lock elects at most one Host Coordinator startup
|
||||
or recovery leader for a Domain. Losers fail closed. Client CLIs start, join, or
|
||||
recover a Domain through that lock and publication rather than a global control
|
||||
plane.
|
||||
|
||||
Startup, registration, cancellation, recovery, and teardown transitions are
|
||||
defined by the [TLA+ application protocol model](protocol/Lazaret.tla).
|
||||
Protocol lifecycle—startup, registration, cancellation, recovery, teardown,
|
||||
publication, escalation, generation-scoped identities, durable intent, network
|
||||
readiness, prepared-lower lease, and connectivity-helper ownership—is defined by
|
||||
the [TLA+ application protocol model](protocol/Lazaret.tla). Product
|
||||
implementation refines that model with physical resources (prepared-lower trees,
|
||||
mounts, `slirp4netns`, PTYs, runsc clients, durable store encoding, exact
|
||||
ownership records) and must not assume those resources disappeared with an owner
|
||||
process.
|
||||
|
||||
A Domain failure first withdraws publication, invalidates active trust material,
|
||||
disconnects sessions, and terminates associated host processes. It does not
|
||||
assume that already-created sandbox, sidecar, or mount resources disappeared.
|
||||
Recovery stops the sandbox, then the sidecar, then unmounts the State Anchor
|
||||
before the Domain may return to the absent state and accept a new startup leader.
|
||||
Session control and escalation use the Session Coordinator ID on the Host
|
||||
Coordinator face, not Runtime Supervisor, attached runsc, or connectivity-helper
|
||||
process identifiers. Network attachment uses the Network Sidecar ID as the
|
||||
generation's network-policy role identity, not a helper or Runtime Supervisor
|
||||
process id.
|
||||
|
||||
The Trust Anchor authenticates distinct Protocol Identities for the Session
|
||||
Coordinator, Client CLI, Network Sidecar, and Agent Sandbox. Certificates bind a
|
||||
peer's role, Agent Profile, Domain ID, and runtime component ID; a certificate for
|
||||
one role or Domain cannot authorize another. Session registration additionally
|
||||
binds the authenticated Client CLI ID to its Session ID and Session Anchor.
|
||||
### 3.3 Session Terminals
|
||||
|
||||
Authorization uses the relevant current identity tuple rather than any identifier
|
||||
alone. Network attachment binds the `(Domain ID, Network Sidecar ID, Agent Sandbox
|
||||
ID)` tuple. Session control binds the `(Domain ID, Session Coordinator ID, Client
|
||||
CLI ID, Session ID)` tuple. Host Escalation binds the authenticated Agent Sandbox
|
||||
ID to the registered `(Client CLI ID, Session ID, Session Anchor)` tuple in that
|
||||
Domain.
|
||||
The Host Coordinator owns one host PTY master per interactive Client Session. The
|
||||
PTY slave is attached to non-detached `runsc exec` standard streams with a guest
|
||||
TTY. The root attached `runsc run` client remains terminal-neutral and is not the
|
||||
Session PTY attachment path. Production must not depend on `runsc exec
|
||||
-console-socket`.
|
||||
|
||||
### 3.3 Filesystem and Git Model
|
||||
Session terminal ownership is the Host Coordinator; a Client CLI never inherits
|
||||
the sandbox Session PTY. For each Client Session the coordinator maintains the
|
||||
session identity needed for routing and cleanup, including Session ID, PTY master,
|
||||
`runsc exec` client process identity, and guest process or process-group identity.
|
||||
|
||||
Interactive terminal control requires:
|
||||
|
||||
- Window resize applied to the host PTY master and guest `SIGWINCH` delivered to
|
||||
the exact session process or process group through runsc.
|
||||
- Client control events (for example interrupt) translated into runsc signal
|
||||
operations for that exact session process or process group; raw host PTY
|
||||
control characters alone are not a sufficient contract.
|
||||
- Per-session exit status collected from the non-detached `runsc exec` client as
|
||||
the primary source.
|
||||
- On session close, PTY master loss, or exec-client loss: deregister the session
|
||||
before further terminal or escalation traffic for that session, stop the guest
|
||||
session process or process group with generation-exact runsc operations, reap
|
||||
the exec client, and close the PTY.
|
||||
|
||||
Disconnected Client Sessions close rather than reattach to an unbounded scrollback
|
||||
owned by the coordinator.
|
||||
|
||||
### 3.4 Filesystem and Git Model
|
||||
|
||||
The Agent Workspace is mounted read-write. Tracked paths and untracked paths that
|
||||
are not ignored propagate in both directions. The Git index, `HEAD`, references,
|
||||
|
|
@ -202,11 +266,52 @@ These protections do not make the workspace immutable. Their purpose is to stop
|
|||
the sandbox from writing the protected host Git configuration and default hook
|
||||
directory while preserving normal Git operations and bidirectional source edits.
|
||||
|
||||
### 3.4 Persistent Sandbox State
|
||||
### 3.5 Persistent Sandbox State
|
||||
|
||||
The State Anchor preserves developer tooling and selected sandbox system paths for
|
||||
one Domain. It combines a read-only lower directory from the selected base image
|
||||
with a Domain-scoped writable upper directory.
|
||||
one Domain. It combines a Lazaret-owned prepared lower from the selected base
|
||||
image with a Domain-scoped writable upper directory.
|
||||
|
||||
#### Prepared lower
|
||||
|
||||
Preparation resolves the selected base image, applies layers with a supported
|
||||
OCI-aware preparer, and materialises an immutable Lazaret-owned root filesystem
|
||||
tree under the Storage Root. The tree carries a prepared-artifact ID and a source
|
||||
image identity. Live container-engine image mounts are not a production State
|
||||
Anchor lower. Archive export alone is not a complete preparation boundary;
|
||||
container tooling may participate only as transport into Lazaret-owned
|
||||
preparation. Ad hoc unsupported tar extractors are not a production preparer.
|
||||
|
||||
Protocol prepared-lower lease, intent, and refuse-while-leased reclaim follow the
|
||||
protocol model. Product encoding binds a lease to prepared-artifact ID (and
|
||||
generation identity) under Host Coordinator durable state—not an engine mount
|
||||
refcount. Distinct Domain generations may share one prepared-artifact ID only
|
||||
through separate protocol leases. Concurrent preparation of the same source may
|
||||
reuse a completed artifact or create a new prepared-artifact ID; an in-progress
|
||||
prepare tree is not a State Anchor lower. After the last lease for an artifact
|
||||
drops, product GC may reclaim that tree; foreign trees under deterministic paths
|
||||
must not be deleted.
|
||||
|
||||
#### Durable generation document
|
||||
|
||||
Durable Domain state is an embedded store opened exclusively by the Host
|
||||
Coordinator process that holds the Domain's exclusive lifecycle lock for write.
|
||||
No other process opens the store for read or write: Client CLIs, the Runtime
|
||||
Supervisor, recovery observers, and status tools obtain state only through Host
|
||||
Coordinator IPC or by becoming the lock-holding Host Coordinator. Domain flock
|
||||
serializes which process may be that exclusive opener. Store mutations use
|
||||
atomic transactions; an interrupted write leaves the last successfully committed
|
||||
document, never a half-applied generation decision.
|
||||
|
||||
Protocol durable decision vocabulary, multi-role intent, and mismatch refuse are
|
||||
defined by the protocol model. The product store encodes that generation document
|
||||
in typed tables under a schema/db version (unknown newer versions fail closed
|
||||
until an explicit Host Coordinator migration), including generation identity,
|
||||
minted runtime component IDs, and participant ownership material (for example
|
||||
prepared-artifact ID, pid/start, mount identity, network readiness fingerprint).
|
||||
Participant roles include at least those the model tracks, plus product modules
|
||||
such as `git_routing`, `sessions`, and `publication` as they land. Deterministic
|
||||
paths are lookup hints for physical recovery, not ownership proofs.
|
||||
|
||||
Files not represented in the upper layer follow the selected base image. Files,
|
||||
directories, and whiteouts recorded in the upper layer remain authoritative when
|
||||
|
|
@ -216,23 +321,47 @@ allowing unmodified base-image content to follow the selected image.
|
|||
Persistent state is sandbox state, not host configuration. It must not contain or
|
||||
override Lazaret's host control plane.
|
||||
|
||||
### 3.5 Network Isolation
|
||||
### 3.6 Network Isolation
|
||||
|
||||
The Network Sidecar establishes the Domain's egress routes before the Agent
|
||||
Sandbox starts. The sidecar alone receives the network-administration capability
|
||||
needed to install policy; the Agent Sandbox does not receive that capability.
|
||||
The Agent Sandbox may join only the sidecar's prepared network namespace, not the
|
||||
host network namespace.
|
||||
The Network Sidecar role is realized on the Runtime Supervisor-owned install
|
||||
path: the Runtime Supervisor (or a packaging-equivalent installer still bound to
|
||||
the same Network Sidecar ID) holds network-administration capability only for
|
||||
install and attestation in the Domain enforcement network namespace. The Agent
|
||||
Sandbox does not receive that capability and may join only that prepared
|
||||
enforcement namespace, not the host network namespace. Production connectivity uses
|
||||
`slirp4netns`. Installing policy by driving nftables through runsc into the guest
|
||||
is not a production path. Protocol helper ownership, network readiness, and
|
||||
publication gates follow the protocol model.
|
||||
|
||||
#### Derived policy and readiness encoding
|
||||
|
||||
The Host Coordinator derives the generation's derived network policy from trusted
|
||||
host configuration. The Runtime Supervisor installs only that derived policy and
|
||||
attests readiness by observing installed routes and helper readiness in the
|
||||
enforcement namespace—not by process exit status alone. The product records a
|
||||
network readiness fingerprint as the durable encoding of protocol network
|
||||
readiness. Before publication, Lazaret verifies from the Agent Sandbox network
|
||||
view (or an equivalent generation-bound probe on the same enforcement namespace)
|
||||
that default-denied private destinations are unreachable and that required
|
||||
permitted reachability, including selected DNS resolvers, works.
|
||||
|
||||
#### Default policy and deny representation
|
||||
|
||||
IPv4 destinations are permitted by default except for the RFC 1918 private
|
||||
address ranges, which are denied by default. Explicit, more-specific allow rules
|
||||
may grant access within those ranges. Lazaret also installs the reachability
|
||||
needed for the Domain's selected DNS resolvers. Other permitted and denied
|
||||
destination prefixes come from trusted host configuration.
|
||||
address ranges (`10.0.0.0/8`, `172.16.0.0/12`, `192.168.0.0/16`), which are denied
|
||||
by default. Explicit, more-specific allow rules may grant access within those
|
||||
ranges. Lazaret also installs the reachability needed for the Domain's selected
|
||||
DNS resolvers. Other permitted and denied destination prefixes come from trusted
|
||||
host configuration.
|
||||
|
||||
Normal Linux longest-prefix routing determines the most specific matching route;
|
||||
an equal-prefix conflict must be rejected or resolved in favor of denial. IPv4
|
||||
and IPv6 must either receive equivalent policy or an address family must be
|
||||
Default and configured deny prefixes are enforced with **loopback-unicast deny
|
||||
routes** in the Domain enforcement network namespace (routes that direct matching
|
||||
destinations to a loopback unicast address so packets are not forwarded). Linux
|
||||
`blackhole` routes are not the production deny representation for this path.
|
||||
Equal-prefix allow/deny conflicts must be rejected or resolved in favor of denial.
|
||||
|
||||
Normal Linux longest-prefix routing determines the most specific matching route.
|
||||
IPv4 and IPv6 must either receive equivalent policy or an address family must be
|
||||
disabled.
|
||||
|
||||
The topology and policy-installation sequence must ensure that all external Agent
|
||||
|
|
@ -240,38 +369,23 @@ Sandbox traffic traverses the configured enforcement path. Dynamic policy change
|
|||
are not a requirement unless the implementation can apply them without weakening
|
||||
that property.
|
||||
|
||||
### 3.6 Host Escalation
|
||||
### 3.7 Host Escalation
|
||||
|
||||
The Escalation Client exchanges request and result records through the
|
||||
Escalation Mailbox. Records are regular files written by atomic rename beneath
|
||||
host-private, Domain-scoped paths. The sandbox-writable request path and
|
||||
sandbox-readable result path may have different mount modes. The mailbox is not
|
||||
trusted as an authentication boundary: each request carries authenticated Domain
|
||||
credentials and a Session Anchor signature binding it to a registered Client
|
||||
Session and to the exact request content. A verified request is routed only to
|
||||
that session's host CLI. Host-only CLI/coordinator control may use host-private
|
||||
Unix sockets that are never mounted into the Agent Sandbox.
|
||||
Escalation Mailbox: regular files written by atomic rename beneath host-private,
|
||||
Domain-scoped paths. Request and result paths may use different mount modes. The
|
||||
mailbox is not an authentication boundary. The Host Coordinator owns the mailbox
|
||||
for the published generation. Host-only CLI/coordinator control may use
|
||||
host-private Unix sockets that are never mounted into the Agent Sandbox.
|
||||
|
||||
A host command may run only when the developer approves it interactively or when
|
||||
it matches an auto-approval rule in trusted host configuration. Auto-approved
|
||||
commands are launched directly as an argument vector without a shell. Rules match
|
||||
the complete vector by default; permission for arbitrary trailing arguments is an
|
||||
explicit property of an individual rule.
|
||||
Auto-approved host commands are launched as an argument vector without a shell.
|
||||
Trailing arguments require an explicit grant on the matched rule.
|
||||
|
||||
Interactive approval may allow the developer to approve, deny, or edit a request.
|
||||
Every accepted request must produce an Escalation Result for its Escalation
|
||||
Client while its Client Session remains connected. The result reports completion,
|
||||
denial, timeout, cancellation, or failure and, when a host command ran, its exit
|
||||
status and standard-output and standard-error data. Approval is an authorization
|
||||
decision, not a terminal result. A request reaches its terminal state only after
|
||||
this result is delivered or its Client Session disconnects.
|
||||
Terminal ownership must return to the sandbox session after resolution.
|
||||
|
||||
Authentication, message correlation, approval, execution, cancellation, and
|
||||
terminal-routing transitions are defined by the
|
||||
Escalation authentication, correlation, approval, execution, cancellation, result
|
||||
delivery, and terminal routing are defined by the
|
||||
[TLA+ application protocol model](protocol/Lazaret.tla).
|
||||
|
||||
### 3.7 State Inspection and Reset
|
||||
### 3.8 State Inspection and Reset
|
||||
|
||||
The host CLI provides read-only discovery, inspection, structural verification,
|
||||
and explicit reset operations for Domain State Anchors. These operations resolve
|
||||
|
|
@ -283,14 +397,15 @@ default. Structural verification requires an inactive Domain and exclusive
|
|||
lifecycle ownership so its result is not invalidated by concurrent writes. A
|
||||
reset may target one configured persistent container path or all State Anchors in
|
||||
the Domain. It discards the selected upper-layer state so the next launch follows
|
||||
the current base-image lower layer; it does not modify the base image, Agent
|
||||
the current prepared lower; it does not modify the prepared lower artifact, Agent
|
||||
Workspace, Ignored Workspace State, or unselected State Anchors.
|
||||
|
||||
Reset is permitted only after Lazaret holds the Domain's exclusive lifecycle lock
|
||||
and has established that no Client Session, coordinator, sandbox, sidecar, host
|
||||
process, or overlay mount is using the selected state. Confirmation flags may
|
||||
suppress the human prompt but may not bypass these safety conditions. Reset must
|
||||
be crash-consistent and must never follow a symlink outside the Domain Root.
|
||||
and has established that no Client Session, Session Coordinator constitutive
|
||||
process, sandbox, network helper, host process, or overlay mount is using the
|
||||
selected state. Confirmation flags may suppress the human prompt but may not
|
||||
bypass these safety conditions. Reset must be crash-consistent and must never
|
||||
follow a symlink outside the Domain Root.
|
||||
|
||||
## 4. Requirements
|
||||
|
||||
|
|
@ -302,32 +417,46 @@ be crash-consistent and must never follow a symlink outside the Domain Root.
|
|||
| **SR-2** | Host configuration shall never be mounted into the Agent Sandbox or located beneath a host path mounted into it. |
|
||||
| **SR-3** | Host paths outside the Agent Workspace, developer-configured volumes, and Lazaret-owned fixed control mounts shall not be accessible to the Agent Sandbox. |
|
||||
| **SR-4** | The sandbox shall be unable to modify the host repository's `.git/config` or default `.git/hooks` directory through the workspace mount. |
|
||||
| **SR-5** | The Network Sidecar shall establish network policy before the Agent Sandbox starts, and the Agent Sandbox shall not receive network-administration capability. |
|
||||
| **SR-6** | Network policy shall cover every enabled address family and shall deny equal-specificity policy conflicts. |
|
||||
| **SR-7** | A host action shall execute only after interactive developer approval or a match against a trusted host auto-approval rule. |
|
||||
| **SR-5** | Domain network policy shall be established before the Agent Sandbox starts. Network-administration capability for policy install shall be held only on the Runtime Supervisor-owned Network Sidecar install path; the Agent Sandbox shall not receive network-administration capability. |
|
||||
| **SR-6** | Network policy shall cover every enabled address family and shall deny equal-specificity policy conflicts. Default and configured deny prefixes shall be enforced with loopback-unicast deny routes in the Domain enforcement network namespace; Linux blackhole routes shall not be the production deny representation. |
|
||||
| **SR-7** | Host actions shall execute only under protocol-model approval (developer or auto-rule). |
|
||||
| **SR-8** | Auto-approved host commands shall execute without a shell and shall permit trailing arguments only when the matched rule explicitly grants them. |
|
||||
| **SR-9** | Every protocol peer shall be authenticated to its component role, Agent Profile, Domain ID, and runtime component ID. Authorization shall require the relevant current identity tuple; an identifier or certificate for another role, Domain, component instance, or Client Session shall not be accepted. |
|
||||
| **SR-9** | Protocol peer authentication and authorization shall follow the protocol model (role, Agent Profile, Domain ID, and runtime component ID binding). |
|
||||
| **SR-10** | Domain sockets, mailboxes, and coordination files shall reside in a host-private directory owned by the developer. |
|
||||
| **SR-11** | Runtime and persistent resources belonging to different Domain IDs shall remain isolated. |
|
||||
| **SR-12** | The Agent Sandbox shall not join host user, PID, IPC, UTS, cgroup, or network namespaces; the only shared network namespace permitted is the Domain's Network Sidecar enforcement namespace. |
|
||||
| **SR-12** | The Agent Sandbox shall not join host user, PID, IPC, UTS, cgroup, or network namespaces; the only shared network namespace permitted is the Domain's Network Sidecar enforcement namespace prepared for that generation. |
|
||||
| **SR-13** | Git-ignored Agent Workspace paths shall use Ignored Workspace State by default, preventing the sandbox from reading or modifying corresponding host content; only trusted host configuration may disable this behavior. |
|
||||
| **SR-14** | State Anchor maintenance shall remain confined to the resolved Domain Root. Destructive maintenance shall require exclusive lifecycle ownership and an inactive, unmounted target. |
|
||||
| **SR-15** | Lazaret shall not use a live container-engine image mount as the production State Anchor lower; the lower shall be a Lazaret-owned prepared lower bound by a prepared-lower lease. Archive export alone shall not be treated as a complete preparation boundary. |
|
||||
| **SR-16** | Session control, registration, and Host Escalation shall authenticate the Session Coordinator ID on the Host Coordinator protocol face and shall not treat Runtime Supervisor or attached runsc process identifiers as substitute protocol peer identities. |
|
||||
| **SR-17** | Network Sidecar ID in attachment authorization shall name the Network Sidecar role instance, not a connectivity-helper or Runtime Supervisor process identifier. |
|
||||
|
||||
### 4.2 Functional Requirements
|
||||
|
||||
| ID | Requirement |
|
||||
| :--- | :--- |
|
||||
| **FR-1** | Lazaret shall derive a stable Domain ID from the selected Agent Profile and canonical Agent Workspace. |
|
||||
| **FR-2** | Concurrent Client Sessions in one Domain shall share one coordinator, Agent Sandbox, Network Sidecar, and State Anchor. |
|
||||
| **FR-2** | Concurrent Client Sessions in one Domain shall share one logical Session Coordinator, Agent Sandbox, Network Sidecar, and State Anchor for the published generation. |
|
||||
| **FR-3** | Tracked and non-ignored workspace edits and supported Git operations shall propagate bidirectionally between host and sandbox. |
|
||||
| **FR-4** | Selected sandbox paths and Ignored Workspace State shall persist across Domain restarts without copying Lazaret host configuration into the sandbox. |
|
||||
| **FR-5** | The coordinator shall route each escalation prompt to the Client Session identified by the verified Session ID and deliver the correlated Escalation Result to the requesting Escalation Client. |
|
||||
| **FR-6** | The final Client Session leaving a Domain shall trigger teardown of transient Domain resources. |
|
||||
| **FR-7** | Startup and teardown shall recover safely from interrupted or stale prior executions without assuming that external runtime resources disappeared with their owner process. |
|
||||
| **FR-5** | Escalation prompt routing and Escalation Result delivery shall follow the protocol model on the Host Coordinator face. |
|
||||
| **FR-6** | Teardown when no Client Sessions remain shall follow the protocol model; product teardown shall release the generation's physical resources. |
|
||||
| **FR-7** | Product recovery shall not assume external runtime resources disappeared with their owner process and shall apply protocol intent/mismatch refuse rules to physical leftovers (exact-owned cleanup only). |
|
||||
| **FR-8** | Lazaret shall support interactive terminal sessions without degrading supported host terminal capabilities. |
|
||||
| **FR-9** | Trusted host configuration shall allow the developer to disable Git-ignored path isolation for an Agent Profile. |
|
||||
| **FR-10** | Session registration shall bind one authenticated Client CLI ID, Session ID, and Session Anchor, and escalation routing and approval shall preserve that binding. |
|
||||
| **FR-10** | Session registration and escalation identity binding shall follow the protocol model. |
|
||||
| **FR-11** | The host CLI shall list, inspect, structurally verify, and reset all or selected State Anchors without requiring direct manipulation of Lazaret's storage layout. |
|
||||
| **FR-12** | The logical Session Coordinator for a Domain generation shall be realized by exactly the Host Coordinator, Runtime Supervisor, and attached runsc client as constitutive processes. |
|
||||
| **FR-13** | The Host Coordinator, Runtime Supervisor, and attached runsc process chain shall realize Session Coordinator presence and sandbox coupling for the protocol model, with product recovery limited to exact-owned physical leftovers. |
|
||||
| **FR-14** | The Host Coordinator shall own one host PTY master per interactive Client Session; the PTY slave shall attach through non-detached `runsc exec` standard streams. The root attached `runsc run` client shall remain terminal-neutral. Production Session PTYs shall not depend on `runsc exec -console-socket`. |
|
||||
| **FR-15** | For each interactive Client Session, Lazaret shall apply window resize to the host PTY master and deliver guest `SIGWINCH` to the exact session process or process group through runsc; translate Client control events into runsc signal operations for that process or process group; collect exit status primarily from the non-detached `runsc exec` client; and on session end deregister before further terminal or escalation traffic for that session, stop the guest session process or process group with generation-exact runsc operations, reap the exec client, and close the PTY. |
|
||||
| **FR-16** | Domain network connectivity shall use `slirp4netns` as the production connectivity helper, with exact-owned process identity for recovery under the protocol helper ownership rules. |
|
||||
| **FR-17** | The Domain durable store shall be opened for read or write only by the Host Coordinator process that holds the Domain exclusive lifecycle lock; no other process shall open the store file. Mutations shall apply as whole store transactions. Protocol durable intent is encoded in that store. |
|
||||
| **FR-18** | Product network readiness encoding shall include a network readiness fingerprint and the pre-publication reachability verification described under network isolation; protocol publication and readiness gates follow the protocol model. |
|
||||
| **FR-19** | The Host Coordinator shall derive generation-bound network policy from trusted host configuration; the Runtime Supervisor shall install only that derived policy and attest readiness by observed namespace state. Durable network participant state shall record the network readiness fingerprint. |
|
||||
| **FR-20** | Before publication, Lazaret shall verify from the Agent Sandbox network view, or an equivalent generation-bound probe using the same enforcement namespace, that default-denied private destinations are unreachable and that required permitted reachability including selected DNS resolvers works. |
|
||||
| **FR-21** | The durable generation document encoding shall include schema/db version, generation identity, minted runtime component IDs, model-governed durable decision and participant intent, and ownership material for product recovery. Unknown newer schema versions shall fail closed until an explicit Host Coordinator migration runs. |
|
||||
| **FR-22** | Preparation shall use a supported OCI-aware preparer that materialises a Lazaret-owned immutable rootfs with source identity and prepared-artifact ID. Protocol prepared-lower lease rules apply before State Anchor mount. |
|
||||
|
||||
### 4.3 Developer-Experience Requirements
|
||||
|
||||
|
|
@ -344,8 +473,10 @@ be crash-consistent and must never follow a symlink outside the Domain Root.
|
|||
|
||||
| ID | Requirement |
|
||||
| :--- | :--- |
|
||||
| **OR-1** | The coordinator shall maintain exclusive runtime ownership of Domain resources. |
|
||||
| **OR-2** | Every accepted protocol request shall resolve to a delivered completed, denied, timed-out, cancelled, or failed result, unless its Client Session disconnects first. |
|
||||
| **OR-3** | Cancellation and process termination shall not strand an active host command or permanently block another Client Session. |
|
||||
| **OR-4** | Security-sensitive behavior shall be covered by integration tests on supported Podman, runsc, filesystem, and network configurations. Test evidence belongs in the journal. |
|
||||
| **OR-1** | The Session Coordinator shall maintain exclusive runtime ownership of Domain generation resources. An exclusive Domain lock shall elect at most one Host Coordinator leader for cold start or recovery of a Domain; concurrent losers shall fail closed. |
|
||||
| **OR-2** | Accepted protocol requests shall resolve per the protocol model. |
|
||||
| **OR-3** | Cancellation and process termination shall follow the protocol model (no stranded host command, no permanent block of another Client Session). |
|
||||
| **OR-4** | Security-sensitive behavior shall be covered by integration tests on supported runsc, filesystem, and network configurations. Test evidence belongs in the journal. |
|
||||
| **OR-5** | An interrupted State Anchor reset shall recover to either the prior generation or a new empty generation; it shall not leave a partially reset active upper layer. |
|
||||
| **OR-6** | Lazaret shall not require a persistent global daemon or multi-Domain resident process that holds mutable runtime authority across Domains. Per-Domain authority shall be scoped by Domain ID, generation, configuration fingerprint, role identity, and exact physical ownership. |
|
||||
| **OR-7** | After protocol leases for a prepared-artifact ID are released, product GC may reclaim that tree. Shared-artifact reclaim must wait until no lease remains for that artifact. In-progress prepare trees and foreign trees must not be deleted except through fail-closed recovery of exact-owned prepare intent. |
|
||||
|
|
|
|||
Loading…
Reference in a new issue