ms2k/lazaret
SHA256
Watch
0
Code Releases 3 Activity

Refine rootless and network readiness contracts

Browse source 
Correct the caller-configured user-namespace topology, bind modeled network readiness to the live sandbox and helper, and keep physical canary, topology, encoding, and capability predicates in compact specification tables below the model boundary.
This commit is contained in:
ms2k 2026-07-19 19:52:41 +09:00
commit 02fc29acb1
2 changed files with 120 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

1
docs/protocol/Lazaret.cfg
View file

@ -91,6 +91,7 @@ INVARIANTS
OrderedFailureRecovery
ResultDeliveryStateConsistent
MultiRoleDurableIntent
NetworkReadinessBoundToSandbox
GenerationScopedIdentitiesDistinct
HelperUnderSupervisor
PreparedLowerLeaseBeforeMount

46
docs/protocol/Lazaret.tla
View file

@ -655,6 +655,8 @@ StartSidecar(d) ==
/\ SidecarCertificateValid[d]
/\ sidecarState[d] = "Stopped"
/\ sidecarState' = [sidecarState EXCEPT ![d] = "Ready"]
/\ durableIntent' = [durableIntent EXCEPT ![d] =
[@ EXCEPT !["network"] = TRUE]]
/\ UNCHANGED <<
domainPhase, stateAnchorState, sandboxState,
trustReady, lockOwner, published, registered, connected, sessionPhase,
@ -663,7 +665,8 @@ StartSidecar(d) ==
hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
durableDecision, pathMismatch, genCoordinatorId, genSidecarId,
genSandboxId, networkReady, preparedLowerLeased, helperProc
>>
ArmRuntimeCausalEdge(d) ==
@ -694,8 +697,9 @@ StartSandbox(d) ==
/\ supervisorLease[d] = "Held"
/\ runtimeCausalEdge[d] = "Armed"
/\ sidecarState[d] = "Ready"
/\ networkReady[d]
/\ durableIntent[d]["network"]
/\ helperProc[d] = "Alive"
/\ durableIntent[d]["helper"]
/\ durableIntent[d]["anchor"]
/\ durableIntent[d]["prepared_lower"]
/\ sandboxState[d] = "Stopped"
@ -876,6 +880,7 @@ StopSandbox(d) ==
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
/\ UNCHANGED <<
domainPhase, stateAnchorState, sidecarState,
trustReady, lockOwner, published, registered, connected, sessionPhase,
@ -884,7 +889,8 @@ StopSandbox(d) ==
hostCoordinatorProc, runtimeSupervisorProc, supervisorLease,
runtimeFaultsRemaining,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, preparedLowerLeased, helperProc
>>
StopSidecar(d) ==
@ -1367,12 +1373,14 @@ HardLoseAttachedRunsc(d) ==
/\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Dead"]
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
/\ UNCHANGED <<
stateAnchorState, sidecarState, approvalSource, approvedCommand,
domainLockHeld, hostCoordinatorProc, runtimeSupervisorProc,
supervisorLease,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, preparedLowerLeased, helperProc
>>
StopHostCoordinatorProcess(d) ==
@ -1506,6 +1514,7 @@ LeaseTeardownStopSandbox(d) ==
/\ attachedRunscProc' = [attachedRunscProc EXCEPT
![d] = IF ProcessPresent(attachedRunscProc[d]) THEN "Dead" ELSE "Absent"]
/\ runtimeCausalEdge' = [runtimeCausalEdge EXCEPT ![d] = "Unarmed"]
/\ networkReady' = [networkReady EXCEPT ![d] = FALSE]
/\ UNCHANGED <<
domainPhase, stateAnchorState, sidecarState,
trustReady, lockOwner, published, registered, connected, sessionPhase,
@ -1514,7 +1523,8 @@ LeaseTeardownStopSandbox(d) ==
hostCoordinatorProc, runtimeSupervisorProc, supervisorLease,
runtimeFaultsRemaining,
domainGeneration,
durableDecision, durableIntent, pathMismatch, genCoordinatorId, genSidecarId, genSandboxId, networkReady, preparedLowerLeased, helperProc
durableDecision, durableIntent, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, preparedLowerLeased, helperProc
>>
LeaseTeardownStopSidecar(d) ==
@ -1835,6 +1845,7 @@ StartConnectivityHelper(d) ==
/\ RuntimeSupervisorAlive(d)
/\ supervisorLease[d] = "Held"
/\ sidecarState[d] = "Ready"
/\ durableIntent[d]["network"]
/\ helperProc[d] = "Absent"
/\ helperProc' = [helperProc EXCEPT ![d] = "Alive"]
/\ durableIntent' = [durableIntent EXCEPT ![d] =
@ -1850,19 +1861,22 @@ StartConnectivityHelper(d) ==
genSidecarId, genSandboxId, networkReady, preparedLowerLeased
>>
\* Authenticated network readiness (abstract fingerprint/attest gate).
\* Physical readiness evidence is an atomic refinement boundary here.
MarkNetworkReady(d) ==
/\ domainPhase[d] = "Starting"
/\ HostCoordinatorAlive(d)
/\ RuntimeSupervisorAlive(d)
/\ supervisorLease[d] = "Held"
/\ sidecarState[d] = "Ready"
/\ sandboxState[d] = "Ready"
/\ attachedRunscProc[d] = "Alive"
/\ runtimeCausalEdge[d] = "Armed"
/\ durableIntent[d]["sandbox"]
/\ durableIntent[d]["network"]
/\ helperProc[d] = "Alive"
/\ durableIntent[d]["helper"]
/\ ~networkReady[d]
/\ networkReady' = [networkReady EXCEPT ![d] = TRUE]
/\ durableIntent' = [durableIntent EXCEPT ![d] =
[@ EXCEPT !["network"] = TRUE]]
/\ UNCHANGED <<
domainPhase, stateAnchorState, sidecarState, sandboxState, trustReady,
lockOwner, published, registered, connected, sessionPhase,
@ -1870,8 +1884,9 @@ MarkNetworkReady(d) ==
approvalSource, approvedCommand, hostRunning, domainLockHeld,
hostCoordinatorProc, runtimeSupervisorProc, attachedRunscProc,
runtimeCausalEdge, supervisorLease, runtimeFaultsRemaining,
domainGeneration, durableDecision, pathMismatch, genCoordinatorId,
genSidecarId, genSandboxId, preparedLowerLeased, helperProc
domainGeneration, durableDecision, durableIntent, pathMismatch,
genCoordinatorId, genSidecarId, genSandboxId, preparedLowerLeased,
helperProc
>>
\* Helper-only hard loss: SC remains present; network readiness withdrawn.
@ -1906,9 +1921,9 @@ DomainServiceProgress(d) ==
\/ MountStateAnchor(d)
\/ StartSidecar(d)
\/ StartConnectivityHelper(d)
\/ MarkNetworkReady(d)
\/ ArmRuntimeCausalEdge(d)
\/ StartSandbox(d)
\/ MarkNetworkReady(d)
\/ PublishDomain(d)
\/ BeginTeardown(d)
\/ StopSandbox(d)
@ -2328,6 +2343,14 @@ MultiRoleDurableIntent ==
/\ (networkReady[d] => durableIntent[d]["network"])
/\ (helperProc[d] = "Alive" => durableIntent[d]["helper"])
NetworkReadinessBoundToSandbox ==
\A d \in Domains :
networkReady[d] =>
/\ sandboxState[d] = "Ready"
/\ ProcessPresent(attachedRunscProc[d])
/\ runtimeCausalEdge[d] = "Armed"
/\ helperProc[d] = "Alive"
Safety ==
/\ TypeOK
/\ ConfigurationConfinement
@ -2366,6 +2389,7 @@ Safety ==
/\ FailedDomainIsolation
/\ OrderedFailureRecovery
/\ ResultDeliveryStateConsistent
/\ NetworkReadinessBoundToSandbox
(***************************************************************************
Liveness properties.