Remove phase vocabulary from Lazaret interfaces
This commit is contained in:
parent
3f9b1b3543
commit
e7dd95aea6
1 changed files with 547 additions and 579 deletions
|
|
@ -98,7 +98,7 @@ implementation, logs, and user interfaces.
|
|||
| **Domain Root** | The host-only directory containing persistent state and metadata for one 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. |
|
||||
| **Connectivity helper** | The supervised process that provides user-space connectivity for the Domain enforcement network namespace. Lazaret v1 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. |
|
||||
|
|
@ -184,9 +184,9 @@ initiated by a host Lazaret CLI invocation, not by a resident scheduler.
|
|||
|
||||
### 3.2 Trusted Host Configuration Refinement
|
||||
|
||||
The repository [design schemas](schema.md) encode the closed v1 trusted-host
|
||||
configuration described by this refinement. Lazaret chooses its configuration
|
||||
file from an explicit host CLI option or, when absent, from
|
||||
The non-authoritative repository [design schemas](schema.md) mirror the closed
|
||||
v1 trusted-host configuration described by this refinement. Lazaret chooses its
|
||||
configuration file from an explicit host CLI option or, when absent, from
|
||||
`$XDG_CONFIG_HOME/lazaret/config.toml`, with
|
||||
`$HOME/.config/lazaret/config.toml` as the XDG fallback. It derives the Storage
|
||||
Root from `storage.data_root` when present, otherwise from
|
||||
|
|
@ -203,9 +203,9 @@ first profile, infers a profile from an image or executable, or falls back to a
|
|||
different profile. The canonical Agent Workspace is the existing directory
|
||||
selected by the caller, normally the current working directory. Lazaret opens
|
||||
it as a directory, obtains its canonical raw pathname and filesystem identity,
|
||||
and retains the descriptor. The selected profile name and canonical workspace
|
||||
bytes produce `DomainIdV1` as described by this refinement and encoded by the
|
||||
repository schema.
|
||||
and retains the descriptor. The v1 Domain ID is SHA-256 over the
|
||||
`lazaret-domain-id-v1` context followed by the selected profile name and
|
||||
canonical workspace bytes, each framed by an unsigned 32-bit big-endian length.
|
||||
|
||||
The explicit configuration path follows this refinement's strict host-path grammar.
|
||||
The loader resolves any declared symlink once to a canonical target and builds
|
||||
|
|
@ -225,10 +225,10 @@ aliased, or unknown-version field meaningful. Every profile is structurally
|
|||
decoded, but filesystem and environment resolution applies only to the
|
||||
explicitly selected profile.
|
||||
|
||||
Path resolution produces a `ConfinedPathPlan`, not an ambient absolute path.
|
||||
Each plan retains a validated ancestor directory descriptor and a normalized
|
||||
relative suffix, records the ancestor's device, inode, and mount identity, and
|
||||
keeps canonical raw pathname bytes only as a diagnostic label or digest input.
|
||||
Path resolution produces confined path authority, not an ambient absolute path.
|
||||
It retains a validated ancestor directory descriptor and a normalized relative
|
||||
suffix, records the ancestor's device, inode, and mount identity, and keeps
|
||||
canonical raw pathname bytes only as a diagnostic label or digest input.
|
||||
Lazaret-owned filesystem access and mutation use descriptor-relative opens with
|
||||
beneath, no-magic-link, no-symlink, and no-mount-crossing resolution and
|
||||
revalidate the expected identity and type. A trusted external component whose
|
||||
|
|
@ -270,30 +270,31 @@ any identity or mount change refuses the complete load. Volume creation is
|
|||
limited to a declared directory strictly beneath the profile directory and uses
|
||||
the same component-wise `0700` creation rules.
|
||||
|
||||
Configuration resolution also requires an internal `SandboxLayoutV1`. Its
|
||||
Configuration resolution also requires a closed sandbox layout. Its
|
||||
closed protected-destination set contains `/workspace` and every product-owned
|
||||
sandbox mount destination selected by production layout construction. Each
|
||||
sandbox mount destination selected by default bundle construction. Each
|
||||
persistent or volume destination is compared with every member in both ancestry
|
||||
directions. The configuration loader does not guess paths for control,
|
||||
credential, mailbox, proc, sys, dev, runtime, or later product mounts, and a
|
||||
layout cannot be constructed without `/workspace`. Production layout
|
||||
layout cannot be constructed without `/workspace`. Bundle
|
||||
construction, rather than trusted-host configuration syntax, owns the remaining
|
||||
exact destination choices.
|
||||
|
||||
The loader resolves environment references only after structural, path, and
|
||||
network validation. A missing, non-UTF-8, or NUL-containing host value refuses
|
||||
the selected profile. Resolved values live only in the move-owned
|
||||
`ResolvedDomainConfiguration`; its representation is not serializable and its
|
||||
diagnostics redact values. Only reference names enter the configuration
|
||||
the selected profile. Resolved values live only in one move-owned,
|
||||
non-serializable configuration authority whose diagnostics redact values. Only
|
||||
reference names enter the configuration
|
||||
fingerprint. Configuration bytes, nonselected profiles, and unreferenced host
|
||||
environment values are not retained as runtime authority or copied into the
|
||||
Agent Sandbox.
|
||||
|
||||
The Host Coordinator derives the selected profile's effective IPv4 policy and
|
||||
`ConfigurationFingerprintV1` using the schema's exact normalization and
|
||||
canonical framing. IPv6 is disabled for a v1 sandbox. Joining a running Domain
|
||||
requires the same Domain ID and configuration fingerprint; the modeled
|
||||
configuration-mismatch path refuses every other value.
|
||||
Configuration Fingerprint from every normalized input that affects Domain
|
||||
behavior, excluding resolved environment values as described above. IPv6 is
|
||||
disabled for a v1 sandbox. Joining a running Domain requires the same Domain ID
|
||||
and configuration fingerprint; the modeled configuration-mismatch path refuses
|
||||
every other value.
|
||||
|
||||
For auto-approval, the configured executable resolves to one canonical path
|
||||
outside every sandbox-writable or Lazaret control tree. That path, rather than a
|
||||
|
|
@ -310,12 +311,11 @@ fallback execution path. Scripts are subject to the kernel's ordinary shebang
|
|||
handling; the rule authorizes the exact opened script object, not an arbitrary
|
||||
requester-selected interpreter.
|
||||
|
||||
`MailboxRequest.command_argv` is nonempty. Every element is UTF-8 and NUL-free;
|
||||
The requested command argument vector is nonempty. Every element is UTF-8 and NUL-free;
|
||||
element zero is an absolute path byte-equal to the rule's canonical executable,
|
||||
and elements one onward are matched against the rule arguments. Lazaret performs
|
||||
no `PATH` lookup. The v1 structured request language accepts no command-string
|
||||
or shell-expansion form; an unsupported form has the physical
|
||||
`CommandRequiresShell` classification and cannot auto-approve. The launcher
|
||||
or shell-expansion form; an unsupported form cannot auto-approve. The launcher
|
||||
never inserts or interprets a shell. An explicitly configured `/bin/sh -c ...`
|
||||
vector can match only its exact configured rule. A directly configured script
|
||||
continues to use ordinary kernel shebang handling for the same opened script
|
||||
|
|
@ -331,11 +331,11 @@ fallback.
|
|||
|
||||
Configuration resolution occurs before a generation, durable intent, external
|
||||
runtime resource, or session admission relies on it. Across a process boundary,
|
||||
a production consumer may resolve its own `ResolvedDomainConfiguration`, but it
|
||||
must first match the exact expected Domain ID and Configuration Fingerprint. A
|
||||
mismatch refuses before creating or joining the generation. Each consumer uses
|
||||
one resolved value for its subsequent path, network, environment, fingerprint,
|
||||
and approval decisions; it does not combine decisions from different loads.
|
||||
a consumer may resolve configuration independently, but it must first match the
|
||||
exact expected Domain ID and Configuration Fingerprint. A mismatch refuses
|
||||
before creating or joining the generation. Each consumer uses one resolved
|
||||
value for its subsequent path, network, environment, fingerprint, and approval
|
||||
decisions; it does not combine decisions from different loads.
|
||||
|
||||
### 3.3 Domain and Session Lifecycle Refinement
|
||||
|
||||
|
|
@ -362,25 +362,26 @@ below 6.9 refuse. Required pidfd and pidfs operations fail closed at their point
|
|||
of use; Lazaret does not attest, qualify, build, update, or roll back the running
|
||||
kernel.
|
||||
|
||||
`PidfsProcessIdentityV1` separates three kinds of data:
|
||||
The v1 pidfs process identity separates three kinds of data:
|
||||
|
||||
- `PidfsProcessAuthorityV1 = (boot_id, pidfs_st_dev, pidfs_st_ino)` is the only
|
||||
positive durable host-process authority. The boot ID is stored as the 16 UUID
|
||||
bytes in canonical UUID field order; both pidfs values are unsigned 64-bit
|
||||
types distinct from general filesystem device and inode identities.
|
||||
- `host_pid` is an unsigned 32-bit lookup locator interpreted only in the host
|
||||
- The boot ID plus pidfs device and inode is the only positive durable
|
||||
host-process authority. The boot ID is stored as the 16 UUID bytes in
|
||||
canonical UUID field order; both pidfs values are unsigned 64-bit values
|
||||
distinct from general filesystem device and inode identities.
|
||||
- The host PID is an unsigned 32-bit lookup locator interpreted only in the host
|
||||
PID namespace where Host Coordinator and bootstrap recovery run.
|
||||
- `start_time_ticks` is unsigned 64-bit `/proc/<pid>/stat` negative evidence.
|
||||
- The unsigned 64-bit `/proc/<pid>/stat` start time is negative evidence.
|
||||
Equality of PID and start time adds no authority; inequality or an unreadable
|
||||
required observation refuses.
|
||||
|
||||
A retained pidfd is the primary live authority. Polling, waiting, signaling,
|
||||
and termination act through that exact retained descriptor. Production process
|
||||
and termination act through that exact retained descriptor. Host process
|
||||
control has no numeric-PID signal or reopen-and-signal fallback.
|
||||
|
||||
`CausalChildAcquisitionV1` applies to every Lazaret-owned child that can become
|
||||
durable process ownership. Each Host Coordinator and Runtime Supervisor has one
|
||||
exclusive in-process broker for all spawn, `SIGCHLD`, and reap operations. The
|
||||
The causal child acquisition protocol applies to every Lazaret-owned child that
|
||||
can become durable process ownership. Each Host Coordinator and Runtime
|
||||
Supervisor has one exclusive in-process broker for all spawn, `SIGCHLD`, and
|
||||
reap operations. The
|
||||
process has default non-auto-reaping `SIGCHLD`; no same-parent spawn or reap and
|
||||
no dependency process API bypasses the broker while acquisition is active. The
|
||||
broker performs this sequence:
|
||||
|
|
@ -397,37 +398,37 @@ broker performs this sequence:
|
|||
5. Call `fstatfs` on that exact pidfd and require `f_type == PID_FS_MAGIC`;
|
||||
any error or wrong magic refuses. Call `fstat` on the same descriptor; any
|
||||
error refuses. Read the current boot ID and diagnostic start time, and form
|
||||
`PidfsProcessIdentityV1`.
|
||||
6. Persist `Staged` ownership. An RS-launched child is sent as the exact
|
||||
`StagedProcessOwnership` tuple to HC, and RS waits for an authenticated
|
||||
`ProcessOwnershipCommitAck` that echoes the same Domain, generation,
|
||||
generation-scoped coordinator ID, ownership slot, and complete process
|
||||
identity. Lost, mismatched, unknown-version, unauthenticated, or duplicate
|
||||
after release acknowledgment is never success.
|
||||
the v1 pidfs process identity.
|
||||
6. Persist staged ownership. For an RS-launched child, HC receives the complete
|
||||
staged ownership tuple and RS waits for an authenticated commit
|
||||
acknowledgement that echoes the same Domain, generation,
|
||||
generation-scoped coordinator ID, ownership role, and process identity.
|
||||
Lost, mismatched, unknown-version, unauthenticated, or duplicate
|
||||
acknowledgement after release is never success.
|
||||
7. Release the wrapper barrier only after the exact staged ownership commit is
|
||||
acknowledged. The receiver consumes the acknowledgment once while that
|
||||
exact barrier is pending.
|
||||
8. The wrapper arms its parent-death action, rechecks the expected parent pidfs
|
||||
authority to close the arming race, and execs the foreground,
|
||||
non-daemonizing target in place.
|
||||
9. Promote ownership to `Committed` only after target-specific readiness.
|
||||
9. Promote ownership to committed only after target-specific readiness.
|
||||
Staged ownership cannot satisfy readiness, publication, dependent-resource
|
||||
creation, or adoption. It remains positive authority for exact same-handle
|
||||
cleanup and `PidfsRecoveryMatch`, including bootstrap recovery.
|
||||
cleanup and exact pidfs recovery matching, including bootstrap recovery.
|
||||
|
||||
Every durable host-process slot is exactly `Unassigned`,
|
||||
`Staged(PidfsProcessIdentityV1)`, or `Committed(HostProcessIdentity)`. Only a
|
||||
Every durable host-process slot is exactly unassigned, staged with a current
|
||||
pidfs process identity, or committed with current host-process ownership. Only a
|
||||
current pidfs identity may be staged or committed. Current staged and committed
|
||||
identity both authorize exact matched cleanup; only committed ownership may
|
||||
satisfy an active role, readiness, publication, or adoption.
|
||||
|
||||
A role-bound Participant is first committed as bare `Intent` with no ownership
|
||||
A role-bound participant is first committed as bare intent with no ownership
|
||||
snapshot. Once physical acquisition begins, its role snapshot is present and
|
||||
never returns to absent. Every non-process physical field is optional while
|
||||
acquisition is partial; every process field uses the three-phase slot above.
|
||||
Within Intent, optional fields move only absent-to-present. A newly acquired
|
||||
child slot moves only `Unassigned` to `Staged` to the exact same current
|
||||
identity in `Committed`. An already committed current owner or supervising
|
||||
During acquisition, optional fields move only absent-to-present. A newly
|
||||
acquired child slot moves only from unassigned to staged to committed with the
|
||||
exact same current identity. An already committed current owner or supervising
|
||||
process may enter a newly created dependent-role snapshot directly, but that
|
||||
recorded identity then remains immutable. Recorded evidence cannot be replaced
|
||||
or cleared.
|
||||
|
|
@ -435,30 +436,29 @@ The direct existing-process edges are Network RS, Helper RS, Sandbox HC, and
|
|||
Session Terminal HC. State Anchor daemon, Git-routing daemon, Helper process,
|
||||
Sandbox RS, attached runsc, and Session Terminal exec client are acquired child
|
||||
edges and require staging.
|
||||
No bare Intent moves directly to an active state: a non-empty acquisition
|
||||
snapshot is committed first. PreparedLower additionally records
|
||||
`lease_state=Intent` before the catalog insertion changes both participant and
|
||||
lease phase to `LeaseHeld`.
|
||||
No bare intent moves directly to an active state: a non-empty acquisition
|
||||
snapshot is committed first. Prepared-lower acquisition records lease intent
|
||||
before catalog insertion and becomes lease-held only after that insertion.
|
||||
|
||||
The active Participant pairs are `prepared_lower=LeaseHeld`,
|
||||
`state_anchor=Prepared`, `git_routing=Prepared`, and
|
||||
`network|helper|sandbox|publication=Committed`. An active snapshot contains all
|
||||
role-required physical evidence and current committed pidfs ownership in every
|
||||
required process slot. `SessionTerminal=Running` likewise requires its
|
||||
An active prepared lower has a held lease; an active State Anchor and Git
|
||||
router are prepared; and active network, helper, sandbox, and publication
|
||||
ownership is committed. An active snapshot contains all role-required physical
|
||||
evidence and current committed pidfs ownership in every required process slot.
|
||||
A running Session Terminal likewise requires its
|
||||
container, PTY, guest identity, and current committed HC and exec-client slots.
|
||||
Staged or unassigned process ownership cannot satisfy either boundary.
|
||||
Network readiness evidence must also name the enclosing generation and match
|
||||
its policy, fingerprint, namespace, and committed RS identity internally.
|
||||
|
||||
Any partial or active snapshot moves to `ReleaseIntent` while preserving every
|
||||
Any partial or active snapshot moves to release intent while preserving every
|
||||
recorded identity. A staged current identity remains exact cleanup and recovery
|
||||
authority in ReleaseIntent. `ReleaseIntent` becomes `Clean` only after exact or
|
||||
independent absence proof; that transaction clears every process slot to
|
||||
Unassigned and every optional physical field to absent. Clean retains the
|
||||
authority during release. Release becomes clean only after exact or independent
|
||||
absence proof; that transaction clears every process slot to unassigned and
|
||||
every optional physical field to absent. Clean retains the
|
||||
logical generation key, role, and state as an explicit empty role snapshot. A
|
||||
bare Intent may become that explicit Clean snapshot only after the sealed
|
||||
bare intent may become that explicit clean snapshot only after the sealed
|
||||
runtime-absence check. No ordinary lifecycle transition may clear evidence or
|
||||
produce Clean.
|
||||
produce clean state.
|
||||
|
||||
An exited, unreaped child remains pinned while acquisition completes. The
|
||||
descriptor-based child check rejects a foreign replacement, while the exclusive
|
||||
|
|
@ -466,7 +466,7 @@ same-parent broker prevents a replacement child from passing the same-parent
|
|||
control case. Implementations preserve these as safety conditions rather than
|
||||
timing assumptions.
|
||||
|
||||
`PidfsRecoveryMatch` is the only positive recovery reacquisition path:
|
||||
Exact pidfs recovery matching is the only positive recovery reacquisition path:
|
||||
|
||||
1. Read and validate the current boot ID.
|
||||
2. On boot mismatch, do not look up the stored PID. Reconcile only resources
|
||||
|
|
@ -500,7 +500,7 @@ protocol credentials use distinct leaf keys physically held by HC; the Agent
|
|||
Sandbox uses another request-signing key. The publication identity pins the CA,
|
||||
manifest, and coordinator TLS leaf in the validated host-private Domain path,
|
||||
while the exact sandbox credential mount pins the same manifest. Protocol
|
||||
credential IDs are SHA-256 digests of their signed claims. `SessionCoordinator`
|
||||
credential IDs are SHA-256 digests of their signed claims. Session Coordinator
|
||||
remains the logical protocol role; HC is its physical key holder, not another
|
||||
principal.
|
||||
|
||||
|
|
@ -532,7 +532,7 @@ generation.
|
|||
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
|
||||
Session PTY attachment path. Lazaret does not depend on `runsc exec
|
||||
-console-socket`.
|
||||
|
||||
Session terminal ownership is the Host Coordinator; a Client CLI never inherits
|
||||
|
|
@ -562,9 +562,10 @@ Disconnected Client Sessions close rather than reattach to an unbounded scrollba
|
|||
owned by the coordinator.
|
||||
|
||||
The session connection carries the terminal events and messages described by
|
||||
this refinement and encoded by the repository schema. One Host Coordinator event
|
||||
loop serializes input, resize, signal, close, prompt-routing, PTY output, and
|
||||
exec-client completion for each Session ID. It uses bounded queues and PTY
|
||||
this refinement. The non-authoritative repository schema mirrors their v1
|
||||
encoding. One Host Coordinator event loop serializes input, resize, signal,
|
||||
close, prompt-routing, PTY output, and exec-client completion for each Session
|
||||
ID. It uses bounded queues and PTY
|
||||
backpressure; terminal data for one session cannot consume another session's
|
||||
control capacity. Input, resize, and signal events are accepted only while the
|
||||
modeled terminal route is the sandbox route. An invalid Session ID, inactive
|
||||
|
|
@ -587,9 +588,9 @@ connection is already lost, the outcome is not retained for reattachment.
|
|||
|
||||
Physical Session Terminal acquisition is ordered as follows:
|
||||
|
||||
1. The Host Coordinator records `SessionTerminal=Intent` in the Domain Store.
|
||||
2. It allocates the PTY and starts the exec wrapper through
|
||||
`CausalChildAcquisitionV1` with the expected committed HC pidfs authority.
|
||||
1. The Host Coordinator records terminal intent in the Domain Store.
|
||||
2. It allocates the PTY and starts the exec wrapper through the causal child
|
||||
acquisition protocol with the expected committed HC pidfs authority.
|
||||
The wrapper arms its HC parent-death edge, rechecks that authority, and aborts
|
||||
before invoking runsc if it differs. It may create the guest process only
|
||||
after staged exec-client ownership is durably committed and the barrier is
|
||||
|
|
@ -598,10 +599,10 @@ Physical Session Terminal acquisition is ordered as follows:
|
|||
start time, and group ID.
|
||||
4. One Domain Store transaction promotes the exact Host Coordinator and exec
|
||||
client ownership to committed, records the PTY, container, guest leader, and
|
||||
guest process-group identities, and sets `SessionTerminal=Running`.
|
||||
guest process-group identities, and marks the Session Terminal running.
|
||||
5. Only then may the Host Coordinator accept terminal events for the session.
|
||||
|
||||
Failure before `Running` never admits the terminal. A live Host Coordinator uses
|
||||
Failure before the running state never admits the terminal. A live Host Coordinator uses
|
||||
its in-memory exact handles to terminate any partial exec and guest group and
|
||||
records release intent. If HC itself is lost, the armed exec edge stops the host
|
||||
client and the generation lease-loss path stops the guest sandbox; bootstrap
|
||||
|
|
@ -611,7 +612,7 @@ Session close, Client connection loss, PTY loss, or exec-client loss starts the
|
|||
same physical release:
|
||||
|
||||
1. Apply the modeled session close, remove terminal and escalation routing, and
|
||||
record `SessionTerminal=ReleaseIntent` while retaining all exact identities.
|
||||
record terminal release intent while retaining all exact identities.
|
||||
2. If the exact generation is still serviceable and the guest leader identity
|
||||
and group still match, send `SIGHUP`, wait for a bounded grace period, then
|
||||
send `SIGTERM`, wait again, and send `SIGKILL` if the group remains. A leader
|
||||
|
|
@ -619,7 +620,7 @@ same physical release:
|
|||
an empty recorded group needs no signal; a nonempty group is left in release
|
||||
intent for Domain teardown.
|
||||
3. Terminate and reap the exact exec client when it is still a Host Coordinator
|
||||
child and close the exact PTY master. Record `SessionTerminal=Clean` only
|
||||
child and close the exact PTY master. Record the terminal clean only
|
||||
after the guest group, exec client, and PTY are absent; otherwise retain
|
||||
release intent.
|
||||
|
||||
|
|
@ -638,7 +639,7 @@ absent, never recreates a PTY or reattaches a Client Session, releases the
|
|||
retained prepared lower under the durable generation refinement, verifies that
|
||||
the exact generation container and guest processes are gone, terminates any
|
||||
still-live exact exec-client host process, and then records each retained Session
|
||||
Terminal `Clean`. An `Intent` without physical identities becomes `Clean` only
|
||||
Terminal clean. Intent without physical identities becomes clean only
|
||||
after that runtime-absence check. A process, container, PTY, or generation
|
||||
mismatch fails closed and retains the record; it is never adopted or signaled as
|
||||
the recorded session.
|
||||
|
|
@ -661,7 +662,8 @@ behavior when fully bidirectional ignored paths are required.
|
|||
|
||||
#### Ignored Workspace State routing contract
|
||||
|
||||
The production router is a dedicated rootless host FUSE filesystem. It presents
|
||||
Lazaret v1 routes Ignored Workspace State through a dedicated rootless host FUSE filesystem.
|
||||
It presents
|
||||
one workspace tree and chooses exactly one backing for each pathname operation:
|
||||
the canonical Agent Workspace for tracked and ordinary non-ignored paths, or the
|
||||
Domain's Ignored Workspace State for ignored untracked paths. The `.git` entry is
|
||||
|
|
@ -775,10 +777,10 @@ image with a Domain-scoped writable upper directory.
|
|||
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
|
||||
image identity. A live container-engine image mount cannot serve as the 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.
|
||||
preparation. Lazaret does not use an unsupported ad hoc tar extractor.
|
||||
|
||||
Prepared-artifact identity is independent of its storage pathname. The Domain
|
||||
Store and Storage Catalog encode the model's generation-to-artifact lease with
|
||||
|
|
@ -802,53 +804,54 @@ 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 versions fail closed before
|
||||
defined by the protocol model. The v1 store encodes that generation document
|
||||
in typed tables under a store version (unknown versions fail closed before
|
||||
row interpretation), including generation identity,
|
||||
minted runtime component IDs, and participant ownership material (for example
|
||||
prepared-artifact ID, staged or committed pidfs process ownership, mount
|
||||
identity, and network readiness fingerprint).
|
||||
Participant roles are `prepared_lower`, `state_anchor`, `git_routing`, `network`,
|
||||
`helper`, `sandbox`, and `publication`. The `helper` participant independently
|
||||
Prepared lower, State Anchor, Git routing, network, connectivity helper, sandbox,
|
||||
and publication ownership remain independently represented. Connectivity-helper
|
||||
ownership independently
|
||||
records durable intent and exact committed connectivity-helper pidfs ownership
|
||||
before the `network` participant records readiness. Sessions and the generation mailbox
|
||||
before network ownership records readiness. Sessions and the generation mailbox
|
||||
are separate generation records. Deterministic paths are lookup hints for
|
||||
physical recovery, not ownership proofs.
|
||||
|
||||
The repository [design schemas](schema.md) encode the logical records and
|
||||
relationships described by these refinements. Their implementation
|
||||
representation must preserve the distinct Domain Store and Storage Catalog
|
||||
boundaries. Opaque generation documents are not a product storage format.
|
||||
The non-authoritative repository [design schemas](schema.md) mirror the logical
|
||||
records and relationships described by these refinements. Implementations must
|
||||
preserve the distinct Domain Store and Storage Catalog authority boundaries and
|
||||
the independently recoverable ownership described above.
|
||||
|
||||
Each catalog operation acquires host-wide `storage-catalog.lock`, opens the
|
||||
catalog, performs one redb transaction, closes it, and releases the lock. The
|
||||
lock covers lease changes, prepare publication, and transition to `Reclaiming`.
|
||||
This permits concurrent Domain coordinators without a persistent global daemon
|
||||
or concurrent redb opens.
|
||||
Lazaret v1 stores the catalog in redb. Each catalog operation holds the
|
||||
host-wide Storage Catalog lock for one bounded open, transaction, and close
|
||||
section. The lock covers lease changes, prepare publication, and transition to
|
||||
reclamation. This permits concurrent Domain coordinators without a persistent
|
||||
global daemon or concurrent catalog opens.
|
||||
|
||||
The physical lease-acquisition refinement is:
|
||||
|
||||
1. Commit `prepared_lower = Intent` in the Domain Store with the intended
|
||||
1. Commit prepared-lower intent in the Domain Store with the intended
|
||||
prepared-artifact identity.
|
||||
2. Under `storage-catalog.lock`, insert the exact `(prepared-artifact ID, Domain
|
||||
2. Under the Storage Catalog lock, insert the exact `(prepared-artifact ID, Domain
|
||||
ID, generation)` lease in one catalog transaction.
|
||||
3. Commit `prepared_lower = LeaseHeld` in the Domain Store.
|
||||
4. Commit `state_anchor = Intent`, create the exact mount, and then commit
|
||||
`state_anchor = Prepared` with its mount identity.
|
||||
3. Commit that the prepared-lower lease is held in the Domain Store.
|
||||
4. Commit State Anchor intent, create the exact mount, and then commit prepared
|
||||
State Anchor ownership with its mount identity.
|
||||
|
||||
The physical unmount and lease-release refinement is:
|
||||
|
||||
1. Commit `state_anchor = ReleaseIntent` while retaining its exact mount and
|
||||
1. Commit State Anchor release intent while retaining its exact mount and
|
||||
prepared-artifact identity.
|
||||
2. Verify the recorded mount identity and unmount it. A mismatched mount refuses
|
||||
release and remains untouched.
|
||||
3. After independently observing that the exact mount is absent, atomically
|
||||
commit `state_anchor = Clean` and `prepared_lower = ReleaseIntent` in the
|
||||
commit clean State Anchor state and prepared-lower release intent in the
|
||||
Domain Store.
|
||||
4. Under `storage-catalog.lock`, recheck the matching Domain release intent and
|
||||
4. Under the Storage Catalog lock, recheck the matching Domain release intent and
|
||||
absence of the exact mount, then remove only the exact generation lease in one
|
||||
catalog transaction.
|
||||
5. Commit `prepared_lower = Clean` in the Domain Store.
|
||||
5. Commit clean prepared-lower state in the Domain Store.
|
||||
|
||||
Host Coordinator hard loss uses the model's split lease-loss refinement. The
|
||||
surviving exact Runtime Supervisor stops the sandbox and sidecar, verifies and
|
||||
|
|
@ -859,27 +862,27 @@ catalog lease removal. The catalog lease remains held after unmount.
|
|||
|
||||
Bootstrap recovery begins only after the Runtime Supervisor and attached runsc
|
||||
are absent. If the exact mount remains, the bootstrap Host Coordinator records
|
||||
`state_anchor = ReleaseIntent` and completes normal exact unmount. If the
|
||||
State Anchor release intent and completes normal exact unmount. If the
|
||||
surviving Runtime Supervisor already unmounted it, bootstrap independently
|
||||
verifies exact mount absence. It then atomically commits `state_anchor = Clean`
|
||||
and `prepared_lower = ReleaseIntent`, removes the exact catalog lease under the
|
||||
catalog lock, and commits `prepared_lower = Clean`. Thus lease-loss unmount and
|
||||
lease release are distinct: only a lock-holding Host Coordinator releases the
|
||||
prepared-lower lease.
|
||||
verifies exact mount absence. It then atomically commits clean State Anchor
|
||||
state and prepared-lower release intent, removes the exact catalog lease under
|
||||
the catalog lock, and commits clean prepared-lower state. Thus lease-loss
|
||||
unmount and lease release are distinct: only a lock-holding Host Coordinator
|
||||
releases the prepared-lower lease.
|
||||
|
||||
Recovery resumes only from matching durable identity. `state_anchor =
|
||||
ReleaseIntent` retains the catalog lease while recovery verifies and completes
|
||||
the unmount. `prepared_lower = ReleaseIntent` permits removal of a still-present
|
||||
exact catalog lease only after the exact mount is absent; an already-absent lease
|
||||
permits the Domain participant to become `Clean`. A catalog lease with missing,
|
||||
Recovery resumes only from matching durable identity. State Anchor release
|
||||
intent retains the catalog lease while recovery verifies and completes the
|
||||
unmount. Prepared-lower release intent permits removal of a still-present exact
|
||||
catalog lease only after the exact mount is absent; an already-absent lease
|
||||
permits the Domain ownership to become clean. A catalog lease with missing,
|
||||
unreadable, non-release, or mismatched Domain evidence is retained and reported.
|
||||
A Domain `LeaseHeld` record whose exact catalog lease is absent is inconsistent
|
||||
and fails closed; recovery neither recreates the lease nor mounts the State
|
||||
Anchor. A failed generation with a Prepared anchor, an absent exact mount, and a
|
||||
still-present exact catalog lease is the conservative HC-loss state above; only
|
||||
bootstrap recovery may advance it to release intent. These rules make every
|
||||
interrupted release conservative and prevent a mounted State Anchor from
|
||||
becoming unleased.
|
||||
A Domain record claiming a held lease whose exact catalog lease is absent is
|
||||
inconsistent and fails closed; recovery neither recreates the lease nor mounts
|
||||
the State Anchor. A failed generation with a prepared anchor, an absent exact
|
||||
mount, and a still-present exact catalog lease is the conservative HC-loss
|
||||
state above; only bootstrap recovery may advance it to release intent. These
|
||||
rules make every interrupted release conservative and prevent a mounted State
|
||||
Anchor from becoming unleased.
|
||||
|
||||
Store version acceptance occurs before row interpretation or physical resource
|
||||
inspection. The first product Domain Store identity is
|
||||
|
|
@ -905,26 +908,25 @@ network-administration capability in the subordinate Domain user namespace for
|
|||
its generation lifetime; it is a trusted host runtime process and has no
|
||||
authority over initial-user-namespace host network resources. The Agent Sandbox
|
||||
OCI process does not receive the 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,
|
||||
enforcement namespace, not the host network namespace. Lazaret v1 uses
|
||||
`slirp4netns` for connectivity. Installing policy by driving nftables through runsc into the
|
||||
guest is not a supported path. Protocol helper ownership, network readiness,
|
||||
and publication gates follow the protocol model.
|
||||
|
||||
#### Derived policy and readiness encoding
|
||||
|
||||
The repository [design schemas](schema.md) encode the policy, attestation,
|
||||
readiness-identity projection, and fingerprint inputs described by this
|
||||
refinement.
|
||||
The non-authoritative repository [design schemas](schema.md) mirror the v1
|
||||
policy, attestation, readiness-identity projection, and fingerprint inputs
|
||||
described by this refinement.
|
||||
|
||||
The Host Coordinator passes canonical policy bytes through a write-sealed
|
||||
inherited memfd. The Runtime Supervisor verifies the seals and digest, installs
|
||||
the policy, and returns observed route, helper, process, and namespace evidence
|
||||
over an inherited Host Coordinator-created private `SOCK_SEQPACKET` channel.
|
||||
Before helper launch, the Host Coordinator commits the independent `helper`
|
||||
participant as `Intent`. It acquires the helper through
|
||||
`CausalChildAcquisitionV1`; after the exact helper and supervising Runtime
|
||||
Supervisor pidfs ownership is committed, it may accept network readiness
|
||||
evidence and advance the `network` participant.
|
||||
The v1 policy transport passes canonical bytes through a write-sealed inherited
|
||||
memfd. The Runtime Supervisor verifies the seals and digest, installs the policy,
|
||||
and returns observed route, helper, process, and namespace evidence over an
|
||||
inherited Host Coordinator-created private `SOCK_SEQPACKET` channel.
|
||||
Before helper launch, the Host Coordinator durably records independent helper
|
||||
intent. It acquires the helper through the causal child acquisition protocol;
|
||||
after the exact helper and supervising Runtime Supervisor pidfs ownership is
|
||||
committed, it may accept network readiness evidence.
|
||||
The Host Coordinator independently reads the Runtime Supervisor's namespace
|
||||
identity and records the network readiness fingerprint as the durable encoding
|
||||
of protocol network readiness. Before publication, Lazaret verifies from the
|
||||
|
|
@ -946,7 +948,7 @@ host configuration.
|
|||
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.
|
||||
`blackhole` routes are not used for denial on 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.
|
||||
|
|
@ -967,19 +969,21 @@ generation identity and are opened through Host Coordinator-owned directory
|
|||
handles. Host-only CLI/coordinator control may use host-private Unix sockets that
|
||||
are never mounted into the Agent Sandbox.
|
||||
|
||||
Mailbox files carry the signed protocol records described by this refinement and
|
||||
encoded by the repository schema; TLS is not layered over the regular-file
|
||||
transport. HC opens each ready entry relative to a confined directory handle,
|
||||
Mailbox files carry the signed protocol records described by this refinement;
|
||||
the non-authoritative repository schema mirrors their v1 encoding. TLS is not
|
||||
layered over the regular-file transport. HC opens each ready entry relative to a
|
||||
confined directory handle,
|
||||
rejects links and non-regular files, bounds the complete file before allocation,
|
||||
and reads it once. It verifies the signature over those owned bytes before
|
||||
parsing. Pathnames, file ownership, mailbox identity files, PIDs, and start times
|
||||
are not authentication evidence.
|
||||
|
||||
Requests, cancellations, acknowledgements, developer decisions, chunks, and
|
||||
terminal results use the signer relationships in the schema. Postcard payloads
|
||||
are signed with `lazaret/v1/` plus the lower-kebab schema record name and their
|
||||
exact encoded length and bytes. A complete record is at most 65,536 bytes; a
|
||||
result chunk contains at most 49,152 output bytes.
|
||||
terminal results use the signer relationships defined by the protocol
|
||||
cryptography refinement. The v1 wire format uses Postcard payloads and signs
|
||||
`lazaret/v1/`, the lower-kebab record name, the exact encoded length, and the
|
||||
encoded bytes. A complete record is at most 65,536 bytes; a result chunk
|
||||
contains at most 49,152 output bytes.
|
||||
|
||||
The Escalation Client acknowledges the highest contiguous result sequence with an
|
||||
Agent Sandbox signature. HC retains at most eight unacknowledged chunks per
|
||||
|
|
@ -1030,13 +1034,13 @@ not duplicated here.
|
|||
| **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 Runtime Supervisor shall irreversibly drop network-administration capability after initial attached-runsc network import and before publication. Trusted attached runsc may retain that capability only in the subordinate Domain user namespace for its generation lifetime. The Agent Sandbox process specification shall omit the capability and set `noNewPrivileges`. |
|
||||
| **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-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 used for denial on this path. |
|
||||
| **SR-10** | Domain sockets, mailboxes, and coordination files shall reside in a host-private directory owned by the developer. |
|
||||
| **SR-11** | Runtime and persistent path construction shall begin from validated Domain roots, include the Domain ID in resource identities, and verify stored Domain identity before reuse. |
|
||||
| **SR-12** | The runsc OCI specification shall create private PID, IPC, UTS, mount, and user namespaces and set its network namespace path to the independently verified Runtime Supervisor namespace descriptor. It shall contain no host namespace path entry. |
|
||||
| **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. Archive export alone shall not be treated as a complete preparation boundary. |
|
||||
| **SR-15** | Lazaret shall not use a live container-engine image mount as the State Anchor lower; the lower shall be a Lazaret-owned prepared lower. Archive export alone shall not be treated as a complete preparation boundary. |
|
||||
|
||||
### 4.2 Functional Requirements
|
||||
|
||||
|
|
@ -1045,18 +1049,18 @@ not duplicated here.
|
|||
| **FR-1** | Lazaret shall derive a stable Domain ID from the selected Agent Profile and canonical Agent Workspace. |
|
||||
| **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-7** | Product recovery shall inspect external runtime resources independently of owner-process liveness. Host-process action shall require the retained pidfd or `PidfsRecoveryMatch` against staged or committed current `PidfsProcessIdentityV1`; unequal pidfs authority, boot or namespace ambiguity, and unreadable negative evidence shall refuse without numeric-PID signaling. Staged ownership authorizes only exact cleanup/recovery, never service or adoption. Recovery shall also compare typed namespace, mount, artifact, path, and inode evidence before physical cleanup. |
|
||||
| **FR-7** | Product recovery shall inspect external runtime resources independently of owner-process liveness. Host-process action shall require a retained pidfd or exact pidfs recovery match against staged or committed current process identity; unequal pidfs authority, boot or namespace ambiguity, and unreadable negative evidence shall refuse without numeric-PID signaling. Staged ownership authorizes only exact cleanup/recovery, never service or adoption. Recovery shall also compare namespace, mount, artifact, path, and inode evidence before physical cleanup. |
|
||||
| **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-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-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 preserve the Session Terminal record and protocol described by the Session Terminal refinement; serialize bounded terminal events and merged output by Session ID; map resize and the `Interrupt`, `Quit`, and `Suspend` events to the specified exact process-group operations; collect exit status from the non-detached `runsc exec` client; and follow the specified release and hard-loss recovery ordering without reattachment or mismatched cleanup. |
|
||||
| **FR-16** | Domain network connectivity shall use `slirp4netns` as the production connectivity helper. The Domain Store shall record independent `helper` intent before launch and exact committed helper and supervising Runtime Supervisor pidfs ownership before network readiness. |
|
||||
| **FR-17** | The Domain Store shall be opened only by the Host Coordinator process holding the Domain `flock`; mutations shall use whole redb transactions. Storage Catalog opens shall be bounded by `storage-catalog.lock` and one transaction. Cross-store lease release shall follow the durable release-intent, exact-unmount, catalog-delete, Domain-clean ordering defined by the durable generation refinement. |
|
||||
| **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. Session PTYs shall not depend on `runsc exec -console-socket`. |
|
||||
| **FR-15** | For each interactive Client Session, Lazaret shall preserve the durable terminal authority and protocol described by the Session Terminal refinement; serialize bounded terminal events and merged output by Session ID; map resize and the `Interrupt`, `Quit`, and `Suspend` events to the specified exact process-group operations; collect exit status from the non-detached `runsc exec` client; and follow the specified release and hard-loss recovery ordering without reattachment or mismatched cleanup. |
|
||||
| **FR-16** | Lazaret v1 shall use `slirp4netns` as the Domain connectivity helper. The Domain Store shall record independent helper intent before launch and exact committed helper and supervising Runtime Supervisor pidfs ownership before network readiness. |
|
||||
| **FR-17** | The Domain Store shall be opened only by the Host Coordinator process holding the Domain `flock`; mutations shall use atomic transactions. Storage Catalog access shall use one bounded lock/open/transaction/close section. Cross-store lease release shall follow the durable release-intent, exact-unmount, catalog-delete, Domain-clean ordering defined by the durable generation refinement. |
|
||||
| **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 Domain Store and Storage Catalog shall preserve the records, ownership variants, identities, and relationships described by the durable-generation and prepared-lower refinements. |
|
||||
| **FR-21** | The Domain Store and Storage Catalog shall preserve the independently recoverable ownership, identities, and authority relationships described by the durable-generation and prepared-lower refinements. |
|
||||
| **FR-22** | Preparation shall use a supported OCI-aware preparer that materialises a Lazaret-owned immutable rootfs with source identity and prepared-artifact ID. |
|
||||
|
||||
### 4.3 Developer-Experience Requirements
|
||||
|
|
@ -1074,7 +1078,7 @@ not duplicated here.
|
|||
|
||||
| ID | Requirement |
|
||||
| :--- | :--- |
|
||||
| **OR-4** | Security-sensitive behavior shall be covered by integration tests on supported runsc, filesystem, and network configurations. |
|
||||
| **OR-4** | Release qualification shall cover the supported runsc launch, routed-workspace filesystem, and rootless network paths. |
|
||||
| **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. Shared Storage Catalog operations shall use bounded lock/open/transaction/close critical sections. |
|
||||
| **OR-7** | Product GC shall provide policy-controlled reclamation for prepared artifacts after all protocol leases for the prepared-artifact ID are released. Shared-artifact reclaim shall wait until no lease remains for that artifact. In-progress prepare trees and foreign trees shall not be deleted; exact-owned abandoned prepare trees may be reclaimed only through fail-closed recovery backed by durable prepare intent. |
|
||||
|
|
|
|||
Loading…
Reference in a new issue