889 lines
33 KiB
Text
889 lines
33 KiB
Text
------------------------------ MODULE Lazaret ------------------------------
|
|
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.
|
|
Cryptographic algorithms, serialization, container commands, filesystems, and
|
|
network packet handling are refinement boundaries validated by implementation
|
|
tests rather than modeled internally.
|
|
***************************************************************************)
|
|
|
|
CONSTANTS
|
|
Domains,
|
|
Sessions,
|
|
Requests,
|
|
Commands,
|
|
NoSession,
|
|
NoRequest,
|
|
NoCommand,
|
|
NoApproval,
|
|
SessionDomain,
|
|
SessionFingerprint,
|
|
DomainFingerprint,
|
|
ConfigSafe,
|
|
SandboxIsolationSafe,
|
|
RequestSession,
|
|
RequestCommand,
|
|
CertificateValid,
|
|
SignatureValid,
|
|
AutoRuleMatches,
|
|
CommandRequiresShell,
|
|
D1,
|
|
S1,
|
|
S2,
|
|
R1,
|
|
R2,
|
|
R3,
|
|
ExactCmd,
|
|
PromptCmd,
|
|
ShellCmd,
|
|
EditedCmd
|
|
|
|
ASSUME
|
|
/\ IsFiniteSet(Domains)
|
|
/\ IsFiniteSet(Sessions)
|
|
/\ IsFiniteSet(Requests)
|
|
/\ IsFiniteSet(Commands)
|
|
/\ Domains # {}
|
|
/\ Sessions # {}
|
|
/\ Requests # {}
|
|
/\ NoSession \notin Sessions
|
|
/\ NoRequest \notin Requests
|
|
/\ NoCommand \notin Commands
|
|
/\ SessionDomain \in [Sessions -> Domains]
|
|
/\ SessionFingerprint \in [Sessions -> STRING]
|
|
/\ DomainFingerprint \in [Domains -> STRING]
|
|
/\ ConfigSafe \in [Domains -> BOOLEAN]
|
|
/\ SandboxIsolationSafe \in [Domains -> BOOLEAN]
|
|
/\ RequestSession \in [Requests -> Sessions]
|
|
/\ RequestCommand \in [Requests -> Commands]
|
|
/\ CertificateValid \in [Requests -> BOOLEAN]
|
|
/\ SignatureValid \in [Requests -> BOOLEAN]
|
|
/\ AutoRuleMatches \in [Requests -> BOOLEAN]
|
|
/\ CommandRequiresShell \in [Commands -> BOOLEAN]
|
|
|
|
DomainPhases == {"Absent", "Starting", "Ready", "Stopping", "Failed"}
|
|
CoordinatorStates == {"Absent", "Starting", "Ready", "Stopping", "Failed"}
|
|
MountStates == {"Unmounted", "Mounted"}
|
|
ResourceStates == {"Stopped", "Ready", "Failed"}
|
|
SessionPhases == {
|
|
"New", "Waiting", "Registering", "Attached", "Prompting",
|
|
"HostExecuting", "Closed", "Failed"
|
|
}
|
|
TerminalRoutes == {"Detached", "Sandbox", "Prompt", "HostProcess"}
|
|
ConnectionStates == {"Disconnected", "Connected"}
|
|
RequestPhases == {
|
|
"Unused", "Verified", "AwaitingApproval", "Approved", "Executing",
|
|
"CompletionPending", "DenialPending", "TimeoutPending",
|
|
"CancellationPending", "FailurePending",
|
|
"Completed", "Denied", "TimedOut", "Cancelled", "Failed"
|
|
}
|
|
ApprovalSources == {NoApproval, "AutoRule", "Developer"}
|
|
PendingResultPhases == {
|
|
"CompletionPending", "DenialPending", "TimeoutPending",
|
|
"CancellationPending", "FailurePending"
|
|
}
|
|
TerminalRequestPhases == {"Completed", "Denied", "TimedOut", "Cancelled", "Failed"}
|
|
|
|
DeliveredResultPhase(p) ==
|
|
CASE p = "CompletionPending" -> "Completed"
|
|
[] p = "DenialPending" -> "Denied"
|
|
[] p = "TimeoutPending" -> "TimedOut"
|
|
[] p = "CancellationPending" -> "Cancelled"
|
|
[] p = "FailurePending" -> "Failed"
|
|
|
|
(***************************************************************************
|
|
Finite fixture operators used by Lazaret.cfg. The protocol itself depends only
|
|
on the abstract constants above; other TLC configurations may override them with
|
|
different finite operators.
|
|
***************************************************************************)
|
|
|
|
DomainsFixture == {D1}
|
|
SessionsFixture == {S1, S2}
|
|
RequestsFixture == {R1, R2, R3}
|
|
CommandsFixture == {ExactCmd, PromptCmd, ShellCmd, EditedCmd}
|
|
|
|
SessionDomainFixture == (S1 :> D1) @@ (S2 :> D1)
|
|
SessionFingerprintFixture ==
|
|
(S1 :> "config-a") @@ (S2 :> "config-a")
|
|
DomainFingerprintFixture == D1 :> "config-a"
|
|
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)
|
|
AutoRuleMatchesFixture ==
|
|
(R1 :> TRUE) @@ (R2 :> FALSE) @@ (R3 :> TRUE)
|
|
CommandRequiresShellFixture ==
|
|
(ExactCmd :> FALSE) @@
|
|
(PromptCmd :> FALSE) @@
|
|
(ShellCmd :> TRUE) @@
|
|
(EditedCmd :> FALSE)
|
|
|
|
VARIABLES
|
|
domainPhase,
|
|
coordinatorState,
|
|
stateAnchorState,
|
|
sidecarState,
|
|
sandboxState,
|
|
trustReady,
|
|
lockOwner,
|
|
published,
|
|
registered,
|
|
connected,
|
|
sessionPhase,
|
|
terminalRoute,
|
|
connectionState,
|
|
activeRequest,
|
|
requestPhase,
|
|
approvalSource,
|
|
approvedCommand,
|
|
hostRunning
|
|
|
|
vars == <<
|
|
domainPhase,
|
|
coordinatorState,
|
|
stateAnchorState,
|
|
sidecarState,
|
|
sandboxState,
|
|
trustReady,
|
|
lockOwner,
|
|
published,
|
|
registered,
|
|
connected,
|
|
sessionPhase,
|
|
terminalRoute,
|
|
connectionState,
|
|
activeRequest,
|
|
requestPhase,
|
|
approvalSource,
|
|
approvedCommand,
|
|
hostRunning
|
|
>>
|
|
|
|
Dom(s) == SessionDomain[s]
|
|
ReqSession(r) == RequestSession[r]
|
|
ReqDomain(r) == Dom(ReqSession(r))
|
|
IsTerminalRequest(r) == requestPhase[r] \in TerminalRequestPhases
|
|
|
|
Interested(d) == {
|
|
s \in Sessions :
|
|
Dom(s) = d /\
|
|
sessionPhase[s] \in {
|
|
"Waiting", "Registering", "Attached", "Prompting", "HostExecuting"
|
|
}
|
|
}
|
|
|
|
RequestsForDomain(d) == {r \in Requests : ReqDomain(r) = d}
|
|
|
|
Init ==
|
|
/\ domainPhase = [d \in Domains |-> "Absent"]
|
|
/\ coordinatorState = [d \in Domains |-> "Absent"]
|
|
/\ stateAnchorState = [d \in Domains |-> "Unmounted"]
|
|
/\ sidecarState = [d \in Domains |-> "Stopped"]
|
|
/\ sandboxState = [d \in Domains |-> "Stopped"]
|
|
/\ trustReady = [d \in Domains |-> FALSE]
|
|
/\ lockOwner = [d \in Domains |-> NoSession]
|
|
/\ published = {}
|
|
/\ registered = [d \in Domains |-> {}]
|
|
/\ connected = [d \in Domains |-> {}]
|
|
/\ sessionPhase = [s \in Sessions |-> "New"]
|
|
/\ terminalRoute = [s \in Sessions |-> "Detached"]
|
|
/\ connectionState = [s \in Sessions |-> "Disconnected"]
|
|
/\ activeRequest = [s \in Sessions |-> NoRequest]
|
|
/\ requestPhase = [r \in Requests |-> "Unused"]
|
|
/\ approvalSource = [r \in Requests |-> NoApproval]
|
|
/\ approvedCommand = [r \in Requests |-> NoCommand]
|
|
/\ hostRunning = {}
|
|
|
|
(***************************************************************************
|
|
Domain and Session lifecycle
|
|
***************************************************************************)
|
|
|
|
StartNewDomain(s) ==
|
|
LET d == Dom(s) IN
|
|
/\ sessionPhase[s] = "New"
|
|
/\ ConfigSafe[d]
|
|
/\ domainPhase[d] = "Absent"
|
|
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Starting"]
|
|
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Starting"]
|
|
/\ lockOwner' = [lockOwner EXCEPT ![d] = s]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Waiting"]
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, sandboxState, trustReady, published,
|
|
registered, connected, terminalRoute, connectionState, activeRequest,
|
|
requestPhase, approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
StartReadySession(s) ==
|
|
LET d == Dom(s) IN
|
|
/\ sessionPhase[s] = "New"
|
|
/\ domainPhase[d] = "Ready"
|
|
/\ SessionFingerprint[s] = DomainFingerprint[d]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Registering"]
|
|
/\ connectionState' = [connectionState EXCEPT ![s] = "Connected"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
terminalRoute, activeRequest, requestPhase, approvalSource,
|
|
approvedCommand, hostRunning
|
|
>>
|
|
|
|
WaitForDomain(s) ==
|
|
LET d == Dom(s) IN
|
|
/\ sessionPhase[s] = "New"
|
|
/\ domainPhase[d] \in {"Starting", "Stopping"}
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Waiting"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
RestartWaitingDomain(s) ==
|
|
LET d == Dom(s) IN
|
|
/\ sessionPhase[s] = "Waiting"
|
|
/\ ConfigSafe[d]
|
|
/\ domainPhase[d] = "Absent"
|
|
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Starting"]
|
|
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Starting"]
|
|
/\ lockOwner' = [lockOwner EXCEPT ![d] = s]
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, sandboxState, trustReady, published,
|
|
registered, connected, sessionPhase, terminalRoute, connectionState,
|
|
activeRequest, requestPhase, approvalSource, approvedCommand,
|
|
hostRunning
|
|
>>
|
|
|
|
MountStateAnchor(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ coordinatorState[d] = "Starting"
|
|
/\ stateAnchorState[d] = "Unmounted"
|
|
/\ stateAnchorState' = [stateAnchorState EXCEPT ![d] = "Mounted"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, sidecarState, sandboxState, trustReady,
|
|
lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
CreateTrustAnchor(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ coordinatorState[d] = "Starting"
|
|
/\ ~trustReady[d]
|
|
/\ trustReady' = [trustReady EXCEPT ![d] = TRUE]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, lockOwner, published, registered, connected,
|
|
sessionPhase, terminalRoute, connectionState, activeRequest,
|
|
requestPhase, approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
StartSidecar(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ stateAnchorState[d] = "Mounted"
|
|
/\ trustReady[d]
|
|
/\ sidecarState[d] = "Stopped"
|
|
/\ sidecarState' = [sidecarState EXCEPT ![d] = "Ready"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sandboxState,
|
|
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
StartSandbox(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ SandboxIsolationSafe[d]
|
|
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Ready"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
PublishDomain(d) ==
|
|
/\ domainPhase[d] = "Starting"
|
|
/\ coordinatorState[d] = "Starting"
|
|
/\ stateAnchorState[d] = "Mounted"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ sandboxState[d] = "Ready"
|
|
/\ trustReady[d]
|
|
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Ready"]
|
|
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Ready"]
|
|
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
|
/\ published' = published \cup {d}
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, sandboxState, trustReady, registered,
|
|
connected, sessionPhase, terminalRoute, connectionState,
|
|
activeRequest, requestPhase, approvalSource, approvedCommand,
|
|
hostRunning
|
|
>>
|
|
|
|
AdvanceWaitingSession(s) ==
|
|
LET d == Dom(s) IN
|
|
/\ sessionPhase[s] = "Waiting"
|
|
/\ domainPhase[d] = "Ready"
|
|
/\ SessionFingerprint[s] = DomainFingerprint[d]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Registering"]
|
|
/\ connectionState' = [connectionState EXCEPT ![s] = "Connected"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
terminalRoute, activeRequest, requestPhase, approvalSource,
|
|
approvedCommand, hostRunning
|
|
>>
|
|
|
|
RejectConfigurationMismatch(s) ==
|
|
LET d == Dom(s) IN
|
|
/\ sessionPhase[s] \in {"New", "Waiting"}
|
|
/\ domainPhase[d] = "Ready"
|
|
/\ SessionFingerprint[s] # DomainFingerprint[d]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Failed"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Detached"]
|
|
/\ connectionState' = [connectionState EXCEPT ![s] = "Disconnected"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
activeRequest, requestPhase, approvalSource, approvedCommand,
|
|
hostRunning
|
|
>>
|
|
|
|
RegisterSession(s) ==
|
|
LET d == Dom(s) IN
|
|
/\ sessionPhase[s] = "Registering"
|
|
/\ connectionState[s] = "Connected"
|
|
/\ domainPhase[d] = "Ready"
|
|
/\ SessionFingerprint[s] = DomainFingerprint[d]
|
|
/\ registered' = [registered EXCEPT ![d] = @ \cup {s}]
|
|
/\ connected' = [connected EXCEPT ![d] = @ \cup {s}]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, connectionState,
|
|
activeRequest, requestPhase, approvalSource, approvedCommand,
|
|
hostRunning
|
|
>>
|
|
|
|
DisconnectSession(s) ==
|
|
LET d == Dom(s)
|
|
r == activeRequest[s]
|
|
IN
|
|
/\ sessionPhase[s] \in {
|
|
"Waiting", "Registering", "Attached", "Prompting", "HostExecuting"
|
|
}
|
|
/\ registered' = [registered EXCEPT ![d] = @ \ {s}]
|
|
/\ connected' = [connected EXCEPT ![d] = @ \ {s}]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Closed"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Detached"]
|
|
/\ connectionState' = [connectionState EXCEPT ![s] = "Disconnected"]
|
|
/\ activeRequest' = [activeRequest EXCEPT ![s] = NoRequest]
|
|
/\ requestPhase' = [q \in Requests |->
|
|
IF r # NoRequest /\ q = r /\ ~IsTerminalRequest(q)
|
|
THEN "Cancelled"
|
|
ELSE requestPhase[q]]
|
|
/\ hostRunning' = IF r = NoRequest THEN hostRunning ELSE hostRunning \ {r}
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, approvalSource,
|
|
approvedCommand
|
|
>>
|
|
|
|
BeginTeardown(d) ==
|
|
/\ domainPhase[d] = "Ready"
|
|
/\ Interested(d) = {}
|
|
/\ registered[d] = {}
|
|
/\ connected[d] = {}
|
|
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Stopping"]
|
|
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Stopping"]
|
|
/\ published' = published \ {d}
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
|
|
registered, connected, sessionPhase, terminalRoute, connectionState,
|
|
activeRequest, requestPhase, approvalSource, approvedCommand,
|
|
hostRunning
|
|
>>
|
|
|
|
StopSandbox(d) ==
|
|
/\ domainPhase[d] = "Stopping"
|
|
/\ sandboxState[d] = "Ready"
|
|
/\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
StopSidecar(d) ==
|
|
/\ domainPhase[d] = "Stopping"
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ sidecarState' = [sidecarState EXCEPT ![d] = "Stopped"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sandboxState,
|
|
trustReady, lockOwner, published, registered, connected, sessionPhase,
|
|
terminalRoute, connectionState, activeRequest, requestPhase,
|
|
approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
UnmountStateAnchor(d) ==
|
|
/\ domainPhase[d] = "Stopping"
|
|
/\ 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
|
|
>>
|
|
|
|
FinishTeardown(d) ==
|
|
/\ domainPhase[d] = "Stopping"
|
|
/\ stateAnchorState[d] = "Unmounted"
|
|
/\ sidecarState[d] = "Stopped"
|
|
/\ sandboxState[d] = "Stopped"
|
|
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Absent"]
|
|
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
|
|
/\ trustReady' = [trustReady EXCEPT ![d] = FALSE]
|
|
/\ lockOwner' = [lockOwner EXCEPT ![d] = NoSession]
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, sandboxState, published, registered,
|
|
connected, sessionPhase, terminalRoute, connectionState,
|
|
activeRequest, requestPhase, approvalSource, approvedCommand,
|
|
hostRunning
|
|
>>
|
|
|
|
(***************************************************************************
|
|
Host escalation protocol
|
|
***************************************************************************)
|
|
|
|
ReceiveEscalation(r) ==
|
|
LET s == ReqSession(r)
|
|
d == ReqDomain(r)
|
|
IN
|
|
/\ requestPhase[r] = "Unused"
|
|
/\ sessionPhase[s] = "Attached"
|
|
/\ activeRequest[s] = NoRequest
|
|
/\ s \in registered[d]
|
|
/\ s \in connected[d]
|
|
/\ CertificateValid[r]
|
|
/\ SignatureValid[r]
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "Verified"]
|
|
/\ activeRequest' = [activeRequest EXCEPT ![s] = r]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
sessionPhase, terminalRoute, connectionState, approvalSource,
|
|
approvedCommand, hostRunning
|
|
>>
|
|
|
|
AutoApprove(r) ==
|
|
/\ requestPhase[r] = "Verified"
|
|
/\ AutoRuleMatches[r]
|
|
/\ ~CommandRequiresShell[RequestCommand[r]]
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "Approved"]
|
|
/\ approvalSource' = [approvalSource EXCEPT ![r] = "AutoRule"]
|
|
/\ approvedCommand' = [approvedCommand EXCEPT ![r] = RequestCommand[r]]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
sessionPhase, terminalRoute, connectionState, activeRequest, hostRunning
|
|
>>
|
|
|
|
QueuePrompt(r) ==
|
|
/\ requestPhase[r] = "Verified"
|
|
/\ ~(AutoRuleMatches[r] /\ ~CommandRequiresShell[RequestCommand[r]])
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "AwaitingApproval"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
sessionPhase, terminalRoute, connectionState, activeRequest,
|
|
approvalSource, approvedCommand, hostRunning
|
|
>>
|
|
|
|
BeginPrompt(r) ==
|
|
LET s == ReqSession(r) IN
|
|
/\ requestPhase[r] = "AwaitingApproval"
|
|
/\ sessionPhase[s] = "Attached"
|
|
/\ activeRequest[s] = r
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Prompting"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Prompt"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
connectionState, activeRequest, requestPhase, approvalSource,
|
|
approvedCommand, hostRunning
|
|
>>
|
|
|
|
DeveloperApprove(r, cmd) ==
|
|
LET s == ReqSession(r) IN
|
|
/\ requestPhase[r] = "AwaitingApproval"
|
|
/\ sessionPhase[s] = "Prompting"
|
|
/\ cmd \in Commands
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "Approved"]
|
|
/\ approvalSource' = [approvalSource EXCEPT ![r] = "Developer"]
|
|
/\ approvedCommand' = [approvedCommand EXCEPT ![r] = cmd]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
sessionPhase, terminalRoute, connectionState, activeRequest, hostRunning
|
|
>>
|
|
|
|
DeveloperDeny(r) ==
|
|
LET s == ReqSession(r) IN
|
|
/\ requestPhase[r] = "AwaitingApproval"
|
|
/\ sessionPhase[s] = "Prompting"
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "DenialPending"]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
connectionState, activeRequest, approvalSource, approvedCommand,
|
|
hostRunning
|
|
>>
|
|
|
|
StartHostExecution(r) ==
|
|
LET s == ReqSession(r)
|
|
d == ReqDomain(r)
|
|
IN
|
|
/\ requestPhase[r] = "Approved"
|
|
/\ activeRequest[s] = r
|
|
/\ s \in connected[d]
|
|
/\ sessionPhase[s] \in {"Attached", "Prompting"}
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "Executing"]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "HostExecuting"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "HostProcess"]
|
|
/\ hostRunning' = hostRunning \cup {r}
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
connectionState, activeRequest, approvalSource, approvedCommand
|
|
>>
|
|
|
|
CompleteHostExecution(r) ==
|
|
LET s == ReqSession(r) IN
|
|
/\ requestPhase[r] = "Executing"
|
|
/\ r \in hostRunning
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "CompletionPending"]
|
|
/\ hostRunning' = hostRunning \ {r}
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
connectionState, activeRequest, approvalSource, approvedCommand
|
|
>>
|
|
|
|
TimeoutRequest(r) ==
|
|
LET s == ReqSession(r) IN
|
|
/\ requestPhase[r] \in {"Verified", "AwaitingApproval", "Approved", "Executing"}
|
|
/\ activeRequest[s] = r
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "TimeoutPending"]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
|
|
/\ hostRunning' = hostRunning \ {r}
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
connectionState, activeRequest, approvalSource, approvedCommand
|
|
>>
|
|
|
|
CancelRequest(r) ==
|
|
LET s == ReqSession(r) IN
|
|
/\ requestPhase[r] \in {
|
|
"Verified", "AwaitingApproval", "Approved", "Executing"
|
|
}
|
|
/\ activeRequest[s] = r
|
|
/\ connectionState[s] = "Connected"
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "CancellationPending"]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
|
|
/\ hostRunning' = hostRunning \ {r}
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
connectionState, activeRequest, approvalSource, approvedCommand
|
|
>>
|
|
|
|
FailHostExecution(r) ==
|
|
LET s == ReqSession(r) IN
|
|
/\ requestPhase[r] = "Executing"
|
|
/\ activeRequest[s] = r
|
|
/\ connectionState[s] = "Connected"
|
|
/\ requestPhase' = [requestPhase EXCEPT ![r] = "FailurePending"]
|
|
/\ sessionPhase' = [sessionPhase EXCEPT ![s] = "Attached"]
|
|
/\ terminalRoute' = [terminalRoute EXCEPT ![s] = "Sandbox"]
|
|
/\ hostRunning' = hostRunning \ {r}
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
connectionState, activeRequest, approvalSource, approvedCommand
|
|
>>
|
|
|
|
DeliverResult(r) ==
|
|
LET s == ReqSession(r) IN
|
|
/\ requestPhase[r] \in PendingResultPhases
|
|
/\ activeRequest[s] = r
|
|
/\ connectionState[s] = "Connected"
|
|
/\ sessionPhase[s] = "Attached"
|
|
/\ requestPhase' = [requestPhase EXCEPT
|
|
![r] = DeliveredResultPhase(@)]
|
|
/\ activeRequest' = [activeRequest EXCEPT ![s] = NoRequest]
|
|
/\ UNCHANGED <<
|
|
domainPhase, coordinatorState, stateAnchorState, sidecarState,
|
|
sandboxState, trustReady, lockOwner, published, registered, connected,
|
|
sessionPhase, terminalRoute, connectionState, approvalSource,
|
|
approvedCommand, hostRunning
|
|
>>
|
|
|
|
(***************************************************************************
|
|
Failure and recovery
|
|
***************************************************************************)
|
|
|
|
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}
|
|
/\ registered' = [registered EXCEPT ![d] = {}]
|
|
/\ connected' = [connected EXCEPT ![d] = {}]
|
|
/\ sessionPhase' = [s \in Sessions |->
|
|
IF Dom(s) = d /\ sessionPhase[s] \notin {"New", "Closed"}
|
|
THEN "Failed"
|
|
ELSE sessionPhase[s]]
|
|
/\ terminalRoute' = [s \in Sessions |->
|
|
IF Dom(s) = d THEN "Detached" ELSE terminalRoute[s]]
|
|
/\ connectionState' = [s \in Sessions |->
|
|
IF Dom(s) = d THEN "Disconnected" ELSE connectionState[s]]
|
|
/\ activeRequest' = [s \in Sessions |->
|
|
IF Dom(s) = d THEN NoRequest ELSE activeRequest[s]]
|
|
/\ requestPhase' = [r \in Requests |->
|
|
IF ReqDomain(r) = d /\ requestPhase[r] # "Unused" /\ ~IsTerminalRequest(r)
|
|
THEN "Failed"
|
|
ELSE requestPhase[r]]
|
|
/\ hostRunning' = hostRunning \ RequestsForDomain(d)
|
|
/\ UNCHANGED <<approvalSource, approvedCommand>>
|
|
|
|
ResetFailedDomain(d) ==
|
|
/\ domainPhase[d] = "Failed"
|
|
/\ domainPhase' = [domainPhase EXCEPT ![d] = "Absent"]
|
|
/\ coordinatorState' = [coordinatorState EXCEPT ![d] = "Absent"]
|
|
/\ UNCHANGED <<
|
|
stateAnchorState, sidecarState, sandboxState, trustReady, lockOwner,
|
|
published, registered, connected, sessionPhase, terminalRoute,
|
|
connectionState, activeRequest, requestPhase, approvalSource,
|
|
approvedCommand, hostRunning
|
|
>>
|
|
|
|
DomainProgress(d) ==
|
|
\/ MountStateAnchor(d)
|
|
\/ CreateTrustAnchor(d)
|
|
\/ StartSidecar(d)
|
|
\/ StartSandbox(d)
|
|
\/ PublishDomain(d)
|
|
\/ BeginTeardown(d)
|
|
\/ StopSandbox(d)
|
|
\/ StopSidecar(d)
|
|
\/ UnmountStateAnchor(d)
|
|
\/ FinishTeardown(d)
|
|
\/ ResetFailedDomain(d)
|
|
|
|
SessionProgress(s) ==
|
|
\/ StartNewDomain(s)
|
|
\/ StartReadySession(s)
|
|
\/ WaitForDomain(s)
|
|
\/ RestartWaitingDomain(s)
|
|
\/ AdvanceWaitingSession(s)
|
|
\/ RejectConfigurationMismatch(s)
|
|
\/ RegisterSession(s)
|
|
|
|
RequestProgress(r) ==
|
|
\/ AutoApprove(r)
|
|
\/ QueuePrompt(r)
|
|
\/ BeginPrompt(r)
|
|
\/ (\E cmd \in Commands : DeveloperApprove(r, cmd))
|
|
\/ DeveloperDeny(r)
|
|
\/ StartHostExecution(r)
|
|
\/ CompleteHostExecution(r)
|
|
\/ TimeoutRequest(r)
|
|
\/ CancelRequest(r)
|
|
\/ FailHostExecution(r)
|
|
\/ DeliverResult(r)
|
|
|
|
Next ==
|
|
\/ (\E s \in Sessions :
|
|
StartNewDomain(s) \/ StartReadySession(s) \/ WaitForDomain(s) \/
|
|
RestartWaitingDomain(s) \/ AdvanceWaitingSession(s) \/
|
|
RejectConfigurationMismatch(s) \/
|
|
RegisterSession(s) \/ DisconnectSession(s))
|
|
\/ (\E d \in Domains :
|
|
DomainProgress(d) \/ FailDomain(d))
|
|
\/ (\E r \in Requests :
|
|
ReceiveEscalation(r) \/ RequestProgress(r))
|
|
|
|
Spec ==
|
|
/\ Init
|
|
/\ [][Next]_vars
|
|
/\ \A d \in Domains : WF_vars(DomainProgress(d))
|
|
/\ \A s \in Sessions : WF_vars(SessionProgress(s))
|
|
/\ \A r \in Requests : WF_vars(RequestProgress(r))
|
|
|
|
(***************************************************************************
|
|
Safety properties
|
|
***************************************************************************)
|
|
|
|
TypeOK ==
|
|
/\ domainPhase \in [Domains -> DomainPhases]
|
|
/\ coordinatorState \in [Domains -> CoordinatorStates]
|
|
/\ stateAnchorState \in [Domains -> MountStates]
|
|
/\ sidecarState \in [Domains -> ResourceStates]
|
|
/\ sandboxState \in [Domains -> ResourceStates]
|
|
/\ trustReady \in [Domains -> BOOLEAN]
|
|
/\ lockOwner \in [Domains -> Sessions \cup {NoSession}]
|
|
/\ published \subseteq Domains
|
|
/\ registered \in [Domains -> SUBSET Sessions]
|
|
/\ connected \in [Domains -> SUBSET Sessions]
|
|
/\ sessionPhase \in [Sessions -> SessionPhases]
|
|
/\ terminalRoute \in [Sessions -> TerminalRoutes]
|
|
/\ connectionState \in [Sessions -> ConnectionStates]
|
|
/\ activeRequest \in [Sessions -> Requests \cup {NoRequest}]
|
|
/\ requestPhase \in [Requests -> RequestPhases]
|
|
/\ approvalSource \in [Requests -> ApprovalSources]
|
|
/\ approvedCommand \in [Requests -> Commands \cup {NoCommand}]
|
|
/\ hostRunning \subseteq Requests
|
|
|
|
ConfigurationConfinement ==
|
|
\A d \in Domains : domainPhase[d] # "Absent" => ConfigSafe[d]
|
|
|
|
SandboxNamespaceIsolation ==
|
|
\A d \in Domains : sandboxState[d] = "Ready" => SandboxIsolationSafe[d]
|
|
|
|
OrderedNetworkStartup ==
|
|
\A d \in Domains : sandboxState[d] = "Ready" => sidecarState[d] = "Ready"
|
|
|
|
PublishedDomainsReady ==
|
|
\A d \in published :
|
|
/\ domainPhase[d] = "Ready"
|
|
/\ coordinatorState[d] = "Ready"
|
|
/\ stateAnchorState[d] = "Mounted"
|
|
/\ sidecarState[d] = "Ready"
|
|
/\ sandboxState[d] = "Ready"
|
|
/\ trustReady[d]
|
|
|
|
RegisteredSessionsConnected ==
|
|
\A d \in Domains : registered[d] \subseteq connected[d]
|
|
|
|
AttachedSessionsValid ==
|
|
\A s \in Sessions :
|
|
sessionPhase[s] \in {"Attached", "Prompting", "HostExecuting"} =>
|
|
/\ s \in registered[Dom(s)]
|
|
/\ s \in connected[Dom(s)]
|
|
/\ domainPhase[Dom(s)] = "Ready"
|
|
/\ SessionFingerprint[s] = DomainFingerprint[Dom(s)]
|
|
|
|
AuthenticatedRequestsOnly ==
|
|
\A r \in Requests : requestPhase[r] # "Unused" =>
|
|
/\ CertificateValid[r]
|
|
/\ SignatureValid[r]
|
|
|
|
HostExecutionAuthorized ==
|
|
\A r \in hostRunning :
|
|
/\ requestPhase[r] = "Executing"
|
|
/\ approvalSource[r] \in {"AutoRule", "Developer"}
|
|
/\ approvedCommand[r] \in Commands
|
|
|
|
AutoApprovalNoShell ==
|
|
\A r \in Requests : approvalSource[r] = "AutoRule" =>
|
|
/\ approvedCommand[r] = RequestCommand[r]
|
|
/\ ~CommandRequiresShell[approvedCommand[r]]
|
|
|
|
TerminalIsolation ==
|
|
\A s \in Sessions : sessionPhase[s] = "Prompting" =>
|
|
terminalRoute[s] = "Prompt"
|
|
|
|
NoOrphanHostProcess ==
|
|
\A r \in hostRunning :
|
|
LET s == ReqSession(r) IN
|
|
/\ activeRequest[s] = r
|
|
/\ sessionPhase[s] = "HostExecuting"
|
|
/\ connectionState[s] = "Connected"
|
|
|
|
StateAnchorOwnership ==
|
|
\A d \in Domains : stateAnchorState[d] = "Mounted" =>
|
|
coordinatorState[d] \in {"Starting", "Ready", "Stopping"}
|
|
|
|
ResultDeliveryStateConsistent ==
|
|
/\ \A r \in Requests : requestPhase[r] \in PendingResultPhases =>
|
|
LET s == ReqSession(r) IN
|
|
/\ activeRequest[s] = r
|
|
/\ connectionState[s] = "Connected"
|
|
/\ sessionPhase[s] = "Attached"
|
|
/\ r \notin hostRunning
|
|
/\ \A r \in Requests : requestPhase[r] \in TerminalRequestPhases =>
|
|
/\ activeRequest[ReqSession(r)] # r
|
|
/\ r \notin hostRunning
|
|
|
|
Safety ==
|
|
/\ TypeOK
|
|
/\ ConfigurationConfinement
|
|
/\ SandboxNamespaceIsolation
|
|
/\ OrderedNetworkStartup
|
|
/\ PublishedDomainsReady
|
|
/\ RegisteredSessionsConnected
|
|
/\ AttachedSessionsValid
|
|
/\ AuthenticatedRequestsOnly
|
|
/\ HostExecutionAuthorized
|
|
/\ AutoApprovalNoShell
|
|
/\ TerminalIsolation
|
|
/\ NoOrphanHostProcess
|
|
/\ StateAnchorOwnership
|
|
/\ ResultDeliveryStateConsistent
|
|
|
|
(***************************************************************************
|
|
Liveness properties. TLC configurations may check these separately from the
|
|
safety sweep when the state space grows.
|
|
***************************************************************************)
|
|
|
|
SessionEventuallyResolves ==
|
|
\A s \in Sessions :
|
|
sessionPhase[s] = "New" ~>
|
|
sessionPhase[s] \in {"Attached", "Closed", "Failed"}
|
|
|
|
RequestEventuallyResolves ==
|
|
\A r \in Requests :
|
|
requestPhase[r] = "Verified" ~>
|
|
requestPhase[r] \in TerminalRequestPhases
|
|
|
|
PromptEventuallyRestoresTerminal ==
|
|
\A s \in Sessions :
|
|
sessionPhase[s] \in {"Prompting", "HostExecuting"} ~>
|
|
terminalRoute[s] \in {"Sandbox", "Detached"}
|
|
|
|
EmptyDomainEventuallyStops ==
|
|
\A d \in Domains :
|
|
(<>[](Interested(d) = {})) => <>(domainPhase[d] = "Absent")
|
|
|
|
=============================================================================
|