Model terminal interaction authority and bounded verification
This commit is contained in:
parent
690738d846
commit
6d3a2cfe16
1 changed files with 785 additions and 14 deletions
|
|
@ -26,8 +26,11 @@ multi-process presence predicates and generation-scoped genCoordinatorId.
|
|||
Durable participant intent is multi-role; networkReady gates publication;
|
||||
preparedLowerLeased and helperProc refine physical ownership under RS.
|
||||
Cryptographic algorithms, serialization, container commands, filesystems, typed
|
||||
redb tables, PTY descriptor identities, process identifiers, signal mechanics,
|
||||
and network packet handling remain refinement boundaries.
|
||||
redb tables, PTY descriptor identities, process identifiers, terminal byte and
|
||||
signal mechanics, and network packet handling remain refinement boundaries.
|
||||
The model does distinguish keyboard PTY delivery, explicit guest-group signals,
|
||||
local Client controls, and terminal metadata because those carry different
|
||||
authorities.
|
||||
***************************************************************************)
|
||||
|
||||
CONSTANTS
|
||||
|
|
@ -69,6 +72,10 @@ CONSTANTS
|
|||
AutoRuleMatches,
|
||||
CommandRequiresShell,
|
||||
CommandContentSafe,
|
||||
TerminalEventPlan,
|
||||
TerminalAuthorityPlan,
|
||||
TerminalAdministrativeAuthorityValid,
|
||||
TerminalRoutingFault,
|
||||
D1,
|
||||
S1,
|
||||
S2,
|
||||
|
|
@ -138,6 +145,24 @@ SessionPhases == {
|
|||
}
|
||||
TerminalRoutes == {"Detached", "Sandbox", "Prompt", "HostProcess"}
|
||||
SessionTerminalStates == {"Clean", "Intent", "Running", "ReleaseIntent"}
|
||||
TerminalEventKinds == {
|
||||
"Keyboard", "ExplicitSignal", "Resize", "Break", "LocalSuspend",
|
||||
"LocalResume", "LocalDisconnect", "HostSignal"
|
||||
}
|
||||
TerminalAuthorities == {
|
||||
"None", "Client", "Administrator", "LocalClient", "HostProcess"
|
||||
}
|
||||
TerminalDispositions == {"None", "Delivered", "Refused"}
|
||||
TerminalTargets == {
|
||||
"None", "GuestPtyForeground", "RecordedGuestGroup", "LocalClient",
|
||||
"ExactSessionPty"
|
||||
}
|
||||
TerminalRoutingFaults == {
|
||||
"Correct", "KeyboardRecordedGroup", "KeyboardDuplicated",
|
||||
"CrossSession", "ClientAdministrativeSignal",
|
||||
"BlockedTransportPreventsLocalControl"
|
||||
}
|
||||
TerminalTransportStates == {"Ready", "Blocked"}
|
||||
ConnectionStates == {"Disconnected", "Connected"}
|
||||
RequestPhases == {
|
||||
"Unused", "Verified", "AwaitingApproval", "Approved", "Executing",
|
||||
|
|
@ -185,6 +210,48 @@ EmptyDurableIntent == [role \in DurableRoles |-> FALSE]
|
|||
SessionAnchorsFixture == {"anchor-1", "anchor-2"}
|
||||
|
||||
SessionDomainFixture == (S1 :> D1) @@ (S2 :> D1)
|
||||
TerminalEventPlanFixture ==
|
||||
(S1 :> <<
|
||||
"Keyboard", "Resize", "LocalSuspend", "LocalResume",
|
||||
"LocalDisconnect"
|
||||
>>) @@
|
||||
(S2 :> <<
|
||||
"ExplicitSignal", "ExplicitSignal", "Break", "Keyboard", "HostSignal"
|
||||
>>)
|
||||
TerminalAuthorityPlanFixture ==
|
||||
(S1 :> <<
|
||||
"Client", "Client", "LocalClient", "LocalClient", "LocalClient"
|
||||
>>) @@
|
||||
(S2 :> <<
|
||||
"Client", "Administrator", "LocalClient", "Client", "HostProcess"
|
||||
>>)
|
||||
TerminalAdministrativeAuthorityValidFixture ==
|
||||
(S1 :> <<FALSE, FALSE, FALSE, FALSE, FALSE>>) @@
|
||||
(S2 :> <<FALSE, TRUE, FALSE, FALSE, FALSE>>)
|
||||
TerminalNoEventPlanFixture ==
|
||||
(S1 :> <<>>) @@ (S2 :> <<>>)
|
||||
TerminalNoAuthorityPlanFixture ==
|
||||
(S1 :> <<>>) @@ (S2 :> <<>>)
|
||||
TerminalNoAdministrativeAuthorityValidFixture ==
|
||||
(S1 :> <<>>) @@ (S2 :> <<>>)
|
||||
TerminalRoutingEventPlanFixture ==
|
||||
(S1 :> <<"Keyboard", "Resize">>) @@
|
||||
(S2 :> <<"ExplicitSignal", "ExplicitSignal">>)
|
||||
TerminalRoutingAuthorityPlanFixture ==
|
||||
(S1 :> <<"Client", "Client">>) @@
|
||||
(S2 :> <<"Client", "Administrator">>)
|
||||
TerminalRoutingAdministrativeAuthorityValidFixture ==
|
||||
(S1 :> <<FALSE, FALSE>>) @@
|
||||
(S2 :> <<FALSE, TRUE>>)
|
||||
TerminalLocalControlEventPlanFixture ==
|
||||
(S1 :> <<"LocalSuspend", "LocalResume", "LocalDisconnect">>) @@
|
||||
(S2 :> <<"Break", "HostSignal">>)
|
||||
TerminalLocalControlAuthorityPlanFixture ==
|
||||
(S1 :> <<"LocalClient", "LocalClient", "LocalClient">>) @@
|
||||
(S2 :> <<"LocalClient", "HostProcess">>)
|
||||
TerminalLocalControlAdministrativeAuthorityValidFixture ==
|
||||
(S1 :> <<FALSE, FALSE, FALSE>>) @@
|
||||
(S2 :> <<FALSE, FALSE>>)
|
||||
SessionFingerprintFixture ==
|
||||
(S1 :> "config-a") @@ (S2 :> "config-a")
|
||||
DomainFingerprintFixture == D1 :> "config-a"
|
||||
|
|
@ -279,7 +346,22 @@ VARIABLES
|
|||
sessionTerminalState,
|
||||
sessionPtyOpen,
|
||||
sessionExecPresent,
|
||||
sessionGuestKnown
|
||||
sessionGuestKnown,
|
||||
terminalEventIndex,
|
||||
terminalLastEventId,
|
||||
terminalLastEvent,
|
||||
terminalLastSourceSession,
|
||||
terminalLastAuthority,
|
||||
terminalLastAdministrativeAuthorityValid,
|
||||
terminalLastDisposition,
|
||||
terminalLastDestination,
|
||||
terminalLastTarget,
|
||||
terminalLastByteDeliveries,
|
||||
terminalLastSignalDeliveries,
|
||||
terminalLastLocalDeliveries,
|
||||
terminalLastMetadataDeliveries,
|
||||
sessionClientSuspended,
|
||||
sessionTerminalTransportState
|
||||
|
||||
baseVars == <<
|
||||
domainPhase,
|
||||
|
|
@ -318,13 +400,35 @@ baseVars == <<
|
|||
helperProc
|
||||
>>
|
||||
|
||||
terminalVars == <<
|
||||
terminalLifecycleVars == <<
|
||||
sessionTerminalState,
|
||||
sessionPtyOpen,
|
||||
sessionExecPresent,
|
||||
sessionGuestKnown
|
||||
>>
|
||||
|
||||
terminalEventRecordVars == <<
|
||||
terminalEventIndex,
|
||||
terminalLastEventId,
|
||||
terminalLastEvent,
|
||||
terminalLastSourceSession,
|
||||
terminalLastAuthority,
|
||||
terminalLastAdministrativeAuthorityValid,
|
||||
terminalLastDisposition,
|
||||
terminalLastDestination,
|
||||
terminalLastTarget,
|
||||
terminalLastByteDeliveries,
|
||||
terminalLastSignalDeliveries,
|
||||
terminalLastLocalDeliveries,
|
||||
terminalLastMetadataDeliveries
|
||||
>>
|
||||
|
||||
terminalInteractionVars == <<
|
||||
terminalEventRecordVars, sessionClientSuspended, sessionTerminalTransportState
|
||||
>>
|
||||
|
||||
terminalVars == <<terminalLifecycleVars, terminalInteractionVars>>
|
||||
|
||||
vars == <<baseVars, terminalVars>>
|
||||
|
||||
Dom(s) == SessionDomain[s]
|
||||
|
|
@ -520,6 +624,22 @@ Init ==
|
|||
/\ sessionPtyOpen = [s \in Sessions |-> FALSE]
|
||||
/\ sessionExecPresent = [s \in Sessions |-> FALSE]
|
||||
/\ sessionGuestKnown = [s \in Sessions |-> FALSE]
|
||||
/\ terminalEventIndex = [s \in Sessions |-> 1]
|
||||
/\ terminalLastEventId = [s \in Sessions |-> 0]
|
||||
/\ terminalLastEvent = [s \in Sessions |-> "None"]
|
||||
/\ terminalLastSourceSession = [s \in Sessions |-> NoSession]
|
||||
/\ terminalLastAuthority = [s \in Sessions |-> "None"]
|
||||
/\ terminalLastAdministrativeAuthorityValid =
|
||||
[s \in Sessions |-> FALSE]
|
||||
/\ terminalLastDisposition = [s \in Sessions |-> "None"]
|
||||
/\ terminalLastDestination = [s \in Sessions |-> NoSession]
|
||||
/\ terminalLastTarget = [s \in Sessions |-> "None"]
|
||||
/\ terminalLastByteDeliveries = [s \in Sessions |-> 0]
|
||||
/\ terminalLastSignalDeliveries = [s \in Sessions |-> 0]
|
||||
/\ terminalLastLocalDeliveries = [s \in Sessions |-> 0]
|
||||
/\ terminalLastMetadataDeliveries = [s \in Sessions |-> 0]
|
||||
/\ sessionClientSuspended = [s \in Sessions |-> FALSE]
|
||||
/\ sessionTerminalTransportState = [s \in Sessions |-> "Ready"]
|
||||
|
||||
(***************************************************************************
|
||||
Domain and Session lifecycle
|
||||
|
|
@ -883,8 +1003,9 @@ DisconnectSession(s) ==
|
|||
Session Terminal and PTY lifecycle
|
||||
|
||||
The model retains durable state plus abstract PTY, exec-client, and guest
|
||||
identity facts. Descriptor identities, PID reuse checks, and signal delivery
|
||||
remain physical refinements.
|
||||
identity facts. It distinguishes interaction authorities and target classes.
|
||||
Descriptor identities, PID reuse checks, control-character values, terminal
|
||||
modes, and physical byte or signal delivery remain refinements.
|
||||
***************************************************************************)
|
||||
|
||||
BeginSessionTerminal(s) ==
|
||||
|
|
@ -898,6 +1019,7 @@ BeginSessionTerminal(s) ==
|
|||
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = TRUE]
|
||||
/\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
|
||||
/\ UNCHANGED baseVars
|
||||
/\ UNCHANGED terminalInteractionVars
|
||||
|
||||
CommitSessionTerminal(s) ==
|
||||
/\ sessionPhase[s] = "Attached"
|
||||
|
|
@ -909,6 +1031,7 @@ CommitSessionTerminal(s) ==
|
|||
/\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Running"]
|
||||
/\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = TRUE]
|
||||
/\ UNCHANGED <<baseVars, sessionPtyOpen, sessionExecPresent>>
|
||||
/\ UNCHANGED terminalInteractionVars
|
||||
|
||||
DisconnectCleanSession(s) ==
|
||||
/\ sessionTerminalState[s] = "Clean"
|
||||
|
|
@ -921,6 +1044,7 @@ DisconnectLiveSessionTerminal(s) ==
|
|||
/\ sessionTerminalState' =
|
||||
[sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
|
||||
/\ UNCHANGED <<sessionPtyOpen, sessionExecPresent, sessionGuestKnown>>
|
||||
/\ UNCHANGED terminalInteractionVars
|
||||
|
||||
CompleteSessionTerminal(s) ==
|
||||
/\ sessionTerminalState[s] = "Running"
|
||||
|
|
@ -929,6 +1053,7 @@ CompleteSessionTerminal(s) ==
|
|||
[sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
|
||||
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
|
||||
/\ UNCHANGED <<sessionPtyOpen, sessionGuestKnown>>
|
||||
/\ UNCHANGED terminalInteractionVars
|
||||
|
||||
ExitSessionTerminalBeforeGuestIdentity(s) ==
|
||||
/\ sessionTerminalState[s] = "Intent"
|
||||
|
|
@ -938,6 +1063,7 @@ ExitSessionTerminalBeforeGuestIdentity(s) ==
|
|||
/\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = FALSE]
|
||||
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
|
||||
/\ UNCHANGED sessionGuestKnown
|
||||
/\ UNCHANGED terminalInteractionVars
|
||||
|
||||
RetainFailedSessionTerminal(s) ==
|
||||
/\ sessionPhase[s] = "Failed"
|
||||
|
|
@ -947,6 +1073,7 @@ RetainFailedSessionTerminal(s) ==
|
|||
/\ sessionPtyOpen' = [sessionPtyOpen EXCEPT ![s] = FALSE]
|
||||
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
|
||||
/\ UNCHANGED <<baseVars, sessionGuestKnown>>
|
||||
/\ UNCHANGED terminalInteractionVars
|
||||
|
||||
CleanKnownSessionTerminal(s) ==
|
||||
/\ sessionPhase[s] \in {"Closed", "Failed"}
|
||||
|
|
@ -958,6 +1085,7 @@ CleanKnownSessionTerminal(s) ==
|
|||
/\ sessionExecPresent' = [sessionExecPresent EXCEPT ![s] = FALSE]
|
||||
/\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
|
||||
/\ UNCHANGED baseVars
|
||||
/\ UNCHANGED terminalInteractionVars
|
||||
|
||||
BootstrapCleanSessionTerminalAfterRuntimeAbsence(s) ==
|
||||
/\ sessionPhase[s] \in {"Closed", "Failed"}
|
||||
|
|
@ -968,7 +1096,200 @@ BootstrapCleanSessionTerminalAfterRuntimeAbsence(s) ==
|
|||
/\ HostCoordinatorAlive(Dom(s))
|
||||
/\ sessionTerminalState' = [sessionTerminalState EXCEPT ![s] = "Clean"]
|
||||
/\ sessionGuestKnown' = [sessionGuestKnown EXCEPT ![s] = FALSE]
|
||||
/\ UNCHANGED <<baseVars, sessionPtyOpen, sessionExecPresent>>
|
||||
/\ UNCHANGED <<baseVars, sessionPtyOpen, sessionExecPresent,
|
||||
terminalInteractionVars>>
|
||||
|
||||
TerminalInteractionAdmissible(s) ==
|
||||
/\ sessionPhase[s] = "Attached"
|
||||
/\ connectionState[s] = "Connected"
|
||||
/\ terminalRoute[s] = "Sandbox"
|
||||
/\ sessionTerminalState[s] = "Running"
|
||||
/\ HostCoordinatorAlive(Dom(s))
|
||||
|
||||
TerminalEventAvailable(s) ==
|
||||
terminalEventIndex[s] <= Len(TerminalEventPlan[s])
|
||||
|
||||
CurrentTerminalEvent(s) ==
|
||||
IF TerminalEventAvailable(s)
|
||||
THEN TerminalEventPlan[s][terminalEventIndex[s]]
|
||||
ELSE "None"
|
||||
|
||||
CurrentTerminalAuthority(s) ==
|
||||
IF TerminalEventAvailable(s)
|
||||
THEN TerminalAuthorityPlan[s][terminalEventIndex[s]]
|
||||
ELSE "None"
|
||||
|
||||
CurrentTerminalAdministrativeAuthorityValid(s) ==
|
||||
IF TerminalEventAvailable(s)
|
||||
THEN TerminalAdministrativeAuthorityValid[s][terminalEventIndex[s]]
|
||||
ELSE FALSE
|
||||
|
||||
OtherSession(s) == CHOOSE t \in Sessions : t # s
|
||||
|
||||
TerminalDelivery(disposition, destination, target, bytes, signals, local, metadata) ==
|
||||
[disposition |-> disposition,
|
||||
destination |-> destination,
|
||||
target |-> target,
|
||||
byteDeliveries |-> bytes,
|
||||
signalDeliveries |-> signals,
|
||||
localDeliveries |-> local,
|
||||
metadataDeliveries |-> metadata]
|
||||
|
||||
NoTerminalDelivery ==
|
||||
TerminalDelivery("None", NoSession, "None", 0, 0, 0, 0)
|
||||
|
||||
RefusedTerminalDelivery ==
|
||||
TerminalDelivery("Refused", NoSession, "None", 0, 0, 0, 0)
|
||||
|
||||
ExpectedTerminalDelivery(s, event, authority, administrativeAuthorityValid) ==
|
||||
CASE /\ event = "Keyboard"
|
||||
/\ authority = "Client" ->
|
||||
TerminalDelivery("Delivered", s, "GuestPtyForeground", 1, 0, 0, 0)
|
||||
[] /\ event = "ExplicitSignal"
|
||||
/\ authority = "Administrator"
|
||||
/\ administrativeAuthorityValid ->
|
||||
TerminalDelivery("Delivered", s, "RecordedGuestGroup", 0, 1, 0, 0)
|
||||
[] event = "ExplicitSignal" -> RefusedTerminalDelivery
|
||||
[] /\ event = "Resize"
|
||||
/\ authority = "Client" ->
|
||||
TerminalDelivery("Delivered", s, "ExactSessionPty", 0, 0, 0, 1)
|
||||
[] /\ event = "Break"
|
||||
/\ authority = "LocalClient" ->
|
||||
TerminalDelivery("Delivered", s, "ExactSessionPty", 0, 0, 0, 1)
|
||||
[] /\ event \in {"LocalSuspend", "LocalResume", "LocalDisconnect"}
|
||||
/\ authority = "LocalClient" ->
|
||||
TerminalDelivery("Delivered", s, "LocalClient", 0, 0, 1, 0)
|
||||
[] /\ event = "HostSignal"
|
||||
/\ authority = "HostProcess" ->
|
||||
TerminalDelivery("Delivered", s, "LocalClient", 0, 0, 1, 0)
|
||||
[] OTHER -> RefusedTerminalDelivery
|
||||
|
||||
RoutedTerminalDelivery(s, event, authority, administrativeAuthorityValid) ==
|
||||
LET expected == ExpectedTerminalDelivery(
|
||||
s, event, authority, administrativeAuthorityValid) IN
|
||||
CASE /\ TerminalRoutingFault = "KeyboardRecordedGroup"
|
||||
/\ event = "Keyboard" ->
|
||||
TerminalDelivery("Delivered", s, "RecordedGuestGroup", 0, 1, 0, 0)
|
||||
[] /\ TerminalRoutingFault = "KeyboardDuplicated"
|
||||
/\ event = "Keyboard" ->
|
||||
TerminalDelivery("Delivered", s, "GuestPtyForeground", 1, 1, 0, 0)
|
||||
[] /\ TerminalRoutingFault = "CrossSession"
|
||||
/\ expected.disposition = "Delivered" ->
|
||||
[expected EXCEPT !.destination = OtherSession(s)]
|
||||
[] /\ TerminalRoutingFault = "ClientAdministrativeSignal"
|
||||
/\ event = "ExplicitSignal"
|
||||
/\ authority = "Client" ->
|
||||
TerminalDelivery("Delivered", s, "RecordedGuestGroup", 0, 1, 0, 0)
|
||||
[] OTHER -> expected
|
||||
|
||||
RecordTerminalEvent(s) ==
|
||||
LET event == CurrentTerminalEvent(s)
|
||||
authority == CurrentTerminalAuthority(s)
|
||||
administrativeAuthorityValid ==
|
||||
CurrentTerminalAdministrativeAuthorityValid(s)
|
||||
delivery == RoutedTerminalDelivery(
|
||||
s, event, authority, administrativeAuthorityValid)
|
||||
IN
|
||||
/\ terminalEventIndex' =
|
||||
[terminalEventIndex EXCEPT ![s] = @ + 1]
|
||||
/\ terminalLastEventId' =
|
||||
[terminalLastEventId EXCEPT ![s] = terminalEventIndex[s]]
|
||||
/\ terminalLastEvent' = [terminalLastEvent EXCEPT ![s] = event]
|
||||
/\ terminalLastSourceSession' =
|
||||
[terminalLastSourceSession EXCEPT ![s] = s]
|
||||
/\ terminalLastAuthority' =
|
||||
[terminalLastAuthority EXCEPT ![s] = authority]
|
||||
/\ terminalLastAdministrativeAuthorityValid' =
|
||||
[terminalLastAdministrativeAuthorityValid EXCEPT
|
||||
![s] = administrativeAuthorityValid]
|
||||
/\ terminalLastDisposition' =
|
||||
[terminalLastDisposition EXCEPT ![s] = delivery.disposition]
|
||||
/\ terminalLastDestination' =
|
||||
[terminalLastDestination EXCEPT ![s] = delivery.destination]
|
||||
/\ terminalLastTarget' =
|
||||
[terminalLastTarget EXCEPT ![s] = delivery.target]
|
||||
/\ terminalLastByteDeliveries' =
|
||||
[terminalLastByteDeliveries EXCEPT ![s] = delivery.byteDeliveries]
|
||||
/\ terminalLastSignalDeliveries' =
|
||||
[terminalLastSignalDeliveries EXCEPT ![s] = delivery.signalDeliveries]
|
||||
/\ terminalLastLocalDeliveries' =
|
||||
[terminalLastLocalDeliveries EXCEPT ![s] = delivery.localDeliveries]
|
||||
/\ terminalLastMetadataDeliveries' =
|
||||
[terminalLastMetadataDeliveries EXCEPT ![s] = delivery.metadataDeliveries]
|
||||
|
||||
DeliverPtyTerminalEvent(s) ==
|
||||
/\ TerminalInteractionAdmissible(s)
|
||||
/\ TerminalEventAvailable(s)
|
||||
/\ CurrentTerminalEvent(s) \in {
|
||||
"Keyboard", "ExplicitSignal", "Resize", "Break"
|
||||
}
|
||||
/\ ~sessionClientSuspended[s]
|
||||
/\ sessionTerminalTransportState[s] = "Ready"
|
||||
/\ RecordTerminalEvent(s)
|
||||
/\ UNCHANGED <<baseVars, terminalLifecycleVars, sessionClientSuspended,
|
||||
sessionTerminalTransportState>>
|
||||
|
||||
SuspendLocalTerminalClient(s) ==
|
||||
/\ TerminalInteractionAdmissible(s)
|
||||
/\ TerminalEventAvailable(s)
|
||||
/\ CurrentTerminalEvent(s) = "LocalSuspend"
|
||||
/\ ~sessionClientSuspended[s]
|
||||
/\ RecordTerminalEvent(s)
|
||||
/\ sessionClientSuspended' =
|
||||
[sessionClientSuspended EXCEPT ![s] = TRUE]
|
||||
/\ UNCHANGED <<baseVars, terminalLifecycleVars,
|
||||
sessionTerminalTransportState>>
|
||||
|
||||
ResumeLocalTerminalClient(s) ==
|
||||
/\ TerminalInteractionAdmissible(s)
|
||||
/\ TerminalEventAvailable(s)
|
||||
/\ CurrentTerminalEvent(s) = "LocalResume"
|
||||
/\ sessionClientSuspended[s]
|
||||
/\ RecordTerminalEvent(s)
|
||||
/\ sessionClientSuspended' =
|
||||
[sessionClientSuspended EXCEPT ![s] = FALSE]
|
||||
/\ UNCHANGED <<baseVars, terminalLifecycleVars,
|
||||
sessionTerminalTransportState>>
|
||||
|
||||
DisconnectTerminalFromLocalAuthority(s, event) ==
|
||||
/\ event \in {"LocalDisconnect", "HostSignal"}
|
||||
/\ TerminalEventAvailable(s)
|
||||
/\ CurrentTerminalEvent(s) = event
|
||||
/\ sessionTerminalState[s] \in {"Intent", "Running"}
|
||||
/\ \/ TerminalRoutingFault # "BlockedTransportPreventsLocalControl"
|
||||
\/ sessionTerminalTransportState[s] = "Ready"
|
||||
/\ DisconnectSession(s)
|
||||
/\ sessionTerminalState' =
|
||||
[sessionTerminalState EXCEPT ![s] = "ReleaseIntent"]
|
||||
/\ RecordTerminalEvent(s)
|
||||
/\ sessionClientSuspended' =
|
||||
[sessionClientSuspended EXCEPT ![s] = FALSE]
|
||||
/\ UNCHANGED <<sessionPtyOpen, sessionExecPresent, sessionGuestKnown,
|
||||
sessionTerminalTransportState>>
|
||||
|
||||
BlockSessionTerminalTransport(s) ==
|
||||
/\ TerminalInteractionAdmissible(s)
|
||||
/\ sessionTerminalTransportState[s] = "Ready"
|
||||
/\ sessionTerminalTransportState' =
|
||||
[sessionTerminalTransportState EXCEPT ![s] = "Blocked"]
|
||||
/\ UNCHANGED <<baseVars, terminalLifecycleVars, terminalEventRecordVars,
|
||||
sessionClientSuspended>>
|
||||
|
||||
UnblockSessionTerminalTransport(s) ==
|
||||
/\ sessionTerminalTransportState[s] = "Blocked"
|
||||
/\ sessionTerminalTransportState' =
|
||||
[sessionTerminalTransportState EXCEPT ![s] = "Ready"]
|
||||
/\ UNCHANGED <<baseVars, terminalLifecycleVars, terminalEventRecordVars,
|
||||
sessionClientSuspended>>
|
||||
|
||||
TerminalInteraction(s) ==
|
||||
\/ DeliverPtyTerminalEvent(s)
|
||||
\/ SuspendLocalTerminalClient(s)
|
||||
\/ ResumeLocalTerminalClient(s)
|
||||
\/ BlockSessionTerminalTransport(s)
|
||||
\/ UnblockSessionTerminalTransport(s)
|
||||
\/ (\E event \in {"LocalDisconnect", "HostSignal"} :
|
||||
DisconnectTerminalFromLocalAuthority(s, event))
|
||||
|
||||
BeginTeardown(d) ==
|
||||
/\ domainPhase[d] = "Ready"
|
||||
|
|
@ -2129,12 +2450,16 @@ Next ==
|
|||
\/ /\ BaseNext
|
||||
/\ UNCHANGED terminalVars
|
||||
\/ (\E s \in Sessions : SessionTerminalProgress(s))
|
||||
\/ (\E s \in Sessions : TerminalInteraction(s))
|
||||
|
||||
\* Resume transitions are enabled but not weakly fair: permanent stop is a
|
||||
\* modeled stuck state for safety, not a guaranteed progress path.
|
||||
Spec ==
|
||||
SafetySpec ==
|
||||
/\ Init
|
||||
/\ [][Next]_vars
|
||||
|
||||
Spec ==
|
||||
/\ SafetySpec
|
||||
/\ \A d \in Domains :
|
||||
WF_vars(DomainServiceProgress(d) /\ UNCHANGED terminalVars)
|
||||
/\ \A s \in Sessions :
|
||||
|
|
@ -2148,6 +2473,15 @@ Safety properties
|
|||
***************************************************************************)
|
||||
|
||||
TypeOK ==
|
||||
/\ TerminalEventPlan \in [Sessions -> Seq(TerminalEventKinds)]
|
||||
/\ TerminalAuthorityPlan \in [Sessions -> Seq(TerminalAuthorities)]
|
||||
/\ TerminalAdministrativeAuthorityValid \in [Sessions -> Seq(BOOLEAN)]
|
||||
/\ \A s \in Sessions :
|
||||
/\ Len(TerminalEventPlan[s]) = Len(TerminalAuthorityPlan[s])
|
||||
/\ Len(TerminalEventPlan[s]) =
|
||||
Len(TerminalAdministrativeAuthorityValid[s])
|
||||
/\ TerminalRoutingFault \in TerminalRoutingFaults
|
||||
/\ (TerminalRoutingFault = "CrossSession" => Cardinality(Sessions) > 1)
|
||||
/\ domainPhase \in [Domains -> DomainPhases]
|
||||
/\ stateAnchorState \in [Domains -> MountStates]
|
||||
/\ sidecarState \in [Domains -> ResourceStates]
|
||||
|
|
@ -2186,6 +2520,23 @@ TypeOK ==
|
|||
/\ sessionPtyOpen \in [Sessions -> BOOLEAN]
|
||||
/\ sessionExecPresent \in [Sessions -> BOOLEAN]
|
||||
/\ sessionGuestKnown \in [Sessions -> BOOLEAN]
|
||||
/\ \A s \in Sessions :
|
||||
terminalEventIndex[s] \in 1..(Len(TerminalEventPlan[s]) + 1)
|
||||
/\ \A s \in Sessions :
|
||||
terminalLastEventId[s] \in 0..Len(TerminalEventPlan[s])
|
||||
/\ terminalLastEvent \in [Sessions -> TerminalEventKinds \cup {"None"}]
|
||||
/\ terminalLastSourceSession \in [Sessions -> Sessions \cup {NoSession}]
|
||||
/\ terminalLastAuthority \in [Sessions -> TerminalAuthorities]
|
||||
/\ terminalLastAdministrativeAuthorityValid \in [Sessions -> BOOLEAN]
|
||||
/\ terminalLastDisposition \in [Sessions -> TerminalDispositions]
|
||||
/\ terminalLastDestination \in [Sessions -> Sessions \cup {NoSession}]
|
||||
/\ terminalLastTarget \in [Sessions -> TerminalTargets]
|
||||
/\ terminalLastByteDeliveries \in [Sessions -> 0..1]
|
||||
/\ terminalLastSignalDeliveries \in [Sessions -> 0..1]
|
||||
/\ terminalLastLocalDeliveries \in [Sessions -> 0..1]
|
||||
/\ terminalLastMetadataDeliveries \in [Sessions -> 0..1]
|
||||
/\ sessionClientSuspended \in [Sessions -> BOOLEAN]
|
||||
/\ sessionTerminalTransportState \in [Sessions -> TerminalTransportStates]
|
||||
|
||||
SessionTerminalPhysicalConsistency ==
|
||||
\A s \in Sessions :
|
||||
|
|
@ -2375,6 +2726,38 @@ TerminalIsolation ==
|
|||
\A s \in Sessions : sessionPhase[s] = "Prompting" =>
|
||||
terminalRoute[s] = "Prompt"
|
||||
|
||||
ObservedTerminalDelivery(s) ==
|
||||
TerminalDelivery(
|
||||
terminalLastDisposition[s],
|
||||
terminalLastDestination[s],
|
||||
terminalLastTarget[s],
|
||||
terminalLastByteDeliveries[s],
|
||||
terminalLastSignalDeliveries[s],
|
||||
terminalLastLocalDeliveries[s],
|
||||
terminalLastMetadataDeliveries[s])
|
||||
|
||||
TerminalInteractionAuthoritySeparated ==
|
||||
\A s \in Sessions :
|
||||
/\ terminalEventIndex[s] = terminalLastEventId[s] + 1
|
||||
/\ IF terminalLastEventId[s] = 0
|
||||
THEN /\ terminalLastEvent[s] = "None"
|
||||
/\ terminalLastSourceSession[s] = NoSession
|
||||
/\ terminalLastAuthority[s] = "None"
|
||||
/\ ~terminalLastAdministrativeAuthorityValid[s]
|
||||
/\ ObservedTerminalDelivery(s) = NoTerminalDelivery
|
||||
ELSE LET event == TerminalEventPlan[s][terminalLastEventId[s]]
|
||||
authority == TerminalAuthorityPlan[s][terminalLastEventId[s]]
|
||||
administrativeAuthorityValid ==
|
||||
TerminalAdministrativeAuthorityValid[s][terminalLastEventId[s]]
|
||||
IN /\ terminalLastEvent[s] = event
|
||||
/\ terminalLastSourceSession[s] = s
|
||||
/\ terminalLastAuthority[s] = authority
|
||||
/\ terminalLastAdministrativeAuthorityValid[s] =
|
||||
administrativeAuthorityValid
|
||||
/\ ObservedTerminalDelivery(s) =
|
||||
ExpectedTerminalDelivery(
|
||||
s, event, authority, administrativeAuthorityValid)
|
||||
|
||||
NoOrphanHostProcess ==
|
||||
\A r \in hostRunning :
|
||||
LET s == ReqSession(r) IN
|
||||
|
|
@ -2544,6 +2927,7 @@ Safety ==
|
|||
/\ HostExecutionAuthorized
|
||||
/\ AutoApprovalNoShell
|
||||
/\ TerminalIsolation
|
||||
/\ TerminalInteractionAuthoritySeparated
|
||||
/\ NoOrphanHostProcess
|
||||
/\ StateAnchorOwnership
|
||||
/\ FailedDomainIsolation
|
||||
|
|
@ -2551,6 +2935,65 @@ Safety ==
|
|||
/\ ResultDeliveryStateConsistent
|
||||
/\ NetworkReadinessBoundToSandbox
|
||||
|
||||
TerminalEventAdvanced(s) ==
|
||||
/\ terminalLastEventId'[s] = terminalEventIndex[s]
|
||||
/\ terminalEventIndex'[s] = terminalEventIndex[s] + 1
|
||||
|
||||
TerminalSessionProjection(s) == <<
|
||||
sessionPhase[s], terminalRoute[s], connectionState[s], activeRequest[s],
|
||||
sessionTerminalState[s], sessionPtyOpen[s], sessionExecPresent[s],
|
||||
sessionGuestKnown[s], terminalEventIndex[s], terminalLastEventId[s],
|
||||
terminalLastEvent[s], terminalLastSourceSession[s],
|
||||
terminalLastAuthority[s], terminalLastAdministrativeAuthorityValid[s],
|
||||
terminalLastDisposition[s],
|
||||
terminalLastDestination[s], terminalLastTarget[s],
|
||||
terminalLastByteDeliveries[s], terminalLastSignalDeliveries[s],
|
||||
terminalLastLocalDeliveries[s], terminalLastMetadataDeliveries[s],
|
||||
sessionClientSuspended[s], sessionTerminalTransportState[s]
|
||||
>>
|
||||
|
||||
DomainRuntimeProjection(d) == <<
|
||||
domainPhase[d], stateAnchorState[d], sidecarState[d], sandboxState[d],
|
||||
trustReady[d], domainLockHeld[d], hostCoordinatorProc[d],
|
||||
runtimeSupervisorProc[d], attachedRunscProc[d], runtimeCausalEdge[d],
|
||||
supervisorLease[d], domainGeneration[d], durableDecision[d],
|
||||
durableIntent[d], genCoordinatorId[d], genSidecarId[d], genSandboxId[d],
|
||||
networkReady[d], preparedLowerLeased[d], helperProc[d]
|
||||
>>
|
||||
|
||||
TerminalPeerIsolationAction ==
|
||||
\A s \in Sessions :
|
||||
TerminalEventAdvanced(s) =>
|
||||
\A t \in Sessions \ {s} : UNCHANGED TerminalSessionProjection(t)
|
||||
|
||||
TerminalPeerIsolation ==
|
||||
[][TerminalPeerIsolationAction]_vars
|
||||
|
||||
LocalTerminalControlKinds == {
|
||||
"LocalSuspend", "LocalResume", "LocalDisconnect", "HostSignal"
|
||||
}
|
||||
|
||||
TerminalLocalControlPreservesDomainAction ==
|
||||
\A s \in Sessions :
|
||||
/\ TerminalEventAdvanced(s)
|
||||
/\ CurrentTerminalEvent(s) \in LocalTerminalControlKinds
|
||||
/\ \E t \in Sessions \ {s} : connectionState[t] = "Connected"
|
||||
=> UNCHANGED DomainRuntimeProjection(Dom(s))
|
||||
|
||||
TerminalLocalControlPreservesDomain ==
|
||||
[][TerminalLocalControlPreservesDomainAction]_vars
|
||||
|
||||
LocalTerminationAvailableWhileTransportBlocked ==
|
||||
\A s \in Sessions :
|
||||
/\ sessionTerminalTransportState[s] = "Blocked"
|
||||
/\ sessionPhase[s] = "Attached"
|
||||
/\ connectionState[s] = "Connected"
|
||||
/\ sessionTerminalState[s] \in {"Intent", "Running"}
|
||||
/\ TerminalEventAvailable(s)
|
||||
/\ CurrentTerminalEvent(s) \in {"LocalDisconnect", "HostSignal"}
|
||||
=> ENABLED DisconnectTerminalFromLocalAuthority(
|
||||
s, CurrentTerminalEvent(s))
|
||||
|
||||
(***************************************************************************
|
||||
Liveness properties.
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue