docs: formalize protocol identity and transition to regular-file escalation mailbox
- Replaces stream/socket escalation with a sandboxed regular-file Escalation Mailbox to satisfy runsc isolation boundaries without exposing `host-uds=open`. - Expands the TLA+ protocol model with role-bound certificates, tuple authorization, and structured domain-failure recovery paths. - Adds physical integration journals for host terminfo injection, persistent /etc DNS shims, rootless Podman network topology, and static client delivery. - Establishes specification requirements for safe host-only State Anchor inspection and crash-consistent reset operations.
This commit is contained in:
parent
045387dc79
commit
682d7c7db7
1 changed files with 408 additions and 50 deletions
|
|
@ -4,9 +4,10 @@ EXTENDS Naturals, FiniteSets, Sequences, TLC
|
|||
(***************************************************************************
|
||||
Application-wide protocol model for Lazaret.
|
||||
|
||||
The model covers Domain startup, ordered resource preparation, sandbox launch
|
||||
isolation, Client Session registration, host escalation, correlated result
|
||||
delivery, terminal ownership, failure, and teardown.
|
||||
The model covers Domain startup, ordered resource preparation, role-separated
|
||||
runtime identity tuples, sandbox launch isolation, Client Session registration,
|
||||
host escalation, correlated result delivery, terminal ownership, failure, and
|
||||
teardown.
|
||||
Cryptographic algorithms, serialization, container commands, filesystems, and
|
||||
network packet handling are refinement boundaries validated by implementation
|
||||
tests rather than modeled internally.
|
||||
|
|
@ -17,6 +18,8 @@ CONSTANTS
|
|||
Sessions,
|
||||
Requests,
|
||||
Commands,
|
||||
Identities,
|
||||
SessionAnchors,
|
||||
NoSession,
|
||||
NoRequest,
|
||||
NoCommand,
|
||||
|
|
@ -24,14 +27,31 @@ CONSTANTS
|
|||
SessionDomain,
|
||||
SessionFingerprint,
|
||||
DomainFingerprint,
|
||||
DomainCoordinatorIdentity,
|
||||
DomainSidecarIdentity,
|
||||
DomainSandboxIdentity,
|
||||
SessionCliIdentity,
|
||||
SessionAnchorIdentity,
|
||||
CoordinatorCertificateValid,
|
||||
SidecarCertificateValid,
|
||||
SandboxCertificateValid,
|
||||
CliCertificateValid,
|
||||
ConfigSafe,
|
||||
SandboxIsolationSafe,
|
||||
RequestSession,
|
||||
RequestCommand,
|
||||
CertificateValid,
|
||||
SignatureValid,
|
||||
RequestSandboxIdentity,
|
||||
RequestCliIdentity,
|
||||
RequestSessionAnchor,
|
||||
RequestCredentialValid,
|
||||
RequestSignatureValid,
|
||||
ApprovalCliIdentity,
|
||||
ApprovalSessionAnchor,
|
||||
ApprovalSignatureValid,
|
||||
ApprovalCommand,
|
||||
AutoRuleMatches,
|
||||
CommandRequiresShell,
|
||||
CommandContentSafe,
|
||||
D1,
|
||||
S1,
|
||||
S2,
|
||||
|
|
@ -48,6 +68,8 @@ ASSUME
|
|||
/\ IsFiniteSet(Sessions)
|
||||
/\ IsFiniteSet(Requests)
|
||||
/\ IsFiniteSet(Commands)
|
||||
/\ IsFiniteSet(Identities)
|
||||
/\ IsFiniteSet(SessionAnchors)
|
||||
/\ Domains # {}
|
||||
/\ Sessions # {}
|
||||
/\ Requests # {}
|
||||
|
|
@ -57,16 +79,35 @@ ASSUME
|
|||
/\ SessionDomain \in [Sessions -> Domains]
|
||||
/\ SessionFingerprint \in [Sessions -> STRING]
|
||||
/\ DomainFingerprint \in [Domains -> STRING]
|
||||
/\ DomainCoordinatorIdentity \in [Domains -> Identities]
|
||||
/\ DomainSidecarIdentity \in [Domains -> Identities]
|
||||
/\ DomainSandboxIdentity \in [Domains -> Identities]
|
||||
/\ SessionCliIdentity \in [Sessions -> Identities]
|
||||
/\ SessionAnchorIdentity \in [Sessions -> SessionAnchors]
|
||||
/\ CoordinatorCertificateValid \in [Domains -> BOOLEAN]
|
||||
/\ SidecarCertificateValid \in [Domains -> BOOLEAN]
|
||||
/\ SandboxCertificateValid \in [Domains -> BOOLEAN]
|
||||
/\ CliCertificateValid \in [Sessions -> BOOLEAN]
|
||||
/\ ConfigSafe \in [Domains -> BOOLEAN]
|
||||
/\ SandboxIsolationSafe \in [Domains -> BOOLEAN]
|
||||
/\ RequestSession \in [Requests -> Sessions]
|
||||
/\ RequestCommand \in [Requests -> Commands]
|
||||
/\ CertificateValid \in [Requests -> BOOLEAN]
|
||||
/\ SignatureValid \in [Requests -> BOOLEAN]
|
||||
/\ RequestSandboxIdentity \in [Requests -> Identities]
|
||||
/\ RequestCliIdentity \in [Requests -> Identities]
|
||||
/\ RequestSessionAnchor \in [Requests -> SessionAnchors]
|
||||
/\ RequestCredentialValid \in [Requests -> BOOLEAN]
|
||||
/\ RequestSignatureValid \in [Requests -> BOOLEAN]
|
||||
/\ ApprovalCliIdentity \in [Requests -> Identities]
|
||||
/\ ApprovalSessionAnchor \in [Requests -> SessionAnchors]
|
||||
/\ ApprovalSignatureValid \in [Requests -> BOOLEAN]
|
||||
/\ ApprovalCommand \in [Requests -> Commands]
|
||||
/\ AutoRuleMatches \in [Requests -> BOOLEAN]
|
||||
/\ CommandRequiresShell \in [Commands -> BOOLEAN]
|
||||
/\ CommandContentSafe \in [Commands -> BOOLEAN]
|
||||
|
||||
DomainPhases == {"Absent", "Starting", "Ready", "Stopping", "Failed"}
|
||||
DomainPhases == {
|
||||
"Absent", "Starting", "Ready", "Stopping", "Failed", "Recovering"
|
||||
}
|
||||
CoordinatorStates == {"Absent", "Starting", "Ready", "Stopping", "Failed"}
|
||||
MountStates == {"Unmounted", "Mounted"}
|
||||
ResourceStates == {"Stopped", "Ready", "Failed"}
|
||||
|
|
@ -106,21 +147,56 @@ DomainsFixture == {D1}
|
|||
SessionsFixture == {S1, S2}
|
||||
RequestsFixture == {R1, R2, R3}
|
||||
CommandsFixture == {ExactCmd, PromptCmd, ShellCmd, EditedCmd}
|
||||
IdentitiesFixture == {
|
||||
"coordinator-1", "sidecar-1", "sandbox-1", "sandbox-other",
|
||||
"cli-1", "cli-2"
|
||||
}
|
||||
SessionAnchorsFixture == {"anchor-1", "anchor-2"}
|
||||
|
||||
SessionDomainFixture == (S1 :> D1) @@ (S2 :> D1)
|
||||
SessionFingerprintFixture ==
|
||||
(S1 :> "config-a") @@ (S2 :> "config-a")
|
||||
DomainFingerprintFixture == D1 :> "config-a"
|
||||
DomainCoordinatorIdentityFixture == D1 :> "coordinator-1"
|
||||
DomainSidecarIdentityFixture == D1 :> "sidecar-1"
|
||||
DomainSandboxIdentityFixture == D1 :> "sandbox-1"
|
||||
SessionCliIdentityFixture == (S1 :> "cli-1") @@ (S2 :> "cli-2")
|
||||
SessionAnchorIdentityFixture ==
|
||||
(S1 :> "anchor-1") @@ (S2 :> "anchor-2")
|
||||
CoordinatorCertificateValidFixture == D1 :> TRUE
|
||||
SidecarCertificateValidFixture == D1 :> TRUE
|
||||
SandboxCertificateValidFixture == D1 :> TRUE
|
||||
CliCertificateValidFixture == (S1 :> TRUE) @@ (S2 :> TRUE)
|
||||
ConfigSafeFixture == D1 :> TRUE
|
||||
SandboxIsolationSafeFixture == D1 :> TRUE
|
||||
RequestSessionFixture ==
|
||||
(R1 :> S1) @@ (R2 :> S2) @@ (R3 :> S1)
|
||||
RequestCommandFixture ==
|
||||
(R1 :> ExactCmd) @@ (R2 :> PromptCmd) @@ (R3 :> ShellCmd)
|
||||
CertificateValidFixture ==
|
||||
(R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> FALSE)
|
||||
SignatureValidFixture ==
|
||||
(R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> FALSE)
|
||||
RequestSandboxIdentityFixture ==
|
||||
(R1 :> "sandbox-1") @@
|
||||
(R2 :> "sandbox-1") @@
|
||||
(R3 :> "sandbox-other")
|
||||
RequestCliIdentityFixture ==
|
||||
(R1 :> "cli-1") @@ (R2 :> "cli-2") @@ (R3 :> "cli-1")
|
||||
RequestSessionAnchorFixture ==
|
||||
(R1 :> "anchor-1") @@
|
||||
(R2 :> "anchor-2") @@
|
||||
(R3 :> "anchor-1")
|
||||
RequestCredentialValidFixture ==
|
||||
(R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> TRUE)
|
||||
RequestSignatureValidFixture ==
|
||||
(R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> TRUE)
|
||||
ApprovalCliIdentityFixture ==
|
||||
(R1 :> "cli-1") @@ (R2 :> "cli-2") @@ (R3 :> "cli-1")
|
||||
ApprovalSessionAnchorFixture ==
|
||||
(R1 :> "anchor-1") @@
|
||||
(R2 :> "anchor-2") @@
|
||||
(R3 :> "anchor-1")
|
||||
ApprovalSignatureValidFixture ==
|
||||
(R1 :> TRUE) @@ (R2 :> TRUE) @@ (R3 :> TRUE)
|
||||
ApprovalCommandFixture ==
|
||||
(R1 :> ExactCmd) @@ (R2 :> EditedCmd) @@ (R3 :> ShellCmd)
|
||||
AutoRuleMatchesFixture ==
|
||||
(R1 :> TRUE) @@ (R2 :> FALSE) @@ (R3 :> TRUE)
|
||||
CommandRequiresShellFixture ==
|
||||
|
|
@ -128,6 +204,11 @@ CommandRequiresShellFixture ==
|
|||
(PromptCmd :> FALSE) @@
|
||||
(ShellCmd :> TRUE) @@
|
||||
(EditedCmd :> FALSE)
|
||||
CommandContentSafeFixture ==
|
||||
(ExactCmd :> TRUE) @@
|
||||
(PromptCmd :> TRUE) @@
|
||||
(ShellCmd :> TRUE) @@
|
||||
(EditedCmd :> TRUE)
|
||||
|
||||
VARIABLES
|
||||
domainPhase,
|
||||
|
|
@ -175,6 +256,41 @@ ReqSession(r) == RequestSession[r]
|
|||
ReqDomain(r) == Dom(ReqSession(r))
|
||||
IsTerminalRequest(r) == requestPhase[r] \in TerminalRequestPhases
|
||||
|
||||
RuntimeIdentityTupleReady(d) ==
|
||||
/\ trustReady[d]
|
||||
/\ sidecarState[d] = "Ready"
|
||||
/\ sandboxState[d] = "Ready"
|
||||
/\ CoordinatorCertificateValid[d]
|
||||
/\ SidecarCertificateValid[d]
|
||||
/\ SandboxCertificateValid[d]
|
||||
/\ Cardinality({
|
||||
DomainCoordinatorIdentity[d],
|
||||
DomainSidecarIdentity[d],
|
||||
DomainSandboxIdentity[d]
|
||||
}) = 3
|
||||
|
||||
SessionIdentityTupleRegistered(s) ==
|
||||
/\ s \in registered[Dom(s)]
|
||||
/\ s \in connected[Dom(s)]
|
||||
/\ CliCertificateValid[s]
|
||||
|
||||
RequestIdentityTupleMatches(r) ==
|
||||
LET s == ReqSession(r)
|
||||
d == ReqDomain(r)
|
||||
IN
|
||||
/\ RequestSandboxIdentity[r] = DomainSandboxIdentity[d]
|
||||
/\ RequestCliIdentity[r] = SessionCliIdentity[s]
|
||||
/\ RequestSessionAnchor[r] = SessionAnchorIdentity[s]
|
||||
|
||||
ApprovalIdentityTupleMatches(r) ==
|
||||
LET s == ReqSession(r) IN
|
||||
/\ ApprovalCliIdentity[r] = SessionCliIdentity[s]
|
||||
/\ ApprovalSessionAnchor[r] = SessionAnchorIdentity[s]
|
||||
\* This predicate abstracts verification over the request ID, decision, and
|
||||
\* exact approved command bytes, not merely verification of any signature by
|
||||
\* the registered key.
|
||||
/\ ApprovalSignatureValid[r]
|
||||
|
||||
Interested(d) == {
|
||||
s \in Sessions :
|
||||
Dom(s) = d /\
|
||||
|
|
@ -281,6 +397,7 @@ CreateTrustAnchor(d) ==
|
|||
/\ domainPhase[d] = "Starting"
|
||||
/\ coordinatorState[d] = "Starting"
|
||||
/\ ~trustReady[d]
|
||||
/\ CoordinatorCertificateValid[d]
|
||||
/\ trustReady' = [trustReady EXCEPT ![d] = TRUE]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
|
|
@ -293,6 +410,7 @@ StartSidecar(d) ==
|
|||
/\ domainPhase[d] = "Starting"
|
||||
/\ stateAnchorState[d] = "Mounted"
|
||||
/\ trustReady[d]
|
||||
/\ SidecarCertificateValid[d]
|
||||
/\ sidecarState[d] = "Stopped"
|
||||
/\ sidecarState' = [sidecarState EXCEPT ![d] = "Ready"]
|
||||
/\ UNCHANGED <<
|
||||
|
|
@ -307,6 +425,7 @@ StartSandbox(d) ==
|
|||
/\ sidecarState[d] = "Ready"
|
||||
/\ sandboxState[d] = "Stopped"
|
||||
/\ SandboxIsolationSafe[d]
|
||||
/\ SandboxCertificateValid[d]
|
||||
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Ready"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
|
|
@ -368,6 +487,7 @@ RegisterSession(s) ==
|
|||
/\ connectionState[s] = "Connected"
|
||||
/\ domainPhase[d] = "Ready"
|
||||
/\ SessionFingerprint[s] = DomainFingerprint[d]
|
||||
/\ CliCertificateValid[s]
|
||||
/\ registered' = [registered EXCEPT ![d] = @ \cup {s}]
|
||||
/\ connected' = [connected EXCEPT ![d] = @ \cup {s}]
|
||||
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
|
||||
|
|
@ -382,6 +502,8 @@ RegisterSession(s) ==
|
|||
DisconnectSession(s) ==
|
||||
LET d == Dom(s)
|
||||
r == activeRequest[s]
|
||||
leaderLost ==
|
||||
lockOwner[d] = s /\ domainPhase[d] = "Starting"
|
||||
IN
|
||||
/\ sessionPhase[s] \in {
|
||||
"Waiting", "Registering", "Attached", "Prompting", "HostExecuting"
|
||||
|
|
@ -397,9 +519,17 @@ DisconnectSession(s) ==
|
|||
THEN "Cancelled"
|
||||
ELSE requestPhase[q]]
|
||||
/\ hostRunning' = IF r = NoRequest THEN hostRunning ELSE hostRunning \ {r}
|
||||
/\ domainPhase' = [domainPhase EXCEPT
|
||||
![d] = IF leaderLost THEN "Failed" ELSE @]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT
|
||||
![d] = IF leaderLost THEN "Failed" ELSE @]
|
||||
/\ trustReady' = [trustReady EXCEPT
|
||||
![d] = IF leaderLost THEN FALSE ELSE @]
|
||||
/\ lockOwner' = [lockOwner EXCEPT
|
||||
![d] = IF leaderLost THEN NoSession ELSE @]
|
||||
/\ published' = IF leaderLost THEN published \ {d} ELSE published
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
sandboxState, trustReady, lockOwner, published, approvalSource,
|
||||
stateAnchorState, sidecarState, sandboxState, approvalSource,
|
||||
approvedCommand
|
||||
>>
|
||||
|
||||
|
|
@ -483,8 +613,11 @@ ReceiveEscalation(r) ==
|
|||
/\ activeRequest[s] = NoRequest
|
||||
/\ s \in registered[d]
|
||||
/\ s \in connected[d]
|
||||
/\ CertificateValid[r]
|
||||
/\ SignatureValid[r]
|
||||
/\ RuntimeIdentityTupleReady(d)
|
||||
/\ SessionIdentityTupleRegistered(s)
|
||||
/\ RequestIdentityTupleMatches(r)
|
||||
/\ RequestCredentialValid[r]
|
||||
/\ RequestSignatureValid[r]
|
||||
/\ requestPhase' = [requestPhase EXCEPT ![r] = "Verified"]
|
||||
/\ activeRequest' = [activeRequest EXCEPT ![s] = r]
|
||||
/\ UNCHANGED <<
|
||||
|
|
@ -536,7 +669,9 @@ DeveloperApprove(r, cmd) ==
|
|||
LET s == ReqSession(r) IN
|
||||
/\ requestPhase[r] = "AwaitingApproval"
|
||||
/\ sessionPhase[s] = "Prompting"
|
||||
/\ ApprovalIdentityTupleMatches(r)
|
||||
/\ cmd \in Commands
|
||||
/\ cmd = ApprovalCommand[r]
|
||||
/\ requestPhase' = [requestPhase EXCEPT ![r] = "Approved"]
|
||||
/\ approvalSource' = [approvalSource EXCEPT ![r] = "Developer"]
|
||||
/\ approvedCommand' = [approvedCommand EXCEPT ![r] = cmd]
|
||||
|
|
@ -550,6 +685,7 @@ DeveloperDeny(r) ==
|
|||
LET s == ReqSession(r) IN
|
||||
/\ requestPhase[r] = "AwaitingApproval"
|
||||
/\ sessionPhase[s] = "Prompting"
|
||||
/\ ApprovalIdentityTupleMatches(r)
|
||||
/\ requestPhase' = [requestPhase EXCEPT ![r] = "DenialPending"]
|
||||
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
|
||||
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
|
||||
|
|
@ -568,6 +704,7 @@ StartHostExecution(r) ==
|
|||
/\ activeRequest[s] = r
|
||||
/\ s \in connected[d]
|
||||
/\ sessionPhase[s] \in {"Attached", "Prompting"}
|
||||
/\ CommandContentSafe[approvedCommand[r]]
|
||||
/\ requestPhase' = [requestPhase EXCEPT ![r] = "Executing"]
|
||||
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "HostExecuting"]
|
||||
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "HostProcess"]
|
||||
|
|
@ -662,9 +799,6 @@ FailDomain(d) ==
|
|||
/\ domainPhase[d] \in {"Starting", "Ready", "Stopping"}
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Failed"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Failed"]
|
||||
/\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
|
||||
/\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
|
||||
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
|
||||
/\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
||||
/\ published' = published \ {d}
|
||||
|
|
@ -685,12 +819,18 @@ FailDomain(d) ==
|
|||
THEN "Failed"
|
||||
ELSE requestPhase[r]]
|
||||
/\ hostRunning' = hostRunning \ RequestsForDomain(d)
|
||||
/\ UNCHANGED <<approvalSource, approvedCommand>>
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, approvalSource,
|
||||
approvedCommand
|
||||
>>
|
||||
|
||||
ResetFailedDomain(d) ==
|
||||
BeginRecovery(d) ==
|
||||
/\ domainPhase[d] = "Failed"
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Absent"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
|
||||
/\ registered[d] = {}
|
||||
/\ connected[d] = {}
|
||||
/\ hostRunning \cap RequestsForDomain(d) = {}
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Recovering"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Stopping"]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
|
||||
published, registered, connected, sessionPhase, terminalRoute,
|
||||
|
|
@ -698,6 +838,57 @@ ResetFailedDomain(d) ==
|
|||
approvedCommand, hostRunning
|
||||
>>
|
||||
|
||||
RecoverSandbox(d) ==
|
||||
/\ domainPhase[d] = "Recovering"
|
||||
/\ sandboxState[d] # "Stopped"
|
||||
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
||||
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
>>
|
||||
|
||||
RecoverSidecar(d) ==
|
||||
/\ domainPhase[d] = "Recovering"
|
||||
/\ sandboxState[d] = "Stopped"
|
||||
/\ sidecarState[d] # "Stopped"
|
||||
/\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, stateAnchorState, sandboxState,
|
||||
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
>>
|
||||
|
||||
RecoverStateAnchor(d) ==
|
||||
/\ domainPhase[d] = "Recovering"
|
||||
/\ sandboxState[d] = "Stopped"
|
||||
/\ sidecarState[d] = "Stopped"
|
||||
/\ stateAnchorState[d] = "Mounted"
|
||||
/\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Unmounted"]
|
||||
/\ UNCHANGED <<
|
||||
domainPhase, coordinatorState, sidecarState, sandboxState, trustReady,
|
||||
lockOwner, published, registered, connected, sessionPhase,
|
||||
terminalRoute, connectionState, activeRequest, requestPhase,
|
||||
approvalSource, approvedCommand, hostRunning
|
||||
>>
|
||||
|
||||
FinishRecovery(d) ==
|
||||
/\ domainPhase[d] = "Recovering"
|
||||
/\ stateAnchorState[d] = "Unmounted"
|
||||
/\ sidecarState[d] = "Stopped"
|
||||
/\ sandboxState[d] = "Stopped"
|
||||
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Absent"]
|
||||
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
|
||||
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
||||
/\ UNCHANGED <<
|
||||
stateAnchorState, sidecarState, sandboxState, trustReady, published,
|
||||
registered, connected, sessionPhase, terminalRoute, connectionState,
|
||||
activeRequest, requestPhase, approvalSource, approvedCommand,
|
||||
hostRunning
|
||||
>>
|
||||
|
||||
DomainProgress(d) ==
|
||||
\/ MountStateAnchor(d)
|
||||
\/ CreateTrustAnchor(d)
|
||||
|
|
@ -709,7 +900,11 @@ DomainProgress(d) ==
|
|||
\/ StopSidecar(d)
|
||||
\/ UnmountStateAnchor(d)
|
||||
\/ FinishTeardown(d)
|
||||
\/ ResetFailedDomain(d)
|
||||
\/ BeginRecovery(d)
|
||||
\/ RecoverSandbox(d)
|
||||
\/ RecoverSidecar(d)
|
||||
\/ RecoverStateAnchor(d)
|
||||
\/ FinishRecovery(d)
|
||||
|
||||
SessionProgress(s) ==
|
||||
\/ StartNewDomain(s)
|
||||
|
|
@ -793,6 +988,18 @@ PublishedDomainsReady ==
|
|||
/\ sandboxState[d] = "Ready"
|
||||
/\ trustReady[d]
|
||||
|
||||
ExclusiveBootstrapOwnership ==
|
||||
\A d \in Domains : lockOwner[d] # NoSession =>
|
||||
/\ domainPhase[d] = "Starting"
|
||||
/\ coordinatorState[d] = "Starting"
|
||||
/\ sessionPhase[lockOwner[d]] = "Waiting"
|
||||
|
||||
TeardownNotJoinable ==
|
||||
\A d \in Domains : domainPhase[d] \in {"Stopping", "Failed", "Recovering"} =>
|
||||
/\ d \notin published
|
||||
/\ registered[d] = {}
|
||||
/\ connected[d] = {}
|
||||
|
||||
RegisteredSessionsConnected ==
|
||||
\A d \in Domains : registered[d] \subseteq connected[d]
|
||||
|
||||
|
|
@ -806,14 +1013,52 @@ AttachedSessionsValid ==
|
|||
|
||||
AuthenticatedRequestsOnly ==
|
||||
\A r \in Requests : requestPhase[r] # "Unused" =>
|
||||
/\ CertificateValid[r]
|
||||
/\ SignatureValid[r]
|
||||
/\ RequestCredentialValid[r]
|
||||
/\ RequestSignatureValid[r]
|
||||
/\ RequestIdentityTupleMatches(r)
|
||||
|
||||
RuntimeRoleIdentitySeparation ==
|
||||
/\ \A d \in Domains :
|
||||
Cardinality({
|
||||
DomainCoordinatorIdentity[d],
|
||||
DomainSidecarIdentity[d],
|
||||
DomainSandboxIdentity[d]
|
||||
}) = 3
|
||||
/\ \A s \in Sessions :
|
||||
LET d == Dom(s) IN
|
||||
SessionCliIdentity[s] \notin {
|
||||
DomainCoordinatorIdentity[d],
|
||||
DomainSidecarIdentity[d],
|
||||
DomainSandboxIdentity[d]
|
||||
}
|
||||
|
||||
RegisteredSessionIdentityUniqueness ==
|
||||
\A s1, s2 \in Sessions :
|
||||
/\ s1 # s2
|
||||
/\ s1 \in registered[Dom(s1)]
|
||||
/\ s2 \in registered[Dom(s2)]
|
||||
=> /\ SessionCliIdentity[s1] # SessionCliIdentity[s2]
|
||||
/\ SessionAnchorIdentity[s1] # SessionAnchorIdentity[s2]
|
||||
|
||||
LiveRequestIdentityAuthorized ==
|
||||
\A r \in Requests :
|
||||
requestPhase[r] \notin {"Unused"} \cup TerminalRequestPhases =>
|
||||
/\ RuntimeIdentityTupleReady(ReqDomain(r))
|
||||
/\ SessionIdentityTupleRegistered(ReqSession(r))
|
||||
|
||||
DeveloperApprovalAuthenticated ==
|
||||
\A r \in Requests : approvalSource[r] = "Developer" =>
|
||||
/\ ApprovalCliIdentity[r] = SessionCliIdentity[ReqSession(r)]
|
||||
/\ ApprovalSessionAnchor[r] = SessionAnchorIdentity[ReqSession(r)]
|
||||
/\ ApprovalSignatureValid[r]
|
||||
/\ approvedCommand[r] = ApprovalCommand[r]
|
||||
|
||||
HostExecutionAuthorized ==
|
||||
\A r \in hostRunning :
|
||||
/\ requestPhase[r] = "Executing"
|
||||
/\ approvalSource[r] \in {"AutoRule", "Developer"}
|
||||
/\ approvedCommand[r] \in Commands
|
||||
/\ CommandContentSafe[approvedCommand[r]]
|
||||
|
||||
AutoApprovalNoShell ==
|
||||
\A r \in Requests : approvalSource[r] = "AutoRule" =>
|
||||
|
|
@ -833,7 +1078,22 @@ NoOrphanHostProcess ==
|
|||
|
||||
StateAnchorOwnership ==
|
||||
\A d \in Domains : stateAnchorState[d] = "Mounted" =>
|
||||
coordinatorState[d] \in {"Starting", "Ready", "Stopping"}
|
||||
coordinatorState[d] \in {"Starting", "Ready", "Stopping", "Failed"}
|
||||
|
||||
FailedDomainIsolation ==
|
||||
\A d \in Domains : domainPhase[d] \in {"Failed", "Recovering"} =>
|
||||
/\ d \notin published
|
||||
/\ registered[d] = {}
|
||||
/\ connected[d] = {}
|
||||
/\ ~trustReady[d]
|
||||
/\ hostRunning \cap RequestsForDomain(d) = {}
|
||||
|
||||
OrderedFailureRecovery ==
|
||||
\A d \in Domains : domainPhase[d] = "Recovering" =>
|
||||
/\ (sidecarState[d] = "Stopped" => sandboxState[d] = "Stopped")
|
||||
/\ (stateAnchorState[d] = "Unmounted" =>
|
||||
/\ sandboxState[d] = "Stopped"
|
||||
/\ sidecarState[d] = "Stopped")
|
||||
|
||||
ResultDeliveryStateConsistent ==
|
||||
/\ \A r \in Requests : requestPhase[r] \in PendingResultPhases =>
|
||||
|
|
@ -852,14 +1112,22 @@ Safety ==
|
|||
/\ SandboxNamespaceIsolation
|
||||
/\ OrderedNetworkStartup
|
||||
/\ PublishedDomainsReady
|
||||
/\ ExclusiveBootstrapOwnership
|
||||
/\ TeardownNotJoinable
|
||||
/\ RegisteredSessionsConnected
|
||||
/\ AttachedSessionsValid
|
||||
/\ AuthenticatedRequestsOnly
|
||||
/\ RuntimeRoleIdentitySeparation
|
||||
/\ RegisteredSessionIdentityUniqueness
|
||||
/\ LiveRequestIdentityAuthorized
|
||||
/\ DeveloperApprovalAuthenticated
|
||||
/\ HostExecutionAuthorized
|
||||
/\ AutoApprovalNoShell
|
||||
/\ TerminalIsolation
|
||||
/\ NoOrphanHostProcess
|
||||
/\ StateAnchorOwnership
|
||||
/\ FailedDomainIsolation
|
||||
/\ OrderedFailureRecovery
|
||||
/\ ResultDeliveryStateConsistent
|
||||
|
||||
(***************************************************************************
|
||||
|
|
@ -886,4 +1154,8 @@ EmptyDomainEventuallyStops ==
|
|||
\A d \in Domains :
|
||||
(<>[](Interested(d) = {})) => <>(domainPhase[d] = "Absent")
|
||||
|
||||
FailedDomainEventuallyRecovers ==
|
||||
\A d \in Domains :
|
||||
domainPhase[d] = "Failed" ~> domainPhase[d] = "Absent"
|
||||
|
||||
=============================================================================
|
||||
|
|
|
|||
Loading…
Reference in a new issue