105 lines
3.7 KiB
INI
105 lines
3.7 KiB
INI
|
CONSTANTS
|
||
|
|
D1 = d1
|
||
|
|
S1 = s1
|
||
|
|
S2 = s2
|
||
|
|
R1 = r1
|
||
|
|
R2 = r2
|
||
|
|
R3 = r3
|
||
|
|
ExactCmd = exactCmd
|
||
|
|
PromptCmd = promptCmd
|
||
|
|
ShellCmd = shellCmd
|
||
|
|
EditedCmd = editedCmd
|
||
|
|
Identities <- IdentitiesFixture
|
||
|
|
SessionAnchors <- SessionAnchorsFixture
|
||
|
|
Domains <- DomainsFixture
|
||
|
|
Sessions <- SessionsFixture
|
||
|
|
Requests <- RequestsFixture
|
||
|
|
Commands <- CommandsFixture
|
||
|
|
NoSession = NoSession
|
||
|
|
NoRequest = NoRequest
|
||
|
|
NoCommand = NoCommand
|
||
|
|
NoApproval = NoApproval
|
||
|
|
SessionDomain <- SessionDomainFixture
|
||
|
|
SessionFingerprint <- SessionFingerprintFixture
|
||
|
|
DomainFingerprint <- DomainFingerprintFixture
|
||
|
|
DomainCoordinatorIdentity <- DomainCoordinatorIdentityFixture
|
||
|
|
DomainSidecarIdentity <- DomainSidecarIdentityFixture
|
||
|
|
DomainSandboxIdentity <- DomainSandboxIdentityFixture
|
||
|
|
SessionCliIdentity <- SessionCliIdentityFixture
|
||
|
|
SessionAnchorIdentity <- SessionAnchorIdentityFixture
|
||
|
|
CoordinatorCertificateValid <- CoordinatorCertificateValidFixture
|
||
|
|
SidecarCertificateValid <- SidecarCertificateValidFixture
|
||
|
|
SandboxCertificateValid <- SandboxCertificateValidFixture
|
||
|
|
CliCertificateValid <- CliCertificateValidFixture
|
||
|
|
ConfigSafe <- ConfigSafeFixture
|
||
|
|
SandboxIsolationSafe <- SandboxIsolationSafeFixture
|
||
|
|
RequestSession <- RequestSessionFixture
|
||
|
|
RequestCommand <- RequestCommandFixture
|
||
|
|
RequestSandboxIdentity <- RequestSandboxIdentityFixture
|
||
|
|
RequestCliIdentity <- RequestCliIdentityFixture
|
||
|
|
RequestSessionAnchor <- RequestSessionAnchorFixture
|
||
|
|
RequestCredentialValid <- RequestCredentialValidFixture
|
||
|
|
RequestSignatureValid <- RequestSignatureValidFixture
|
||
|
|
ApprovalCliIdentity <- ApprovalCliIdentityFixture
|
||
|
|
ApprovalSessionAnchor <- ApprovalSessionAnchorFixture
|
||
|
|
ApprovalSignatureValid <- ApprovalSignatureValidFixture
|
||
|
|
ApprovalCommand <- ApprovalCommandFixture
|
||
|
|
AutoRuleMatches <- AutoRuleMatchesFixture
|
||
|
|
CommandRequiresShell <- CommandRequiresShellFixture
|
||
|
|
CommandContentSafe <- CommandContentSafeFixture
|
||
|
|
TerminalEventPlan <- TerminalEventPlanFixture
|
||
|
|
TerminalAuthorityPlan <- TerminalAuthorityPlanFixture
|
||
|
|
TerminalAdministrativeAuthorityValid <-
|
||
|
|
TerminalAdministrativeAuthorityValidFixture
|
||
|
|
TerminalRoutingFault = "Correct"
|
||
|
|
|
||
|
|
SPECIFICATION SafetySpec
|
||
|
|
CHECK_DEADLOCK FALSE
|
||
|
|
|
||
|
|
INVARIANTS
|
||
|
|
TypeOK
|
||
|
|
SessionTerminalPhysicalConsistency
|
||
|
|
ConfigurationConfinement
|
||
|
|
SandboxNamespaceIsolation
|
||
|
|
OrderedNetworkStartup
|
||
|
|
PublishedDomainsReady
|
||
|
|
DomainLockLifetime
|
||
|
|
RuntimeCausalEdgeArmedBeforeSandbox
|
||
|
|
RuntimeCausalEdgeOwnerPresent
|
||
|
|
SandboxRunningImpliesCoordinatorPresent
|
||
|
|
PublishedRuntimeAuthorityPresent
|
||
|
|
SupervisorLeaseConsistency
|
||
|
|
RuntimeResourceOwnership
|
||
|
|
CoordinatorPhysicalConsistency
|
||
|
|
HostCoordinatorRequiresDomainOwnership
|
||
|
|
NoVanishPresentRuntime
|
||
|
|
OrderedLeaseTeardown
|
||
|
|
DomainGenerationBounds
|
||
|
|
DurableIntentBeforeSandboxReady
|
||
|
|
DurableDecisionPublicationConsistent
|
||
|
|
PathMismatchNotAdopted
|
||
|
|
ExclusiveBootstrapOwnership
|
||
|
|
TeardownNotJoinable
|
||
|
|
RegisteredSessionsConnected
|
||
|
|
AttachedSessionsValid
|
||
|
|
AuthenticatedRequestsOnly
|
||
|
|
RuntimeRoleIdentitySeparation
|
||
|
|
RegisteredSessionIdentityUniqueness
|
||
|
|
LiveRequestIdentityAuthorized
|
||
|
|
DeveloperApprovalAuthenticated
|
||
|
|
HostExecutionAuthorized
|
||
|
|
AutoApprovalNoShell
|
||
|
|
TerminalIsolation
|
||
|
|
TerminalInteractionAuthoritySeparated
|
||
|
|
LocalTerminationAvailableWhileTransportBlocked
|
||
|
|
NoOrphanHostProcess
|
||
|
|
StateAnchorOwnership
|
||
|
|
FailedDomainIsolation
|
||
|
|
OrderedFailureRecovery
|
||
|
|
ResultDeliveryStateConsistent
|
||
|
|
MultiRoleDurableIntent
|
||
|
|
NetworkReadinessBoundToSandbox
|
||
|
|
GenerationScopedIdentitiesDistinct
|
||
|
|
HelperUnderSupervisor
|
||
|
|
PreparedLowerLeaseBeforeMount
|
||
|
|
NetworkReadyBeforePublish
|