From 2795f576a92bb1cbcee5194b5751c45b3e2c5fe4 Mon Sep 17 00:00:00 2001 From: Kenny Root Date: Thu, 23 Jul 2026 19:55:01 -0700 Subject: [PATCH 1/4] fix(channels): close old channels in registry --- .../connectbot/sshlib/client/SshConnection.kt | 10 ++++-- .../sshlib/client/SshClientIntegrationTest.kt | 33 +++++++++++++++++++ .../sshlib/client/SshConnectionFlowTest.kt | 23 ++++++++++++- 3 files changed, 63 insertions(+), 3 deletions(-) diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt index a25f0ad..20a3a96 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt @@ -2560,9 +2560,15 @@ class SshConnection( val recipientChannel = msg.recipientChannel().toInt() logger.debug("Received CHANNEL_CLOSE for local channel $recipientChannel") when (val entry = channelRegistry.findByLocalRecipient(recipientChannel)) { - is SshChannelRegistry.Entry.Established.Session -> entry.channel.onClose() + is SshChannelRegistry.Entry.Established.Session -> { + entry.channel.onClose() + channelRegistry.unregister(recipientChannel) + } - is SshChannelRegistry.Entry.Established.Agent -> entry.channel.onClose() + is SshChannelRegistry.Entry.Established.Agent -> { + entry.channel.onClose() + channelRegistry.unregister(recipientChannel) + } is SshChannelRegistry.Entry.Established.Forwarding -> { entry.channel.onClose() diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshClientIntegrationTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshClientIntegrationTest.kt index 9e2a76a..5c9b2b7 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshClientIntegrationTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshClientIntegrationTest.kt @@ -1441,4 +1441,37 @@ class SshClientIntegrationTest { client.disconnect() } } + + @Test + fun `should support opening multiple session channels sequentially on single connection`() = runBlocking { + val host = opensshContainer.host + val port = opensshContainer.getMappedPort(22) + + val client = SshClient( + SshClientConfig { + this.host = host + this.port = port + this.hostKeyVerifier = acceptAllVerifier + }, + ) + + try { + assertTrue(client.connect() is ConnectResult.Success, "Should connect to SSH server") + assertTrue( + client.authenticatePassword(USERNAME, PASSWORD) is AuthResult.Success, + "Should authenticate successfully", + ) + + repeat(5) { attempt -> + val session = withTimeout(10_000) { client.openSession() } + assertNotNull(session, "openSession returned null on attempt $attempt") + val execGranted = withTimeout(10_000) { session!!.requestExec("true") } + assertTrue(execGranted, "requestExec failed on attempt $attempt") + session!!.close() + assertFalse(session.isOpen, "session should be closed on attempt $attempt") + } + } finally { + client.disconnect() + } + } } diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt index d120a9f..7d9c18e 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt @@ -527,6 +527,26 @@ class SshConnectionFlowTest { } } + @Test + fun `opening a second session channel after closing the first succeeds when server reuses remote channel number`() = runTest { + connectedFixture { connection, server, dispatcher -> + authenticate(connection, server, dispatcher) + + val session1 = openSession(connection, server, dispatcher, remoteChannelNumber = 100) + val localChannel1 = session1.localChannelNumber + + server.sendChannelClose(localChannel1) + withTimeout(5_000) { + while (session1.isOpen) { + yield() + } + } + + val session2 = openSession(connection, server, dispatcher, remoteChannelNumber = 100) + assertTrue(session2.isOpen) + } + } + @Test fun `direct tcpip channel routes data eof and close`() = runTest { connectedFixture { connection, server, dispatcher -> @@ -745,11 +765,12 @@ class SshConnectionFlowTest { connection: SshConnection, server: FakeSshServer, dispatcher: CoroutineDispatcher, + remoteChannelNumber: Int = 100, ): SessionChannel { val open = CoroutineScope(dispatcher).async { connection.openSessionChannel() } val openRequest = withTimeout(5_000) { server.awaitChannelOpen() } assertEquals("session", openRequest.channelType().value()) - server.sendChannelOpenConfirmation(openRequest.senderChannel().toInt(), senderChannel = 100) + server.sendChannelOpenConfirmation(openRequest.senderChannel().toInt(), senderChannel = remoteChannelNumber) return assertNotNull(withTimeout(5_000) { open.await() }) } From edeb42884106f1ee6f6e1c8959af653b61fb1b45 Mon Sep 17 00:00:00 2001 From: Kenny Root Date: Thu, 23 Jul 2026 19:56:17 -0700 Subject: [PATCH 2/4] chore(tla+): tighten up the SFTP model Make sure we have matching for request to response. --- .../sshlib/protocol/SftpStateMachine.kt | 162 +++++++++++++++--- .../protocol/SftpStateMachineFormalModel.kt | 55 ++++-- .../sshlib/protocol/SftpStateMachineTest.kt | 25 +++ .../resources/tla/SftpClientStateMachine.cfg | 2 + .../resources/tla/SftpClientStateMachine.tla | 60 ++++++- .../tla/SftpClientStateMachineGenerated.tla | 65 ++++--- 6 files changed, 308 insertions(+), 61 deletions(-) diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachine.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachine.kt index 3b8234c..c199867 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachine.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachine.kt @@ -48,6 +48,8 @@ internal enum class SftpState { */ internal enum class SftpHandleState { Unallocated, + PendingFile, + PendingDir, OpenFile, OpenDir, Closed, @@ -115,6 +117,15 @@ internal enum class SftpTransitionId { DISCONNECT_READY, } +internal enum class SftpPendingRequest(val tlaName: String) { + OPEN("PendingOpen"), + READ("PendingRead"), + WRITE("PendingWrite"), + READ_DIR("PendingReadDir"), + CLOSE("PendingClose"), + REQUEST("PendingRequest"), +} + internal data class SftpTransitionMeta( val id: SftpTransitionId, val eventId: SftpEventId, @@ -123,6 +134,7 @@ internal data class SftpTransitionMeta( val effects: Set, val origin: SftpEventOrigin, val requiresReadySession: Boolean, + val expectsPending: SftpPendingRequest? = null, ) : MetaInfo internal data class SftpAcceptedTransition( @@ -139,6 +151,7 @@ internal data class SftpFormalTransition( val effects: Set, val origin: SftpEventOrigin, val requiresReadySession: Boolean, + val expectsPending: SftpPendingRequest? = null, ) internal data class SftpFormalModel( @@ -281,7 +294,15 @@ internal class SftpStateMachine { ) } + private enum class PendingRequestKind { + OPEN, + READ, + READ_DIR, + GENERIC, + } + private val mutex = Mutex() + private val pendingRequests = mutableListOf() @Volatile private var activeState: SftpState = SftpState.UNINITIALIZED @@ -297,26 +318,111 @@ internal class SftpStateMachine { bindState(ready, SftpState.READY) bindState(closed, SftpState.CLOSED) - uninitialized.sftpTransition(SftpEvent.SendInit {}, SftpTransitionId.SEND_INIT_UNINITIALIZED, waitVersion) - waitVersion.sftpTransition(SftpEvent.ReceiveVersion {}, SftpTransitionId.RECEIVE_VERSION_WAIT_VERSION, ready) - - ready.sftpTransition(SftpEvent.OpenFile {}, SftpTransitionId.OPEN_FILE_READY) - ready.sftpTransition(SftpEvent.OpenDir {}, SftpTransitionId.OPEN_DIR_READY) - ready.sftpTransition(SftpEvent.ReadFile {}, SftpTransitionId.READ_FILE_READY) - ready.sftpTransition(SftpEvent.WriteFile {}, SftpTransitionId.WRITE_FILE_READY) - ready.sftpTransition(SftpEvent.ReadDir {}, SftpTransitionId.READ_DIR_READY) - ready.sftpTransition(SftpEvent.CloseHandle {}, SftpTransitionId.CLOSE_HANDLE_READY) - ready.sftpTransition(SftpEvent.Request {}, SftpTransitionId.REQUEST_READY) - - ready.sftpTransition(SftpEvent.ReceiveHandle {}, SftpTransitionId.RECEIVE_HANDLE_READY) - ready.sftpTransition(SftpEvent.ReceiveData {}, SftpTransitionId.RECEIVE_DATA_READY) - ready.sftpTransition(SftpEvent.ReceiveName {}, SftpTransitionId.RECEIVE_NAME_READY) - ready.sftpTransition(SftpEvent.ReceiveAttrs {}, SftpTransitionId.RECEIVE_ATTRS_READY) - ready.sftpTransition(SftpEvent.ReceiveStatus {}, SftpTransitionId.RECEIVE_STATUS_READY) - - uninitialized.sftpTransition(SftpEvent.Disconnect {}, SftpTransitionId.DISCONNECT_UNINITIALIZED, closed) - waitVersion.sftpTransition(SftpEvent.Disconnect {}, SftpTransitionId.DISCONNECT_WAIT_VERSION, closed) - ready.sftpTransition(SftpEvent.Disconnect {}, SftpTransitionId.DISCONNECT_READY, closed) + uninitialized.sftpTransition( + SftpEvent.SendInit {}, + SftpTransitionId.SEND_INIT_UNINITIALIZED, + target = waitVersion, + ) + waitVersion.sftpTransition( + SftpEvent.ReceiveVersion {}, + SftpTransitionId.RECEIVE_VERSION_WAIT_VERSION, + target = ready, + ) + + ready.sftpTransition( + SftpEvent.OpenFile {}, + SftpTransitionId.OPEN_FILE_READY, + onEffect = { pendingRequests.add(PendingRequestKind.OPEN) }, + ) + ready.sftpTransition( + SftpEvent.OpenDir {}, + SftpTransitionId.OPEN_DIR_READY, + onEffect = { pendingRequests.add(PendingRequestKind.OPEN) }, + ) + ready.sftpTransition( + SftpEvent.ReadFile {}, + SftpTransitionId.READ_FILE_READY, + onEffect = { pendingRequests.add(PendingRequestKind.READ) }, + ) + ready.sftpTransition( + SftpEvent.WriteFile {}, + SftpTransitionId.WRITE_FILE_READY, + onEffect = { pendingRequests.add(PendingRequestKind.GENERIC) }, + ) + ready.sftpTransition( + SftpEvent.ReadDir {}, + SftpTransitionId.READ_DIR_READY, + onEffect = { pendingRequests.add(PendingRequestKind.READ_DIR) }, + ) + ready.sftpTransition( + SftpEvent.CloseHandle {}, + SftpTransitionId.CLOSE_HANDLE_READY, + onEffect = { pendingRequests.add(PendingRequestKind.GENERIC) }, + ) + ready.sftpTransition( + SftpEvent.Request {}, + SftpTransitionId.REQUEST_READY, + onEffect = { pendingRequests.add(PendingRequestKind.GENERIC) }, + ) + + ready.sftpTransition( + SftpEvent.ReceiveHandle {}, + SftpTransitionId.RECEIVE_HANDLE_READY, + expectsPending = SftpPendingRequest.OPEN, + guard = { pendingRequests.contains(PendingRequestKind.OPEN) }, + onEffect = { pendingRequests.remove(PendingRequestKind.OPEN) }, + ) + ready.sftpTransition( + SftpEvent.ReceiveData {}, + SftpTransitionId.RECEIVE_DATA_READY, + expectsPending = SftpPendingRequest.READ, + guard = { pendingRequests.contains(PendingRequestKind.READ) }, + onEffect = { pendingRequests.remove(PendingRequestKind.READ) }, + ) + ready.sftpTransition( + SftpEvent.ReceiveName {}, + SftpTransitionId.RECEIVE_NAME_READY, + expectsPending = SftpPendingRequest.READ_DIR, + guard = { pendingRequests.contains(PendingRequestKind.READ_DIR) }, + onEffect = { pendingRequests.remove(PendingRequestKind.READ_DIR) }, + ) + ready.sftpTransition( + SftpEvent.ReceiveAttrs {}, + SftpTransitionId.RECEIVE_ATTRS_READY, + expectsPending = SftpPendingRequest.REQUEST, + guard = { pendingRequests.contains(PendingRequestKind.GENERIC) }, + onEffect = { pendingRequests.remove(PendingRequestKind.GENERIC) }, + ) + ready.sftpTransition( + SftpEvent.ReceiveStatus {}, + SftpTransitionId.RECEIVE_STATUS_READY, + expectsPending = null, + guard = { pendingRequests.isNotEmpty() }, + onEffect = { + if (pendingRequests.isNotEmpty()) { + pendingRequests.removeAt(0) + } + }, + ) + + uninitialized.sftpTransition( + SftpEvent.Disconnect {}, + SftpTransitionId.DISCONNECT_UNINITIALIZED, + target = closed, + onEffect = { pendingRequests.clear() }, + ) + waitVersion.sftpTransition( + SftpEvent.Disconnect {}, + SftpTransitionId.DISCONNECT_WAIT_VERSION, + target = closed, + onEffect = { pendingRequests.clear() }, + ) + ready.sftpTransition( + SftpEvent.Disconnect {}, + SftpTransitionId.DISCONNECT_READY, + target = closed, + onEffect = { pendingRequests.clear() }, + ) } val state: SftpState get() = activeState @@ -350,6 +456,7 @@ internal class SftpStateMachine { meta.effects, meta.origin, meta.requiresReadySession, + meta.expectsPending, ) } } @@ -360,7 +467,12 @@ internal class SftpStateMachine { } private suspend fun process(event: SftpEvent): Boolean = mutex.withLock { - stateMachine.processEvent(event) == ProcessingResult.PROCESSED + val result = stateMachine.processEvent(event) + if (result == ProcessingResult.PROCESSED) { + true + } else { + false + } } private fun bindState(state: IState, lifecycleState: SftpState) { @@ -372,9 +484,15 @@ internal class SftpStateMachine { id: SftpTransitionId, target: State? = null, effects: Set = event.effects, + expectsPending: SftpPendingRequest? = null, + noinline guard: (() -> Boolean)? = null, + noinline onEffect: (() -> Unit)? = null, ) { transition(id.name) { targetState = target + if (guard != null) { + this.guard = { guard() } + } metaInfo = SftpTransitionMeta( id = id, eventId = event.id, @@ -384,8 +502,10 @@ internal class SftpStateMachine { effects = effects, origin = event.origin, requiresReadySession = event.requiresReadySession, + expectsPending = expectsPending, ) }.onTriggered { + onEffect?.invoke() it.event.action(SftpAcceptedTransition(id, effects, event.origin)) } } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineFormalModel.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineFormalModel.kt index 8b66cd4..6979cba 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineFormalModel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineFormalModel.kt @@ -34,6 +34,7 @@ internal class SftpStateMachineFormalModel( val activeHandle: String = "activeHandle' = 0", val pendingRequests: String = "pendingRequests", val activeRequest: String = "activeRequest' = 0", + val requestHandles: String = "requestHandles", ) fun renderTla(moduleName: String = "SftpClientStateMachineGenerated"): String { @@ -100,6 +101,7 @@ internal class SftpStateMachineFormalModel( "handles" }, pendingRequests = if (disconnect) "[r \\in RequestIDs |-> \"None\"]" else "pendingRequests", + requestHandles = if (disconnect) "[r \\in RequestIDs |-> 0]" else "requestHandles", ), variables, ) @@ -110,10 +112,11 @@ internal class SftpStateMachineFormalModel( "AllocateHandle", FormalStep( transition = openFile, - handles = "[handles EXCEPT ![activeHandle'] = \"OpenFile\"]", + handles = "[handles EXCEPT ![activeHandle'] = \"PendingFile\"]", activeHandle = "activeHandle' \\in HandleIDs", pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = \"PendingOpen\"]", activeRequest = "activeRequest' \\in RequestIDs", + requestHandles = "[requestHandles EXCEPT ![activeRequest'] = activeHandle']", ), variables, "handles[activeHandle'] = \"Unallocated\"", @@ -125,10 +128,11 @@ internal class SftpStateMachineFormalModel( "AllocateDirHandle", FormalStep( transition = openDir, - handles = "[handles EXCEPT ![activeHandle'] = \"OpenDir\"]", + handles = "[handles EXCEPT ![activeHandle'] = \"PendingDir\"]", activeHandle = "activeHandle' \\in HandleIDs", pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = \"PendingOpen\"]", activeRequest = "activeRequest' \\in RequestIDs", + requestHandles = "[requestHandles EXCEPT ![activeRequest'] = activeHandle']", ), variables, "handles[activeHandle'] = \"Unallocated\"", @@ -171,7 +175,7 @@ internal class SftpStateMachineFormalModel( handles = "[handles EXCEPT ![activeHandle'] = \"Closed\"]", ), variables, - "handles[activeHandle'] \\in {\"OpenFile\", \"OpenDir\"}", + "handles[activeHandle'] \\in {\"PendingFile\", \"PendingDir\", \"OpenFile\", \"OpenDir\"}", "pendingRequests[activeRequest'] = \"None\"", ) appendLine() @@ -190,16 +194,42 @@ internal class SftpStateMachineFormalModel( appendLine("FulfillResponse ==") responseTransitions.forEach { transition -> - val step = FormalStep( - transition = transition, - pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = \"None\"]", - activeRequest = "activeRequest' \\in RequestIDs", - ) - appendLine(" \\/ /\\ state = ${quote(transition.source.name)}") - variables.forEach { variable -> - appendLine(" /\\ ${variable.renderNext(step)}") + val isReceiveHandle = transition.eventId == SftpEventId.RECEIVE_HANDLE + val pendingGuard = when (val expected = transition.expectsPending) { + null -> "pendingRequests[activeRequest'] # \"None\"" + else -> "pendingRequests[activeRequest'] = \"${expected.tlaName}\"" + } + if (isReceiveHandle) { + // Use \E to bind request ID before referencing requestHandles[r] + appendLine(" \\/ /\\ state = ${quote(transition.source.name)}") + appendLine(" /\\ \\E r \\in RequestIDs :") + appendLine(" /\\ pendingRequests[r] = \"PendingOpen\"") + appendLine(" /\\ requestHandles[r] # 0") + appendLine(" /\\ handles[requestHandles[r]] \\in {\"PendingFile\", \"PendingDir\"}") + appendLine(" /\\ state' = ${quote(transition.target.name)}") + appendLine(" /\\ previousState' = state") + appendLine(" /\\ event' = ${quote(transition.eventId.tlaName)}") + appendLine(" /\\ origin' = ${quote(transition.origin.name)}") + appendLine(" /\\ effects' = ${renderSet(transition.effects.map(SftpEffect::name))}") + appendLine(" /\\ previousHandles' = handles") + appendLine(" /\\ activeHandle' = 0") + appendLine(" /\\ handles' = [handles EXCEPT ![requestHandles[r]] = IF handles[requestHandles[r]] = \"PendingFile\" THEN \"OpenFile\" ELSE \"OpenDir\"]") + appendLine(" /\\ previousPendingRequests' = pendingRequests") + appendLine(" /\\ activeRequest' = r") + appendLine(" /\\ pendingRequests' = [pendingRequests EXCEPT ![r] = \"None\"]") + appendLine(" /\\ requestHandles' = [requestHandles EXCEPT ![r] = 0]") + } else { + val step = FormalStep( + transition = transition, + pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = \"None\"]", + activeRequest = "activeRequest' \\in RequestIDs", + ) + appendLine(" \\/ /\\ state = ${quote(transition.source.name)}") + variables.forEach { variable -> + appendLine(" /\\ ${variable.renderNext(step)}") + } + appendLine(" /\\ $pendingGuard") } - appendLine(" /\\ pendingRequests[activeRequest'] # \"None\"") } appendLine() @@ -270,6 +300,7 @@ internal class SftpStateMachineFormalModel( variable("previousPendingRequests", "[r \\in RequestIDs |-> \"None\"]") { "pendingRequests" }, FormalVariable("activeRequest", "0", FormalStep::activeRequest), variable("pendingRequests", "[r \\in RequestIDs |-> \"None\"]", FormalStep::pendingRequests), + variable("requestHandles", "[r \\in RequestIDs |-> 0]", FormalStep::requestHandles), ) private fun variable( diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineTest.kt index 720e540..c89b514 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineTest.kt @@ -133,4 +133,29 @@ class SftpStateMachineTest { assertEquals(renderer.renderTla(), fileContent) } } + + @Test + fun `enforces response matching in state machine`() = runBlocking { + val machine = SftpStateMachine() + assertTrue(machine.sendInit { }) + assertTrue(machine.receiveVersion { }) + + // Issue OpenFile -> expect PendingOpen + assertTrue(machine.openFile { }) + + // ReceiveData is declined because no READ is pending + assertFalse(machine.receiveData { }) + + // ReceiveHandle is accepted + assertTrue(machine.receiveHandle { }) + + // Issue ReadFile -> expect PendingRead + assertTrue(machine.readFile { }) + + // ReceiveHandle is declined because no OPEN is pending + assertFalse(machine.receiveHandle { }) + + // ReceiveData is accepted + assertTrue(machine.receiveData { }) + } } diff --git a/sshlib/src/test/resources/tla/SftpClientStateMachine.cfg b/sshlib/src/test/resources/tla/SftpClientStateMachine.cfg index 2402533..6ec492f 100644 --- a/sshlib/src/test/resources/tla/SftpClientStateMachine.cfg +++ b/sshlib/src/test/resources/tla/SftpClientStateMachine.cfg @@ -10,5 +10,7 @@ INVARIANT ClosedSessionClosesHandles INVARIANT HandleTypeOKAndOperationsGuarded INVARIANT HandleIsolation INVARIANT RequestCorrelationAndNonInterference +INVARIANT ResponseSemanticMatching +INVARIANT HandlePromotionSafety CHECK_DEADLOCK FALSE diff --git a/sshlib/src/test/resources/tla/SftpClientStateMachine.tla b/sshlib/src/test/resources/tla/SftpClientStateMachine.tla index 6f39937..366944a 100644 --- a/sshlib/src/test/resources/tla/SftpClientStateMachine.tla +++ b/sshlib/src/test/resources/tla/SftpClientStateMachine.tla @@ -13,6 +13,7 @@ TypeOK == /\ pendingRequests \in [RequestIDs -> {"None", "PendingOpen", "PendingRead", "PendingWrite", "PendingReadDir", "PendingClose", "PendingRequest"}] /\ previousPendingRequests \in [RequestIDs -> {"None", "PendingOpen", "PendingRead", "PendingWrite", "PendingReadDir", "PendingClose", "PendingRequest"}] /\ activeRequest \in 0..MaxRequests + /\ requestHandles \in [RequestIDs -> 0..MaxHandles] \* Invariant 1: Initialization Guard \* No handle operations or allocated handles are permitted before session reaches READY. @@ -25,17 +26,25 @@ ClosedSessionClosesHandles == \A h \in HandleIDs : handles[h] \in {"Unallocated", "Closed"} \* Invariant 2: Handle Safety & Type Guards -\* Read/Write requires OpenFile, ReadDir requires OpenDir, CloseHandle requires OpenFile/OpenDir. +\* Read/Write requires a fully confirmed OpenFile, ReadDir requires a confirmed OpenDir. +\* Operations on pending (unconfirmed) handles are forbidden. HandleTypeOKAndOperationsGuarded == /\ (event \in {"ReadFile", "WriteFile"} => activeHandle # 0 /\ previousHandles[activeHandle] = "OpenFile") /\ (event = "ReadDir" => activeHandle # 0 /\ previousHandles[activeHandle] = "OpenDir") - /\ (event = "CloseHandle" => activeHandle # 0 /\ previousHandles[activeHandle] \in {"OpenFile", "OpenDir"}) + /\ (event = "CloseHandle" => activeHandle # 0 /\ previousHandles[activeHandle] \in {"PendingFile", "PendingDir", "OpenFile", "OpenDir"}) \* Invariant 3: Handle Isolation -\* Targeted handle operations alter activeHandle while keeping sibling handles unchanged. +\* Targeted handle operations alter only the intended handle, keeping siblings unchanged. +\* For direct operations (activeHandle # 0), only activeHandle may change. +\* For ReceiveHandle responses, the handle referenced by requestHandles[activeRequest] may change. HandleIsolation == - activeHandle \in HandleIDs => - \A other \in HandleIDs \ {activeHandle} : + LET modifiedHandle == + IF activeHandle \in HandleIDs THEN activeHandle + ELSE IF event = "ReceiveHandle" /\ activeRequest \in RequestIDs + THEN requestHandles[activeRequest] + ELSE 0 + IN modifiedHandle \in HandleIDs => + \A other \in HandleIDs \ {modifiedHandle} : handles[other] = previousHandles[other] \* Invariant 4: Request ID Correlation & Non-Interference @@ -45,18 +54,57 @@ RequestCorrelationAndNonInterference == \A other \in RequestIDs \ {activeRequest} : pendingRequests[other] = previousPendingRequests[other] +\* Invariant 5: Response Semantic Matching +\* Verifies that incoming response events match the expected pending request type. +ResponseSemanticMatching == + (event \in {"ReceiveData", "ReceiveHandle", "ReceiveName", "ReceiveStatus", "ReceiveAttrs"} /\ activeRequest # 0) => + CASE event = "ReceiveHandle" -> + previousPendingRequests[activeRequest] = "PendingOpen" + [] event = "ReceiveData" -> + previousPendingRequests[activeRequest] = "PendingRead" + [] event = "ReceiveName" -> + previousPendingRequests[activeRequest] = "PendingReadDir" + [] event = "ReceiveAttrs" -> + previousPendingRequests[activeRequest] = "PendingRequest" + [] event = "ReceiveStatus" -> + previousPendingRequests[activeRequest] \in { + "PendingOpen", + "PendingRead", + "PendingWrite", + "PendingReadDir", + "PendingClose", + "PendingRequest" + } + [] OTHER -> FALSE + +\* Invariant 6: Handle Promotion Safety +\* ReceiveHandle must promote exactly one pending handle; handles must not be usable before promotion. +HandlePromotionSafety == + \* When ReceiveHandle fires, exactly one handle must transition from Pending* to Open* + /\ (event = "ReceiveHandle" /\ activeRequest # 0 => + \E h \in HandleIDs : + /\ previousHandles[h] \in {"PendingFile", "PendingDir"} + /\ handles[h] = IF previousHandles[h] = "PendingFile" THEN "OpenFile" ELSE "OpenDir" + /\ \A other \in HandleIDs \ {h} : handles[other] = previousHandles[other]) + \* I/O operations (Read/Write/ReadDir) must never target a pending (unconfirmed) handle + /\ (event \in {"ReadFile", "WriteFile", "ReadDir"} => + \A h \in HandleIDs : handles[h] \notin {"PendingFile", "PendingDir"} \/ handles[h] = previousHandles[h]) + \* ModelView abstraction to reduce state space explosion and keep TLC fast ModelView == << state, handles, pendingRequests, + requestHandles, activeHandle, activeRequest, NoOperationsBeforeInitialization, ClosedSessionClosesHandles, HandleTypeOKAndOperationsGuarded, HandleIsolation, - RequestCorrelationAndNonInterference + RequestCorrelationAndNonInterference, + ResponseSemanticMatching, + HandlePromotionSafety >> ==== diff --git a/sshlib/src/test/resources/tla/SftpClientStateMachineGenerated.tla b/sshlib/src/test/resources/tla/SftpClientStateMachineGenerated.tla index 0313b50..b052e29 100644 --- a/sshlib/src/test/resources/tla/SftpClientStateMachineGenerated.tla +++ b/sshlib/src/test/resources/tla/SftpClientStateMachineGenerated.tla @@ -1,6 +1,6 @@ ---- MODULE SftpClientStateMachineGenerated ---- \* Generated from SftpStateMachine. Do not edit. -\* Model SHA-256: 66c6ecb224482047f6437721e0f69ecc6ad240c631519a17776df4038ef3cff1 +\* Model SHA-256: a7f1fe5d3c3f7cad3881332410271e5cd067ecc1df7c4947f3640602b35946e7 EXTENDS Naturals CONSTANT MaxHandles, MaxRequests @@ -8,15 +8,15 @@ CONSTANT MaxHandles, MaxRequests HandleIDs == 1..MaxHandles RequestIDs == 1..MaxRequests -VARIABLES state, previousState, event, origin, effects, previousHandles, activeHandle, handles, previousPendingRequests, activeRequest, pendingRequests +VARIABLES state, previousState, event, origin, effects, previousHandles, activeHandle, handles, previousPendingRequests, activeRequest, pendingRequests, requestHandles -vars == <> +vars == <> States == {"CLOSED", "READY", "UNINITIALIZED", "WAIT_VERSION"} Events == {"CloseHandle", "Disconnect", "OpenDir", "OpenFile", "ReadDir", "ReadFile", "ReceiveAttrs", "ReceiveData", "ReceiveHandle", "ReceiveName", "ReceiveStatus", "ReceiveVersion", "Request", "SendInit", "WriteFile"} Origins == {"CONNECTION_CONTROL", "LOCAL_COMMAND", "PARSED_PACKET"} Effects == {"DELIVER_ATTRS", "DELIVER_DATA", "DELIVER_HANDLE", "DELIVER_NAME", "DELIVER_STATUS", "DISCONNECT_SFTP", "RECEIVE_VERSION", "SEND_CLOSE_HANDLE", "SEND_INIT", "SEND_OPEN_DIR", "SEND_OPEN_FILE", "SEND_READ", "SEND_READDIR", "SEND_REQUEST", "SEND_WRITE"} -HandleStates == {"Closed", "OpenDir", "OpenFile", "Unallocated"} +HandleStates == {"Closed", "OpenDir", "OpenFile", "PendingDir", "PendingFile", "Unallocated"} Init == /\ state = "UNINITIALIZED" @@ -30,6 +30,7 @@ Init == /\ previousPendingRequests = [r \in RequestIDs |-> "None"] /\ activeRequest = 0 /\ pendingRequests = [r \in RequestIDs |-> "None"] + /\ requestHandles = [r \in RequestIDs |-> 0] DISCONNECT_READY == /\ state = "READY" @@ -44,6 +45,7 @@ DISCONNECT_READY == /\ previousPendingRequests' = pendingRequests /\ activeRequest' = 0 /\ pendingRequests' = [r \in RequestIDs |-> "None"] + /\ requestHandles' = [r \in RequestIDs |-> 0] DISCONNECT_UNINITIALIZED == /\ state = "UNINITIALIZED" @@ -58,6 +60,7 @@ DISCONNECT_UNINITIALIZED == /\ previousPendingRequests' = pendingRequests /\ activeRequest' = 0 /\ pendingRequests' = [r \in RequestIDs |-> "None"] + /\ requestHandles' = [r \in RequestIDs |-> 0] DISCONNECT_WAIT_VERSION == /\ state = "WAIT_VERSION" @@ -72,6 +75,7 @@ DISCONNECT_WAIT_VERSION == /\ previousPendingRequests' = pendingRequests /\ activeRequest' = 0 /\ pendingRequests' = [r \in RequestIDs |-> "None"] + /\ requestHandles' = [r \in RequestIDs |-> 0] RECEIVE_VERSION_WAIT_VERSION == /\ state = "WAIT_VERSION" @@ -86,6 +90,7 @@ RECEIVE_VERSION_WAIT_VERSION == /\ previousPendingRequests' = pendingRequests /\ activeRequest' = 0 /\ pendingRequests' = pendingRequests + /\ requestHandles' = requestHandles SEND_INIT_UNINITIALIZED == /\ state = "UNINITIALIZED" @@ -100,6 +105,7 @@ SEND_INIT_UNINITIALIZED == /\ previousPendingRequests' = pendingRequests /\ activeRequest' = 0 /\ pendingRequests' = pendingRequests + /\ requestHandles' = requestHandles AllocateHandle == /\ state = "READY" @@ -110,10 +116,11 @@ AllocateHandle == /\ effects' = {"SEND_OPEN_FILE"} /\ previousHandles' = handles /\ activeHandle' \in HandleIDs - /\ handles' = [handles EXCEPT ![activeHandle'] = "OpenFile"] + /\ handles' = [handles EXCEPT ![activeHandle'] = "PendingFile"] /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingOpen"] + /\ requestHandles' = [requestHandles EXCEPT ![activeRequest'] = activeHandle'] /\ handles[activeHandle'] = "Unallocated" /\ pendingRequests[activeRequest'] = "None" @@ -126,10 +133,11 @@ AllocateDirHandle == /\ effects' = {"SEND_OPEN_DIR"} /\ previousHandles' = handles /\ activeHandle' \in HandleIDs - /\ handles' = [handles EXCEPT ![activeHandle'] = "OpenDir"] + /\ handles' = [handles EXCEPT ![activeHandle'] = "PendingDir"] /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingOpen"] + /\ requestHandles' = [requestHandles EXCEPT ![activeRequest'] = activeHandle'] /\ handles[activeHandle'] = "Unallocated" /\ pendingRequests[activeRequest'] = "None" @@ -146,6 +154,7 @@ ReadFileOp == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingRead"] + /\ requestHandles' = requestHandles /\ handles[activeHandle'] = "OpenFile" /\ pendingRequests[activeRequest'] = "None" @@ -162,6 +171,7 @@ WriteFileOp == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingWrite"] + /\ requestHandles' = requestHandles /\ handles[activeHandle'] = "OpenFile" /\ pendingRequests[activeRequest'] = "None" @@ -178,6 +188,7 @@ ReadDirOp == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingReadDir"] + /\ requestHandles' = requestHandles /\ handles[activeHandle'] = "OpenDir" /\ pendingRequests[activeRequest'] = "None" @@ -194,7 +205,8 @@ CloseHandleOp == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingClose"] - /\ handles[activeHandle'] \in {"OpenFile", "OpenDir"} + /\ requestHandles' = requestHandles + /\ handles[activeHandle'] \in {"PendingFile", "PendingDir", "OpenFile", "OpenDir"} /\ pendingRequests[activeRequest'] = "None" RequestOp == @@ -210,22 +222,27 @@ RequestOp == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingRequest"] + /\ requestHandles' = requestHandles /\ pendingRequests[activeRequest'] = "None" FulfillResponse == \/ /\ state = "READY" - /\ state' = "READY" - /\ previousState' = state - /\ event' = "ReceiveHandle" - /\ origin' = "PARSED_PACKET" - /\ effects' = {"DELIVER_HANDLE"} - /\ previousHandles' = handles - /\ activeHandle' = 0 - /\ handles' = handles - /\ previousPendingRequests' = pendingRequests - /\ activeRequest' \in RequestIDs - /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] - /\ pendingRequests[activeRequest'] # "None" + /\ \E r \in RequestIDs : + /\ pendingRequests[r] = "PendingOpen" + /\ requestHandles[r] # 0 + /\ handles[requestHandles[r]] \in {"PendingFile", "PendingDir"} + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReceiveHandle" + /\ origin' = "PARSED_PACKET" + /\ effects' = {"DELIVER_HANDLE"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = [handles EXCEPT ![requestHandles[r]] = IF handles[requestHandles[r]] = "PendingFile" THEN "OpenFile" ELSE "OpenDir"] + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' = r + /\ pendingRequests' = [pendingRequests EXCEPT ![r] = "None"] + /\ requestHandles' = [requestHandles EXCEPT ![r] = 0] \/ /\ state = "READY" /\ state' = "READY" /\ previousState' = state @@ -238,7 +255,8 @@ FulfillResponse == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] - /\ pendingRequests[activeRequest'] # "None" + /\ requestHandles' = requestHandles + /\ pendingRequests[activeRequest'] = "PendingRead" \/ /\ state = "READY" /\ state' = "READY" /\ previousState' = state @@ -251,7 +269,8 @@ FulfillResponse == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] - /\ pendingRequests[activeRequest'] # "None" + /\ requestHandles' = requestHandles + /\ pendingRequests[activeRequest'] = "PendingReadDir" \/ /\ state = "READY" /\ state' = "READY" /\ previousState' = state @@ -264,6 +283,7 @@ FulfillResponse == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] + /\ requestHandles' = requestHandles /\ pendingRequests[activeRequest'] # "None" \/ /\ state = "READY" /\ state' = "READY" @@ -277,7 +297,8 @@ FulfillResponse == /\ previousPendingRequests' = pendingRequests /\ activeRequest' \in RequestIDs /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] - /\ pendingRequests[activeRequest'] # "None" + /\ requestHandles' = requestHandles + /\ pendingRequests[activeRequest'] = "PendingRequest" Next == \/ DISCONNECT_READY From 45cd34e50babea94ed08e50ad8d5747e9fe98d84 Mon Sep 17 00:00:00 2001 From: Kenny Root Date: Thu, 23 Jul 2026 19:55:30 -0700 Subject: [PATCH 3/4] chore(tla+): bind Terrapin model to implementation --- .../sshlib/protocol/SshStateMachineTlaGenerator.kt | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt index 242e053..2ae8fea 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt @@ -185,6 +185,19 @@ class SshStateMachineFormalModelTest { assertTrue("StrictKex = FALSE" in nonStrictConfig) assertTrue("INVARIANT NoTerrapin" in strictConfig) assertTrue("INVARIANT NoTerrapin" in nonStrictConfig) + + // Bind SshTerrapin.tla abstractions to SshClientStateMachine formal model declarations + val transitions = createFormalModel().transitions.associateBy { it.meta.id } + val strictInit = transitions.getValue(SshTransitionId.RECEIVE_INITIAL_STRICT_KEX_INIT).meta + assertTrue(SshEffect.ENABLE_STRICT_KEX in strictInit.effects) + + // Sequence number reset on initial KEX completion (modeled in SshTerrapin.CompleteInitialKex) + val ecdhReply = transitions.getValue(SshTransitionId.RECEIVE_KEX_ECDH_REPLY).meta + assertTrue(SshEffect.RESET_OUTBOUND_SEQUENCE in ecdhReply.effects) + + // Unauthenticated packet injection abort under strict KEX (modeled in SshTerrapin.InjectUnauthenticatedIgnore) + val rejectNotFirst = transitions.getValue(SshTransitionId.REJECT_STRICT_KEX_INIT_NOT_FIRST).meta + assertTrue(SshEffect.DISCONNECT in rejectNotFirst.effects) } @Test From ea346a013f43067988d680bcc48e7c4a4ccfa6b7 Mon Sep 17 00:00:00 2001 From: Kenny Root Date: Thu, 23 Jul 2026 20:00:02 -0700 Subject: [PATCH 4/4] fix(channels): unregister channels when closed --- sshlib/api.txt | 5 +++ .../kotlin/org/connectbot/sshlib/SshClient.kt | 1 + .../org/connectbot/sshlib/SshClientConfig.kt | 9 ++++- .../connectbot/sshlib/client/AgentChannel.kt | 8 +++- .../sshlib/client/ForwardingChannel.kt | 15 +++++-- .../sshlib/client/SessionChannel.kt | 17 ++++++-- .../connectbot/sshlib/client/SshConnection.kt | 39 +++++++++---------- .../sshlib/protocol/SshChannelStateMachine.kt | 10 ++++- .../sshlib/client/SshClientIntegrationTest.kt | 6 +++ .../sshlib/client/SshConnectionFlowTest.kt | 1 + .../protocol/SshChannelStateMachineTest.kt | 2 +- .../tla/SshClientStateMachineGenerated.tla | 22 ++++++++--- 12 files changed, 99 insertions(+), 36 deletions(-) diff --git a/sshlib/api.txt b/sshlib/api.txt index 905488b..fd179a2 100644 --- a/sshlib/api.txt +++ b/sshlib/api.txt @@ -612,6 +612,7 @@ package org.connectbot.sshlib { } public final class SshClientConfig { + method @InaccessibleFromKotlin public boolean getAutoDisconnectOnLastChannelClose(); method @InaccessibleFromKotlin public java.lang.String getClientVersion(); method @InaccessibleFromKotlin public java.lang.String getEncryptionAlgorithms(); method @InaccessibleFromKotlin public java.lang.String getHostKeyAlgorithms(); @@ -623,6 +624,7 @@ package org.connectbot.sshlib { method @InaccessibleFromKotlin public long getRekeyBytesLimit(); method @InaccessibleFromKotlin public long getRekeyIntervalMs(); method @InaccessibleFromKotlin public org.connectbot.sshlib.transport.TransportFactory getTransportFactory(); + property public boolean autoDisconnectOnLastChannelClose; property public String clientVersion; property public String encryptionAlgorithms; property public String hostKeyAlgorithms; @@ -640,6 +642,7 @@ package org.connectbot.sshlib { public static final class SshClientConfig.Builder { ctor public SshClientConfig.Builder(); method public org.connectbot.sshlib.SshClientConfig build(); + method @InaccessibleFromKotlin public boolean getAutoDisconnectOnLastChannelClose(); method @InaccessibleFromKotlin public java.lang.String getClientVersion(); method @InaccessibleFromKotlin public boolean getEnableCompression(); method @InaccessibleFromKotlin public java.lang.String getEncryptionAlgorithms(); @@ -655,6 +658,7 @@ package org.connectbot.sshlib { method @InaccessibleFromKotlin public long getRekeyBytesLimit(); method @InaccessibleFromKotlin public long getRekeyIntervalMs(); method @InaccessibleFromKotlin public org.connectbot.sshlib.transport.TransportFactory? getTransportFactory(); + method @InaccessibleFromKotlin public void setAutoDisconnectOnLastChannelClose(boolean); method @InaccessibleFromKotlin public void setClientVersion(java.lang.String); method @InaccessibleFromKotlin public void setEnableCompression(boolean); method @InaccessibleFromKotlin public void setEncryptionAlgorithms(java.lang.String); @@ -670,6 +674,7 @@ package org.connectbot.sshlib { method @InaccessibleFromKotlin public void setRekeyBytesLimit(long); method @InaccessibleFromKotlin public void setRekeyIntervalMs(long); method @InaccessibleFromKotlin public void setTransportFactory(org.connectbot.sshlib.transport.TransportFactory?); + property public boolean autoDisconnectOnLastChannelClose; property public String clientVersion; property public boolean enableCompression; property public String encryptionAlgorithms; diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/SshClient.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/SshClient.kt index 7353d9e..f8dfafc 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/SshClient.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/SshClient.kt @@ -184,6 +184,7 @@ class SshClient private constructor( rekeyBytesLimit = config.rekeyBytesLimit, obscureKeystrokeTimingIntervalMs = config.obscureKeystrokeTimingIntervalMs, ) + sshConnection.autoDisconnectOnLastChannelClose = config.autoDisconnectOnLastChannelClose val result = sshConnection.connect() if (result is ConnectResult.Success) { diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/SshClientConfig.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/SshClientConfig.kt index b8e9994..d82a3e2 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/SshClientConfig.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/SshClientConfig.kt @@ -1,6 +1,6 @@ /* * ConnectBot SSH Library - * Copyright 2025 Kenny Root + * Copyright 2025-2026 Kenny Root * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. @@ -58,6 +58,7 @@ class SshClientConfig private constructor( val rekeyIntervalMs: Long, val rekeyBytesLimit: Long, val obscureKeystrokeTimingIntervalMs: Long, + val autoDisconnectOnLastChannelClose: Boolean, ) { class Builder { /** @@ -128,6 +129,11 @@ class SshClientConfig private constructor( */ var obscureKeystrokeTimingIntervalMs: Long = 20L + /** + * Whether to automatically disconnect the SSH connection when the last channel is closed. + */ + var autoDisconnectOnLastChannelClose: Boolean = true + fun build(): SshClientConfig { val factory = transportFactory ?: run { require(host.isNotBlank()) { "Host must be specified when using default TCP transport" } @@ -159,6 +165,7 @@ class SshClientConfig private constructor( rekeyIntervalMs, rekeyBytesLimit, obscureKeystrokeTimingIntervalMs, + autoDisconnectOnLastChannelClose, ) } } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/AgentChannel.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/AgentChannel.kt index c232ea5..6491125 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/AgentChannel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/AgentChannel.kt @@ -104,14 +104,20 @@ internal class AgentChannel( requests.close() requestWorker.cancelAndJoin() windowAvailable.close() + if (SshChannelEffect.CLOSE_CHANNEL in transition.effects) { + connection.notifyChannelClosed(localChannelNumber) + } } } suspend fun onDisconnected() { - lifecycle.disconnect { + lifecycle.disconnect { transition -> requests.close() requestWorker.cancelAndJoin() windowAvailable.close() + if (SshChannelEffect.CLOSE_CHANNEL in transition.effects) { + connection.notifyChannelClosed(localChannelNumber) + } } } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/ForwardingChannel.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/ForwardingChannel.kt index 10895ad..c359e78 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/ForwardingChannel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/ForwardingChannel.kt @@ -111,18 +111,24 @@ internal class ForwardingChannel( incomingDeliveryJob.cancel() _incomingData.close() windowAvailable.close() + if (SshChannelEffect.CLOSE_CHANNEL in transition.effects) { + connection.notifyChannelClosed(localChannelNumber) + } } ) { - throw SshException("Received duplicate CLOSE on forwarding channel $localChannelNumber") + logger.debug("Received duplicate CLOSE on forwarding channel $localChannelNumber") } } internal suspend fun onDisconnected() { - lifecycle.disconnect { + lifecycle.disconnect { transition -> incomingIngress.close() incomingDeliveryJob.cancel() _incomingData.close() windowAvailable.close() + if (SshChannelEffect.CLOSE_CHANNEL in transition.effects) { + connection.notifyChannelClosed(localChannelNumber) + } } } @@ -152,11 +158,14 @@ internal class ForwardingChannel( } suspend fun close() { - lifecycle.sendClose { + lifecycle.sendClose { transition -> incomingIngress.close() incomingDeliveryJob.cancel() _incomingData.close() connection.sendChannelClose(remoteChannelNumber) + if (SshChannelEffect.CLOSE_CHANNEL in transition.effects) { + connection.notifyChannelClosed(localChannelNumber) + } } } } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SessionChannel.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SessionChannel.kt index bdd01cf..40ba22d 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SessionChannel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SessionChannel.kt @@ -183,9 +183,12 @@ class SessionChannel internal constructor( internal suspend fun onClose() { if (!lifecycle.receiveClose { transition -> closeResources(SshChannelEffect.SEND_CLOSE in transition.effects, "Received CLOSE") + if (SshChannelEffect.CLOSE_CHANNEL in transition.effects) { + connection.notifyChannelClosed(localChannelNumber) + } } ) { - throw org.connectbot.sshlib.SshException("Received duplicate CLOSE on channel $localChannelNumber") + logger.debug("Received duplicate CLOSE on channel $localChannelNumber") } } @@ -218,7 +221,12 @@ class SessionChannel internal constructor( } internal suspend fun onDisconnected() { - lifecycle.disconnect { closeResources(replyRequired = false, reason = "Disconnected") } + lifecycle.disconnect { transition -> + closeResources(replyRequired = false, reason = "Disconnected") + if (SshChannelEffect.CLOSE_CHANNEL in transition.effects) { + connection.notifyChannelClosed(localChannelNumber) + } + } } internal suspend fun receiveRequest(action: suspend () -> Unit): Boolean = lifecycle.receiveRequest { action() } @@ -449,7 +457,7 @@ class SessionChannel internal constructor( override fun close() { connectionScope.launch(start = CoroutineStart.UNDISPATCHED) { - lifecycle.sendClose { + lifecycle.sendClose { transition -> logger.debug("Closing channel $localChannelNumber") obfuscatorMutex.withLock { obfuscator?.stop() } chaffJob?.cancel() @@ -468,6 +476,9 @@ class SessionChannel internal constructor( } catch (e: Exception) { logger.debug("Failed to send CHANNEL_CLOSE", e) } + if (SshChannelEffect.CLOSE_CHANNEL in transition.effects) { + connection.notifyChannelClosed(localChannelNumber) + } } } } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt index 20a3a96..61c3ec3 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt @@ -255,6 +255,7 @@ class SshConnection( private val obscureKeystrokeTimingIntervalMs: Long = 20L, coroutineDispatcher: CoroutineDispatcher = Dispatchers.IO, ) { + internal var autoDisconnectOnLastChannelClose: Boolean = true companion object { private val logger = LoggerFactory.getLogger(SshConnection::class.java) @@ -2560,24 +2561,11 @@ class SshConnection( val recipientChannel = msg.recipientChannel().toInt() logger.debug("Received CHANNEL_CLOSE for local channel $recipientChannel") when (val entry = channelRegistry.findByLocalRecipient(recipientChannel)) { - is SshChannelRegistry.Entry.Established.Session -> { - entry.channel.onClose() - channelRegistry.unregister(recipientChannel) - } - - is SshChannelRegistry.Entry.Established.Agent -> { - entry.channel.onClose() - channelRegistry.unregister(recipientChannel) - } - - is SshChannelRegistry.Entry.Established.Forwarding -> { - entry.channel.onClose() - unregisterForwardingChannel(entry.channel) - } - + is SshChannelRegistry.Entry.Established.Session -> entry.channel.onClose() + is SshChannelRegistry.Entry.Established.Agent -> entry.channel.onClose() + is SshChannelRegistry.Entry.Established.Forwarding -> entry.channel.onClose() null -> throw ProtocolViolationException("Close for unknown channel $recipientChannel") } - checkAllChannelsClosed() } SshEnums.MessageType.SSH_MSG_CHANNEL_REQUEST -> { @@ -2887,11 +2875,20 @@ class SshConnection( ) } - private suspend fun checkAllChannelsClosed() { - val established = channelRegistry.establishedSnapshot() - val allClosed = established.all { !it.isOpen } - logger.debug("checkAllChannelsClosed: established=${established.size}, allClosed=$allClosed") - if (allClosed && established.any { it.kind == SshChannelRegistry.Kind.SESSION }) { + internal suspend fun notifyChannelClosed(localChannelNumber: Int) { + val entry = channelRegistry.findByLocalRecipient(localChannelNumber) + val wasSession = entry is SshChannelRegistry.Entry.Established.Session + channelRegistry.unregister(localChannelNumber) + if (entry is SshChannelRegistry.Entry.Established.Forwarding) { + unregisterForwardingChannel(entry.channel) + } + + val snapshot = channelRegistry.snapshot() + val allClosed = snapshot.none { it is SshChannelRegistry.Entry.Pending } && + snapshot.filterIsInstance().all { !it.isOpen } + val hasSession = snapshot.any { it.kind == SshChannelRegistry.Kind.SESSION } + + if (autoDisconnectOnLastChannelClose && allClosed && (hasSession || wasSession)) { logger.info("All channels closed, sending disconnect") sendDisconnect() } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachine.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachine.kt index 0acf536..7fa0d42 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachine.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachine.kt @@ -136,6 +136,10 @@ internal enum class SshChannelTransitionId { RECEIVE_CLOSE_REMOTE_EOF, RECEIVE_CLOSE_BOTH_EOF, RECEIVE_CLOSE_CLOSE_SENT, + RECEIVE_DATA_CLOSE_SENT, + RECEIVE_REQUEST_CLOSE_SENT, + RECEIVE_WINDOW_ADJUST_CLOSE_SENT, + RECEIVE_EOF_CLOSE_SENT, DISCONNECT_OPENING, DISCONNECT_OPEN, DISCONNECT_LOCAL_EOF, @@ -304,7 +308,7 @@ internal class SshChannelStateMachine( class SendClose(action: suspend (SshChannelAcceptedTransition) -> Unit) : ChannelEvent( SshChannelEventId.SEND_CLOSE, - setOf(SshChannelEffect.SEND_CLOSE, SshChannelEffect.CLOSE_CHANNEL), + setOf(SshChannelEffect.SEND_CLOSE), SshChannelEventOrigin.LOCAL_COMMAND, action, ) @@ -393,6 +397,10 @@ internal class SshChannelStateMachine( localEof.channelTransition(ChannelEvent.ReceiveClose {}, SshChannelTransitionId.RECEIVE_CLOSE_LOCAL_EOF, closed) remoteEof.channelTransition(ChannelEvent.ReceiveClose {}, SshChannelTransitionId.RECEIVE_CLOSE_REMOTE_EOF, closed) bothEof.channelTransition(ChannelEvent.ReceiveClose {}, SshChannelTransitionId.RECEIVE_CLOSE_BOTH_EOF, closed) + closeSent.channelTransition(ChannelEvent.ReceiveData {}, SshChannelTransitionId.RECEIVE_DATA_CLOSE_SENT, effects = emptySet()) + closeSent.channelTransition(ChannelEvent.ReceiveRequest {}, SshChannelTransitionId.RECEIVE_REQUEST_CLOSE_SENT, effects = emptySet()) + closeSent.channelTransition(ChannelEvent.ReceiveWindowAdjust {}, SshChannelTransitionId.RECEIVE_WINDOW_ADJUST_CLOSE_SENT, effects = emptySet()) + closeSent.channelTransition(ChannelEvent.ReceiveEof {}, SshChannelTransitionId.RECEIVE_EOF_CLOSE_SENT, effects = emptySet()) closeSent.channelTransition( ChannelEvent.ReceiveClose {}, SshChannelTransitionId.RECEIVE_CLOSE_CLOSE_SENT, diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshClientIntegrationTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshClientIntegrationTest.kt index 5c9b2b7..418796f 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshClientIntegrationTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshClientIntegrationTest.kt @@ -1452,6 +1452,7 @@ class SshClientIntegrationTest { this.host = host this.port = port this.hostKeyVerifier = acceptAllVerifier + this.autoDisconnectOnLastChannelClose = false }, ) @@ -1468,6 +1469,11 @@ class SshClientIntegrationTest { val execGranted = withTimeout(10_000) { session!!.requestExec("true") } assertTrue(execGranted, "requestExec failed on attempt $attempt") session!!.close() + withTimeout(5_000) { + while (session.isOpen) { + yield() + } + } assertFalse(session.isOpen, "session should be closed on attempt $attempt") } } finally { diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt index 7d9c18e..4fc0e63 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt @@ -530,6 +530,7 @@ class SshConnectionFlowTest { @Test fun `opening a second session channel after closing the first succeeds when server reuses remote channel number`() = runTest { connectedFixture { connection, server, dispatcher -> + connection.autoDisconnectOnLastChannelClose = false authenticate(connection, server, dispatcher) val session1 = openSession(connection, server, dispatcher, remoteChannelNumber = 100) diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachineTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachineTest.kt index d688295..21bfa81 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachineTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachineTest.kt @@ -171,7 +171,7 @@ class SshChannelStateMachineTest { assertEquals(SshChannelState.CLOSE_SENT, machine.state) assertFalse(machine.isOpen) assertFalse(machine.sendData {}) - assertFalse(machine.receiveData {}) + assertTrue(machine.receiveData {}) assertFalse(machine.sendEof {}) assertTrue(machine.receiveClose {}) assertEquals(SshChannelState.CLOSED, machine.state) diff --git a/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla b/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla index 5aa5ea9..2336016 100644 --- a/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla +++ b/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla @@ -1,6 +1,6 @@ ---- MODULE SshClientStateMachineGenerated ---- \* Generated from SshClientStateMachine. Do not edit. -\* Model SHA-256: 51a83d84a0f081b32e4dfcf4d185ef2c83fec2c9a640b385db78f35607733b78 +\* Model SHA-256: 04f78793763d07d60314395341b04de0a29ebc5a024845d80d27599ad75f0214 \* Lifecycle states: 11; transitions: 43. \* TLC distinct states count full variable valuations, not lifecycle nodes. EXTENDS Naturals @@ -35,6 +35,10 @@ ChannelTransitions == { <<"BOTH_EOF", "SendClose", "CLOSE_SENT">>, <<"BOTH_EOF", "SendRequest", "BOTH_EOF">>, <<"CLOSE_SENT", "ReceiveClose", "CLOSED">>, + <<"CLOSE_SENT", "ReceiveData", "CLOSE_SENT">>, + <<"CLOSE_SENT", "ReceiveEof", "CLOSE_SENT">>, + <<"CLOSE_SENT", "ReceiveRequest", "CLOSE_SENT">>, + <<"CLOSE_SENT", "ReceiveWindowAdjust", "CLOSE_SENT">>, <<"LOCAL_EOF", "ReceiveClose", "CLOSED">>, <<"LOCAL_EOF", "ReceiveData", "LOCAL_EOF">>, <<"LOCAL_EOF", "ReceiveEof", "BOTH_EOF">>, @@ -70,6 +74,10 @@ ChannelAuthenticationRequired == { <<"BOTH_EOF", "SendClose">>, <<"BOTH_EOF", "SendRequest">>, <<"CLOSE_SENT", "ReceiveClose">>, + <<"CLOSE_SENT", "ReceiveData">>, + <<"CLOSE_SENT", "ReceiveEof">>, + <<"CLOSE_SENT", "ReceiveRequest">>, + <<"CLOSE_SENT", "ReceiveWindowAdjust">>, <<"LOCAL_EOF", "ReceiveClose">>, <<"LOCAL_EOF", "ReceiveData">>, <<"LOCAL_EOF", "ReceiveEof">>, @@ -109,22 +117,26 @@ ChannelEffectsFor(channelState, operation) == CASE /\ channelState = "BOTH_EOF" /\ operation = "ReceiveClose" -> {"SEND_CLOSE", "CLOSE_CHANNEL"} [] /\ channelState = "BOTH_EOF" /\ operation = "ReceiveRequest" -> {"DELIVER_REQUEST"} [] /\ channelState = "BOTH_EOF" /\ operation = "ReceiveWindowAdjust" -> {"ADJUST_WINDOW"} - [] /\ channelState = "BOTH_EOF" /\ operation = "SendClose" -> {"SEND_CLOSE", "CLOSE_CHANNEL"} + [] /\ channelState = "BOTH_EOF" /\ operation = "SendClose" -> {"SEND_CLOSE"} [] /\ channelState = "BOTH_EOF" /\ operation = "SendRequest" -> {"SEND_REQUEST"} [] /\ channelState = "CLOSE_SENT" /\ operation = "ReceiveClose" -> {"CLOSE_CHANNEL"} + [] /\ channelState = "CLOSE_SENT" /\ operation = "ReceiveData" -> {} + [] /\ channelState = "CLOSE_SENT" /\ operation = "ReceiveEof" -> {} + [] /\ channelState = "CLOSE_SENT" /\ operation = "ReceiveRequest" -> {} + [] /\ channelState = "CLOSE_SENT" /\ operation = "ReceiveWindowAdjust" -> {} [] /\ channelState = "LOCAL_EOF" /\ operation = "ReceiveClose" -> {"SEND_CLOSE", "CLOSE_CHANNEL"} [] /\ channelState = "LOCAL_EOF" /\ operation = "ReceiveData" -> {"DELIVER_DATA"} [] /\ channelState = "LOCAL_EOF" /\ operation = "ReceiveEof" -> {"CLOSE_INBOUND_STREAMS"} [] /\ channelState = "LOCAL_EOF" /\ operation = "ReceiveRequest" -> {"DELIVER_REQUEST"} [] /\ channelState = "LOCAL_EOF" /\ operation = "ReceiveWindowAdjust" -> {"ADJUST_WINDOW"} - [] /\ channelState = "LOCAL_EOF" /\ operation = "SendClose" -> {"SEND_CLOSE", "CLOSE_CHANNEL"} + [] /\ channelState = "LOCAL_EOF" /\ operation = "SendClose" -> {"SEND_CLOSE"} [] /\ channelState = "LOCAL_EOF" /\ operation = "SendRequest" -> {"SEND_REQUEST"} [] /\ channelState = "OPEN" /\ operation = "ReceiveClose" -> {"SEND_CLOSE", "CLOSE_CHANNEL"} [] /\ channelState = "OPEN" /\ operation = "ReceiveData" -> {"DELIVER_DATA"} [] /\ channelState = "OPEN" /\ operation = "ReceiveEof" -> {"CLOSE_INBOUND_STREAMS"} [] /\ channelState = "OPEN" /\ operation = "ReceiveRequest" -> {"DELIVER_REQUEST"} [] /\ channelState = "OPEN" /\ operation = "ReceiveWindowAdjust" -> {"ADJUST_WINDOW"} - [] /\ channelState = "OPEN" /\ operation = "SendClose" -> {"SEND_CLOSE", "CLOSE_CHANNEL"} + [] /\ channelState = "OPEN" /\ operation = "SendClose" -> {"SEND_CLOSE"} [] /\ channelState = "OPEN" /\ operation = "SendData" -> {"SEND_DATA"} [] /\ channelState = "OPEN" /\ operation = "SendEof" -> {"SEND_EOF"} [] /\ channelState = "OPEN" /\ operation = "SendRequest" -> {"SEND_REQUEST"} @@ -133,7 +145,7 @@ ChannelEffectsFor(channelState, operation) == [] /\ channelState = "REMOTE_EOF" /\ operation = "ReceiveClose" -> {"SEND_CLOSE", "CLOSE_CHANNEL"} [] /\ channelState = "REMOTE_EOF" /\ operation = "ReceiveRequest" -> {"DELIVER_REQUEST"} [] /\ channelState = "REMOTE_EOF" /\ operation = "ReceiveWindowAdjust" -> {"ADJUST_WINDOW"} - [] /\ channelState = "REMOTE_EOF" /\ operation = "SendClose" -> {"SEND_CLOSE", "CLOSE_CHANNEL"} + [] /\ channelState = "REMOTE_EOF" /\ operation = "SendClose" -> {"SEND_CLOSE"} [] /\ channelState = "REMOTE_EOF" /\ operation = "SendData" -> {"SEND_DATA"} [] /\ channelState = "REMOTE_EOF" /\ operation = "SendEof" -> {"SEND_EOF"} [] /\ channelState = "REMOTE_EOF" /\ operation = "SendRequest" -> {"SEND_REQUEST"}