diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1b58b6f4..be26b915 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -65,6 +65,22 @@ jobs: dependency-graph: disabled validate-wrappers: true + - name: Download TLA+ tools + if: matrix.java == '17' + env: + TLA2TOOLS_SHA256: 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 + TLA2TOOLS_URL: https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar + run: | + tla2tools_jar="${RUNNER_TEMP}/tla2tools-1.7.4.jar" + curl --fail --location --proto '=https' --tlsv1.2 \ + --output "${tla2tools_jar}" "${TLA2TOOLS_URL}" + echo "${TLA2TOOLS_SHA256} ${tla2tools_jar}" | sha256sum --check + echo "TLA2TOOLS_JAR=${tla2tools_jar}" >> "${GITHUB_ENV}" + + - name: Check SSH lifecycle TLA+ model + if: matrix.java == '17' + run: ./gradlew :sshlib:checkSshStateMachineTla + - name: Configure Docker mirror run: | echo '{"registry-mirrors": ["https://mirror.gcr.io"]}' | sudo tee /etc/docker/daemon.json diff --git a/sshlib/build.gradle.kts b/sshlib/build.gradle.kts index 02e7205d..5c09d075 100644 --- a/sshlib/build.gradle.kts +++ b/sshlib/build.gradle.kts @@ -67,6 +67,45 @@ tasks.test { ) } +val tlaModelDirectory = layout.projectDirectory.dir("src/test/resources/tla") +val tlaStateDirectory = layout.buildDirectory.dir("tla/states") + +tasks.register("generateSshStateMachineTla") { + group = "verification" + description = "Regenerates the TLA+ lifecycle model from SshClientStateMachine" + dependsOn(tasks.testClasses) + classpath = sourceSets.test.get().runtimeClasspath + mainClass.set("org.connectbot.sshlib.protocol.SshStateMachineTlaGenerator") + args(tlaModelDirectory.file("SshClientStateMachineGenerated.tla").asFile.absolutePath) +} + +val tla2toolsJar = providers.gradleProperty("tla2toolsJar") + .orElse(providers.environmentVariable("TLA2TOOLS_JAR")) + +tasks.register("checkSshStateMachineTla") { + group = "verification" + description = "Checks the generated SSH lifecycle model with TLC" + mainClass.set("tlc2.TLC") + workingDir(tlaModelDirectory) + args( + "-workers", + "1", + "-metadir", + tlaStateDirectory.get().asFile.absolutePath, + "-config", + "SshClientStateMachine.cfg", + "SshClientStateMachine.tla", + ) + jvmArgs("-XX:+UseParallelGC") + doFirst { + val jarPath = tla2toolsJar.orNull + ?: throw GradleException( + "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", + ) + classpath = files(jarPath) + } +} + java { withSourcesJar() toolchain { 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 aa4fcbe3..c232ea5c 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/AgentChannel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/AgentChannel.kt @@ -22,14 +22,18 @@ import kotlinx.coroutines.Job import kotlinx.coroutines.cancelAndJoin import kotlinx.coroutines.channels.Channel import kotlinx.coroutines.launch +import org.connectbot.sshlib.SshException +import org.connectbot.sshlib.protocol.SshChannelEffect +import org.connectbot.sshlib.protocol.SshChannelState +import org.connectbot.sshlib.protocol.SshChannelStateMachine import org.slf4j.LoggerFactory internal class AgentChannel( private val handler: AgentProtocolHandler, private val connection: SshConnection, scope: CoroutineScope, - private val localChannelNumber: Int, - private var remoteChannelNumber: Int, + internal val localChannelNumber: Int, + internal val remoteChannelNumber: Int, private val maxPacketSize: Int, remoteWindowSizeInitial: Long, initialWindowSize: Int = 64 * 1024, @@ -38,8 +42,7 @@ internal class AgentChannel( private val logger = LoggerFactory.getLogger(AgentChannel::class.java) } - private var _isOpen = true - private var closeSent = false + private val lifecycle = SshChannelStateMachine(SshChannelState.OPEN) private val window = LocalChannelWindow(initialWindowSize, remoteInitial = remoteWindowSizeInitial) private val windowAvailable = Channel(Channel.CONFLATED) @@ -54,50 +57,66 @@ internal class AgentChannel( } } - val isOpen: Boolean get() = _isOpen + val isOpen: Boolean get() = lifecycle.isOpen suspend fun handleData(data: ByteArray) { - if (!_isOpen) { + if (!lifecycle.receiveData { + window.consumeLocal(data.size) + logger.debug("Queueing ${data.size} bytes received on agent channel") + if (requests.trySend(data).isFailure) { + window.releaseLocal(data.size) + logger.warn("Discarding data received while agent channel is closing") + } + } + ) { logger.warn("Received data on closed agent channel") return } - window.consumeLocal(data.size) - - logger.debug("Queueing ${data.size} bytes received on agent channel") - if (requests.trySend(data).isFailure) { - window.releaseLocal(data.size) - logger.warn("Discarding data received while agent channel is closing") - } } - fun onWindowAdjust(bytesToAdd: Long) { - window.adjustRemote(bytesToAdd) - logger.debug("Agent channel window adjust +$bytesToAdd, remote window now ${window.remoteRemaining}") - if (window.remoteRemaining > 0) { - windowAvailable.trySend(Unit) + suspend fun onWindowAdjust(bytesToAdd: Long) { + if (!lifecycle.receiveWindowAdjust { + window.adjustRemote(bytesToAdd) + logger.debug("Agent channel window adjust +$bytesToAdd, remote window now ${window.remoteRemaining}") + if (window.remoteRemaining > 0) windowAvailable.trySend(Unit) + } + ) { + throw SshException("Received window adjustment after CLOSE on agent channel $localChannelNumber") } } - fun onEof() { - logger.debug("Agent channel received EOF") + suspend fun onEof() { + if (!lifecycle.receiveEof { logger.debug("Agent channel received EOF") }) { + throw SshException("Received duplicate EOF or EOF after CLOSE on agent channel $localChannelNumber") + } } suspend fun onClose() { - logger.debug("Agent channel closed") - if (!closeSent) { - closeSent = true - try { - connection.sendChannelClose(remoteChannelNumber) - } catch (e: Exception) { - logger.debug("Failed to send CHANNEL_CLOSE reply", e) + lifecycle.receiveClose { transition -> + logger.debug("Agent channel closed") + if (SshChannelEffect.SEND_CLOSE in transition.effects) { + try { + connection.sendChannelClose(remoteChannelNumber) + } catch (e: Exception) { + logger.debug("Failed to send CHANNEL_CLOSE reply", e) + } } + requests.close() + requestWorker.cancelAndJoin() + windowAvailable.close() } - _isOpen = false - requests.close() - requestWorker.cancelAndJoin() - windowAvailable.close() } + suspend fun onDisconnected() { + lifecycle.disconnect { + requests.close() + requestWorker.cancelAndJoin() + windowAvailable.close() + } + } + + suspend fun receiveRequest(action: suspend () -> Unit): Boolean = lifecycle.receiveRequest { action() } + private suspend fun sendData(data: ByteArray) { var offset = 0 while (offset < data.size) { @@ -106,8 +125,13 @@ internal class AgentChannel( } val chunkSize = window.sendChunkSize(data.size - offset, maxPacketSize) val chunk = data.copyOfRange(offset, offset + chunkSize) - connection.sendChannelData(remoteChannelNumber, chunk) - window.consumeRemote(chunkSize) + if (!lifecycle.sendData { + connection.sendChannelData(remoteChannelNumber, chunk) + window.consumeRemote(chunkSize) + } + ) { + throw SshException("Cannot send data after EOF or CLOSE on agent channel $localChannelNumber") + } offset += chunkSize } } 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 15d0112d..10895add 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/ForwardingChannel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/ForwardingChannel.kt @@ -21,6 +21,10 @@ import kotlinx.coroutines.CoroutineScope import kotlinx.coroutines.channels.Channel import kotlinx.coroutines.channels.ReceiveChannel import kotlinx.coroutines.launch +import org.connectbot.sshlib.SshException +import org.connectbot.sshlib.protocol.SshChannelEffect +import org.connectbot.sshlib.protocol.SshChannelState +import org.connectbot.sshlib.protocol.SshChannelStateMachine import org.slf4j.LoggerFactory internal class ForwardingChannel( @@ -31,13 +35,12 @@ internal class ForwardingChannel( private val maxPacketSize: Int, remoteWindowSizeInitial: Long, private val initialWindowSize: Int = 256 * 1024, + private val lifecycle: SshChannelStateMachine = SshChannelStateMachine(SshChannelState.OPEN), ) { companion object { private val logger = LoggerFactory.getLogger(ForwardingChannel::class.java) } - private var _isOpen = true - private var closeSent = false private val window = LocalChannelWindow( initialWindowSize, remoteInitial = remoteWindowSizeInitial, @@ -59,45 +62,72 @@ internal class ForwardingChannel( } } - val isOpen: Boolean get() = _isOpen + val isOpen: Boolean get() = lifecycle.isOpen internal suspend fun onData(data: ByteArray) { - window.consumeLocal(data.size) - if (incomingIngress.trySend(data).isFailure) { - throw org.connectbot.sshlib.SshException("Received data for a closed forwarding stream") + if (!lifecycle.receiveData { + window.consumeLocal(data.size) + if (incomingIngress.trySend(data).isFailure) { + throw org.connectbot.sshlib.SshException("Received data for a closed forwarding stream") + } + } + ) { + throw SshException("Received data after EOF or CLOSE on forwarding channel $localChannelNumber") } } - internal fun onWindowAdjust(bytesToAdd: Long) { - window.adjustRemote(bytesToAdd) - logger.debug("Forwarding channel window adjust +$bytesToAdd, remote window now ${window.remoteRemaining}") - if (window.remoteRemaining > 0) { - windowAvailable.trySend(Unit) + internal suspend fun onWindowAdjust(bytesToAdd: Long) { + if (!lifecycle.receiveWindowAdjust { + window.adjustRemote(bytesToAdd) + logger.debug("Forwarding channel window adjust +$bytesToAdd, remote window now ${window.remoteRemaining}") + if (window.remoteRemaining > 0) windowAvailable.trySend(Unit) + } + ) { + throw SshException("Received window adjustment after CLOSE on forwarding channel $localChannelNumber") } } - internal fun onEof() { - logger.debug("Forwarding channel $localChannelNumber received EOF") - incomingIngress.close() + internal suspend fun onEof() { + if (!lifecycle.receiveEof { + logger.debug("Forwarding channel $localChannelNumber received EOF") + incomingIngress.close() + } + ) { + throw SshException("Received duplicate EOF or EOF after CLOSE on forwarding channel $localChannelNumber") + } } internal suspend fun onClose() { - logger.debug("Forwarding channel $localChannelNumber closed") - if (!closeSent) { - closeSent = true - try { - connection.sendChannelClose(remoteChannelNumber) - } catch (e: Exception) { - logger.debug("Failed to send CHANNEL_CLOSE reply", e) + if (!lifecycle.receiveClose { transition -> + logger.debug("Forwarding channel $localChannelNumber closed") + if (SshChannelEffect.SEND_CLOSE in transition.effects) { + try { + connection.sendChannelClose(remoteChannelNumber) + } catch (e: Exception) { + logger.debug("Failed to send CHANNEL_CLOSE reply", e) + } + } + incomingIngress.close() + incomingDeliveryJob.cancel() + _incomingData.close() + windowAvailable.close() } + ) { + throw SshException("Received duplicate CLOSE on forwarding channel $localChannelNumber") + } + } + + internal suspend fun onDisconnected() { + lifecycle.disconnect { + incomingIngress.close() + incomingDeliveryJob.cancel() + _incomingData.close() + windowAvailable.close() } - _isOpen = false - incomingIngress.close() - incomingDeliveryJob.cancel() - _incomingData.close() - windowAvailable.close() } + internal suspend fun receiveRequest(action: suspend () -> Unit): Boolean = lifecycle.receiveRequest { action() } + suspend fun sendData(data: ByteArray) { var offset = 0 while (offset < data.size) { @@ -106,23 +136,27 @@ internal class ForwardingChannel( } val chunkSize = window.sendChunkSize(data.size - offset, maxPacketSize) val chunk = data.copyOfRange(offset, offset + chunkSize) - connection.sendChannelData(remoteChannelNumber, chunk) - window.consumeRemote(chunkSize) + if (!lifecycle.sendData { + connection.sendChannelData(remoteChannelNumber, chunk) + window.consumeRemote(chunkSize) + } + ) { + throw SshException("Cannot send data after EOF or CLOSE on forwarding channel $localChannelNumber") + } offset += chunkSize } } suspend fun sendEof() { - connection.sendChannelEof(remoteChannelNumber) + lifecycle.sendEof { connection.sendChannelEof(remoteChannelNumber) } } suspend fun close() { - if (!_isOpen) return - closeSent = true - _isOpen = false - incomingIngress.close() - incomingDeliveryJob.cancel() - _incomingData.close() - connection.sendChannelClose(remoteChannelNumber) + lifecycle.sendClose { + incomingIngress.close() + incomingDeliveryJob.cancel() + _incomingData.close() + connection.sendChannelClose(remoteChannelNumber) + } } } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/RemotePortForwarder.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/RemotePortForwarder.kt index bbef815d..a911b2f3 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/RemotePortForwarder.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/RemotePortForwarder.kt @@ -86,6 +86,8 @@ internal class RemotePortForwarder( ) { logger.debug("Incoming forwarded-tcpip from $originAddr:$originPort, connecting to $localHost:$localPort") + var registeredChannel: ForwardingChannel? = null + var confirmationSent = false try { val localChannelNumber = connection.allocateChannelNumber() @@ -102,6 +104,7 @@ internal class RemotePortForwarder( initialWindowSize = 256 * 1024, ) connection.registerForwardingChannel(fwdChannel) + registeredChannel = fwdChannel connection.sendChannelOpenConfirmationPublic( recipientChannel = senderChannel, @@ -109,6 +112,7 @@ internal class RemotePortForwarder( initialWindowSize = 256 * 1024, maximumPacketSize = 32 * 1024, ) + confirmationSent = true val readChannel = socket.openReadChannel() val writeChannel = socket.openWriteChannel(autoFlush = false) @@ -117,13 +121,19 @@ internal class RemotePortForwarder( synchronized(dataForwarders) { dataForwarders.add(forwarder) } forwarder.start() } catch (e: Exception) { + registeredChannel?.let { channel -> + connection.unregisterForwardingChannel(channel) + if (confirmationSent) channel.close() else channel.onDisconnected() + } logger.warn("Failed to handle incoming forwarded-tcpip: ${e.message}") - connection.sendChannelOpenFailurePublic( - recipientChannel = senderChannel, - reasonCode = 2, // SSH_OPEN_CONNECT_FAILED - description = "Failed to connect to local target: ${e.message}", - languageTag = "", - ) + if (!confirmationSent) { + connection.sendChannelOpenFailurePublic( + recipientChannel = senderChannel, + reasonCode = 2, // SSH_OPEN_CONNECT_FAILED + description = "Failed to connect to local target: ${e.message}", + languageTag = "", + ) + } } } 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 1b0ec3de..581bbdbb 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SessionChannel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SessionChannel.kt @@ -17,7 +17,9 @@ package org.connectbot.sshlib.client +import kotlinx.coroutines.CompletableDeferred import kotlinx.coroutines.CoroutineScope +import kotlinx.coroutines.CoroutineStart import kotlinx.coroutines.Job import kotlinx.coroutines.channels.Channel import kotlinx.coroutines.channels.ReceiveChannel @@ -32,6 +34,9 @@ import org.connectbot.sshlib.protocol.ChannelRequestPtyReq import org.connectbot.sshlib.protocol.ChannelRequestShell import org.connectbot.sshlib.protocol.ChannelRequestSubsystem import org.connectbot.sshlib.protocol.ChannelRequestWindowChange +import org.connectbot.sshlib.protocol.SshChannelEffect +import org.connectbot.sshlib.protocol.SshChannelState +import org.connectbot.sshlib.protocol.SshChannelStateMachine import org.slf4j.LoggerFactory import java.util.concurrent.atomic.AtomicInteger import kotlin.random.Random @@ -48,13 +53,12 @@ class SessionChannel internal constructor( private val obscureKeystrokeTimingIntervalMs: Long = 20L, private val obfuscatorClockMs: () -> Long = { System.nanoTime() / 1_000_000L }, private val obfuscatorRandom: Random = Random.Default, + private val lifecycle: SshChannelStateMachine = SshChannelStateMachine(SshChannelState.OPEN), ) : SshSession { companion object { private val logger = LoggerFactory.getLogger(SessionChannel::class.java) } - private var _isOpen = true - private var closeSent = false private val window = LocalChannelWindow(initialWindowSize, remoteInitial = remoteWindowSizeInitial) private val windowAvailable = Channel(Channel.CONFLATED) @@ -75,7 +79,7 @@ class SessionChannel internal constructor( deliverData(extendedDataIngress, _extendedData) { it.second.size } } - override val isOpen: Boolean get() = _isOpen + override val isOpen: Boolean get() = lifecycle.isOpen override val remoteChannelNumber: Int get() = _remoteChannelNumber override val stdout: ReceiveChannel get() = _stdout override val stderr: ReceiveChannel get() = _stderr @@ -96,20 +100,30 @@ class SessionChannel internal constructor( get() = ptyGranted && canSendChaff && obscureKeystrokeTimingIntervalMs > 0 internal suspend fun onData(data: ByteArray) { - window.consumeLocal(data.size) - if (stdoutIngress.trySend(data).isFailure) { - throw org.connectbot.sshlib.SshException("Received data for a closed stdout stream") + if (!lifecycle.receiveData { + window.consumeLocal(data.size) + if (stdoutIngress.trySend(data).isFailure) { + throw org.connectbot.sshlib.SshException("Received data for a closed stdout stream") + } + } + ) { + throw org.connectbot.sshlib.SshException("Received data after EOF or CLOSE on channel $localChannelNumber") } } internal suspend fun onExtendedData(dataType: Int, data: ByteArray) { - window.consumeLocal(data.size) - if (dataType == 1) { - if (stderrIngress.trySend(data).isFailure) { - throw org.connectbot.sshlib.SshException("Received data for a closed stderr stream") + if (!lifecycle.receiveData { + window.consumeLocal(data.size) + if (dataType == 1) { + if (stderrIngress.trySend(data).isFailure) { + throw org.connectbot.sshlib.SshException("Received data for a closed stderr stream") + } + } else if (extendedDataIngress.trySend(dataType to data).isFailure) { + throw org.connectbot.sshlib.SshException("Received data for a closed extended-data stream") + } } - } else if (extendedDataIngress.trySend(dataType to data).isFailure) { - throw org.connectbot.sshlib.SshException("Received data for a closed extended-data stream") + ) { + throw org.connectbot.sshlib.SshException("Received extended data after EOF or CLOSE on channel $localChannelNumber") } } @@ -129,36 +143,51 @@ class SessionChannel internal constructor( } } - internal fun onWindowAdjust(bytesToAdd: Long) { - window.adjustRemote(bytesToAdd) - logger.debug("Window adjust +$bytesToAdd, remote window now ${window.remoteRemaining}") - if (window.remoteRemaining > 0) { - windowAvailable.trySend(Unit) + internal suspend fun onWindowAdjust(bytesToAdd: Long) { + if (!lifecycle.receiveWindowAdjust { + window.adjustRemote(bytesToAdd) + logger.debug("Window adjust +$bytesToAdd, remote window now ${window.remoteRemaining}") + if (window.remoteRemaining > 0) windowAvailable.trySend(Unit) + } + ) { + throw org.connectbot.sshlib.SshException("Received window adjustment after CLOSE on channel $localChannelNumber") } } - internal fun onEof() { - logger.debug("Received EOF on channel $localChannelNumber") - stdoutIngress.close() - stderrIngress.close() - extendedDataIngress.close() + internal suspend fun onEof() { + if (!lifecycle.receiveEof { + logger.debug("Received EOF on channel $localChannelNumber") + stdoutIngress.close() + stderrIngress.close() + extendedDataIngress.close() + } + ) { + throw org.connectbot.sshlib.SshException("Received duplicate EOF or EOF after CLOSE on channel $localChannelNumber") + } } internal suspend fun onClose() { - logger.debug("Received CLOSE on channel $localChannelNumber") + if (!lifecycle.receiveClose { transition -> + closeResources(SshChannelEffect.SEND_CLOSE in transition.effects, "Received CLOSE") + } + ) { + throw org.connectbot.sshlib.SshException("Received duplicate CLOSE on channel $localChannelNumber") + } + } + + private suspend fun closeResources(replyRequired: Boolean, reason: String) { + logger.debug("$reason on channel $localChannelNumber") obfuscatorMutex.withLock { obfuscator?.stop() } chaffJob?.cancel() - if (!closeSent) { - closeSent = true + if (replyRequired) { try { connection.sendChannelClose(_remoteChannelNumber) } catch (e: Exception) { logger.debug("Failed to send CHANNEL_CLOSE reply", e) } } - _isOpen = false stdoutIngress.close() stderrIngress.close() extendedDataIngress.close() @@ -171,6 +200,12 @@ class SessionChannel internal constructor( windowAvailable.close() } + internal suspend fun onDisconnected() { + lifecycle.disconnect { closeResources(replyRequired = false, reason = "Disconnected") } + } + + internal suspend fun receiveRequest(action: suspend () -> Unit): Boolean = lifecycle.receiveRequest { action() } + override suspend fun write(data: ByteArray) { if (obfuscationActive) { writeObfuscated(data) @@ -187,8 +222,13 @@ class SessionChannel internal constructor( } val chunkSize = window.sendChunkSize(data.size - offset, maxPacketSize) val chunk = data.copyOfRange(offset, offset + chunkSize) - connection.sendChannelData(_remoteChannelNumber, chunk) - window.consumeRemote(chunkSize) + if (!lifecycle.sendData { + connection.sendChannelData(_remoteChannelNumber, chunk) + window.consumeRemote(chunkSize) + } + ) { + throw org.connectbot.sshlib.SshException("Cannot send data after EOF or CLOSE on channel $localChannelNumber") + } offset += chunkSize } } @@ -262,7 +302,18 @@ class SessionChannel internal constructor( override suspend fun readExtended(): Pair? = _extendedData.receiveCatching().getOrNull() override suspend fun sendEof() { - connection.sendChannelEof(_remoteChannelNumber) + lifecycle.sendEof { connection.sendChannelEof(_remoteChannelNumber) } + } + + private suspend fun performSendRequest(action: suspend () -> CompletableDeferred?): Boolean { + var pendingReply: CompletableDeferred? = null + if (!lifecycle.sendRequest { pendingReply = action() }) return false + val deferred = pendingReply ?: return true + return try { + deferred.await() + } finally { + connection.finishChannelRequest(deferred) + } } override suspend fun resizeTerminal( @@ -270,9 +321,9 @@ class SessionChannel internal constructor( heightRows: Int, widthPixels: Int, heightPixels: Int, - ): Boolean { + ): Boolean = performSendRequest { logger.debug("Resizing terminal: ${widthChars}x$heightRows") - return connection.sendChannelRequest( + connection.beginChannelRequest( _remoteChannelNumber, "window-change", wantReply = false, @@ -295,41 +346,44 @@ class SessionChannel internal constructor( heightPixels: Int, terminalModes: ByteArray, ): Boolean { - logger.debug("Requesting PTY: $terminalType ${widthChars}x$heightRows") - val granted = connection.sendChannelRequest( - _remoteChannelNumber, - "pty-req", - wantReply = true, - ) { msg -> - val ptyReq = ChannelRequestPtyReq() - - val termBytes = ByteString() - termBytes.setLenData(terminalType.length.toLong()) - termBytes.setData(terminalType.toByteArray(Charsets.US_ASCII)) - termBytes._check() - ptyReq.setTerm(termBytes) - - ptyReq.setTerminalWidth(widthChars.toLong()) - ptyReq.setTerminalHeight(heightRows.toLong()) - ptyReq.setTerminalWidthPixels(widthPixels.toLong()) - ptyReq.setTerminalHeightPixels(heightPixels.toLong()) - - val modeString = ByteString() - modeString.setLenData(terminalModes.size.toLong()) - modeString.setData(terminalModes) - modeString._check() - ptyReq.setTerminalModes(modeString) - - ptyReq._check() - msg.setRequestSpecificFields(ptyReq) + val granted = performSendRequest { + logger.debug("Requesting PTY: $terminalType ${widthChars}x$heightRows") + val pendingReply = connection.beginChannelRequest( + _remoteChannelNumber, + "pty-req", + wantReply = true, + ) { msg -> + val ptyReq = ChannelRequestPtyReq() + + val termBytes = ByteString() + termBytes.setLenData(terminalType.length.toLong()) + termBytes.setData(terminalType.toByteArray(Charsets.US_ASCII)) + termBytes._check() + ptyReq.setTerm(termBytes) + + ptyReq.setTerminalWidth(widthChars.toLong()) + ptyReq.setTerminalHeight(heightRows.toLong()) + ptyReq.setTerminalWidthPixels(widthPixels.toLong()) + ptyReq.setTerminalHeightPixels(heightPixels.toLong()) + + val modeString = ByteString() + modeString.setLenData(terminalModes.size.toLong()) + modeString.setData(terminalModes) + modeString._check() + ptyReq.setTerminalModes(modeString) + + ptyReq._check() + msg.setRequestSpecificFields(ptyReq) + } + pendingReply } if (granted) ptyGranted = true return granted } - override suspend fun requestShell(): Boolean { + override suspend fun requestShell(): Boolean = performSendRequest { logger.debug("Requesting shell on channel $localChannelNumber") - return connection.sendChannelRequest( + connection.beginChannelRequest( _remoteChannelNumber, "shell", wantReply = true, @@ -340,9 +394,9 @@ class SessionChannel internal constructor( } } - override suspend fun requestExec(command: String): Boolean { + override suspend fun requestExec(command: String): Boolean = performSendRequest { logger.debug("Requesting exec on channel $localChannelNumber: $command") - return connection.sendChannelRequest( + connection.beginChannelRequest( _remoteChannelNumber, "exec", wantReply = true, @@ -358,9 +412,9 @@ class SessionChannel internal constructor( } } - override suspend fun requestSubsystem(name: String): Boolean { + override suspend fun requestSubsystem(name: String): Boolean = performSendRequest { logger.debug("Requesting subsystem on channel $localChannelNumber: $name") - return connection.sendChannelRequest( + connection.beginChannelRequest( _remoteChannelNumber, "subsystem", wantReply = true, @@ -377,27 +431,25 @@ class SessionChannel internal constructor( } override fun close() { - if (!_isOpen) return - - logger.debug("Closing channel $localChannelNumber") - obfuscator?.stop() - chaffJob?.cancel() - closeSent = true - _isOpen = false - stdoutIngress.close() - stderrIngress.close() - extendedDataIngress.close() - stdoutDeliveryJob.cancel() - stderrDeliveryJob.cancel() - extendedDeliveryJob.cancel() - _stdout.close() - _stderr.close() - _extendedData.close() - connectionScope.launch { - try { - connection.sendChannelClose(_remoteChannelNumber) - } catch (e: Exception) { - logger.debug("Failed to send CHANNEL_CLOSE", e) + connectionScope.launch(start = CoroutineStart.UNDISPATCHED) { + lifecycle.sendClose { + logger.debug("Closing channel $localChannelNumber") + obfuscatorMutex.withLock { obfuscator?.stop() } + chaffJob?.cancel() + stdoutIngress.close() + stderrIngress.close() + extendedDataIngress.close() + stdoutDeliveryJob.cancel() + stderrDeliveryJob.cancel() + extendedDeliveryJob.cancel() + _stdout.close() + _stderr.close() + _extendedData.close() + try { + connection.sendChannelClose(_remoteChannelNumber) + } catch (e: Exception) { + logger.debug("Failed to send CHANNEL_CLOSE", e) + } } } } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshChannelRegistry.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshChannelRegistry.kt new file mode 100644 index 00000000..78e3d5ea --- /dev/null +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshChannelRegistry.kt @@ -0,0 +1,264 @@ +/* + * ConnectBot SSH Library + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.connectbot.sshlib.client + +import kotlinx.coroutines.CompletableDeferred +import org.connectbot.sshlib.protocol.SshChannelStateMachine +import org.connectbot.sshlib.protocol.SshMsgChannelOpenConfirmation + +/** + * Authoritative owner of allocated SSH channel IDs and channel lifecycle objects. + * + * Inbound `recipient_channel` values use [findByLocalRecipient]. Outbound recipient values use the + * peer's namespace and can be resolved with [findByRemoteRecipient]. Local and remote indexes are + * changed together under one lock; callers must never maintain a second authoritative ID map. + */ +internal class SshChannelRegistry { + internal enum class Kind { + SESSION, + FORWARDING, + AGENT, + } + + internal sealed interface Entry { + val localChannelNumber: Int + val remoteChannelNumber: Int? + val kind: Kind + + sealed interface Pending : Entry { + val lifecycle: SshChannelStateMachine + override var remoteChannelNumber: Int? + + data class Session( + override val localChannelNumber: Int, + val deferred: CompletableDeferred, + override val lifecycle: SshChannelStateMachine, + override var remoteChannelNumber: Int? = null, + ) : Pending { + override val kind = Kind.SESSION + } + + data class Forwarding( + override val localChannelNumber: Int, + val deferred: CompletableDeferred, + val maxPacketSize: Int, + val initialWindowSize: Int, + override val lifecycle: SshChannelStateMachine, + override var remoteChannelNumber: Int? = null, + ) : Pending { + override val kind = Kind.FORWARDING + } + } + + sealed interface Established : Entry { + override val remoteChannelNumber: Int + val isOpen: Boolean + + suspend fun disconnect() + + data class Session( + val channel: SessionChannel, + ) : Established { + override val localChannelNumber = channel.localChannelNumber + override val remoteChannelNumber = channel.remoteChannelNumber + override val kind = Kind.SESSION + override val isOpen get() = channel.isOpen + override suspend fun disconnect() = channel.onDisconnected() + } + + data class Forwarding( + val channel: ForwardingChannel, + ) : Established { + override val localChannelNumber = channel.localChannelNumber + override val remoteChannelNumber = channel.remoteChannelNumber + override val kind = Kind.FORWARDING + override val isOpen get() = channel.isOpen + override suspend fun disconnect() = channel.onDisconnected() + } + + data class Agent( + val channel: AgentChannel, + ) : Established { + override val localChannelNumber = channel.localChannelNumber + override val remoteChannelNumber = channel.remoteChannelNumber + override val kind = Kind.AGENT + override val isOpen get() = channel.isOpen + override suspend fun disconnect() = channel.onDisconnected() + } + } + } + + private val lock = Any() + private val entriesByLocalRecipient = HashMap() + private val localRecipientByRemoteRecipient = HashMap() + private var disconnected = false + + fun registerPendingSession( + localChannelNumber: Int, + deferred: CompletableDeferred, + lifecycle: SshChannelStateMachine, + ) = register(Entry.Pending.Session(localChannelNumber, deferred, lifecycle)) + + fun registerPendingForwarding( + localChannelNumber: Int, + deferred: CompletableDeferred, + maxPacketSize: Int, + initialWindowSize: Int, + lifecycle: SshChannelStateMachine, + ) = register(Entry.Pending.Forwarding(localChannelNumber, deferred, maxPacketSize, initialWindowSize, lifecycle)) + + fun register(channel: SessionChannel) = register(Entry.Established.Session(channel)) + + fun register(channel: ForwardingChannel) = register(Entry.Established.Forwarding(channel)) + + fun register(channel: AgentChannel) = register(Entry.Established.Agent(channel)) + + fun findByLocalRecipient(localChannelNumber: Int): Entry.Established? = synchronized(lock) { + entriesByLocalRecipient[localChannelNumber] as? Entry.Established + } + + fun findByRemoteRecipient(remoteChannelNumber: Int): Entry.Established? = synchronized(lock) { + localRecipientByRemoteRecipient[remoteChannelNumber] + ?.let(entriesByLocalRecipient::get) as? Entry.Established + } + + fun findPendingSession(localChannelNumber: Int): Entry.Pending.Session? = synchronized(lock) { + entriesByLocalRecipient[localChannelNumber] as? Entry.Pending.Session + } + + fun findPendingForwarding(localChannelNumber: Int): Entry.Pending.Forwarding? = synchronized(lock) { + entriesByLocalRecipient[localChannelNumber] as? Entry.Pending.Forwarding + } + + fun bindRemoteRecipient(entry: Entry.Pending, remoteChannelNumber: Int) = synchronized(lock) { + check(!disconnected) { "Channel registry is disconnected" } + check(entriesByLocalRecipient[entry.localChannelNumber] === entry) { + "Pending local channel ${entry.localChannelNumber} is no longer registered" + } + check(entry.remoteChannelNumber == null) { + "Pending local channel ${entry.localChannelNumber} already has a remote channel" + } + check(localRecipientByRemoteRecipient[remoteChannelNumber] == null) { + "Remote channel $remoteChannelNumber is already registered" + } + entry.remoteChannelNumber = remoteChannelNumber + localRecipientByRemoteRecipient[remoteChannelNumber] = entry.localChannelNumber + } + + fun promote(entry: Entry.Pending.Session, channel: SessionChannel) = promote(entry, Entry.Established.Session(channel)) + + fun promote(entry: Entry.Pending.Forwarding, channel: ForwardingChannel) = promote(entry, Entry.Established.Forwarding(channel)) + + fun removePendingSessionIf( + localChannelNumber: Int, + deferred: CompletableDeferred, + ): Entry.Pending.Session? = synchronized(lock) { + val pending = entriesByLocalRecipient[localChannelNumber] as? Entry.Pending.Session + if (pending?.deferred !== deferred) return@synchronized null + removeLocked(pending) + pending + } + + fun removePendingForwardingIf( + localChannelNumber: Int, + deferred: CompletableDeferred, + ): Entry.Pending.Forwarding? = synchronized(lock) { + val pending = entriesByLocalRecipient[localChannelNumber] as? Entry.Pending.Forwarding + if (pending?.deferred !== deferred) return@synchronized null + removeLocked(pending) + pending + } + + fun unregister(localChannelNumber: Int): Entry? = synchronized(lock) { + val removed = entriesByLocalRecipient[localChannelNumber] ?: return@synchronized null + removeLocked(removed) + removed + } + + fun snapshot(): List = synchronized(lock) { entriesByLocalRecipient.values.toList() } + + fun establishedSnapshot(): List = synchronized(lock) { + entriesByLocalRecipient.values.filterIsInstance() + } + + /** Atomically removes every entry, then tears each lifecycle down exactly once. */ + suspend fun disconnectAll(cause: Throwable) { + val entries = synchronized(lock) { + disconnected = true + val snapshot = entriesByLocalRecipient.values.toList() + entriesByLocalRecipient.clear() + localRecipientByRemoteRecipient.clear() + snapshot + } + entries.forEach { entry -> + try { + when (entry) { + is Entry.Pending.Session -> entry.lifecycle.disconnect { + entry.deferred.completeExceptionally(cause) + } + + is Entry.Pending.Forwarding -> entry.lifecycle.disconnect { + entry.deferred.completeExceptionally(cause) + } + + is Entry.Established -> entry.disconnect() + } + } catch (cleanupFailure: Throwable) { + cause.addSuppressed(cleanupFailure) + } + } + } + + private fun promote(pending: Entry.Pending, established: Entry.Established) = synchronized(lock) { + check(!disconnected) { "Channel registry is disconnected" } + check(entriesByLocalRecipient[pending.localChannelNumber] === pending) { + "Pending local channel ${pending.localChannelNumber} is no longer registered" + } + check(established.localChannelNumber == pending.localChannelNumber) + check(established.kind == pending.kind) + check(established.remoteChannelNumber == pending.remoteChannelNumber) { + "Remote channel changed while promoting local channel ${pending.localChannelNumber}" + } + entriesByLocalRecipient[pending.localChannelNumber] = established + } + + private fun register(entry: Entry) = synchronized(lock) { + check(!disconnected) { "Channel registry is disconnected" } + check(entriesByLocalRecipient[entry.localChannelNumber] == null) { + "Local channel ${entry.localChannelNumber} is already registered" + } + entry.remoteChannelNumber?.let { remoteChannelNumber -> + check(localRecipientByRemoteRecipient[remoteChannelNumber] == null) { + "Remote channel $remoteChannelNumber is already registered" + } + } + entriesByLocalRecipient[entry.localChannelNumber] = entry + entry.remoteChannelNumber?.let { remoteChannelNumber -> + localRecipientByRemoteRecipient[remoteChannelNumber] = entry.localChannelNumber + } + } + + private fun removeLocked(entry: Entry) { + check(entriesByLocalRecipient.remove(entry.localChannelNumber) === entry) + entry.remoteChannelNumber?.let { remoteChannelNumber -> + check(localRecipientByRemoteRecipient.remove(remoteChannelNumber) == entry.localChannelNumber) { + "Remote channel index is inconsistent for local channel ${entry.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 b1ec62b0..62ebb4fd 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt @@ -84,6 +84,8 @@ import org.connectbot.sshlib.protocol.IdBanner import org.connectbot.sshlib.protocol.KexDhGexPayload import org.connectbot.sshlib.protocol.KexEcdhPayload import org.connectbot.sshlib.protocol.KexdhPayload +import org.connectbot.sshlib.protocol.SshChannelState +import org.connectbot.sshlib.protocol.SshChannelStateMachine import org.connectbot.sshlib.protocol.SshClientCallbacks import org.connectbot.sshlib.protocol.SshClientStateMachine import org.connectbot.sshlib.protocol.SshEnums @@ -256,6 +258,8 @@ class SshConnection( private const val ERROR_SESSION_ID_NOT_ESTABLISHED = "Session ID not established" private const val ERROR_CLIENT_PUBLIC_KEY_NOT_GENERATED = "Client public key not generated" private const val ERROR_NO_KEX_ALGORITHM_INITIALIZED = "No KEX algorithm initialized" + private const val SSH_MSG_USERAUTH_REQUEST_ID = 50 + private const val MAX_REKEY_IN_FLIGHT_PACKETS = 1_024 private fun stripExtInfoC(kexAlgorithms: String): String = kexAlgorithms.split(",") .filter { it.isNotEmpty() && it != KEX_EXT_INFO_C } @@ -280,7 +284,11 @@ class SshConnection( private class HostKeyRejectedException(val key: PublicKey) : Exception("Host key rejected") - private class ProtocolViolationException(message: String, cause: Throwable? = null) : SshException(message, cause) + private class ProtocolViolationException( + message: String, + cause: Throwable? = null, + val responseSent: Boolean = false, + ) : SshException(message, cause) private val packetIO = PacketIO(transport) @@ -294,6 +302,13 @@ class SshConnection( override suspend fun receiveKexEcdhReply(msg: SshMsgKexEcdhReply) = this@SshConnection.receiveKexEcdhReply(msg) override suspend fun receiveKexDhGexReply(msg: SshMsgKexDhGexReply) = this@SshConnection.receiveKexDhGexReply(msg) override fun isRekeying(): Boolean = this@SshConnection.isRekeying + override fun isAuthenticationRequestPending(): Boolean = this@SshConnection.authRequestPending + override fun authenticationRequestStarted() { + this@SshConnection.authRequestPending = true + } + override fun authenticationRequestResponseReceived() { + this@SshConnection.authRequestPending = false + } override fun rekeyStarted() = this@SshConnection.rekeyStarted() override fun rekeyComplete() = this@SshConnection.rekeyComplete() override suspend fun sendKexDhGexInit() = this@SshConnection.sendKexDhGexInit() @@ -309,8 +324,8 @@ class SshConnection( override fun receiveUserauthInfoRequest(msg: SshMsgUserauthInfoRequest) = this@SshConnection.receiveUserauthInfoRequest(msg) override fun receiveUserauthBanner(msg: SshMsgUserauthBanner) = this@SshConnection.receiveUserauthBanner(msg) override suspend fun sendChannelOpen(channelType: String, localChannelNumber: Int, initialWindowSize: Int, maxPacketSize: Int) = this@SshConnection.sendChannelOpen(channelType, localChannelNumber, initialWindowSize, maxPacketSize) - override fun receiveChannelOpenConfirmation(msg: SshMsgChannelOpenConfirmation) = this@SshConnection.receiveChannelOpenConfirmation(msg) - override fun receiveChannelOpenFailure(msg: SshMsgChannelOpenFailure) = this@SshConnection.receiveChannelOpenFailure(msg) + override suspend fun receiveChannelOpenConfirmation(msg: SshMsgChannelOpenConfirmation) = this@SshConnection.receiveChannelOpenConfirmation(msg) + override suspend fun receiveChannelOpenFailure(msg: SshMsgChannelOpenFailure) = this@SshConnection.receiveChannelOpenFailure(msg) override suspend fun sendChannelRequest(recipientChannel: Int, requestType: String, wantReply: Boolean, message: SshMsgChannelRequest) = this@SshConnection.sendChannelRequest(recipientChannel, requestType, wantReply, message) override fun receiveChannelSuccess(recipientChannel: Int) = this@SshConnection.receiveChannelSuccess(recipientChannel) override fun receiveChannelFailure(recipientChannel: Int) = this@SshConnection.receiveChannelFailure(recipientChannel) @@ -318,6 +333,7 @@ class SshConnection( override fun debug(msg: SshMsgDebug) = this@SshConnection.debug(msg) override fun ignore() = this@SshConnection.ignore() override suspend fun disconnect() = this@SshConnection.disconnect() + override suspend fun sendProtocolError(description: String) = this@SshConnection.sendProtocolError(description) override fun onStateEnter(stateName: String) = this@SshConnection.onStateEnter(stateName) override fun onStateExit(stateName: String) = this@SshConnection.onStateExit(stateName) } @@ -326,6 +342,8 @@ class SshConnection( private val inboundPacketController = InboundPacketController() internal val connectionScope = CoroutineScope(SupervisorJob() + coroutineDispatcher) private val writeMutex = Mutex() + private val outboundPacketController = OutboundPacketController() + private var transportClosing = false private val _disconnectedFlow = MutableSharedFlow(extraBufferCapacity = 1) val disconnectedFlow: SharedFlow = _disconnectedFlow.asSharedFlow() @@ -355,12 +373,7 @@ class SshConnection( private var nextLocalChannelNumber = 0 private val channelNumberLock = Mutex() - private val channels = ConcurrentHashMap() - private val channelsByRemote = ConcurrentHashMap() - private val agentChannels = ConcurrentHashMap() - private val agentChannelsByRemote = ConcurrentHashMap() - private val forwardingChannels = ConcurrentHashMap() - private val forwardingChannelsByRemote = ConcurrentHashMap() + private val channelRegistry = SshChannelRegistry() private var agentProvider: AgentProvider? = null private var serverHostKeyBlob: ByteArray? = null @@ -435,13 +448,6 @@ class SshConnection( // Pending async operations - completed by callbacks private val pendingAuth = PendingValue() - private val pendingSessionChannelOpens = HashMap>() - private class PendingChannelOpen( - val deferred: CompletableDeferred, - val maxPacketSize: Int, - val initialWindowSize: Int, - ) - private val pendingChannelOpens = ConcurrentHashMap() private val pendingChannelRequests = HashMap>() private val pendingGlobalRequest = PendingValue() @@ -461,6 +467,8 @@ class SshConnection( @Volatile internal var isRekeying = false + @Volatile private var authRequestPending = false + private var rekeyTimerJob: Job? = null @Volatile private var pendingConnect: CompletableDeferred? = null @@ -482,12 +490,71 @@ class SshConnection( } } - /** - * Serialized write to the transport. - */ + /** Serialized write to the transport, subject to the RFC 4253 key-exchange gate. */ private suspend fun writePacket(messageType: Int, payload: ByteArray = byteArrayOf()) { - writeMutex.withLock { - packetIO.writePacket(messageType, payload) + outboundPacketController.writePacket(messageType, payload) + } + + private inner class OutboundPacketController { + @Volatile + private var kexCompletion = CompletableDeferred(Unit) + + fun beginKex() { + check(kexCompletion.isCompleted) { "Key exchange is already in progress" } + kexCompletion = CompletableDeferred() + } + + fun completeKex() { + kexCompletion.complete(Unit) + } + + suspend fun writePacket( + messageType: Int, + payload: ByteArray = byteArrayOf(), + beforeWrite: () -> Unit = {}, + afterWrite: () -> Unit = {}, + ) { + while (true) { + val observedKex = kexCompletion + if (!isAllowedDuringKex(messageType)) { + observedKex.await() + } + + var written = false + writeMutex.withLock { + checkTransportOpen() + if (isAllowedDuringKex(messageType) || kexCompletion.isCompleted) { + beforeWrite() + packetIO.writePacket(messageType, payload) + afterWrite() + written = true + } + } + if (written) return + } + } + + private fun isAllowedDuringKex(messageType: Int): Boolean = messageType in 1..4 || messageType in 7..49 + } + + private fun checkTransportOpen() { + if (transportClosing) { + throw TransportException("Transport is closed") + } + } + + /** Prevent new writes before closing the underlying transport exactly once. */ + private suspend fun closeTransport() { + withContext(NonCancellable) { + writeMutex.withLock { + if (transportClosing) return@withLock + transportClosing = true + try { + transport.close() + } finally { + outboundPacketController.completeKex() + } + } } } @@ -1093,13 +1160,11 @@ class SshConnection( configure() _check() } - writeMutex.withLock { - currentAuthMethod = AuthMethod.fromString(method) - packetIO.writePacket( - SshEnums.MessageType.SSH_MSG_USERAUTH_REQUEST.id().toInt(), - req.toByteArray(), - ) - } + outboundPacketController.writePacket( + SshEnums.MessageType.SSH_MSG_USERAUTH_REQUEST.id().toInt(), + req.toByteArray(), + beforeWrite = { currentAuthMethod = AuthMethod.fromString(method) }, + ) } // SshClientCallbacks implementation @@ -1118,6 +1183,7 @@ class SshConnection( } private suspend fun sendKexInit() { + outboundPacketController.beginKex() logger.debug("Sending KEX_INIT") val localKexAlgorithms = if (isRekeying) kexAlgorithms else initialKexAlgorithms @@ -1456,17 +1522,20 @@ class SshConnection( logger.info("Sending NEW_KEYS") prepareEncryption() try { - writeMutex.withLock { - packetIO.writePacket(SshEnums.MessageType.SSH_MSG_NEWKEYS.id().toInt()) - val protection = pendingProtection - ?: throw SshException("No staged packet protection") - protection.installOutbound(packetIO) - packetIO.enableSendCompression(pendingSendCompressor, pendingCompressionImmediate) - pendingSendCompressor = null - if (strictKexEnabled) { - packetIO.resetSendSequenceNumber() - } - } + outboundPacketController.writePacket( + SshEnums.MessageType.SSH_MSG_NEWKEYS.id().toInt(), + afterWrite = { + val protection = pendingProtection + ?: throw SshException("No staged packet protection") + protection.installOutbound(packetIO) + packetIO.enableSendCompression(pendingSendCompressor, pendingCompressionImmediate) + pendingSendCompressor = null + if (strictKexEnabled) { + packetIO.resetSendSequenceNumber() + } + outboundPacketController.completeKex() + }, + ) } catch (e: Exception) { discardPendingEncryption() throw e @@ -1764,12 +1833,14 @@ class SshConnection( private fun authenticationSuccess() { logger.info("Authentication successful") + authRequestPending = false packetIO.activateCompression() pendingAuth.complete(true) } private fun authenticationFailure() { logger.warn("Authentication failed") + authRequestPending = false pendingAuth.complete(false) } @@ -1807,8 +1878,10 @@ class SshConnection( private suspend fun disconnect() { logger.info("Disconnecting (received SSH_MSG_DISCONNECT from server)") + isRekeying = false + authRequestPending = false _disconnectedFlow.tryEmit(null) - transport.close() + closeTransport() } /** @@ -1877,15 +1950,19 @@ class SshConnection( initialWindow, ) - agentChannels[localChannelNumber] = agentChannel - agentChannelsByRemote[localChannelNumber] = agentChannel - - sendChannelOpenConfirmation( - recipientChannel = senderChannel, - senderChannel = localChannelNumber, - initialWindowSize = 64 * 1024, - maximumPacketSize = 32 * 1024, - ) + channelRegistry.register(agentChannel) + try { + sendChannelOpenConfirmation( + recipientChannel = senderChannel, + senderChannel = localChannelNumber, + initialWindowSize = 64 * 1024, + maximumPacketSize = 32 * 1024, + ) + } catch (failure: Throwable) { + channelRegistry.unregister(localChannelNumber) + agentChannel.onDisconnected() + throw failure + } logger.info("Accepted agent channel: local=$localChannelNumber, remote=$senderChannel") } @@ -1985,8 +2062,8 @@ class SshConnection( } suspend fun close() { - transport.close() connectionScope.cancel() + closeTransport() packetLoopJob?.join() packetLoopJob = null @@ -2033,20 +2110,32 @@ class SshConnection( ) } - private fun receiveChannelOpenConfirmation(msg: SshMsgChannelOpenConfirmation) { + private suspend fun receiveChannelOpenConfirmation(msg: SshMsgChannelOpenConfirmation) { logger.info("Channel open confirmed") val recipientChannel = msg.recipientChannel().toInt() - val pending = pendingSessionChannelOpens.remove(recipientChannel) + val pending = channelRegistry.findPendingSession(recipientChannel) ?: throw ProtocolViolationException("Channel confirmation with no pending open for channel $recipientChannel") - pending.complete(msg) + if (!pending.lifecycle.openConfirmed { + channelRegistry.bindRemoteRecipient(pending, msg.senderChannel().toInt()) + pending.deferred.complete(msg) + } + ) { + throw ProtocolViolationException("Channel confirmation in ${pending.lifecycle.state} state for channel $recipientChannel") + } } - private fun receiveChannelOpenFailure(msg: SshMsgChannelOpenFailure) { + private suspend fun receiveChannelOpenFailure(msg: SshMsgChannelOpenFailure) { logger.error("Channel open failed: ${msg.reasonCode()}") val recipientChannel = msg.recipientChannel().toInt() - val pending = pendingSessionChannelOpens.remove(recipientChannel) + val pending = channelRegistry.findPendingSession(recipientChannel) ?: throw ProtocolViolationException("Channel failure with no pending open for channel $recipientChannel") - pending.complete(null) + if (!pending.lifecycle.openFailed { + channelRegistry.removePendingSessionIf(recipientChannel, pending.deferred) + pending.deferred.complete(null) + } + ) { + throw ProtocolViolationException("Channel failure in ${pending.lifecycle.state} state for channel $recipientChannel") + } } private suspend fun sendChannelRequest(recipientChannel: Int, requestType: String, wantReply: Boolean, message: SshMsgChannelRequest) { @@ -2104,7 +2193,14 @@ class SshConnection( logger.info("Opening direct-tcpip channel to $host:$port (local=$localChannelNumber)") val deferred = CompletableDeferred() - pendingChannelOpens[localChannelNumber] = PendingChannelOpen(deferred, maxPacketSize, initialWindowSize) + val lifecycle = SshChannelStateMachine(SshChannelState.OPENING) + channelRegistry.registerPendingForwarding( + localChannelNumber, + deferred, + maxPacketSize, + initialWindowSize, + lifecycle, + ) val channelSpecificData = ChannelOpenDirectTcpip().apply { setHostToConnect(createByteString(host.toByteArray(Charsets.US_ASCII))) @@ -2123,15 +2219,14 @@ class SshConnection( _check() } - writePacket( - SshEnums.MessageType.SSH_MSG_CHANNEL_OPEN.id().toInt(), - msg.toByteArray(), - ) - return try { + writePacket( + SshEnums.MessageType.SSH_MSG_CHANNEL_OPEN.id().toInt(), + msg.toByteArray(), + ) deferred.await() } finally { - pendingChannelOpens.remove(localChannelNumber) + channelRegistry.removePendingForwardingIf(localChannelNumber, deferred)?.lifecycle?.disconnect {} } } @@ -2208,13 +2303,11 @@ class SshConnection( } internal fun registerForwardingChannel(channel: ForwardingChannel) { - forwardingChannels[channel.localChannelNumber] = channel - forwardingChannelsByRemote[channel.localChannelNumber] = channel + channelRegistry.register(channel) } internal fun unregisterForwardingChannel(channel: ForwardingChannel) { - forwardingChannels.remove(channel.localChannelNumber) - forwardingChannelsByRemote.remove(channel.localChannelNumber) + channelRegistry.unregister(channel.localChannelNumber) } internal suspend fun sendChannelOpenConfirmationPublic( @@ -2242,6 +2335,8 @@ class SshConnection( * This is the central packet processing loop that converts packets to events. */ private inner class InboundPacketController { + private val packetsReceivedDuringRekey = ArrayDeque() + private fun requireAccepted(accepted: Boolean, messageType: Any) { if (!accepted) { throw ProtocolViolationException("Unexpected SSH packet $messageType in the current protocol state") @@ -2249,13 +2344,29 @@ class SshConnection( } suspend fun processNextPacket() { - val packet = packetIO.readPacket() + val queuedPacket = withContext(stateMachineDispatcher) { + if (stateMachine.isKexInProgress()) null else packetsReceivedDuringRekey.removeFirstOrNull() + } + val packet = queuedPacket ?: packetIO.readPacket() val msgType = packet.messageType() logger.debug("Received packet: $msgType") withContext(stateMachineDispatcher) { + if (isRekeying && stateMachine.isKexInProgress() && msgType.id().toInt() >= SSH_MSG_USERAUTH_REQUEST_ID) { + if (packetsReceivedDuringRekey.size >= MAX_REKEY_IN_FLIGHT_PACKETS) { + throw ProtocolViolationException("Too many higher-layer packets received during key exchange") + } + packetsReceivedDuringRekey.addLast(packet) + return@withContext + } + when (msgType) { SshEnums.MessageType.SSH_MSG_KEXINIT -> { + if (stateMachine.isKexInProgress() && !stateMachine.isWaitingForKexInit()) { + val description = "Unexpected SSH_MSG_KEXINIT while key exchange is already in progress" + requireAccepted(stateMachine.unexpectedKexInit(description), msgType) + throw ProtocolViolationException(description, responseSent = true) + } val kexInitMsgType = msgType.id().toByte() serverKexInit = byteArrayOf(kexInitMsgType) + packet._raw_body() val kexInit = packet.body() as SshMsgKexinit @@ -2311,28 +2422,40 @@ class SshConnection( requireAccepted(stateMachine.authorizeAuthenticatedPacket(), msgType) val confirmationMsg = parseBody(packet) val recipientChannel = confirmationMsg.recipientChannel().toInt() - val pending = pendingChannelOpens.remove(recipientChannel) + val pending = channelRegistry.findPendingForwarding(recipientChannel) if (pending != null) { val remoteChannelNumber = confirmationMsg.senderChannel().toInt() val remoteWindow = confirmationMsg.initialWindowSize() val remoteMaxPacketSize = boundRemotePacketSize(confirmationMsg.maximumPacketSize()) - if (remoteMaxPacketSize == null) { + var invalidPacketSize = false + if (!pending.lifecycle.openConfirmed { + channelRegistry.bindRemoteRecipient(pending, remoteChannelNumber) + if (remoteMaxPacketSize == null) { + invalidPacketSize = true + channelRegistry.removePendingForwardingIf(recipientChannel, pending.deferred) + pending.deferred.complete(null) + } else { + logger.info("Direct-tcpip channel opened: local=$recipientChannel, remote=$remoteChannelNumber") + val channel = ForwardingChannel( + this@SshConnection, + connectionScope, + recipientChannel, + remoteChannelNumber, + remoteMaxPacketSize, + remoteWindowSizeInitial = remoteWindow, + initialWindowSize = pending.initialWindowSize, + lifecycle = pending.lifecycle, + ) + channelRegistry.promote(pending, channel) + pending.deferred.complete(channel) + } + } + ) { + throw ProtocolViolationException("Channel confirmation in ${pending.lifecycle.state} state for channel $recipientChannel") + } + if (invalidPacketSize) { logger.warn("Rejecting channel confirmation with invalid maximum packet size: ${confirmationMsg.maximumPacketSize()}") - pending.deferred.complete(null) - sendChannelClose(remoteChannelNumber) - } else { - logger.info("Direct-tcpip channel opened: local=$recipientChannel, remote=$remoteChannelNumber") - val channel = ForwardingChannel( - this@SshConnection, - connectionScope, - recipientChannel, - remoteChannelNumber, - remoteMaxPacketSize, - remoteWindowSizeInitial = remoteWindow, - initialWindowSize = pending.initialWindowSize, - ) - registerForwardingChannel(channel) - pending.deferred.complete(channel) + pending.lifecycle.sendClose { sendChannelClose(remoteChannelNumber) } } } else { requireAccepted(stateMachine.receiveChannelOpenConfirmation(confirmationMsg), msgType) @@ -2343,9 +2466,15 @@ class SshConnection( requireAccepted(stateMachine.authorizeAuthenticatedPacket(), msgType) val failureMsg = parseBody(packet) val recipientChannel = failureMsg.recipientChannel().toInt() - val pending = pendingChannelOpens.remove(recipientChannel) + val pending = channelRegistry.findPendingForwarding(recipientChannel) if (pending != null) { - pending.deferred.complete(null) + if (!pending.lifecycle.openFailed { + channelRegistry.removePendingForwardingIf(recipientChannel, pending.deferred) + pending.deferred.complete(null) + } + ) { + throw ProtocolViolationException("Channel failure in ${pending.lifecycle.state} state for channel $recipientChannel") + } } else { requireAccepted(stateMachine.receiveChannelOpenFailure(failureMsg), msgType) } @@ -2355,25 +2484,27 @@ class SshConnection( requireAccepted(stateMachine.authorizeAuthenticatedPacket(), msgType) val msg = parseBody(packet) val recipientChannel = msg.recipientChannel().toInt() - val channel = channelsByRemote[recipientChannel] - val agentChannel = agentChannelsByRemote[recipientChannel] - val fwdChannel = forwardingChannelsByRemote[recipientChannel] - when { - channel != null -> channel.onData(msg.data().data()) - agentChannel != null -> agentChannel.handleData(msg.data().data()) - fwdChannel != null -> fwdChannel.onData(msg.data().data()) - else -> throw ProtocolViolationException("Channel data for unknown channel $recipientChannel") + when (val entry = channelRegistry.findByLocalRecipient(recipientChannel)) { + is SshChannelRegistry.Entry.Established.Session -> entry.channel.onData(msg.data().data()) + is SshChannelRegistry.Entry.Established.Agent -> entry.channel.handleData(msg.data().data()) + is SshChannelRegistry.Entry.Established.Forwarding -> entry.channel.onData(msg.data().data()) + null -> throw ProtocolViolationException("Channel data for unknown channel $recipientChannel") } } SshEnums.MessageType.SSH_MSG_CHANNEL_EXTENDED_DATA -> { requireAccepted(stateMachine.authorizeAuthenticatedPacket(), msgType) val msg = parseBody(packet) - val channel = channelsByRemote[msg.recipientChannel().toInt()] - if (channel != null) { - channel.onExtendedData(msg.dataTypeCode().toInt(), msg.data().data()) - } else { - throw ProtocolViolationException("Extended data for unknown channel ${msg.recipientChannel()}") + val recipientChannel = msg.recipientChannel().toInt() + when (val entry = channelRegistry.findByLocalRecipient(recipientChannel)) { + is SshChannelRegistry.Entry.Established.Session -> + entry.channel.onExtendedData(msg.dataTypeCode().toInt(), msg.data().data()) + + is SshChannelRegistry.Entry.Established.Agent, + is SshChannelRegistry.Entry.Established.Forwarding, + -> throw ProtocolViolationException("Extended data is invalid for channel $recipientChannel") + + null -> throw ProtocolViolationException("Extended data for unknown channel $recipientChannel") } } @@ -2381,14 +2512,11 @@ class SshConnection( requireAccepted(stateMachine.authorizeAuthenticatedPacket(), msgType) val msg = parseBody(packet) val recipientChannel = msg.recipientChannel().toInt() - val channel = channelsByRemote[recipientChannel] - val agentChannel = agentChannelsByRemote[recipientChannel] - val fwdChannel = forwardingChannelsByRemote[recipientChannel] - when { - channel != null -> channel.onWindowAdjust(msg.bytesToAdd()) - agentChannel != null -> agentChannel.onWindowAdjust(msg.bytesToAdd()) - fwdChannel != null -> fwdChannel.onWindowAdjust(msg.bytesToAdd()) - else -> throw ProtocolViolationException("Window adjust for unknown channel $recipientChannel") + when (val entry = channelRegistry.findByLocalRecipient(recipientChannel)) { + is SshChannelRegistry.Entry.Established.Session -> entry.channel.onWindowAdjust(msg.bytesToAdd()) + is SshChannelRegistry.Entry.Established.Agent -> entry.channel.onWindowAdjust(msg.bytesToAdd()) + is SshChannelRegistry.Entry.Established.Forwarding -> entry.channel.onWindowAdjust(msg.bytesToAdd()) + null -> throw ProtocolViolationException("Window adjust for unknown channel $recipientChannel") } } @@ -2396,14 +2524,11 @@ class SshConnection( requireAccepted(stateMachine.authorizeAuthenticatedPacket(), msgType) val msg = parseBody(packet) val recipientChannel = msg.recipientChannel().toInt() - val channel = channelsByRemote[recipientChannel] - val agentChannel = agentChannelsByRemote[recipientChannel] - val fwdChannel = forwardingChannelsByRemote[recipientChannel] - when { - channel != null -> channel.onEof() - agentChannel != null -> agentChannel.onEof() - fwdChannel != null -> fwdChannel.onEof() - else -> throw ProtocolViolationException("EOF for unknown channel $recipientChannel") + when (val entry = channelRegistry.findByLocalRecipient(recipientChannel)) { + is SshChannelRegistry.Entry.Established.Session -> entry.channel.onEof() + is SshChannelRegistry.Entry.Established.Agent -> entry.channel.onEof() + is SshChannelRegistry.Entry.Established.Forwarding -> entry.channel.onEof() + null -> throw ProtocolViolationException("EOF for unknown channel $recipientChannel") } } @@ -2411,21 +2536,18 @@ class SshConnection( requireAccepted(stateMachine.authorizeAuthenticatedPacket(), msgType) val msg = parseBody(packet) val recipientChannel = msg.recipientChannel().toInt() - logger.debug("Received CHANNEL_CLOSE for remote channel $recipientChannel (channels: ${channels.size}, forwardingChannels: ${forwardingChannels.size})") - val channel = channelsByRemote[recipientChannel] - val agentChannel = agentChannelsByRemote[recipientChannel] - val fwdChannel = forwardingChannelsByRemote[recipientChannel] - when { - channel != null -> channel.onClose() + logger.debug("Received CHANNEL_CLOSE for local channel $recipientChannel") + when (val entry = channelRegistry.findByLocalRecipient(recipientChannel)) { + is SshChannelRegistry.Entry.Established.Session -> entry.channel.onClose() - agentChannel != null -> agentChannel.onClose() + is SshChannelRegistry.Entry.Established.Agent -> entry.channel.onClose() - fwdChannel != null -> { - fwdChannel.onClose() - unregisterForwardingChannel(fwdChannel) + is SshChannelRegistry.Entry.Established.Forwarding -> { + entry.channel.onClose() + unregisterForwardingChannel(entry.channel) } - else -> throw ProtocolViolationException("Close for unknown channel $recipientChannel") + null -> throw ProtocolViolationException("Close for unknown channel $recipientChannel") } checkAllChannelsClosed() } @@ -2437,14 +2559,18 @@ class SshConnection( val msg = SshMsgChannelRequest(stream) msg._read() val recipientChannel = msg.recipientChannel().toInt() - if ( - !channelsByRemote.containsKey(recipientChannel) && - !agentChannelsByRemote.containsKey(recipientChannel) && - !forwardingChannelsByRemote.containsKey(recipientChannel) - ) { - throw ProtocolViolationException("Channel request for unknown channel $recipientChannel") + val deliverRequest = suspend { + logger.debug("Received channel request: ${msg.requestType().value()} (want_reply=${msg.wantReply() != 0})") + } + val requestAccepted = when (val entry = channelRegistry.findByLocalRecipient(recipientChannel)) { + is SshChannelRegistry.Entry.Established.Session -> entry.channel.receiveRequest(deliverRequest) + is SshChannelRegistry.Entry.Established.Agent -> entry.channel.receiveRequest(deliverRequest) + is SshChannelRegistry.Entry.Established.Forwarding -> entry.channel.receiveRequest(deliverRequest) + null -> throw ProtocolViolationException("Channel request for unknown channel $recipientChannel") + } + if (!requestAccepted) { + throw ProtocolViolationException("Channel request is invalid for channel $recipientChannel lifecycle") } - logger.debug("Received channel request: ${msg.requestType().value()} (want_reply=${msg.wantReply() != 0})") } SshEnums.MessageType.SSH_MSG_CHANNEL_SUCCESS -> { @@ -2706,11 +2832,10 @@ class SshConnection( } private suspend fun checkAllChannelsClosed() { - val allSessionsClosed = channels.values.all { !it.isOpen } - val allForwardingClosed = forwardingChannels.values.all { !it.isOpen } - val allAgentClosed = agentChannels.values.all { !it.isOpen } - logger.debug("checkAllChannelsClosed: sessions=${channels.size} allSessionsClosed=$allSessionsClosed, forwarding=${forwardingChannels.size} allForwardingClosed=$allForwardingClosed, agent=${agentChannels.size} allAgentClosed=$allAgentClosed") - if (allSessionsClosed && allForwardingClosed && allAgentClosed && channels.isNotEmpty()) { + 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 }) { logger.info("All channels closed, sending disconnect") sendDisconnect() } @@ -2733,7 +2858,7 @@ class SshConnection( logger.debug("Failed to send disconnect", e) } _disconnectedFlow.tryEmit(null) - transport.close() + closeTransport() } private suspend fun sendProtocolError(description: String) { @@ -2770,9 +2895,15 @@ class SshConnection( } catch (e: Exception) { if (e is ProtocolViolationException) { try { - sendProtocolError(e.message ?: "Unexpected SSH packet") + if (!e.responseSent) { + sendProtocolError(e.message ?: "Unexpected SSH packet") + } } catch (sendFailure: Exception) { logger.debug("Failed to send protocol-error disconnect", sendFailure) + } finally { + isRekeying = false + authRequestPending = false + closeTransport() } } val packetFailure = e.kaitaiParseFailureOrNull() @@ -2783,7 +2914,7 @@ class SshConnection( } pendingConnect?.completeExceptionally(loopFailure) pendingConnect = null - val allClosed = channels.values.all { !it.isOpen } + val allClosed = channelRegistry.establishedSnapshot().all { !it.isOpen } if (allClosed) { logger.debug("Packet loop ended (all channels closed)") } else { @@ -2791,24 +2922,13 @@ class SshConnection( } loopException = loopFailure } finally { - for (ch in channels.values) { - ch.onClose() - } - for (ch in forwardingChannels.values) { - ch.onClose() - } val loopError = loopException ?: Exception("Packet loop terminated") + channelRegistry.disconnectAll(loopError) withContext(stateMachineDispatcher) { pendingAuth.completeExceptionally(loopError) - pendingSessionChannelOpens.values.forEach { it.completeExceptionally(loopError) } - pendingSessionChannelOpens.clear() pendingChannelRequests.values.forEach { it.completeExceptionally(loopError) } pendingChannelRequests.clear() pendingGlobalRequest.completeExceptionally(loopError) - for ((_, pending) in pendingChannelOpens) { - pending.deferred.completeExceptionally(loopError) - } - pendingChannelOpens.clear() for ((_, pending) in pendingPings) { pending.deferred.complete(PingResult.Failure(loopError)) @@ -2844,24 +2964,29 @@ class SshConnection( logger.info("Opening session channel (local=$localChannelNumber)") val deferred = CompletableDeferred() - withContext(stateMachineDispatcher) { - check(pendingSessionChannelOpens.put(localChannelNumber, deferred) == null) - check( - stateMachine.openChannel( - "session", - localChannelNumber, - initialWindowSize, - maxPacketSize, - ), - ) + val lifecycle = SshChannelStateMachine(SshChannelState.OPENING) + try { + withContext(stateMachineDispatcher) { + channelRegistry.registerPendingSession(localChannelNumber, deferred, lifecycle) + check( + stateMachine.openChannel( + "session", + localChannelNumber, + initialWindowSize, + maxPacketSize, + ), + ) + } + } catch (failure: Throwable) { + channelRegistry.removePendingSessionIf(localChannelNumber, deferred)?.lifecycle?.disconnect {} + throw failure } val confirmationMsg = try { deferred.await() - } finally { - withContext(stateMachineDispatcher) { - pendingSessionChannelOpens.remove(localChannelNumber, deferred) - } + } catch (failure: Throwable) { + channelRegistry.removePendingSessionIf(localChannelNumber, deferred)?.lifecycle?.disconnect {} + throw failure } ?: return null val remoteChannelNumber = confirmationMsg.senderChannel().toInt() @@ -2869,7 +2994,8 @@ class SshConnection( val remoteMaxPacketSize = boundRemotePacketSize(confirmationMsg.maximumPacketSize()) if (remoteMaxPacketSize == null) { logger.warn("Rejecting session channel confirmation with invalid maximum packet size: ${confirmationMsg.maximumPacketSize()}") - sendChannelClose(remoteChannelNumber) + channelRegistry.removePendingSessionIf(localChannelNumber, deferred) + lifecycle.sendClose { sendChannelClose(remoteChannelNumber) } return null } logger.info("Channel opened: local=$localChannelNumber, remote=$remoteChannelNumber, remoteWindow=$remoteWindow") @@ -2884,10 +3010,12 @@ class SshConnection( initialWindowSize = initialWindowSize, canSendChaff = serverSupportsPing, obscureKeystrokeTimingIntervalMs = obscureKeystrokeTimingIntervalMs, + lifecycle = lifecycle, ) - channels[localChannelNumber] = channel - channelsByRemote[localChannelNumber] = channel - logger.debug("Session channel registered: local=$localChannelNumber, remote=$remoteChannelNumber (total channels: ${channels.size})") + val pending = channelRegistry.findPendingSession(localChannelNumber) + ?: error("Pending session channel $localChannelNumber disappeared before promotion") + channelRegistry.promote(pending, channel) + logger.debug("Session channel registered: local=$localChannelNumber, remote=$remoteChannelNumber") return channel } @@ -2901,12 +3029,12 @@ class SshConnection( * @param configureRequest Lambda to configure request-specific fields * @return true if request succeeded (when wantReply=true), false otherwise */ - internal suspend fun sendChannelRequest( + internal suspend fun beginChannelRequest( recipientChannel: Int, requestType: String, wantReply: Boolean, configureRequest: (SshMsgChannelRequest) -> Unit, - ): Boolean { + ): CompletableDeferred? { val msg = SshMsgChannelRequest().apply { setRecipientChannel(recipientChannel.toLong()) setRequestType(createAsciiString(requestType)) @@ -2919,7 +3047,8 @@ class SshConnection( val deferred = if (wantReply) CompletableDeferred() else null withContext(stateMachineDispatcher) { if (deferred != null) { - val localChannelNumber = channels.values.singleOrNull { it.remoteChannelNumber == recipientChannel }?.localChannelNumber + val remoteEntry = channelRegistry.findByRemoteRecipient(recipientChannel) + val localChannelNumber = (remoteEntry as? SshChannelRegistry.Entry.Established.Session)?.localChannelNumber ?: throw IllegalStateException("No session channel has remote channel number $recipientChannel") check(pendingChannelRequests.put(localChannelNumber, deferred) == null) { "Channel $localChannelNumber already has a pending request" @@ -2935,16 +3064,26 @@ class SshConnection( ) } - if (deferred == null) { - return true - } + return deferred + } + internal suspend fun sendChannelRequest( + recipientChannel: Int, + requestType: String, + wantReply: Boolean, + configureRequest: (SshMsgChannelRequest) -> Unit, + ): Boolean { + val deferred = beginChannelRequest(recipientChannel, requestType, wantReply, configureRequest) ?: return true return try { deferred.await() } finally { - withContext(stateMachineDispatcher) { - pendingChannelRequests.entries.removeIf { it.value === deferred } - } + finishChannelRequest(deferred) + } + } + + internal suspend fun finishChannelRequest(deferred: CompletableDeferred) { + withContext(stateMachineDispatcher) { + pendingChannelRequests.entries.removeIf { it.value === deferred } } } @@ -2970,18 +3109,20 @@ class SshConnection( val data = ByteBuffer.allocate(8).putLong(seq).array() val deferred = CompletableDeferred() - val send: suspend () -> Unit = { + val send: suspend () -> Unit = send@{ try { - writeMutex.withLock { - val current = pendingPings[seq] ?: return@withLock - val ping = SshMsgPing() - ping.setData(createByteString(current.payload)) - ping._check() - - val sentTimeNs = System.nanoTime() - pendingPings[seq] = current.copy(sentTimeNs = sentTimeNs) - packetIO.writePacket(SshEnums.MessageType.SSH_MSG_PING.id().toInt(), ping.toByteArray()) - } + val current = pendingPings[seq] ?: return@send + val ping = SshMsgPing() + ping.setData(createByteString(current.payload)) + ping._check() + + outboundPacketController.writePacket( + SshEnums.MessageType.SSH_MSG_PING.id().toInt(), + ping.toByteArray(), + beforeWrite = { + pendingPings[seq] = current.copy(sentTimeNs = System.nanoTime()) + }, + ) } catch (e: CancellationException) { throw e } catch (e: Exception) { diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachine.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachine.kt new file mode 100644 index 00000000..0acf5360 --- /dev/null +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachine.kt @@ -0,0 +1,530 @@ +/* + * ConnectBot SSH Library + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.connectbot.sshlib.protocol + +import kotlinx.coroutines.sync.Mutex +import kotlinx.coroutines.sync.withLock +import ru.nsk.kstatemachine.event.Event +import ru.nsk.kstatemachine.metainfo.MetaInfo +import ru.nsk.kstatemachine.state.IState +import ru.nsk.kstatemachine.state.State +import ru.nsk.kstatemachine.state.finalState +import ru.nsk.kstatemachine.state.initialState +import ru.nsk.kstatemachine.state.onEntry +import ru.nsk.kstatemachine.state.state +import ru.nsk.kstatemachine.state.transition +import ru.nsk.kstatemachine.statemachine.ProcessingResult +import ru.nsk.kstatemachine.statemachine.StateMachine +import ru.nsk.kstatemachine.statemachine.createStdLibStateMachine +import ru.nsk.kstatemachine.transition.onTriggered + +/** + * The protocol-visible lifecycle of one SSH connection-layer channel. + * + * EOF is directional. Sending EOF only closes the local-to-remote data direction, while receiving + * EOF only closes the remote-to-local direction. CLOSE terminates both directions; after sending + * CLOSE, the channel remains in [CLOSE_SENT] until the peer's CLOSE arrives or the connection is + * disconnected. + */ +internal enum class SshChannelState { + OPENING, + OPEN, + LOCAL_EOF, + REMOTE_EOF, + BOTH_EOF, + CLOSE_SENT, + CLOSED, +} + +internal enum class SshChannelEffect { + ADJUST_WINDOW, + CLOSE_CHANNEL, + CLOSE_INBOUND_STREAMS, + COMPLETE_OPEN, + DELIVER_DATA, + DELIVER_REQUEST, + FAIL_OPEN, + SEND_CLOSE, + SEND_DATA, + SEND_EOF, + SEND_OPEN, + SEND_OPEN_CONFIRMATION, + SEND_REQUEST, +} + +internal enum class SshChannelConstructionId { + ALLOCATE_LOCAL_OPEN, + ACCEPT_REMOTE_OPEN, +} + +internal enum class SshChannelEventId( + val tlaName: String, +) { + ACCEPT_REMOTE_OPEN("AcceptRemoteOpen"), + ALLOCATE_LOCAL_OPEN("AllocateLocalOpen"), + DISCONNECT("Disconnect"), + OPEN_CONFIRMED("OpenConfirmed"), + OPEN_FAILED("OpenFailed"), + RECEIVE_CLOSE("ReceiveClose"), + RECEIVE_DATA("ReceiveData"), + RECEIVE_EOF("ReceiveEof"), + RECEIVE_REQUEST("ReceiveRequest"), + RECEIVE_WINDOW_ADJUST("ReceiveWindowAdjust"), + SEND_CLOSE("SendClose"), + SEND_DATA("SendData"), + SEND_EOF("SendEof"), + SEND_REQUEST("SendRequest"), +} + +internal enum class SshChannelEventOrigin { + CONNECTION_CONTROL, + LOCAL_COMMAND, + PARSED_PACKET, +} + +internal enum class SshChannelOperationScope { + CHANNEL_ATTEMPT, + CONNECTION_TRANSITION, + CONNECTION_TEARDOWN, +} + +/** Stable transition identifiers used by runtime tests and, later, TLA+ generation. */ +internal enum class SshChannelTransitionId { + OPEN_CONFIRMED, + OPEN_FAILED, + SEND_DATA_OPEN, + SEND_DATA_REMOTE_EOF, + RECEIVE_DATA_OPEN, + RECEIVE_DATA_LOCAL_EOF, + SEND_REQUEST_OPEN, + SEND_REQUEST_LOCAL_EOF, + SEND_REQUEST_REMOTE_EOF, + SEND_REQUEST_BOTH_EOF, + RECEIVE_REQUEST_OPEN, + RECEIVE_REQUEST_LOCAL_EOF, + RECEIVE_REQUEST_REMOTE_EOF, + RECEIVE_REQUEST_BOTH_EOF, + RECEIVE_WINDOW_ADJUST_OPEN, + RECEIVE_WINDOW_ADJUST_LOCAL_EOF, + RECEIVE_WINDOW_ADJUST_REMOTE_EOF, + RECEIVE_WINDOW_ADJUST_BOTH_EOF, + SEND_EOF_OPEN, + SEND_EOF_REMOTE_EOF, + RECEIVE_EOF_OPEN, + RECEIVE_EOF_LOCAL_EOF, + SEND_CLOSE_OPEN, + SEND_CLOSE_LOCAL_EOF, + SEND_CLOSE_REMOTE_EOF, + SEND_CLOSE_BOTH_EOF, + RECEIVE_CLOSE_OPEN, + RECEIVE_CLOSE_LOCAL_EOF, + RECEIVE_CLOSE_REMOTE_EOF, + RECEIVE_CLOSE_BOTH_EOF, + RECEIVE_CLOSE_CLOSE_SENT, + DISCONNECT_OPENING, + DISCONNECT_OPEN, + DISCONNECT_LOCAL_EOF, + DISCONNECT_REMOTE_EOF, + DISCONNECT_BOTH_EOF, + DISCONNECT_CLOSE_SENT, +} + +internal data class SshChannelTransitionMeta( + val id: SshChannelTransitionId, + val eventId: SshChannelEventId, + val source: SshChannelState, + val target: SshChannelState, + val effects: Set, + val origin: SshChannelEventOrigin, + val scope: SshChannelOperationScope, + val requiresAuthenticatedConnection: Boolean, +) : MetaInfo + +internal data class SshChannelAcceptedTransition( + val id: SshChannelTransitionId, + val effects: Set, + val origin: SshChannelEventOrigin, +) + +internal data class SshChannelFormalTransition( + val id: SshChannelTransitionId, + val eventId: SshChannelEventId, + val source: SshChannelState, + val target: SshChannelState, + val effects: Set, + val origin: SshChannelEventOrigin, + val scope: SshChannelOperationScope, + val requiresAuthenticatedConnection: Boolean, +) { + val eventName: String + get() = eventId.tlaName +} + +internal data class SshChannelFormalOperation( + val id: String, + val eventId: SshChannelEventId, + val sourceStateName: String, + val targetStateName: String, + val effects: Set, + val origin: SshChannelEventOrigin, + val scope: SshChannelOperationScope, + val requiresAuthenticatedConnection: Boolean, +) { + val eventName: String + get() = eventId.tlaName +} + +internal data class SshChannelFormalModel( + val states: Set, + val transitions: List, + val operations: List, + val unallocatedStateName: String, + val rejectedOperationEffects: Set, +) { + init { + require(states == SshChannelState.entries.toSet()) + require(transitions.map(SshChannelFormalTransition::id).toSet() == SshChannelTransitionId.entries.toSet()) + require(transitions.map(SshChannelFormalTransition::id).distinct().size == transitions.size) + require(operations.map(SshChannelFormalOperation::id).distinct().size == operations.size) + require(operations.mapTo(mutableSetOf(), SshChannelFormalOperation::eventId) == SshChannelEventId.entries.toSet()) + require( + operations.groupBy(SshChannelFormalOperation::eventId).values.all { variants -> + variants.map(SshChannelFormalOperation::origin).distinct().size == 1 + }, + ) { "Every channel event must have exactly one typed origin" } + require(operations.count { it.scope == SshChannelOperationScope.CHANNEL_ATTEMPT } > 0) + } +} + +/** + * Per-channel KStateMachine source of truth. + * + * [process] serializes event delivery because inbound packets and application calls may arrive on + * different coroutines. Effects are executed by the accepted transition's callback while that + * serialization lock is held. Rejected events therefore cannot execute their supplied effect. + */ +internal class SshChannelStateMachine( + initialState: SshChannelState, +) { + init { + require(initialState == SshChannelState.OPENING || initialState == SshChannelState.OPEN) { + "A channel must be created while opening or already open" + } + } + + private sealed class ChannelEvent( + val id: SshChannelEventId, + val effects: Set, + val origin: SshChannelEventOrigin, + val action: suspend (SshChannelAcceptedTransition) -> Unit, + val scope: SshChannelOperationScope = SshChannelOperationScope.CHANNEL_ATTEMPT, + val requiresAuthenticatedConnection: Boolean = true, + ) : Event { + class OpenConfirmed(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.OPEN_CONFIRMED, + setOf(SshChannelEffect.COMPLETE_OPEN), + SshChannelEventOrigin.PARSED_PACKET, + action, + scope = SshChannelOperationScope.CONNECTION_TRANSITION, + ) + class OpenFailed(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.OPEN_FAILED, + setOf(SshChannelEffect.FAIL_OPEN), + SshChannelEventOrigin.PARSED_PACKET, + action, + scope = SshChannelOperationScope.CONNECTION_TRANSITION, + ) + class SendData(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.SEND_DATA, + setOf(SshChannelEffect.SEND_DATA), + SshChannelEventOrigin.LOCAL_COMMAND, + action, + ) + class ReceiveData(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.RECEIVE_DATA, + setOf(SshChannelEffect.DELIVER_DATA), + SshChannelEventOrigin.PARSED_PACKET, + action, + ) + class SendRequest(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.SEND_REQUEST, + setOf(SshChannelEffect.SEND_REQUEST), + SshChannelEventOrigin.LOCAL_COMMAND, + action, + scope = SshChannelOperationScope.CONNECTION_TRANSITION, + ) + class ReceiveRequest(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.RECEIVE_REQUEST, + setOf(SshChannelEffect.DELIVER_REQUEST), + SshChannelEventOrigin.PARSED_PACKET, + action, + ) + class ReceiveWindowAdjust(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.RECEIVE_WINDOW_ADJUST, + setOf(SshChannelEffect.ADJUST_WINDOW), + SshChannelEventOrigin.PARSED_PACKET, + action, + ) + class SendEof(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.SEND_EOF, + setOf(SshChannelEffect.SEND_EOF), + SshChannelEventOrigin.LOCAL_COMMAND, + action, + ) + class ReceiveEof(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.RECEIVE_EOF, + setOf(SshChannelEffect.CLOSE_INBOUND_STREAMS), + SshChannelEventOrigin.PARSED_PACKET, + action, + ) + class SendClose(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.SEND_CLOSE, + setOf(SshChannelEffect.SEND_CLOSE, SshChannelEffect.CLOSE_CHANNEL), + SshChannelEventOrigin.LOCAL_COMMAND, + action, + ) + class ReceiveClose(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.RECEIVE_CLOSE, + setOf(SshChannelEffect.SEND_CLOSE, SshChannelEffect.CLOSE_CHANNEL), + SshChannelEventOrigin.PARSED_PACKET, + action, + ) + class Disconnect(action: suspend (SshChannelAcceptedTransition) -> Unit) : + ChannelEvent( + SshChannelEventId.DISCONNECT, + setOf(SshChannelEffect.CLOSE_CHANNEL), + SshChannelEventOrigin.CONNECTION_CONTROL, + action, + scope = SshChannelOperationScope.CONNECTION_TEARDOWN, + requiresAuthenticatedConnection = false, + ) + } + + private val eventMutex = Mutex() + + @Volatile + private var activeState = initialState + + private val stateMachine: StateMachine = createStdLibStateMachine { + lateinit var opening: State + lateinit var open: State + + if (initialState == SshChannelState.OPENING) { + opening = initialState(SshChannelState.OPENING.name) + open = state(SshChannelState.OPEN.name) + } else { + opening = state(SshChannelState.OPENING.name) + open = initialState(SshChannelState.OPEN.name) + } + + val localEof = state(SshChannelState.LOCAL_EOF.name) + val remoteEof = state(SshChannelState.REMOTE_EOF.name) + val bothEof = state(SshChannelState.BOTH_EOF.name) + val closeSent = state(SshChannelState.CLOSE_SENT.name) + val closed = finalState(SshChannelState.CLOSED.name) + + bindState(opening, SshChannelState.OPENING) + bindState(open, SshChannelState.OPEN) + bindState(localEof, SshChannelState.LOCAL_EOF) + bindState(remoteEof, SshChannelState.REMOTE_EOF) + bindState(bothEof, SshChannelState.BOTH_EOF) + bindState(closeSent, SshChannelState.CLOSE_SENT) + bindState(closed, SshChannelState.CLOSED) + + opening.channelTransition(ChannelEvent.OpenConfirmed {}, SshChannelTransitionId.OPEN_CONFIRMED, open) + opening.channelTransition(ChannelEvent.OpenFailed {}, SshChannelTransitionId.OPEN_FAILED, closed) + + open.channelTransition(ChannelEvent.SendData {}, SshChannelTransitionId.SEND_DATA_OPEN) + remoteEof.channelTransition(ChannelEvent.SendData {}, SshChannelTransitionId.SEND_DATA_REMOTE_EOF) + open.channelTransition(ChannelEvent.ReceiveData {}, SshChannelTransitionId.RECEIVE_DATA_OPEN) + localEof.channelTransition(ChannelEvent.ReceiveData {}, SshChannelTransitionId.RECEIVE_DATA_LOCAL_EOF) + + open.channelTransition(ChannelEvent.SendRequest {}, SshChannelTransitionId.SEND_REQUEST_OPEN) + localEof.channelTransition(ChannelEvent.SendRequest {}, SshChannelTransitionId.SEND_REQUEST_LOCAL_EOF) + remoteEof.channelTransition(ChannelEvent.SendRequest {}, SshChannelTransitionId.SEND_REQUEST_REMOTE_EOF) + bothEof.channelTransition(ChannelEvent.SendRequest {}, SshChannelTransitionId.SEND_REQUEST_BOTH_EOF) + open.channelTransition(ChannelEvent.ReceiveRequest {}, SshChannelTransitionId.RECEIVE_REQUEST_OPEN) + localEof.channelTransition(ChannelEvent.ReceiveRequest {}, SshChannelTransitionId.RECEIVE_REQUEST_LOCAL_EOF) + remoteEof.channelTransition(ChannelEvent.ReceiveRequest {}, SshChannelTransitionId.RECEIVE_REQUEST_REMOTE_EOF) + bothEof.channelTransition(ChannelEvent.ReceiveRequest {}, SshChannelTransitionId.RECEIVE_REQUEST_BOTH_EOF) + + open.channelTransition(ChannelEvent.ReceiveWindowAdjust {}, SshChannelTransitionId.RECEIVE_WINDOW_ADJUST_OPEN) + localEof.channelTransition(ChannelEvent.ReceiveWindowAdjust {}, SshChannelTransitionId.RECEIVE_WINDOW_ADJUST_LOCAL_EOF) + remoteEof.channelTransition(ChannelEvent.ReceiveWindowAdjust {}, SshChannelTransitionId.RECEIVE_WINDOW_ADJUST_REMOTE_EOF) + bothEof.channelTransition(ChannelEvent.ReceiveWindowAdjust {}, SshChannelTransitionId.RECEIVE_WINDOW_ADJUST_BOTH_EOF) + + open.channelTransition(ChannelEvent.SendEof {}, SshChannelTransitionId.SEND_EOF_OPEN, localEof) + remoteEof.channelTransition(ChannelEvent.SendEof {}, SshChannelTransitionId.SEND_EOF_REMOTE_EOF, bothEof) + open.channelTransition(ChannelEvent.ReceiveEof {}, SshChannelTransitionId.RECEIVE_EOF_OPEN, remoteEof) + localEof.channelTransition(ChannelEvent.ReceiveEof {}, SshChannelTransitionId.RECEIVE_EOF_LOCAL_EOF, bothEof) + + open.channelTransition(ChannelEvent.SendClose {}, SshChannelTransitionId.SEND_CLOSE_OPEN, closeSent) + localEof.channelTransition(ChannelEvent.SendClose {}, SshChannelTransitionId.SEND_CLOSE_LOCAL_EOF, closeSent) + remoteEof.channelTransition(ChannelEvent.SendClose {}, SshChannelTransitionId.SEND_CLOSE_REMOTE_EOF, closeSent) + bothEof.channelTransition(ChannelEvent.SendClose {}, SshChannelTransitionId.SEND_CLOSE_BOTH_EOF, closeSent) + + open.channelTransition(ChannelEvent.ReceiveClose {}, SshChannelTransitionId.RECEIVE_CLOSE_OPEN, closed) + 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.ReceiveClose {}, + SshChannelTransitionId.RECEIVE_CLOSE_CLOSE_SENT, + closed, + effects = setOf(SshChannelEffect.CLOSE_CHANNEL), + ) + + opening.channelTransition(ChannelEvent.Disconnect {}, SshChannelTransitionId.DISCONNECT_OPENING, closed) + open.channelTransition(ChannelEvent.Disconnect {}, SshChannelTransitionId.DISCONNECT_OPEN, closed) + localEof.channelTransition(ChannelEvent.Disconnect {}, SshChannelTransitionId.DISCONNECT_LOCAL_EOF, closed) + remoteEof.channelTransition(ChannelEvent.Disconnect {}, SshChannelTransitionId.DISCONNECT_REMOTE_EOF, closed) + bothEof.channelTransition(ChannelEvent.Disconnect {}, SshChannelTransitionId.DISCONNECT_BOTH_EOF, closed) + closeSent.channelTransition(ChannelEvent.Disconnect {}, SshChannelTransitionId.DISCONNECT_CLOSE_SENT, closed) + } + + val state: SshChannelState + get() = activeState + + val isOpen: Boolean + get() = activeState !in setOf(SshChannelState.CLOSE_SENT, SshChannelState.CLOSED) + + suspend fun openConfirmed(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.OpenConfirmed(action)) + suspend fun openFailed(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.OpenFailed(action)) + suspend fun sendData(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.SendData(action)) + suspend fun receiveData(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.ReceiveData(action)) + suspend fun sendRequest(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.SendRequest(action)) + suspend fun receiveRequest(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.ReceiveRequest(action)) + suspend fun receiveWindowAdjust(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.ReceiveWindowAdjust(action)) + suspend fun sendEof(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.SendEof(action)) + suspend fun receiveEof(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.ReceiveEof(action)) + suspend fun sendClose(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.SendClose(action)) + suspend fun receiveClose(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.ReceiveClose(action)) + suspend fun disconnect(action: suspend (SshChannelAcceptedTransition) -> Unit) = process(ChannelEvent.Disconnect(action)) + + internal fun formalModel(): SshChannelFormalModel { + val states = collectChannelStates(stateMachine) + val transitions = states.flatMap { state -> + state.transitions.mapNotNull { transition -> + val meta = transition.metaInfo as? SshChannelTransitionMeta ?: return@mapNotNull null + SshChannelFormalTransition( + meta.id, + meta.eventId, + meta.source, + meta.target, + meta.effects, + meta.origin, + meta.scope, + meta.requiresAuthenticatedConnection, + ) + } + } + val runtimeOperations = transitions.map { transition -> + SshChannelFormalOperation( + id = transition.id.name, + eventId = transition.eventId, + sourceStateName = transition.source.name, + targetStateName = transition.target.name, + effects = transition.effects, + origin = transition.origin, + scope = transition.scope, + requiresAuthenticatedConnection = transition.requiresAuthenticatedConnection, + ) + } + val constructionOperations = listOf( + SshChannelFormalOperation( + id = SshChannelConstructionId.ALLOCATE_LOCAL_OPEN.name, + eventId = SshChannelEventId.ALLOCATE_LOCAL_OPEN, + sourceStateName = UNALLOCATED_STATE, + targetStateName = SshChannelState.OPENING.name, + effects = setOf(SshChannelEffect.SEND_OPEN), + origin = SshChannelEventOrigin.LOCAL_COMMAND, + scope = SshChannelOperationScope.CONNECTION_TRANSITION, + requiresAuthenticatedConnection = true, + ), + SshChannelFormalOperation( + id = SshChannelConstructionId.ACCEPT_REMOTE_OPEN.name, + eventId = SshChannelEventId.ACCEPT_REMOTE_OPEN, + sourceStateName = UNALLOCATED_STATE, + targetStateName = SshChannelState.OPEN.name, + effects = setOf(SshChannelEffect.SEND_OPEN_CONFIRMATION), + origin = SshChannelEventOrigin.PARSED_PACKET, + scope = SshChannelOperationScope.CHANNEL_ATTEMPT, + requiresAuthenticatedConnection = true, + ), + ) + return SshChannelFormalModel( + states = states.mapNotNullTo(mutableSetOf()) { it.name?.let(SshChannelState::valueOf) }, + transitions = transitions, + operations = runtimeOperations + constructionOperations, + unallocatedStateName = UNALLOCATED_STATE, + rejectedOperationEffects = emptySet(), + ) + } + + private suspend fun process(event: ChannelEvent): Boolean = eventMutex.withLock { + stateMachine.processEvent(event) == ProcessingResult.PROCESSED + } + + private fun bindState(state: IState, lifecycleState: SshChannelState) { + state.onEntry { activeState = lifecycleState } + } + + private inline fun IState.channelTransition( + event: E, + id: SshChannelTransitionId, + target: State? = null, + effects: Set = event.effects, + ) { + transition(id.name) { + targetState = target + metaInfo = SshChannelTransitionMeta( + id = id, + eventId = event.id, + source = SshChannelState.valueOf(requireNotNull(this@channelTransition.name)), + target = target?.name?.let(SshChannelState::valueOf) + ?: SshChannelState.valueOf(requireNotNull(this@channelTransition.name)), + effects = effects, + origin = event.origin, + scope = event.scope, + requiresAuthenticatedConnection = event.requiresAuthenticatedConnection, + ) + }.onTriggered { + it.event.action(SshChannelAcceptedTransition(id, effects, event.origin)) + } + } + + companion object { + private const val UNALLOCATED_STATE = "Unallocated" + } +} + +private fun collectChannelStates(root: IState): List = buildList { + add(root) + root.states.forEach { addAll(collectChannelStates(it)) } +} diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt index aebe2b9d..68af679b 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt @@ -20,6 +20,8 @@ package org.connectbot.sshlib.protocol import ru.nsk.kstatemachine.event.Event import ru.nsk.kstatemachine.state.HistoryState import ru.nsk.kstatemachine.state.HistoryType +import ru.nsk.kstatemachine.state.IState +import ru.nsk.kstatemachine.state.State import ru.nsk.kstatemachine.state.activeStates import ru.nsk.kstatemachine.state.finalState import ru.nsk.kstatemachine.state.historyState @@ -32,6 +34,7 @@ import ru.nsk.kstatemachine.state.transition import ru.nsk.kstatemachine.statemachine.ProcessingResult import ru.nsk.kstatemachine.statemachine.StateMachine import ru.nsk.kstatemachine.statemachine.createStdLibStateMachine +import ru.nsk.kstatemachine.transition.TransitionParams import ru.nsk.kstatemachine.transition.onTriggered /** @@ -57,6 +60,10 @@ import ru.nsk.kstatemachine.transition.onTriggered internal class SshClientStateMachine( private val callbacks: SshClientCallbacks, ) { + private val parsedPacket = setOf(SshEventOrigin.PARSED_PACKET) + private val localCommand = setOf(SshEventOrigin.LOCAL_COMMAND) + private val rekeying = SshFormalGuard.Fact(SshBooleanFact.REKEYING) + private sealed class SshEvent : Event { object Connect : SshEvent() data class ReceiveVersion(val banner: IdBanner) : SshEvent() @@ -99,6 +106,7 @@ internal class SshClientStateMachine( object AuthorizeExtInfo : SshEvent() object Disconnect : SshEvent() object RekeyStarted : SshEvent() + data class UnexpectedKexInit(val description: String) : SshEvent() } private val stateMachine: StateMachine = createStdLibStateMachine { @@ -121,76 +129,119 @@ internal class SshClientStateMachine( onEntry { callbacks.onStateEnter("AuthenticationReady") } onExit { callbacks.onStateExit("AuthenticationReady") } - transition { - targetState = authenticating - } - transition { - onTriggered { callbacks.receiveUserauthBanner(it.event.msg) } - } + formalTransition( + id = SshTransitionId.BEGIN_AUTHENTICATION, + targetState = authenticating, + guard = !SshFormalGuard.Fact(SshBooleanFact.AUTH_REQUEST_PENDING), + origins = localCommand, + effects = setOf(SshEffect.SEND_USERAUTH_REQUEST), + ) { callbacks.authenticationRequestStarted() } + formalTransition( + id = SshTransitionId.RECEIVE_USERAUTH_BANNER_READY, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_USERAUTH_BANNER), + ) { callbacks.receiveUserauthBanner(it.event.msg) } } authenticating { onEntry { callbacks.onStateEnter("Authenticating") } onExit { callbacks.onStateExit("Authenticating") } - transition {} - transition { - targetState = authenticated - onTriggered { callbacks.authenticationSuccess() } - } - transition { - targetState = authenticationReady - onTriggered { callbacks.authenticationFailure() } - } - transition { - onTriggered { callbacks.receiveUserauthInfoRequest(it.event.msg) } - } - transition { - onTriggered { callbacks.receiveUserauthBanner(it.event.msg) } - } - transition {} + formalTransition( + id = SshTransitionId.REPEAT_BEGIN_AUTHENTICATION, + guard = !SshFormalGuard.Fact(SshBooleanFact.AUTH_REQUEST_PENDING), + origins = localCommand, + effects = setOf(SshEffect.SEND_USERAUTH_REQUEST), + ) { callbacks.authenticationRequestStarted() } + formalTransition( + id = SshTransitionId.AUTHENTICATION_SUCCESS, + targetState = authenticated, + origins = parsedPacket, + effects = setOf(SshEffect.AUTHENTICATION_SUCCESS), + ) { callbacks.authenticationSuccess() } + formalTransition( + id = SshTransitionId.AUTHENTICATION_FAILURE, + targetState = authenticationReady, + origins = parsedPacket, + effects = setOf(SshEffect.AUTHENTICATION_FAILURE), + ) { callbacks.authenticationFailure() } + formalTransition( + id = SshTransitionId.RECEIVE_USERAUTH_INFO_REQUEST, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_USERAUTH_INFO_REQUEST), + ) { callbacks.receiveUserauthInfoRequest(it.event.msg) } + formalTransition( + id = SshTransitionId.RECEIVE_USERAUTH_BANNER_AUTHENTICATING, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_USERAUTH_BANNER), + ) { callbacks.receiveUserauthBanner(it.event.msg) } + formalTransition( + id = SshTransitionId.AUTHORIZE_AUTHENTICATION_PACKET, + origins = parsedPacket, + ) { callbacks.authenticationRequestResponseReceived() } } authenticated { onEntry { callbacks.onStateEnter("Authenticated") } onExit { callbacks.onStateExit("Authenticated") } - transition {} - transition { - onTriggered { callbacks.receiveGlobalRequest(it.event.msg) } - } - transition { - onTriggered { - callbacks.sendChannelOpen( - it.event.channelType, - it.event.localChannelNumber, - it.event.initialWindowSize, - it.event.maxPacketSize, - ) - } - } - transition { - onTriggered { callbacks.receiveChannelOpenConfirmation(it.event.msg) } + formalTransition( + id = SshTransitionId.AUTHORIZE_AUTHENTICATED_PACKET, + origins = parsedPacket, + ) + formalTransition( + id = SshTransitionId.RECEIVE_GLOBAL_REQUEST, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_GLOBAL_REQUEST), + ) { callbacks.receiveGlobalRequest(it.event.msg) } + formalTransition( + id = SshTransitionId.OPEN_CHANNEL, + origins = localCommand, + effects = setOf(SshEffect.SEND_CHANNEL_OPEN), + channelOperationEvent = SshChannelEventId.ALLOCATE_LOCAL_OPEN, + ) { + callbacks.sendChannelOpen( + it.event.channelType, + it.event.localChannelNumber, + it.event.initialWindowSize, + it.event.maxPacketSize, + ) } - transition { - onTriggered { callbacks.receiveChannelOpenFailure(it.event.msg) } - } - transition { - onTriggered { - callbacks.sendChannelRequest( - it.event.recipientChannel, - it.event.requestType, - it.event.wantReply, - it.event.message, - ) - } - } - transition { - onTriggered { callbacks.receiveChannelSuccess(it.event.recipientChannel) } - } - transition { - onTriggered { callbacks.receiveChannelFailure(it.event.recipientChannel) } + formalTransition( + id = SshTransitionId.RECEIVE_CHANNEL_OPEN_CONFIRMATION, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_CHANNEL_OPEN_CONFIRMATION), + channelOperationEvent = SshChannelEventId.OPEN_CONFIRMED, + ) { callbacks.receiveChannelOpenConfirmation(it.event.msg) } + formalTransition( + id = SshTransitionId.RECEIVE_CHANNEL_OPEN_FAILURE, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_CHANNEL_OPEN_FAILURE), + channelOperationEvent = SshChannelEventId.OPEN_FAILED, + ) { callbacks.receiveChannelOpenFailure(it.event.msg) } + formalTransition( + id = SshTransitionId.SEND_CHANNEL_REQUEST, + origins = localCommand, + effects = setOf(SshEffect.SEND_CHANNEL_REQUEST), + channelOperationEvent = SshChannelEventId.SEND_REQUEST, + ) { + callbacks.sendChannelRequest( + it.event.recipientChannel, + it.event.requestType, + it.event.wantReply, + it.event.message, + ) } + formalTransition( + id = SshTransitionId.RECEIVE_CHANNEL_SUCCESS, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_CHANNEL_SUCCESS), + ) { callbacks.receiveChannelSuccess(it.event.recipientChannel) } + formalTransition( + id = SshTransitionId.RECEIVE_CHANNEL_FAILURE, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_CHANNEL_FAILURE), + ) { callbacks.receiveChannelFailure(it.event.recipientChannel) } } postAuthHistory = historyState( @@ -199,37 +250,49 @@ internal class SshClientStateMachine( historyType = HistoryType.DEEP, ) - transition { - targetState = waitKexInit - onTriggered { - callbacks.rekeyStarted() - callbacks.sendKexInit() - } + formalTransition( + id = SshTransitionId.REKEY_STARTED, + targetState = waitKexInit, + origins = setOf(SshEventOrigin.LOCAL_COMMAND, SshEventOrigin.PARSED_PACKET, SshEventOrigin.TIMER), + effects = setOf(SshEffect.REKEY_STARTED, SshEffect.SEND_KEX_INIT), + ) { + callbacks.rekeyStarted() + callbacks.sendKexInit() } - transition {} - transition {} + formalTransition( + id = SshTransitionId.AUTHORIZE_POST_AUTH_EXT_INFO, + origins = parsedPacket, + ) + formalTransition( + id = SshTransitionId.AUTHORIZE_CONNECTION_PACKET, + origins = parsedPacket, + ) } initialState("Unconnected") { onEntry { callbacks.onStateEnter("Unconnected") } onExit { callbacks.onStateExit("Unconnected") } - transition { - targetState = waitVersion - onTriggered { callbacks.sendVersion() } - } + formalTransition( + id = SshTransitionId.CONNECT, + targetState = waitVersion, + origins = localCommand, + effects = setOf(SshEffect.SEND_VERSION), + ) { callbacks.sendVersion() } } waitVersion { onEntry { callbacks.onStateEnter("WaitVersion") } onExit { callbacks.onStateExit("WaitVersion") } - transition { - targetState = waitKexInit - onTriggered { - callbacks.receiveVersion(it.event.banner) - callbacks.sendKexInit() - } + formalTransition( + id = SshTransitionId.RECEIVE_VERSION, + targetState = waitKexInit, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_VERSION, SshEffect.SEND_KEX_INIT), + ) { + callbacks.receiveVersion(it.event.banner) + callbacks.sendKexInit() } } @@ -237,12 +300,14 @@ internal class SshClientStateMachine( onEntry { callbacks.onStateEnter("WaitKexInit") } onExit { callbacks.onStateExit("WaitKexInit") } - transition { - targetState = waitKex - onTriggered { - callbacks.receiveKexInit(it.event.msg) - callbacks.sendKexExchangeInit() - } + formalTransition( + id = SshTransitionId.RECEIVE_KEX_INIT, + targetState = waitKex, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_KEX_INIT, SshEffect.SEND_KEX_EXCHANGE_INIT), + ) { + callbacks.receiveKexInit(it.event.msg) + callbacks.sendKexExchangeInit() } } @@ -250,87 +315,164 @@ internal class SshClientStateMachine( onEntry { callbacks.onStateEnter("WaitKex") } onExit { callbacks.onStateExit("WaitKex") } - transition { - targetState = waitNewKeys - onTriggered { - callbacks.receiveKexDhReply(it.event.msg) - callbacks.sendNewKeys() - } - } - transition { - targetState = waitNewKeys - onTriggered { - callbacks.receiveKexEcdhReply(it.event.msg) - callbacks.sendNewKeys() - } + formalTransition( + id = SshTransitionId.RECEIVE_KEX_DH_REPLY, + targetState = waitNewKeys, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_KEX_DH_REPLY, SshEffect.SEND_NEW_KEYS), + ) { + callbacks.receiveKexDhReply(it.event.msg) + callbacks.sendNewKeys() } - transition { - targetState = waitKexDhGexInit - onTriggered { callbacks.sendKexDhGexInit() } + formalTransition( + id = SshTransitionId.RECEIVE_KEX_ECDH_REPLY, + targetState = waitNewKeys, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_KEX_ECDH_REPLY, SshEffect.SEND_NEW_KEYS), + ) { + callbacks.receiveKexEcdhReply(it.event.msg) + callbacks.sendNewKeys() } + formalTransition( + id = SshTransitionId.RECEIVE_KEX_DH_GEX_GROUP, + targetState = waitKexDhGexInit, + origins = parsedPacket, + effects = setOf(SshEffect.SEND_KEX_DH_GEX_INIT), + ) { callbacks.sendKexDhGexInit() } + formalTransition( + id = SshTransitionId.UNEXPECTED_KEX_INIT_WAIT_KEX, + targetState = disconnected, + origins = parsedPacket, + effects = setOf(SshEffect.SEND_PROTOCOL_ERROR, SshEffect.DISCONNECT), + ) { callbacks.sendProtocolError(it.event.description) } } waitKexDhGexInit { onEntry { callbacks.onStateEnter("WaitKexDhGexInit") } onExit { callbacks.onStateExit("WaitKexDhGexInit") } - transition { - targetState = waitNewKeys - onTriggered { - callbacks.receiveKexDhGexReply(it.event.msg) - callbacks.sendNewKeys() - } + formalTransition( + id = SshTransitionId.RECEIVE_KEX_DH_GEX_REPLY, + targetState = waitNewKeys, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_KEX_DH_GEX_REPLY, SshEffect.SEND_NEW_KEYS), + ) { + callbacks.receiveKexDhGexReply(it.event.msg) + callbacks.sendNewKeys() } + formalTransition( + id = SshTransitionId.UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT, + targetState = disconnected, + origins = parsedPacket, + effects = setOf(SshEffect.SEND_PROTOCOL_ERROR, SshEffect.DISCONNECT), + ) { callbacks.sendProtocolError(it.event.description) } } waitNewKeys { onEntry { callbacks.onStateEnter("WaitNewKeys") } onExit { callbacks.onStateExit("WaitNewKeys") } - transition { - guard = { !callbacks.isRekeying() } - targetState = waitService - onTriggered { - callbacks.receiveNewKeys() - callbacks.activateEncryption() - callbacks.sendClientExtInfo() - callbacks.sendServiceRequest("ssh-userauth") - } + formalTransition( + id = SshTransitionId.RECEIVE_INITIAL_NEW_KEYS, + targetState = waitService, + guard = !rekeying, + origins = parsedPacket, + effects = setOf( + SshEffect.RECEIVE_NEW_KEYS, + SshEffect.ACTIVATE_ENCRYPTION, + SshEffect.SEND_CLIENT_EXT_INFO, + SshEffect.SEND_SERVICE_REQUEST, + ), + ) { + callbacks.receiveNewKeys() + callbacks.activateEncryption() + callbacks.sendClientExtInfo() + callbacks.sendServiceRequest("ssh-userauth") } - transition { - guard = { callbacks.isRekeying() } - targetState = postAuthHistory - onTriggered { - callbacks.receiveNewKeys() - callbacks.activateEncryption() - callbacks.rekeyComplete() - } + formalTransition( + id = SshTransitionId.RECEIVE_REKEY_NEW_KEYS, + targetState = postAuthHistory, + guard = rekeying, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_NEW_KEYS, SshEffect.ACTIVATE_ENCRYPTION, SshEffect.REKEY_COMPLETE), + ) { + callbacks.receiveNewKeys() + callbacks.activateEncryption() + callbacks.rekeyComplete() } + formalTransition( + id = SshTransitionId.UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS, + targetState = disconnected, + origins = parsedPacket, + effects = setOf(SshEffect.SEND_PROTOCOL_ERROR, SshEffect.DISCONNECT), + ) { callbacks.sendProtocolError(it.event.description) } } waitService { onEntry { callbacks.onStateEnter("WaitService") } onExit { callbacks.onStateExit("WaitService") } - transition { - targetState = postAuthenticated - onTriggered { - callbacks.receiveServiceAccept(it.event.service) - callbacks.startAuthentication() - } + formalTransition( + id = SshTransitionId.RECEIVE_SERVICE_ACCEPT, + targetState = postAuthenticated, + origins = parsedPacket, + effects = setOf(SshEffect.RECEIVE_SERVICE_ACCEPT, SshEffect.START_AUTHENTICATION), + ) { + callbacks.receiveServiceAccept(it.event.service) + callbacks.startAuthentication() } - transition {} + formalTransition( + id = SshTransitionId.AUTHORIZE_SERVICE_EXT_INFO, + origins = parsedPacket, + ) } - transition { - onTriggered { callbacks.debug(it.event.msg) } - } - transition { - onTriggered { callbacks.ignore() } + formalTransition( + id = SshTransitionId.RECEIVE_DEBUG, + origins = parsedPacket, + effects = setOf(SshEffect.DEBUG), + ) { callbacks.debug(it.event.msg) } + formalTransition( + id = SshTransitionId.RECEIVE_IGNORE, + origins = parsedPacket, + effects = setOf(SshEffect.IGNORE), + ) { callbacks.ignore() } + formalTransition( + id = SshTransitionId.DISCONNECT, + targetState = disconnected, + origins = parsedPacket, + effects = setOf(SshEffect.DISCONNECT), + ) { callbacks.disconnect() } + } + + private inline fun IState.formalTransition( + id: SshTransitionId, + targetState: State? = null, + guard: SshFormalGuard = SshFormalGuard.Always, + origins: Set, + effects: Set = emptySet(), + channelOperationEvent: SshChannelEventId? = null, + noinline action: (suspend (TransitionParams) -> Unit)? = null, + ) { + val meta = SshFormalTransitionMeta( + id = id, + eventClass = E::class, + targetStateName = targetState?.name, + targetIsHistory = targetState is HistoryState, + guard = guard, + origins = origins, + effects = effects, + channelOperationEvent = channelOperationEvent, + ) + val transition = transition(id.name) { + this.targetState = targetState + metaInfo = meta + if (guard != SshFormalGuard.Always) { + this.guard = { guard.evaluate(callbacks) } + } } - transition { - targetState = disconnected - onTriggered { callbacks.disconnect() } + if (action != null) { + transition.onTriggered(action) } } @@ -397,12 +539,18 @@ internal class SshClientStateMachine( suspend fun requestRekey(): Boolean = process(SshEvent.RekeyStarted) + suspend fun unexpectedKexInit(description: String): Boolean = process(SshEvent.UnexpectedKexInit(description)) + fun isPostAuthenticated(): Boolean = stateMachine.activeStates().any { it.name == "PostAuthenticated" } fun isKexInProgress(): Boolean = stateMachine.activeStates().any { it.name == "WaitKexInit" || it.name == "WaitKex" || it.name == "WaitKexDhGexInit" || it.name == "WaitNewKeys" } + fun isWaitingForKexInit(): Boolean = stateMachine.activeStates().any { it.name == "WaitKexInit" } + + internal fun formalModel(): SshStateMachineFormalModel = stateMachine.toSshFormalModel() + private suspend fun process(event: SshEvent): Boolean = stateMachine.processEvent(event) == ProcessingResult.PROCESSED } @@ -416,6 +564,9 @@ internal interface SshClientCallbacks { suspend fun receiveKexEcdhReply(msg: SshMsgKexEcdhReply) suspend fun receiveKexDhGexReply(msg: SshMsgKexDhGexReply) fun isRekeying(): Boolean + fun isAuthenticationRequestPending(): Boolean + fun authenticationRequestStarted() + fun authenticationRequestResponseReceived() fun rekeyStarted() fun rekeyComplete() suspend fun sendKexDhGexInit() @@ -431,8 +582,8 @@ internal interface SshClientCallbacks { fun receiveUserauthInfoRequest(msg: SshMsgUserauthInfoRequest) fun receiveUserauthBanner(msg: SshMsgUserauthBanner) suspend fun sendChannelOpen(channelType: String, localChannelNumber: Int, initialWindowSize: Int, maxPacketSize: Int) - fun receiveChannelOpenConfirmation(msg: SshMsgChannelOpenConfirmation) - fun receiveChannelOpenFailure(msg: SshMsgChannelOpenFailure) + suspend fun receiveChannelOpenConfirmation(msg: SshMsgChannelOpenConfirmation) + suspend fun receiveChannelOpenFailure(msg: SshMsgChannelOpenFailure) suspend fun sendChannelRequest(recipientChannel: Int, requestType: String, wantReply: Boolean, message: SshMsgChannelRequest) fun receiveChannelSuccess(recipientChannel: Int) fun receiveChannelFailure(recipientChannel: Int) @@ -440,6 +591,7 @@ internal interface SshClientCallbacks { fun debug(msg: SshMsgDebug) fun ignore() suspend fun disconnect() + suspend fun sendProtocolError(description: String) fun onStateEnter(stateName: String) fun onStateExit(stateName: String) } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt new file mode 100644 index 00000000..504a5e0b --- /dev/null +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt @@ -0,0 +1,617 @@ +/* + * ConnectBot SSH Library + * 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.connectbot.sshlib.protocol + +import ru.nsk.kstatemachine.event.Event +import ru.nsk.kstatemachine.event.StartEvent +import ru.nsk.kstatemachine.metainfo.MetaInfo +import ru.nsk.kstatemachine.state.FinalState +import ru.nsk.kstatemachine.state.HistoryState +import ru.nsk.kstatemachine.state.IState +import ru.nsk.kstatemachine.state.PseudoState +import ru.nsk.kstatemachine.statemachine.StateMachine +import java.security.MessageDigest +import kotlin.reflect.KClass + +internal enum class SshTransitionId { + BEGIN_AUTHENTICATION, + REPEAT_BEGIN_AUTHENTICATION, + AUTHENTICATION_SUCCESS, + AUTHENTICATION_FAILURE, + RECEIVE_USERAUTH_INFO_REQUEST, + RECEIVE_USERAUTH_BANNER_READY, + RECEIVE_USERAUTH_BANNER_AUTHENTICATING, + AUTHORIZE_AUTHENTICATION_PACKET, + AUTHORIZE_AUTHENTICATED_PACKET, + RECEIVE_GLOBAL_REQUEST, + OPEN_CHANNEL, + RECEIVE_CHANNEL_OPEN_CONFIRMATION, + RECEIVE_CHANNEL_OPEN_FAILURE, + SEND_CHANNEL_REQUEST, + RECEIVE_CHANNEL_SUCCESS, + RECEIVE_CHANNEL_FAILURE, + REKEY_STARTED, + AUTHORIZE_POST_AUTH_EXT_INFO, + AUTHORIZE_CONNECTION_PACKET, + CONNECT, + RECEIVE_VERSION, + RECEIVE_KEX_INIT, + RECEIVE_KEX_DH_REPLY, + RECEIVE_KEX_ECDH_REPLY, + RECEIVE_KEX_DH_GEX_GROUP, + RECEIVE_KEX_DH_GEX_REPLY, + RECEIVE_INITIAL_NEW_KEYS, + RECEIVE_REKEY_NEW_KEYS, + RECEIVE_SERVICE_ACCEPT, + AUTHORIZE_SERVICE_EXT_INFO, + RECEIVE_DEBUG, + RECEIVE_IGNORE, + UNEXPECTED_KEX_INIT_WAIT_KEX, + UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT, + UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS, + DISCONNECT, +} + +internal enum class SshEventOrigin { + INTERNAL, + LOCAL_COMMAND, + PARSED_PACKET, + TIMER, +} + +internal enum class SshEffect { + ACTIVATE_ENCRYPTION, + AUTHENTICATION_FAILURE, + AUTHENTICATION_SUCCESS, + DEBUG, + DISCONNECT, + IGNORE, + RECEIVE_CHANNEL_FAILURE, + RECEIVE_CHANNEL_OPEN_CONFIRMATION, + RECEIVE_CHANNEL_OPEN_FAILURE, + RECEIVE_CHANNEL_SUCCESS, + RECEIVE_GLOBAL_REQUEST, + RECEIVE_KEX_DH_GEX_REPLY, + RECEIVE_KEX_DH_REPLY, + RECEIVE_KEX_ECDH_REPLY, + RECEIVE_KEX_INIT, + RECEIVE_NEW_KEYS, + RECEIVE_SERVICE_ACCEPT, + RECEIVE_USERAUTH_BANNER, + RECEIVE_USERAUTH_INFO_REQUEST, + RECEIVE_VERSION, + REKEY_COMPLETE, + REKEY_STARTED, + SEND_CHANNEL_OPEN, + SEND_CHANNEL_REQUEST, + SEND_CLIENT_EXT_INFO, + SEND_KEX_DH_GEX_INIT, + SEND_KEX_EXCHANGE_INIT, + SEND_KEX_INIT, + SEND_NEW_KEYS, + SEND_SERVICE_REQUEST, + SEND_PROTOCOL_ERROR, + SEND_USERAUTH_REQUEST, + SEND_VERSION, + START_AUTHENTICATION, +} + +internal enum class SshBooleanFact( + val tlaName: String, +) { + AUTH_REQUEST_PENDING("authRequestPending"), + REKEYING("rekeying"), + ; + + fun evaluate(callbacks: SshClientCallbacks): Boolean = when (this) { + AUTH_REQUEST_PENDING -> callbacks.isAuthenticationRequestPending() + REKEYING -> callbacks.isRekeying() + } +} + +internal sealed interface SshFormalGuard { + fun evaluate(callbacks: SshClientCallbacks): Boolean + + fun renderTla(): String + + data object Always : SshFormalGuard { + override fun evaluate(callbacks: SshClientCallbacks) = true + + override fun renderTla() = "TRUE" + } + + data class Fact( + val fact: SshBooleanFact, + ) : SshFormalGuard { + override fun evaluate(callbacks: SshClientCallbacks) = fact.evaluate(callbacks) + + override fun renderTla() = fact.tlaName + } + + data class Not( + val expression: SshFormalGuard, + ) : SshFormalGuard { + override fun evaluate(callbacks: SshClientCallbacks) = !expression.evaluate(callbacks) + + override fun renderTla() = "~(${expression.renderTla()})" + } +} + +internal operator fun SshFormalGuard.not(): SshFormalGuard = SshFormalGuard.Not(this) + +internal data class SshFormalTransitionMeta( + val id: SshTransitionId, + val eventClass: KClass, + val targetStateName: String?, + val targetIsHistory: Boolean, + val guard: SshFormalGuard, + val origins: Set, + val effects: Set, + val channelOperationEvent: SshChannelEventId?, +) : MetaInfo { + init { + require(origins.isNotEmpty()) { "Formal transition ${id.name} must have an origin" } + require(!targetIsHistory || targetStateName != null) { + "Formal transition ${id.name} has a history target without a state name" + } + } + + val eventName: String + get() = requireNotNull(eventClass.qualifiedName) + .substringAfter(".SshEvent.") +} + +internal data class SshFormalState( + val name: String, + val parentName: String?, + val initialChildName: String?, + val isFinal: Boolean, + val isHistory: Boolean, +) + +internal data class SshFormalTransition( + val sourceStateNames: Set, + val meta: SshFormalTransitionMeta, +) + +internal data class SshStateMachineFormalModel( + val initialStateName: String, + val states: List, + val transitions: List, + val channelModel: SshChannelFormalModel, +) { + private data class FormalVariable( + val name: String, + val initialValue: String, + val renderNext: (SshFormalTransitionMeta) -> String, + ) + + private val stateByName = states.associateBy(SshFormalState::name) + private val leafStateNames = states + .filterNot { it.isHistory } + .filter { state -> states.none { it.parentName == state.name && !it.isHistory } } + .mapTo(sortedSetOf(), SshFormalState::name) + + init { + require(states.map(SshFormalState::name).distinct().size == states.size) { + "Formal state names must be unique" + } + require(transitions.map { it.meta.id }.distinct().size == transitions.size) { + "Formal transition IDs must be unique" + } + require(initialStateName in leafStateNames) { "Initial state $initialStateName is not a leaf state" } + require(transitions.size == SshTransitionId.entries.size) { + "Expected ${SshTransitionId.entries.size} formal transitions, found ${transitions.size}" + } + val generatedConnectionOperations = transitions.mapNotNull { it.meta.channelOperationEvent }.toSet() + val declaredConnectionOperations = channelModel.operations + .filter { it.scope == SshChannelOperationScope.CONNECTION_TRANSITION } + .mapTo(mutableSetOf(), SshChannelFormalOperation::eventId) + require(generatedConnectionOperations == declaredConnectionOperations) { + "Connection transitions $generatedConnectionOperations do not match channel operations $declaredConnectionOperations" + } + transitions.filter { it.meta.channelOperationEvent != null }.forEach { transition -> + val channelEvent = requireNotNull(transition.meta.channelOperationEvent) + val channelOrigin = channelModel.operations.first { it.eventId == channelEvent }.origin + val expectedOrigin = channelOrigin.connectionOrigin + require(transition.meta.origins == setOf(expectedOrigin)) { + "Connection transition ${transition.meta.id} has origins ${transition.meta.origins}, " + + "but channel event $channelEvent requires $expectedOrigin" + } + } + } + + fun renderTla(moduleName: String = GENERATED_MODULE_NAME): String { + val variables = formalVariables() + val body = buildString { + appendLine("EXTENDS Naturals") + appendLine() + appendLine("CONSTANT MaxChannels") + appendLine() + appendLine("ChannelIDs == 1..MaxChannels") + appendLine("ChannelAttemptIDs == 0..(MaxChannels + 1)") + appendLine() + appendLine("VARIABLES ${variables.joinToString(", ", transform = FormalVariable::name)}") + appendLine() + appendLine("vars == <<${variables.joinToString(", ", transform = FormalVariable::name)}>>") + appendLine() + appendLine("States == ${renderSet(leafStateNames)}") + appendLine("PostAuthenticatedStates == ${renderSet(descendantLeaves(POST_AUTHENTICATED_STATE))}") + appendLine("KexStates == ${renderSet(KEX_STATE_NAMES)}") + appendLine("Events == ${renderSet(transitions.mapTo(sortedSetOf()) { it.meta.eventName })}") + appendLine("Origins == ${renderSet(SshEventOrigin.entries.mapTo(sortedSetOf()) { it.tlaName })}") + appendLine("Effects == ${renderSet(SshEffect.entries.mapTo(sortedSetOf()) { it.tlaName })}") + appendChannelDefinitions() + appendLine() + appendLine("Init ==") + variables.forEach { variable -> + appendLine(" /\\ ${variable.name} = ${variable.initialValue}") + } + appendLine() + transitions.sortedBy { it.meta.id.name }.forEach { transition -> + appendTransition(transition, variables) + appendLine() + } + appendLine("Next ==") + transitions.sortedBy { it.meta.id.name }.forEach { transition -> + appendLine(" \\/ ${transition.meta.id.name}") + } + appendLine(" \\/ AttemptChannelOperation") + appendLine() + appendLine("Spec == Init /\\ [][Next]_vars") + } + val fingerprint = MessageDigest.getInstance("SHA-256") + .digest(body.toByteArray(Charsets.UTF_8)) + .joinToString("") { "%02x".format(it) } + + return buildString { + appendLine("---- MODULE $moduleName ----") + appendLine("\\* Generated from SshClientStateMachine. Do not edit.") + appendLine("\\* Model SHA-256: $fingerprint") + appendLine("\\* Lifecycle states: ${leafStateNames.size}; transitions: ${transitions.size}.") + appendLine("\\* TLC distinct states count full variable valuations, not lifecycle nodes.") + append(body) + appendLine("====") + } + } + + private fun StringBuilder.appendTransition( + transition: SshFormalTransition, + variables: List, + ) { + val meta = transition.meta + appendLine("${meta.id.name} ==") + appendLine(" /\\ state \\in ${renderSet(transition.sourceStateNames)}") + if (meta.guard != SshFormalGuard.Always) { + appendLine(" /\\ ${meta.guard.renderTla()}") + } + variables.forEach { variable -> + appendLine(" /\\ ${variable.renderNext(meta)}") + } + } + + private fun formalVariables(): List = listOf( + variable("state", quote(initialStateName), ::renderTarget), + variable("previousState", quote(initialStateName)) { "state" }, + variable("history", quote(initialPostAuthenticatedState()), ::renderHistoryUpdate), + variable("event", quote("None")) { quote(it.eventName) }, + FormalVariable("origin", quote(SshEventOrigin.INTERNAL.tlaName)) { meta -> + if (meta.origins.size == 1) { + "origin' = ${quote(meta.origins.single().tlaName)}" + } else { + "origin' \\in ${renderSet(meta.origins.mapTo(sortedSetOf()) { it.tlaName })}" + } + }, + variable("packetWasParsed", "FALSE") { "(origin' = ${quote(SshEventOrigin.PARSED_PACKET.tlaName)})" }, + variable("effects", "{}") { renderSet(it.effects.mapTo(sortedSetOf()) { effect -> effect.tlaName }) }, + variable("rekeying", "FALSE", ::renderRekeyingUpdate), + variable("authenticationEstablished", "FALSE", ::renderAuthenticationEstablishedUpdate), + variable("initialNewKeysActive", "FALSE", ::renderInitialNewKeysActiveUpdate), + variable("authRequestPending", "FALSE", ::renderAuthRequestPendingUpdate), + variable("previousAuthRequestPending", "FALSE") { "authRequestPending" }, + variable("previousChannels", "[c \\in ChannelIDs |-> \"Unallocated\"]") { "channels" }, + FormalVariable("activeChannel", "0") { meta -> + val operation = meta.channelOperationEvent + if (operation == null) { + "activeChannel' = 0" + } else { + "activeChannel' \\in ChannelIDs /\\ " + + "ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], ${quote(operation.tlaName)})" + } + }, + variable("channelEvent", quote("None")) { quote(it.channelOperationEvent?.tlaName ?: "None") }, + FormalVariable("channelOrigin", quote("None")) { meta -> + val operation = meta.channelOperationEvent + if (operation == null) "channelOrigin' = \"None\"" else "channelOrigin' = ChannelOriginFor(${quote(operation.tlaName)})" + }, + FormalVariable("channels", "[c \\in ChannelIDs |-> \"Unallocated\"]") { meta -> + when { + SshEffect.DISCONNECT in meta.effects -> + "channels' = [c \\in ChannelIDs |-> IF channels[c] = \"Unallocated\" THEN \"Unallocated\" ELSE \"CLOSED\"]" + + meta.channelOperationEvent != null -> + "channels' = [channels EXCEPT ![activeChannel'] = " + + "ChannelTransitionTarget(channels[activeChannel'], ${quote(meta.channelOperationEvent.tlaName)})]" + + else -> "channels' = channels" + } + }, + FormalVariable("channelEffects", "{}") { meta -> + val operation = meta.channelOperationEvent + if (operation == null) { + "channelEffects' = {}" + } else { + "channelEffects' = ChannelEffectsFor(channels[activeChannel'], ${quote(operation.tlaName)})" + } + }, + ) + + private fun StringBuilder.appendChannelDefinitions() { + val operations = channelModel.operations + .filter { it.scope != SshChannelOperationScope.CONNECTION_TEARDOWN } + .sortedWith(compareBy(SshChannelFormalOperation::sourceStateName, SshChannelFormalOperation::eventName)) + val attemptedOperations = operations.filter { it.scope == SshChannelOperationScope.CHANNEL_ATTEMPT } + val channelStates = channelModel.states.mapTo(sortedSetOf()) { it.name }.apply { + add(channelModel.unallocatedStateName) + } + val channelEvents = operations.mapTo(sortedSetOf(), SshChannelFormalOperation::eventName) + val channelAttemptEvents = attemptedOperations.mapTo(sortedSetOf(), SshChannelFormalOperation::eventName) + val channelEffects = SshChannelEffect.entries.mapTo(sortedSetOf()) { it.name } + val authenticationRequired = operations.filter(SshChannelFormalOperation::requiresAuthenticatedConnection) + + appendLine() + appendLine("ChannelStates == ${renderSet(channelStates)}") + appendLine("ChannelEvents == ${renderSet(channelEvents)}") + appendLine("ChannelAttemptEvents == ${renderSet(channelAttemptEvents)}") + appendLine("ChannelEffectSet == ${renderSet(channelEffects)}") + appendLine("ChannelOrigins == ${renderSet(SshChannelEventOrigin.entries.mapTo(sortedSetOf()) { it.tlaName })}") + appendLine("ChannelTransitions == {") + operations.forEachIndexed { index, operation -> + val suffix = if (index == operations.lastIndex) "" else "," + appendLine(" <<${quote(operation.sourceStateName)}, ${quote(operation.eventName)}, ${quote(operation.targetStateName)}>>$suffix") + } + appendLine("}") + appendLine("ChannelAuthenticationRequired == {") + authenticationRequired.forEachIndexed { index, operation -> + val suffix = if (index == authenticationRequired.lastIndex) "" else "," + appendLine(" <<${quote(operation.sourceStateName)}, ${quote(operation.eventName)}>>$suffix") + } + appendLine("}") + appendLine() + appendLine("ChannelTransitionDefined(channelState, operation) ==") + appendLine(" \\E target \\in ChannelStates : <> \\in ChannelTransitions") + appendLine() + appendLine("ChannelTransitionTarget(channelState, operation) ==") + appendLine(" CHOOSE target \\in ChannelStates : <> \\in ChannelTransitions") + appendLine() + appendLine("ChannelEffectsFor(channelState, operation) ==") + operations.forEachIndexed { index, operation -> + val prefix = if (index == 0) " CASE " else " [] " + appendLine( + "$prefix/\\ channelState = ${quote(operation.sourceStateName)} /\\ operation = ${quote(operation.eventName)} -> " + + renderSet(operation.effects.map { it.name }), + ) + } + appendLine(" [] OTHER -> ${renderSet(channelModel.rejectedOperationEffects.map { it.name })}") + appendLine() + appendLine("ChannelOriginFor(operation) ==") + operations.distinctBy(SshChannelFormalOperation::eventId).forEachIndexed { index, operation -> + val prefix = if (index == 0) " CASE " else " [] " + appendLine("$prefix operation = ${quote(operation.eventName)} -> ${quote(operation.origin.tlaName)}") + } + appendLine(" [] OTHER -> \"None\"") + appendLine() + appendLine("ChannelOperationAllowed(isAuthenticated, connectionState, channelState, operation) ==") + appendLine(" /\\ ChannelTransitionDefined(channelState, operation)") + appendLine(" /\\ connectionState # \"Disconnected\"") + appendLine(" /\\ (<> \\notin ChannelAuthenticationRequired") + appendLine(" \\/ isAuthenticated)") + appendLine() + appendLine("AttemptChannelOperation ==") + appendLine(" /\\ activeChannel' \\in ChannelAttemptIDs") + appendLine(" /\\ channelEvent' \\in ChannelAttemptEvents") + appendLine(" /\\ channelOrigin' = ChannelOriginFor(channelEvent')") + appendLine(" /\\ previousChannels' = channels") + appendLine(" /\\ IF activeChannel' \\in ChannelIDs") + appendLine(" /\\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], channelEvent')") + appendLine(" THEN") + appendLine(" /\\ channels' = [channels EXCEPT ![activeChannel'] = ChannelTransitionTarget(channels[activeChannel'], channelEvent')]") + appendLine(" /\\ channelEffects' = ChannelEffectsFor(channels[activeChannel'], channelEvent')") + appendLine(" ELSE") + appendLine(" /\\ channels' = channels") + appendLine( + " /\\ channelEffects' = ${renderSet(channelModel.rejectedOperationEffects.map { it.name })}", + ) + val globalVariableNames = formalVariables() + .map(FormalVariable::name) + .filterNot { it in CHANNEL_VARIABLE_NAMES } + appendLine(" /\\ UNCHANGED <<${globalVariableNames.joinToString()}>>") + } + + private fun variable( + name: String, + initialValue: String, + nextValue: (SshFormalTransitionMeta) -> String, + ) = FormalVariable(name, initialValue) { meta -> "$name' = ${nextValue(meta)}" } + + private fun renderTarget(meta: SshFormalTransitionMeta): String { + val targetName = meta.targetStateName ?: return "state" + if (meta.targetIsHistory) return "history" + return quote(resolveInitialLeaf(targetName)) + } + + private fun renderHistoryUpdate(meta: SshFormalTransitionMeta): String = if (SshEffect.REKEY_STARTED in meta.effects) "state" else "history" + + private fun renderRekeyingUpdate(meta: SshFormalTransitionMeta): String = when { + SshEffect.REKEY_STARTED in meta.effects -> "TRUE" + SshEffect.REKEY_COMPLETE in meta.effects -> "FALSE" + SshEffect.DISCONNECT in meta.effects -> "FALSE" + else -> "rekeying" + } + + private fun renderAuthenticationEstablishedUpdate(meta: SshFormalTransitionMeta): String = if (SshEffect.AUTHENTICATION_SUCCESS in meta.effects) "TRUE" else "authenticationEstablished" + + private fun renderInitialNewKeysActiveUpdate(meta: SshFormalTransitionMeta): String = if (SshEffect.ACTIVATE_ENCRYPTION in meta.effects) "TRUE" else "initialNewKeysActive" + + private fun renderAuthRequestPendingUpdate(meta: SshFormalTransitionMeta): String = when { + SshEffect.SEND_USERAUTH_REQUEST in meta.effects -> "TRUE" + SshEffect.DISCONNECT in meta.effects -> "FALSE" + meta.id in AUTH_REQUEST_RESPONSE_TRANSITIONS -> "FALSE" + else -> "authRequestPending" + } + + private fun initialPostAuthenticatedState() = resolveInitialLeaf(POST_AUTHENTICATED_STATE) + + private fun resolveInitialLeaf(stateName: String): String { + val state = requireNotNull(stateByName[stateName]) { "Unknown formal state $stateName" } + if (state.isHistory) { + error("History state $stateName must be represented as a history target") + } + val initialChild = state.initialChildName ?: return state.name + return resolveInitialLeaf(initialChild) + } + + private fun descendantLeaves(stateName: String): Set { + require(stateName in stateByName) { "Unknown formal state $stateName" } + val children = states.filter { it.parentName == stateName && !it.isHistory } + if (children.isEmpty()) return setOf(stateName) + return children.flatMapTo(sortedSetOf()) { descendantLeaves(it.name) } + } + + private fun renderSet(values: Collection): String = values + .joinToString(prefix = "{", postfix = "}") { quote(it) } + + private fun quote(value: String) = "\"${value.replace("\\", "\\\\").replace("\"", "\\\"")}\"" + + private val SshEventOrigin.tlaName: String + get() = name.lowercase().split('_').joinToString("") { it.replaceFirstChar(Char::uppercase) } + + private val SshEffect.tlaName: String + get() = name.lowercase().split('_').joinToString("") { it.replaceFirstChar(Char::uppercase) } + + companion object { + const val GENERATED_MODULE_NAME = "SshClientStateMachineGenerated" + private const val POST_AUTHENTICATED_STATE = "PostAuthenticated" + private val KEX_STATE_NAMES = sortedSetOf("WaitKexInit", "WaitKex", "WaitKexDhGexInit", "WaitNewKeys") + private val AUTH_REQUEST_RESPONSE_TRANSITIONS = setOf( + SshTransitionId.AUTHENTICATION_SUCCESS, + SshTransitionId.AUTHENTICATION_FAILURE, + SshTransitionId.AUTHORIZE_AUTHENTICATION_PACKET, + ) + private val CHANNEL_VARIABLE_NAMES = setOf( + "channels", + "previousChannels", + "activeChannel", + "channelEvent", + "channelOrigin", + "channelEffects", + ) + } +} + +private val SshChannelEventOrigin.tlaName: String + get() = when (this) { + SshChannelEventOrigin.CONNECTION_CONTROL -> "ConnectionControl" + SshChannelEventOrigin.LOCAL_COMMAND -> "LocalCommand" + SshChannelEventOrigin.PARSED_PACKET -> "ParsedPacket" + } + +private val SshChannelEventOrigin.connectionOrigin: SshEventOrigin + get() = when (this) { + SshChannelEventOrigin.CONNECTION_CONTROL -> SshEventOrigin.INTERNAL + SshChannelEventOrigin.LOCAL_COMMAND -> SshEventOrigin.LOCAL_COMMAND + SshChannelEventOrigin.PARSED_PACKET -> SshEventOrigin.PARSED_PACKET + } + +internal fun StateMachine.toSshFormalModel(): SshStateMachineFormalModel { + val allStates = collectStates(this) + val formalStates = allStates + .filterNot { it === this } + .map { state -> + SshFormalState( + name = state.requireName(), + parentName = state.parent?.takeUnless { it === this }?.requireName(), + initialChildName = state.initialState?.requireName(), + isFinal = state is FinalState, + isHistory = state is HistoryState, + ) + } + .sortedBy(SshFormalState::name) + val formalStateByName = formalStates.associateBy(SshFormalState::name) + val leafStates = formalStates + .filterNot { it.isHistory } + .filter { state -> formalStates.none { it.parentName == state.name && !it.isHistory } } + .mapTo(sortedSetOf(), SshFormalState::name) + + fun descendantLeaves(source: IState): Set { + if (source === this) { + return leafStates.filterTo(sortedSetOf()) { formalStateByName.getValue(it).isFinal.not() } + } + val sourceName = source.requireName() + val children = formalStates.filter { it.parentName == sourceName && !it.isHistory } + return if (children.isEmpty()) { + setOf(sourceName) + } else { + children.flatMapTo(sortedSetOf()) { child -> + val childState = allStates.single { it.name == child.name } + descendantLeaves(childState) + } + } + } + + val transitions = allStates.flatMap { source -> + source.transitions.mapNotNull { transition -> + val meta = transition.metaInfo as? SshFormalTransitionMeta + if (meta == null && transition.eventMatcher.eventClass == StartEvent::class) { + return@mapNotNull null + } + requireNotNull(meta) { + "Transition ${transition.name} on ${source.name} has no formal metadata" + } + require(transition.name == meta.id.name) { + "Transition ${transition.name} does not match formal ID ${meta.id.name}" + } + SshFormalTransition( + sourceStateNames = descendantLeaves(source), + meta = meta, + ) + } + } + + return SshStateMachineFormalModel( + initialStateName = resolveInitialLeaf(requireNotNull(initialState)), + states = formalStates, + transitions = transitions, + channelModel = SshChannelStateMachine(SshChannelState.OPEN).formalModel(), + ) +} + +private fun collectStates(root: IState): List = buildList { + add(root) + root.states.sortedBy { it.name }.forEach { addAll(collectStates(it)) } +} + +private fun resolveInitialLeaf(state: IState): String { + require(state !is PseudoState) { "Initial state ${state.name} cannot be a pseudo state" } + val initialChild = state.initialState ?: return state.requireName() + return resolveInitialLeaf(initialChild) +} + +private fun IState.requireName(): String = requireNotNull(name).also { + require(it.isNotBlank()) { "Formal state names must not be blank" } +} diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/AgentChannelTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/AgentChannelTest.kt index 224d3a4f..bee37d7e 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/AgentChannelTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/AgentChannelTest.kt @@ -112,7 +112,7 @@ class AgentChannelTest { } @Test - fun `onEof does not throw`() { + fun `onEof does not throw`() = runTest { val agentChannel = newChannel(kotlinx.coroutines.CoroutineScope(kotlinx.coroutines.Dispatchers.Unconfined)) agentChannel.onEof() } diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/FakeSshServer.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/FakeSshServer.kt index 03edf784..3534a680 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/FakeSshServer.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/FakeSshServer.kt @@ -104,6 +104,7 @@ class FakeSshServer( var advertiseExtInfo: Boolean = false var kexAlgorithms: String? = null var corruptKexSignature: Boolean = false + var sendDuplicateKexInitDuringRekey: Boolean = false private val receivedPongs = Channel(Channel.UNLIMITED) private val receivedExtInfo = Channel(Channel.UNLIMITED) private val receivedUserauthRequests = Channel(Channel.UNLIMITED) @@ -327,6 +328,11 @@ class FakeSshServer( } raw } + if (sendDuplicateKexInitDuringRekey) { + sendDuplicateKexInitDuringRekey = false + sendKexInit(io) + return + } val (_, ecdhInitRaw) = packets.receive() // ECDH_INIT val clientPublic = parseEcdhInit(ecdhInitRaw) sendEcdhReply(io, clientKexInitRaw, serverKexInitBytes, clientPublic) diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/ForwardingChannelTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/ForwardingChannelTest.kt index 055d8837..acf1061b 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/ForwardingChannelTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/ForwardingChannelTest.kt @@ -23,11 +23,13 @@ import io.mockk.mockk import kotlinx.coroutines.CoroutineScope import kotlinx.coroutines.test.UnconfinedTestDispatcher import kotlinx.coroutines.test.runTest +import org.connectbot.sshlib.SshException import org.junit.jupiter.api.Assertions.assertArrayEquals import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.Assertions.assertFalse import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Test +import kotlin.test.assertFailsWith class ForwardingChannelTest { @@ -87,7 +89,7 @@ class ForwardingChannelTest { } @Test - fun `onEof closes incomingData channel`() { + fun `onEof closes incomingData channel`() = runTest { val (channel, _) = createChannel() channel.onEof() @@ -162,4 +164,16 @@ class ForwardingChannelTest { coVerify(exactly = 1) { conn.sendChannelClose(1) } } + + @Test + fun `data after remote EOF has no delivery side effect`() = runTest { + val (channel, _) = createChannel() + + channel.onEof() + + assertFailsWith { + channel.onData(byteArrayOf(1)) + } + assertTrue(channel.incomingData.isClosedForReceive) + } } diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/KeystrokeObfuscationTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/KeystrokeObfuscationTest.kt index 93bb9f65..811c6ca1 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/KeystrokeObfuscationTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/KeystrokeObfuscationTest.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. @@ -20,6 +20,7 @@ package org.connectbot.sshlib.client import io.mockk.coEvery import io.mockk.coVerify import io.mockk.mockk +import kotlinx.coroutines.CompletableDeferred import kotlinx.coroutines.CoroutineScope import kotlinx.coroutines.ExperimentalCoroutinesApi import kotlinx.coroutines.delay @@ -96,7 +97,7 @@ class KeystrokeObfuscationTest { fun `write without PTY does not send chaff`() = runTest { val dispatcher = StandardTestDispatcher(testScheduler) val conn = mockk(relaxed = true) - coEvery { conn.sendChannelRequest(any(), any(), any(), any()) } returns true + coEvery { conn.beginChannelRequest(any(), any(), any(), any()) } returns CompletableDeferred(true) val channel = createObfuscatingChannel( conn, @@ -117,7 +118,7 @@ class KeystrokeObfuscationTest { fun `write with PTY but canSendChaff false does not send chaff`() = runTest { val dispatcher = StandardTestDispatcher(testScheduler) val conn = mockk(relaxed = true) - coEvery { conn.sendChannelRequest(any(), any(), any(), any()) } returns true + coEvery { conn.beginChannelRequest(any(), any(), any(), any()) } returns CompletableDeferred(true) val channel = createObfuscatingChannel( conn, @@ -138,7 +139,7 @@ class KeystrokeObfuscationTest { fun `write with PTY and intervalMs zero does not send chaff`() = runTest { val dispatcher = StandardTestDispatcher(testScheduler) val conn = mockk(relaxed = true) - coEvery { conn.sendChannelRequest(any(), any(), any(), any()) } returns true + coEvery { conn.beginChannelRequest(any(), any(), any(), any()) } returns CompletableDeferred(true) val channel = createObfuscatingChannel( conn, @@ -182,7 +183,7 @@ class KeystrokeObfuscationTest { fun `write with PTY canSendChaff and interval sends chaff during chaff window`() = runTest { val dispatcher = StandardTestDispatcher(testScheduler) val conn = mockk(relaxed = true) - coEvery { conn.sendChannelRequest(any(), any(), any(), any()) } returns true + coEvery { conn.beginChannelRequest(any(), any(), any(), any()) } returns CompletableDeferred(true) val channel = createObfuscatingChannel( conn, @@ -286,7 +287,7 @@ class KeystrokeObfuscationTest { fun `chaff stops after chaff window expires`() = runTest { val dispatcher = StandardTestDispatcher(testScheduler) val conn = mockk(relaxed = true) - coEvery { conn.sendChannelRequest(any(), any(), any(), any()) } returns true + coEvery { conn.beginChannelRequest(any(), any(), any(), any()) } returns CompletableDeferred(true) var chaffCount = 0 coEvery { conn.sendChaff() } coAnswers { chaffCount++ @@ -320,7 +321,7 @@ class KeystrokeObfuscationTest { fun `requestPty sets ptyGranted on success`() = runTest { val dispatcher = StandardTestDispatcher(testScheduler) val conn = mockk(relaxed = true) - coEvery { conn.sendChannelRequest(any(), eq("pty-req"), any(), any()) } returns true + coEvery { conn.beginChannelRequest(any(), eq("pty-req"), any(), any()) } returns CompletableDeferred(true) val channel = createObfuscatingChannel( conn, @@ -344,7 +345,7 @@ class KeystrokeObfuscationTest { fun `requestPty does not set ptyGranted on failure`() = runTest { val dispatcher = StandardTestDispatcher(testScheduler) val conn = mockk(relaxed = true) - coEvery { conn.sendChannelRequest(any(), eq("pty-req"), any(), any()) } returns false + coEvery { conn.beginChannelRequest(any(), eq("pty-req"), any(), any()) } returns CompletableDeferred(false) val channel = createObfuscatingChannel( conn, diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SessionChannelTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SessionChannelTest.kt index 9effc854..2bb93c63 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SessionChannelTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SessionChannelTest.kt @@ -21,6 +21,7 @@ import io.mockk.coEvery import io.mockk.coVerify import io.mockk.mockk import io.mockk.slot +import kotlinx.coroutines.CompletableDeferred import kotlinx.coroutines.CoroutineScope import kotlinx.coroutines.ExperimentalCoroutinesApi import kotlinx.coroutines.test.UnconfinedTestDispatcher @@ -59,8 +60,8 @@ class SessionChannelTest { val wantReplySlot = slot() val conn = mockk(relaxed = true) coEvery { - conn.sendChannelRequest(any(), capture(requestTypeSlot), capture(wantReplySlot), any()) - } returns true + conn.beginChannelRequest(any(), capture(requestTypeSlot), capture(wantReplySlot), any()) + } returns null val (channel, _) = createChannel(conn) @@ -79,7 +80,7 @@ class SessionChannelTest { @Test fun `resizeTerminal returns false when request fails`() = runTest { val conn = mockk(relaxed = true) - coEvery { conn.sendChannelRequest(any(), any(), any(), any()) } returns false + coEvery { conn.beginChannelRequest(any(), any(), any(), any()) } returns CompletableDeferred(false) val (channel, _) = createChannel(conn) @@ -98,8 +99,8 @@ class SessionChannelTest { val channelSlot = slot() val conn = mockk(relaxed = true) coEvery { - conn.sendChannelRequest(capture(channelSlot), any(), any(), any()) - } returns true + conn.beginChannelRequest(capture(channelSlot), any(), any(), any()) + } returns null val (channel, _) = createChannel(conn) @@ -235,4 +236,26 @@ class SessionChannelTest { channel.onExtendedData(1, ByteArray(513)) } } + + @Test + fun `data after remote EOF is rejected before delivery`() = runTest { + val (channel, _) = createChannel() + + channel.onEof() + + assertFailsWith { + channel.onData(byteArrayOf(1)) + } + assertTrue(channel.stdout.isClosedForReceive) + } + + @Test + fun `duplicate local EOF sends only one packet`() = runTest { + val (channel, conn) = createChannel() + + channel.sendEof() + channel.sendEof() + + coVerify(exactly = 1) { conn.sendChannelEof(1) } + } } diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshChannelRegistryTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshChannelRegistryTest.kt new file mode 100644 index 00000000..c18a54e7 --- /dev/null +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshChannelRegistryTest.kt @@ -0,0 +1,144 @@ +/* + * ConnectBot SSH Library + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.connectbot.sshlib.client + +import io.mockk.coEvery +import io.mockk.coVerify +import io.mockk.every +import io.mockk.mockk +import kotlinx.coroutines.CompletableDeferred +import kotlinx.coroutines.test.runTest +import org.connectbot.sshlib.protocol.SshChannelState +import org.connectbot.sshlib.protocol.SshChannelStateMachine +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertIs +import kotlin.test.assertNull +import kotlin.test.assertSame +import kotlin.test.assertTrue + +class SshChannelRegistryTest { + @Test + fun `local and remote recipients resolve one established channel`() { + val registry = SshChannelRegistry() + val session = sessionChannel(local = 7, remote = 70) + + registry.register(session) + + assertIs(registry.findByLocalRecipient(7)) + assertSame( + session, + registry.findByRemoteRecipient(70)?.let { + (it as SshChannelRegistry.Entry.Established.Session).channel + }, + ) + assertNull(registry.findByLocalRecipient(8)) + assertNull(registry.findByRemoteRecipient(71)) + } + + @Test + fun `duplicate local recipient is rejected across channel kinds`() { + val registry = SshChannelRegistry() + registry.register(sessionChannel(local = 7, remote = 70)) + + assertFailsWith { + registry.register(forwardingChannel(local = 7, remote = 80)) + } + } + + @Test + fun `duplicate remote recipient is rejected across local IDs`() { + val registry = SshChannelRegistry() + registry.register(sessionChannel(local = 7, remote = 70)) + + assertFailsWith { + registry.register(forwardingChannel(local = 8, remote = 70)) + } + } + + @Test + fun `pending open continuously owns local ID through atomic promotion`() { + val registry = SshChannelRegistry() + val deferred = CompletableDeferred() + val lifecycle = SshChannelStateMachine(SshChannelState.OPENING) + registry.registerPendingSession(7, deferred, lifecycle) + val pending = registry.findPendingSession(7)!! + + registry.bindRemoteRecipient(pending, 70) + val session = sessionChannel(local = 7, remote = 70) + registry.promote(pending, session) + + assertNull(registry.findPendingSession(7)) + assertSame( + session, + (registry.findByLocalRecipient(7) as SshChannelRegistry.Entry.Established.Session).channel, + ) + assertEquals(7, registry.findByRemoteRecipient(70)?.localChannelNumber) + } + + @Test + fun `unregister removes local and remote indexes together`() { + val registry = SshChannelRegistry() + registry.register(sessionChannel(local = 7, remote = 70)) + + registry.unregister(7) + + assertNull(registry.findByLocalRecipient(7)) + assertNull(registry.findByRemoteRecipient(70)) + } + + @Test + fun `disconnect cascade removes and closes pending and established entries`() = runTest { + val registry = SshChannelRegistry() + val session = sessionChannel(local = 7, remote = 70) + coEvery { session.onDisconnected() } returns Unit + val pendingDeferred = CompletableDeferred() + registry.register(session) + registry.registerPendingForwarding( + localChannelNumber = 8, + deferred = pendingDeferred, + maxPacketSize = 32 * 1024, + initialWindowSize = 64 * 1024, + lifecycle = SshChannelStateMachine(SshChannelState.OPENING), + ) + val cause = IllegalStateException("connection lost") + + registry.disconnectAll(cause) + + coVerify(exactly = 1) { session.onDisconnected() } + assertTrue(registry.snapshot().isEmpty()) + assertNull(registry.findByRemoteRecipient(70)) + assertEquals(cause.message, assertFailsWith { pendingDeferred.await() }.message) + assertFailsWith { + registry.register(sessionChannel(local = 9, remote = 90)) + } + } + + private fun sessionChannel(local: Int, remote: Int) = mockk { + every { localChannelNumber } returns local + every { remoteChannelNumber } returns remote + every { isOpen } returns true + } + + private fun forwardingChannel(local: Int, remote: Int) = mockk { + every { localChannelNumber } returns local + every { remoteChannelNumber } returns remote + every { isOpen } returns true + } +} diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionCloseTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionCloseTest.kt new file mode 100644 index 00000000..eed33e88 --- /dev/null +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionCloseTest.kt @@ -0,0 +1,98 @@ +/* + * ConnectBot SSH Library + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.connectbot.sshlib.client + +import kotlinx.coroutines.CompletableDeferred +import kotlinx.coroutines.CoroutineDispatcher +import kotlinx.coroutines.ExperimentalCoroutinesApi +import kotlinx.coroutines.async +import kotlinx.coroutines.test.StandardTestDispatcher +import kotlinx.coroutines.test.runTest +import kotlinx.coroutines.yield +import org.connectbot.sshlib.HostKeyVerifier +import org.connectbot.sshlib.transport.Transport +import org.connectbot.sshlib.transport.TransportException +import org.junit.jupiter.api.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +@OptIn(ExperimentalCoroutinesApi::class) +class SshConnectionCloseTest { + + @Test + fun `concurrent close closes transport once`() = runTest { + val transport = RecordingTransport(suspendClose = true) + val connection = connection(transport, StandardTestDispatcher(testScheduler)) + + val first = async { connection.close() } + transport.closeStarted.await() + val second = async { connection.close() } + yield() + + transport.allowClose.complete(Unit) + first.await() + second.await() + + assertEquals(1, transport.closeCalls) + } + + @Test + fun `write after close fails without reaching transport`() = runTest { + val transport = RecordingTransport() + val connection = connection(transport, StandardTestDispatcher(testScheduler)) + + connection.close() + + assertFailsWith { + connection.sendChannelClose(recipientChannel = 0) + } + assertEquals(0, transport.writeCalls) + } + + private fun connection(transport: Transport, dispatcher: CoroutineDispatcher) = SshConnection( + transport = transport, + hostKeyVerifier = object : HostKeyVerifier { + override suspend fun verify(key: org.connectbot.sshlib.PublicKey): Boolean = true + }, + coroutineDispatcher = dispatcher, + ) + + private class RecordingTransport( + private val suspendClose: Boolean = false, + ) : Transport { + val closeStarted = CompletableDeferred() + val allowClose = CompletableDeferred() + var closeCalls = 0 + var writeCalls = 0 + + override val isConnected: Boolean + get() = closeCalls == 0 + + override suspend fun read(count: Int): ByteArray = throw UnsupportedOperationException() + + override suspend fun write(data: ByteArray) { + writeCalls++ + } + + override suspend fun close() { + closeCalls++ + closeStarted.complete(Unit) + if (suspendClose) allowClose.await() + } + } +} 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 058f663c..89430229 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt @@ -75,6 +75,18 @@ class SshConnectionFlowTest { } } + @Test + fun `duplicate kex init during rekey is a fatal protocol error`() = runTest { + connectedFixture { connection, server, dispatcher -> + val disconnected = async(dispatcher) { connection.disconnectedFlow.first() } + server.sendDuplicateKexInitDuringRekey = true + server.initiateRekey() + + val failure = assertNotNull(withTimeout(5_000) { disconnected.await() }) + assertTrue(failure.message.orEmpty().contains("Unexpected SSH_MSG_KEXINIT")) + } + } + @Test fun `connect returns host key rejected when verifier rejects server key`() = runTest { val dispatcher = StandardTestDispatcher(testScheduler) diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachineTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachineTest.kt new file mode 100644 index 00000000..d688295b --- /dev/null +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshChannelStateMachineTest.kt @@ -0,0 +1,200 @@ +/* + * ConnectBot SSH Library + * Copyright 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.connectbot.sshlib.protocol + +import kotlinx.coroutines.test.runTest +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class SshChannelStateMachineTest { + @Test + fun `every channel transition is explicit formal metadata`() { + val model = SshChannelStateMachine(SshChannelState.OPEN).formalModel() + + assertEquals(SshChannelState.entries.toSet(), model.states) + assertEquals(SshChannelTransitionId.entries.toSet(), model.transitions.map { it.id }.toSet()) + val runtimeOperations = model.operations + .filter { it.id in SshChannelTransitionId.entries.map(SshChannelTransitionId::name) } + .associateBy { it.id } + model.transitions.forEach { transition -> + val operation = runtimeOperations.getValue(transition.id.name) + assertEquals(transition.eventName, operation.eventName) + assertEquals(transition.source.name, operation.sourceStateName) + assertEquals(transition.target.name, operation.targetStateName) + assertEquals(transition.effects, operation.effects) + assertEquals(transition.origin, operation.origin) + assertEquals(transition.scope, operation.scope) + assertEquals(transition.requiresAuthenticatedConnection, operation.requiresAuthenticatedConnection) + } + } + + @Test + fun `construction and rejection semantics are explicit formal operations`() { + val model = SshChannelStateMachine(SshChannelState.OPEN).formalModel() + val constructionIds = SshChannelConstructionId.entries.mapTo(mutableSetOf(), SshChannelConstructionId::name) + val constructions = model.operations.filter { it.id in constructionIds } + + assertEquals(constructionIds, constructions.mapTo(mutableSetOf()) { it.id }) + assertTrue(constructions.all { it.sourceStateName == model.unallocatedStateName }) + assertEquals( + SshChannelOperationScope.CONNECTION_TRANSITION, + constructions.single { it.id == SshChannelConstructionId.ALLOCATE_LOCAL_OPEN.name }.scope, + ) + assertEquals( + SshChannelOperationScope.CHANNEL_ATTEMPT, + constructions.single { it.id == SshChannelConstructionId.ACCEPT_REMOTE_OPEN.name }.scope, + ) + assertTrue(constructions.all { it.requiresAuthenticatedConnection }) + assertTrue(model.rejectedOperationEffects.isEmpty()) + } + + @Test + fun `disconnect is teardown rather than a malicious channel attempt`() { + val model = SshChannelStateMachine(SshChannelState.OPEN).formalModel() + val disconnects = model.operations.filter { it.eventId == SshChannelEventId.DISCONNECT } + + assertTrue(disconnects.isNotEmpty()) + assertTrue(disconnects.all { it.scope == SshChannelOperationScope.CONNECTION_TEARDOWN }) + assertTrue(disconnects.none { it.requiresAuthenticatedConnection }) + assertTrue(disconnects.all { it.origin == SshChannelEventOrigin.CONNECTION_CONTROL }) + } + + @Test + fun `packet and local operations have distinct typed origins`() { + val operations = SshChannelStateMachine(SshChannelState.OPEN).formalModel().operations + val localEvents = setOf( + SshChannelEventId.ALLOCATE_LOCAL_OPEN, + SshChannelEventId.SEND_CLOSE, + SshChannelEventId.SEND_DATA, + SshChannelEventId.SEND_EOF, + SshChannelEventId.SEND_REQUEST, + ) + val packetEvents = SshChannelEventId.entries.toSet() - localEvents - SshChannelEventId.DISCONNECT + + assertTrue(operations.filter { it.eventId in packetEvents }.all { it.origin == SshChannelEventOrigin.PARSED_PACKET }) + assertTrue(operations.filter { it.eventId in localEvents }.all { it.origin == SshChannelEventOrigin.LOCAL_COMMAND }) + } + + @Test + fun `only an accepted transition executes its effect callback`() = runTest { + val machine = SshChannelStateMachine(SshChannelState.OPEN) + var effects = 0 + + assertTrue(machine.sendEof { effects++ }) + assertFalse(machine.sendEof { effects++ }) + assertFalse(machine.sendData { effects++ }) + + assertEquals(1, effects) + } + + @Test + fun `accepted callback receives source-specific transition metadata`() = runTest { + val remotelyClosed = SshChannelStateMachine(SshChannelState.OPEN) + val closeSent = SshChannelStateMachine(SshChannelState.OPEN) + var remoteCloseEffects = emptySet() + var closeReplyEffects = emptySet() + + remotelyClosed.receiveClose { remoteCloseEffects = it.effects } + closeSent.sendClose {} + closeSent.receiveClose { closeReplyEffects = it.effects } + + assertTrue(SshChannelEffect.SEND_CLOSE in remoteCloseEffects) + assertFalse(SshChannelEffect.SEND_CLOSE in closeReplyEffects) + assertEquals( + SshChannelEventOrigin.PARSED_PACKET, + closeSent.formalModel().transitions.first { + it.id == SshChannelTransitionId.RECEIVE_CLOSE_CLOSE_SENT + }.origin, + ) + } + + @Test + fun `opening accepts exactly one terminal response`() = runTest { + val confirmed = SshChannelStateMachine(SshChannelState.OPENING) + assertTrue(confirmed.openConfirmed {}) + assertEquals(SshChannelState.OPEN, confirmed.state) + assertFalse(confirmed.openFailed {}) + + val failed = SshChannelStateMachine(SshChannelState.OPENING) + assertTrue(failed.openFailed {}) + assertEquals(SshChannelState.CLOSED, failed.state) + assertFalse(failed.openConfirmed {}) + } + + @Test + fun `EOF independently closes each data direction`() = runTest { + val machine = SshChannelStateMachine(SshChannelState.OPEN) + + assertTrue(machine.sendEof {}) + assertEquals(SshChannelState.LOCAL_EOF, machine.state) + assertFalse(machine.sendData {}) + assertTrue(machine.receiveData {}) + + assertTrue(machine.receiveEof {}) + assertEquals(SshChannelState.BOTH_EOF, machine.state) + assertFalse(machine.sendData {}) + assertFalse(machine.receiveData {}) + } + + @Test + fun `remote EOF still permits outbound data`() = runTest { + val machine = SshChannelStateMachine(SshChannelState.OPEN) + + assertTrue(machine.receiveEof {}) + assertEquals(SshChannelState.REMOTE_EOF, machine.state) + assertTrue(machine.sendData {}) + assertFalse(machine.receiveData {}) + } + + @Test + fun `local close waits for remote close and blocks channel operations`() = runTest { + val machine = SshChannelStateMachine(SshChannelState.OPEN) + + assertTrue(machine.sendClose {}) + assertEquals(SshChannelState.CLOSE_SENT, machine.state) + assertFalse(machine.isOpen) + assertFalse(machine.sendData {}) + assertFalse(machine.receiveData {}) + assertFalse(machine.sendEof {}) + assertTrue(machine.receiveClose {}) + assertEquals(SshChannelState.CLOSED, machine.state) + } + + @Test + fun `remote close is terminal and duplicate close is rejected`() = runTest { + val machine = SshChannelStateMachine(SshChannelState.OPEN) + + assertTrue(machine.receiveClose {}) + assertEquals(SshChannelState.CLOSED, machine.state) + assertFalse(machine.receiveClose {}) + assertFalse(machine.sendClose {}) + } + + @Test + fun `disconnect closes opening and established channels`() = runTest { + val opening = SshChannelStateMachine(SshChannelState.OPENING) + val established = SshChannelStateMachine(SshChannelState.OPEN) + + assertTrue(opening.disconnect {}) + assertTrue(established.disconnect {}) + assertEquals(SshChannelState.CLOSED, opening.state) + assertEquals(SshChannelState.CLOSED, established.state) + } +} diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachineTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachineTest.kt index fa933336..e5c9b797 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachineTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachineTest.kt @@ -62,6 +62,63 @@ class SshClientStateMachineTest { assertTrue(machine.openChannel("session", 0, 1024, 1024)) } + @Test + fun `authentication requests cannot overlap without a server response`() = runTest { + val callbacks = RecordingCallbacks() + val machine = SshClientStateMachine(callbacks) + + assertTrue(machine.connect()) + assertTrue(machine.receiveVersion(IdBanner())) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + assertTrue(machine.receiveKexDhReply(SshMsgKexdhReply())) + assertTrue(machine.receiveNewKeys()) + assertTrue(machine.receiveServiceAccept("ssh-userauth")) + + assertTrue(machine.beginAuthentication()) + assertFalse(machine.beginAuthentication()) + assertTrue(machine.authorizeAuthenticationPacket()) + assertTrue(machine.beginAuthentication()) + } + + @Test + fun `typed rekey guard restores the authenticated state`() = runTest { + val callbacks = RecordingCallbacks() + val machine = SshClientStateMachine(callbacks) + + assertTrue(machine.connect()) + assertTrue(machine.receiveVersion(IdBanner())) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + assertTrue(machine.receiveKexEcdhReply(SshMsgKexEcdhReply())) + assertTrue(machine.receiveNewKeys()) + assertTrue(machine.receiveServiceAccept("ssh-userauth")) + assertTrue(machine.beginAuthentication()) + assertTrue(machine.authenticationSuccess()) + + assertTrue(machine.requestRekey()) + assertTrue(callbacks.rekeying) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + assertTrue(machine.receiveKexEcdhReply(SshMsgKexEcdhReply())) + assertTrue(machine.receiveNewKeys()) + + assertFalse(callbacks.rekeying) + assertTrue(machine.authorizeAuthenticatedPacket()) + } + + @Test + fun `a second kex init during key exchange is fatal`() = runTest { + val callbacks = RecordingCallbacks() + val machine = SshClientStateMachine(callbacks) + + assertTrue(machine.connect()) + assertTrue(machine.receiveVersion(IdBanner())) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + assertTrue(machine.unexpectedKexInit("duplicate KEXINIT")) + + assertTrue("sendProtocolError:duplicate KEXINIT" in callbacks.actions) + assertFalse(machine.receiveKexDhReply(SshMsgKexdhReply())) + assertFalse(machine.receiveKexInit(SshMsgKexinit())) + } + @Test fun `raw KStateMachine and event hierarchy are private`() { val machineField = SshClientStateMachine::class.java.getDeclaredField("stateMachine") @@ -75,6 +132,8 @@ class SshClientStateMachineTest { private class RecordingCallbacks : SshClientCallbacks { val actions = mutableListOf() + var rekeying = false + var authenticationRequestPending = false override fun sendVersion() { actions += "sendVersion" @@ -100,12 +159,21 @@ class SshClientStateMachineTest { override suspend fun receiveKexDhGexReply(msg: SshMsgKexDhGexReply) { actions += "receiveKexDhGexReply" } - override fun isRekeying(): Boolean = false + override fun isRekeying(): Boolean = rekeying + override fun isAuthenticationRequestPending(): Boolean = authenticationRequestPending + override fun authenticationRequestStarted() { + authenticationRequestPending = true + } + override fun authenticationRequestResponseReceived() { + authenticationRequestPending = false + } override fun rekeyStarted() { actions += "rekeyStarted" + rekeying = true } override fun rekeyComplete() { actions += "rekeyComplete" + rekeying = false } override suspend fun sendKexDhGexInit() { actions += "sendKexDhGexInit" @@ -133,9 +201,11 @@ class SshClientStateMachineTest { } override fun authenticationSuccess() { actions += "authenticationSuccess" + authenticationRequestPending = false } override fun authenticationFailure() { actions += "authenticationFailure" + authenticationRequestPending = false } override fun receiveUserauthInfoRequest(msg: SshMsgUserauthInfoRequest) { actions += "receiveUserauthInfoRequest" @@ -151,10 +221,10 @@ class SshClientStateMachineTest { ) { actions += "sendChannelOpen" } - override fun receiveChannelOpenConfirmation(msg: SshMsgChannelOpenConfirmation) { + override suspend fun receiveChannelOpenConfirmation(msg: SshMsgChannelOpenConfirmation) { actions += "receiveChannelOpenConfirmation" } - override fun receiveChannelOpenFailure(msg: SshMsgChannelOpenFailure) { + override suspend fun receiveChannelOpenFailure(msg: SshMsgChannelOpenFailure) { actions += "receiveChannelOpenFailure" } override suspend fun sendChannelRequest( @@ -183,6 +253,9 @@ class SshClientStateMachineTest { override suspend fun disconnect() { actions += "disconnect" } + override suspend fun sendProtocolError(description: String) { + actions += "sendProtocolError:$description" + } override fun onStateEnter(stateName: String) = Unit override fun onStateExit(stateName: String) = Unit } diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt new file mode 100644 index 00000000..d9ccdb62 --- /dev/null +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt @@ -0,0 +1,170 @@ +/* + * ConnectBot SSH Library + * 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.connectbot.sshlib.protocol + +import java.lang.reflect.Proxy +import java.nio.file.Files +import java.nio.file.Path +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +internal object SshStateMachineTlaGenerator { + @JvmStatic + fun main(args: Array) { + require(args.size == 1) { "Expected the generated TLA+ output path" } + val output = Path.of(args.single()) + Files.createDirectories(output.parent) + Files.writeString(output, createFormalModel().renderTla()) + } +} + +class SshStateMachineFormalModelTest { + @Test + fun `channel TLA is serialized from typed runtime operations`() { + val model = createFormalModel() + val rendered = model.renderTla() + + assertTrue("ChannelTransitions == {" in rendered) + model.channelModel.operations + .filter { it.scope != SshChannelOperationScope.CONNECTION_TEARDOWN } + .forEach { operation -> + assertTrue( + "<<\"${operation.sourceStateName}\", \"${operation.eventName}\", \"${operation.targetStateName}\">>" in rendered, + ) + } + } + + @Test + fun `rejected operation policy is not hard coded by TLA renderer`() { + val model = createFormalModel() + val deliberatelyUnsafe = model.copy( + channelModel = model.channelModel.copy( + rejectedOperationEffects = setOf(SshChannelEffect.SEND_DATA), + ), + ) + + assertTrue("channelEffects' = {\"SEND_DATA\"}" in deliberatelyUnsafe.renderTla()) + } + + @Test + fun `channel authorization uses sticky authentication across rekey`() { + val rendered = createFormalModel().renderTla() + + assertTrue("ChannelOperationAllowed(authenticationEstablished, state," in rendered) + assertTrue("ChannelOperationAllowed(isAuthenticated, connectionState, channelState, operation)" in rendered) + assertTrue("connectionState # \"Disconnected\"" in rendered) + assertTrue("\\/ isAuthenticated" in rendered) + assertTrue("connectionState = \"Authenticated\"" !in rendered) + } + + @Test + fun `every KStateMachine transition has unique formal metadata`() { + val model = createFormalModel() + + assertEquals(SshTransitionId.entries.size, model.transitions.size) + assertEquals(SshTransitionId.entries.toSet(), model.transitions.map { it.meta.id }.toSet()) + assertTrue(model.transitions.all { it.sourceStateNames.isNotEmpty() }) + } + + @Test + fun `rekey guards are shared by Kotlin execution and TLA generation`() { + val transitions = createFormalModel().transitions.associateBy { it.meta.id } + + assertEquals( + "~(rekeying)", + transitions.getValue(SshTransitionId.RECEIVE_INITIAL_NEW_KEYS).meta.guard.renderTla(), + ) + assertEquals( + "rekeying", + transitions.getValue(SshTransitionId.RECEIVE_REKEY_NEW_KEYS).meta.guard.renderTla(), + ) + assertTrue(transitions.getValue(SshTransitionId.RECEIVE_REKEY_NEW_KEYS).meta.targetIsHistory) + } + + @Test + fun `authentication requests are explicit formal side effects`() { + val transitions = createFormalModel().transitions.associateBy { it.meta.id } + + assertEquals( + setOf(SshEffect.SEND_USERAUTH_REQUEST), + transitions.getValue(SshTransitionId.BEGIN_AUTHENTICATION).meta.effects, + ) + assertEquals( + setOf(SshEffect.SEND_USERAUTH_REQUEST), + transitions.getValue(SshTransitionId.REPEAT_BEGIN_AUTHENTICATION).meta.effects, + ) + assertEquals( + "~(authRequestPending)", + transitions.getValue(SshTransitionId.BEGIN_AUTHENTICATION).meta.guard.renderTla(), + ) + assertEquals( + "~(authRequestPending)", + transitions.getValue(SshTransitionId.REPEAT_BEGIN_AUTHENTICATION).meta.guard.renderTla(), + ) + } + + @Test + fun `unexpected kex init is modeled as fatal from every mid kex state`() { + val transitions = createFormalModel().transitions + .filter { it.meta.eventName == "UnexpectedKexInit" } + + assertEquals( + setOf("WaitKex", "WaitKexDhGexInit", "WaitNewKeys"), + transitions.flatMapTo(mutableSetOf()) { it.sourceStateNames }, + ) + assertTrue(transitions.all { it.meta.targetStateName == "Disconnected" }) + assertTrue( + transitions.all { + it.meta.effects == setOf(SshEffect.SEND_PROTOCOL_ERROR, SshEffect.DISCONNECT) + }, + ) + } + + @Test + fun `TLC checks global operations for channel non-interference`() { + val handwritten = Files.readString(Path.of("src/test/resources/tla/SshClientStateMachine.tla")) + val config = Files.readString(Path.of("src/test/resources/tla/SshClientStateMachine.cfg")) + + assertTrue("GlobalOperationsPreserveChannels ==" in handwritten) + assertTrue("GlobalChannelMutationIsDisconnectCascade ==" in handwritten) + assertTrue("INVARIANT GlobalOperationsPreserveChannels" in config) + assertTrue("INVARIANT GlobalChannelMutationIsDisconnectCascade" in config) + } + + @Test + fun `checked in TLA model matches KStateMachine declaration`() { + val expected = Files.readString(Path.of("src/test/resources/tla/SshClientStateMachineGenerated.tla")) + + assertEquals(expected, createFormalModel().renderTla()) + } +} + +private fun createFormalModel(): SshStateMachineFormalModel { + val callbacks = Proxy.newProxyInstance( + SshClientCallbacks::class.java.classLoader, + arrayOf(SshClientCallbacks::class.java), + ) { _, method, _ -> + when { + method.returnType == Boolean::class.javaPrimitiveType -> false + method.returnType == Void.TYPE -> null + else -> Unit + } + } as SshClientCallbacks + return SshClientStateMachine(callbacks).formalModel() +} diff --git a/sshlib/src/test/resources/tla/README.md b/sshlib/src/test/resources/tla/README.md new file mode 100644 index 00000000..5a867ce9 --- /dev/null +++ b/sshlib/src/test/resources/tla/README.md @@ -0,0 +1,37 @@ +# SSH lifecycle TLA+ model + +This model uses TLA+ to explore the SSH client's connection and channel state machines and check +that their safety rules hold for every reachable state. It is intended to catch invalid behavior +such as bypassing authentication, treating an unparsed packet as genuine, sending higher-layer +packets during key exchange, or applying channel effects to the wrong channel. It does not +currently check liveness properties. + +The connection model covers initial key exchange, authentication, rekeying, and disconnection. +The channel model adds a small registry of channels so TLC can verify that an operation on one +channel does not affect another. Global connection operations must leave channels unchanged except +for disconnection, which closes every allocated channel. Rekeying must also preserve channel state +and allow valid channel operations to resume with the same guards afterward. + +Most of the model is generated from the KStateMachine declarations and their typed TLA+ metadata: + +- `SshClientStateMachineGenerated.tla` contains the generated states, transitions, guards, and + side effects. Do not edit it directly. +- `SshClientStateMachine.tla` defines the handwritten safety properties. +- `SshClientStateMachine.cfg` configures the states and properties that TLC explores. + +Regenerate the structural model with: + +```bash +./gradlew :sshlib:generateSshStateMachineTla +``` + +The unit tests fail if the checked-in generated model is out of date. To run TLC with an official +`tla2tools.jar`, use: + +```bash +./gradlew :sshlib:checkSshStateMachineTla \ + -Ptla2toolsJar=/path/to/tla2tools.jar +``` + +`TLA2TOOLS_JAR=/path/to/tla2tools.jar` may be used instead of the Gradle property. CI downloads the +pinned official release, verifies its SHA-256 digest, and runs the same check. diff --git a/sshlib/src/test/resources/tla/SshClientStateMachine.cfg b/sshlib/src/test/resources/tla/SshClientStateMachine.cfg new file mode 100644 index 00000000..c3d5b9da --- /dev/null +++ b/sshlib/src/test/resources/tla/SshClientStateMachine.cfg @@ -0,0 +1,36 @@ +SPECIFICATION Spec + +CONSTANT MaxChannels = 2 + +VIEW ModelView + +INVARIANT TypeOK +INVARIANT NoInvalidChannelSideEffects +INVARIANT ChannelIsolation +INVARIANT GlobalOperationsPreserveChannels +INVARIANT GlobalChannelMutationIsDisconnectCascade +INVARIANT DisconnectedClosesChannels +INVARIANT NoChannelsBeforeAuthentication +INVARIANT RekeyTransitionsPreserveChannels +INVARIANT AuthenticatedRekeyChannelGuardsRemainEnabled +INVARIANT NoAuthenticatedEffectsBeforeAuthentication +INVARIANT AuthenticatedEventsAreGuarded +INVARIANT ParsedPacketProvenance +INVARIANT NoForgedPacketProvenance +INVARIANT AuthenticationSuccessIsGuarded +INVARIANT AuthenticationPacketIsGuarded +INVARIANT AuthenticationStateIsMonotonic +INVARIANT RekeyStartIsWellFormed +INVARIANT RekeyingHasSavedPostAuthenticationState +INVARIANT RekeyCompletionIsWellFormed +INVARIANT NoHigherLayerPacketsSentDuringKex +INVARIANT AuthenticationRequestIsGuarded +INVARIANT AuthenticationRequestResponseClearsPending +INVARIANT KexEventsAreStrictlySequenced +INVARIANT UserAuthenticationRequiresInitialNewKeys +INVARIANT UnexpectedKexInitIsFatal + +PROPERTY AuthenticationNeverDowngrades +PROPERTY DisconnectedIsTerminal + +CHECK_DEADLOCK FALSE diff --git a/sshlib/src/test/resources/tla/SshClientStateMachine.tla b/sshlib/src/test/resources/tla/SshClientStateMachine.tla new file mode 100644 index 00000000..1f88d492 --- /dev/null +++ b/sshlib/src/test/resources/tla/SshClientStateMachine.tla @@ -0,0 +1,228 @@ +---- MODULE SshClientStateMachine ---- +EXTENDS SshClientStateMachineGenerated + +AuthenticatedOnlyEffects == { + "ReceiveChannelFailure", + "ReceiveChannelOpenConfirmation", + "ReceiveChannelOpenFailure", + "ReceiveChannelSuccess", + "ReceiveGlobalRequest", + "SendChannelOpen", + "SendChannelRequest" +} + +AuthenticatedOnlyEvents == { + "AuthorizeAuthenticatedPacket", + "OpenChannel", + "ReceiveChannelFailure", + "ReceiveChannelOpenConfirmation", + "ReceiveChannelOpenFailure", + "ReceiveChannelSuccess", + "ReceiveGlobalRequest", + "SendChannelRequest" +} + +AuthenticationEstablishedStates == + {"Authenticated", "Disconnected"} \cup KexStates + +HigherLayerOutboundEffects == { + "SendChannelOpen", + "SendChannelRequest", + "SendServiceRequest", + "SendUserauthRequest" +} + +AuthenticationRequestEvents == + {"BeginAuthentication"} + +TypeOK == + /\ state \in States + /\ previousState \in States + /\ history \in PostAuthenticatedStates + /\ event \in Events \cup {"None"} + /\ origin \in Origins + /\ packetWasParsed \in BOOLEAN + /\ effects \subseteq Effects + /\ rekeying \in BOOLEAN + /\ authenticationEstablished \in BOOLEAN + /\ initialNewKeysActive \in BOOLEAN + /\ authRequestPending \in BOOLEAN + /\ previousAuthRequestPending \in BOOLEAN + /\ MaxChannels \in Nat \ {0} + /\ channels \in [ChannelIDs -> ChannelStates] + /\ previousChannels \in [ChannelIDs -> ChannelStates] + /\ activeChannel \in ChannelAttemptIDs + /\ channelEvent \in ChannelEvents \cup {"None"} + /\ channelOrigin \in ChannelOrigins \cup {"None"} + /\ channelEffects \subseteq ChannelEffectSet + +NoInvalidChannelSideEffects == + channelEffects # {} => + /\ activeChannel \in ChannelIDs + /\ ChannelOperationAllowed( + authenticationEstablished, + state, + previousChannels[activeChannel], + channelEvent + ) + /\ channelEffects = ChannelEffectsFor( + previousChannels[activeChannel], + channelEvent + ) + /\ channelOrigin = ChannelOriginFor(channelEvent) + +ChannelIsolation == + activeChannel \in ChannelIDs => + \A other \in ChannelIDs \ {activeChannel} : + channels[other] = previousChannels[other] + +GlobalOperationsPreserveChannels == + activeChannel = 0 /\ "Disconnect" \notin effects => + channels = previousChannels + +GlobalChannelMutationIsDisconnectCascade == + activeChannel = 0 /\ channels # previousChannels => + /\ "Disconnect" \in effects + /\ state = "Disconnected" + /\ \A channel \in ChannelIDs : + channels[channel] = + IF previousChannels[channel] = "Unallocated" THEN "Unallocated" ELSE "CLOSED" + +DisconnectedClosesChannels == + state = "Disconnected" => + \A channel \in ChannelIDs : + channels[channel] \in {"Unallocated", "CLOSED"} + +NoChannelsBeforeAuthentication == + ~authenticationEstablished => + \A channel \in ChannelIDs : channels[channel] = "Unallocated" + +RekeyTransitionsPreserveChannels == + activeChannel = 0 /\ + (event = "RekeyStarted" \/ rekeying \/ "RekeyComplete" \in effects) => + channels = previousChannels + +AuthenticatedRekeyChannelGuardsRemainEnabled == + authenticationEstablished /\ state \in KexStates => + \A channel \in ChannelIDs : + \A operation \in ChannelEvents : + ChannelTransitionDefined(channels[channel], operation) => + ChannelOperationAllowed( + authenticationEstablished, + state, + channels[channel], + operation + ) + +ModelView == + <> + +AuthenticationStateIsMonotonic == + authenticationEstablished => state \in AuthenticationEstablishedStates + +AuthenticationNeverDowngrades == + [] (authenticationEstablished => [] authenticationEstablished) + +DisconnectedIsTerminal == + [] (state = "Disconnected" => [] (state = "Disconnected")) + +NoAuthenticatedEffectsBeforeAuthentication == + previousState # "Authenticated" => effects \cap AuthenticatedOnlyEffects = {} + +AuthenticatedEventsAreGuarded == + event \in AuthenticatedOnlyEvents => previousState = "Authenticated" + +ParsedPacketProvenance == + origin = "ParsedPacket" => packetWasParsed + +NoForgedPacketProvenance == + packetWasParsed => origin = "ParsedPacket" + +AuthenticationSuccessIsGuarded == + event = "AuthenticationSuccess" => + /\ previousState = "Authenticating" + /\ state = "Authenticated" + +AuthenticationPacketIsGuarded == + event = "AuthorizeAuthenticationPacket" => previousState = "Authenticating" + +RekeyStartIsWellFormed == + event = "RekeyStarted" => + /\ previousState \in PostAuthenticatedStates + /\ state = "WaitKexInit" + /\ history = previousState + /\ rekeying + +RekeyingHasSavedPostAuthenticationState == + rekeying => + /\ state \in KexStates + /\ history \in PostAuthenticatedStates + +RekeyCompletionIsWellFormed == + "RekeyComplete" \in effects => + /\ event = "ReceiveNewKeys" + /\ previousState = "WaitNewKeys" + /\ state = history + /\ ~rekeying + +NoHigherLayerPacketsSentDuringKex == + state \in KexStates => effects \cap HigherLayerOutboundEffects = {} + +AuthenticationRequestIsGuarded == + event \in AuthenticationRequestEvents => + /\ previousState \in {"AuthenticationReady", "Authenticating"} + /\ ~authenticationEstablished + /\ ~previousAuthRequestPending + /\ authRequestPending + +AuthenticationRequestResponseClearsPending == + event \in {"AuthenticationSuccess", "AuthenticationFailure", "AuthorizeAuthenticationPacket"} => + ~authRequestPending + +KexEventsAreStrictlySequenced == + /\ event = "ReceiveKexInit" => + /\ previousState = "WaitKexInit" + /\ state = "WaitKex" + /\ "SendKexExchangeInit" \in effects + /\ event \in {"ReceiveKex.DhReply", "ReceiveKex.EcdhReply"} => + /\ previousState = "WaitKex" + /\ state = "WaitNewKeys" + /\ "SendNewKeys" \in effects + /\ event = "ReceiveKex.DhGexGroup" => + /\ previousState = "WaitKex" + /\ state = "WaitKexDhGexInit" + /\ "SendKexDhGexInit" \in effects + /\ event = "ReceiveKex.DhGexReply" => + /\ previousState = "WaitKexDhGexInit" + /\ state = "WaitNewKeys" + /\ "SendNewKeys" \in effects + /\ event = "ReceiveNewKeys" => + /\ previousState = "WaitNewKeys" + /\ "ActivateEncryption" \in effects + +UserAuthenticationRequiresInitialNewKeys == + event = "BeginAuthentication" \/ "StartAuthentication" \in effects \/ "SendUserauthRequest" \in effects => + initialNewKeysActive + +UnexpectedKexInitIsFatal == + event = "UnexpectedKexInit" => + /\ previousState \in {"WaitKex", "WaitKexDhGexInit", "WaitNewKeys"} + /\ state = "Disconnected" + /\ "SendProtocolError" \in effects + /\ "Disconnect" \in effects + +==== diff --git a/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla b/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla new file mode 100644 index 00000000..3bdf542e --- /dev/null +++ b/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla @@ -0,0 +1,999 @@ +---- MODULE SshClientStateMachineGenerated ---- +\* Generated from SshClientStateMachine. Do not edit. +\* Model SHA-256: 882c266edfb2fed9a28f79bc2ce7a5d343d87371ecfc9c9ca2ff42c467ed0a5f +\* Lifecycle states: 11; transitions: 36. +\* TLC distinct states count full variable valuations, not lifecycle nodes. +EXTENDS Naturals + +CONSTANT MaxChannels + +ChannelIDs == 1..MaxChannels +ChannelAttemptIDs == 0..(MaxChannels + 1) + +VARIABLES state, previousState, history, event, origin, packetWasParsed, effects, rekeying, authenticationEstablished, initialNewKeysActive, authRequestPending, previousAuthRequestPending, previousChannels, activeChannel, channelEvent, channelOrigin, channels, channelEffects + +vars == <> + +States == {"Authenticated", "Authenticating", "AuthenticationReady", "Disconnected", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} +PostAuthenticatedStates == {"Authenticated", "Authenticating", "AuthenticationReady"} +KexStates == {"WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys"} +Events == {"AuthenticationFailure", "AuthenticationSuccess", "AuthorizeAuthenticatedPacket", "AuthorizeAuthenticationPacket", "AuthorizeConnectionPacket", "AuthorizeExtInfo", "BeginAuthentication", "Connect", "Disconnect", "OpenChannel", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveDebug", "ReceiveGlobalRequest", "ReceiveIgnore", "ReceiveKex.DhGexGroup", "ReceiveKex.DhGexReply", "ReceiveKex.DhReply", "ReceiveKex.EcdhReply", "ReceiveKexInit", "ReceiveNewKeys", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RekeyStarted", "SendChannelRequest", "UnexpectedKexInit"} +Origins == {"Internal", "LocalCommand", "ParsedPacket", "Timer"} +Effects == {"ActivateEncryption", "AuthenticationFailure", "AuthenticationSuccess", "Debug", "Disconnect", "Ignore", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveGlobalRequest", "ReceiveKexDhGexReply", "ReceiveKexDhReply", "ReceiveKexEcdhReply", "ReceiveKexInit", "ReceiveNewKeys", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RekeyComplete", "RekeyStarted", "SendChannelOpen", "SendChannelRequest", "SendClientExtInfo", "SendKexDhGexInit", "SendKexExchangeInit", "SendKexInit", "SendNewKeys", "SendProtocolError", "SendServiceRequest", "SendUserauthRequest", "SendVersion", "StartAuthentication"} + +ChannelStates == {"BOTH_EOF", "CLOSED", "CLOSE_SENT", "LOCAL_EOF", "OPEN", "OPENING", "REMOTE_EOF", "Unallocated"} +ChannelEvents == {"AcceptRemoteOpen", "AllocateLocalOpen", "OpenConfirmed", "OpenFailed", "ReceiveClose", "ReceiveData", "ReceiveEof", "ReceiveRequest", "ReceiveWindowAdjust", "SendClose", "SendData", "SendEof", "SendRequest"} +ChannelAttemptEvents == {"AcceptRemoteOpen", "ReceiveClose", "ReceiveData", "ReceiveEof", "ReceiveRequest", "ReceiveWindowAdjust", "SendClose", "SendData", "SendEof"} +ChannelEffectSet == {"ADJUST_WINDOW", "CLOSE_CHANNEL", "CLOSE_INBOUND_STREAMS", "COMPLETE_OPEN", "DELIVER_DATA", "DELIVER_REQUEST", "FAIL_OPEN", "SEND_CLOSE", "SEND_DATA", "SEND_EOF", "SEND_OPEN", "SEND_OPEN_CONFIRMATION", "SEND_REQUEST"} +ChannelOrigins == {"ConnectionControl", "LocalCommand", "ParsedPacket"} +ChannelTransitions == { + <<"BOTH_EOF", "ReceiveClose", "CLOSED">>, + <<"BOTH_EOF", "ReceiveRequest", "BOTH_EOF">>, + <<"BOTH_EOF", "ReceiveWindowAdjust", "BOTH_EOF">>, + <<"BOTH_EOF", "SendClose", "CLOSE_SENT">>, + <<"BOTH_EOF", "SendRequest", "BOTH_EOF">>, + <<"CLOSE_SENT", "ReceiveClose", "CLOSED">>, + <<"LOCAL_EOF", "ReceiveClose", "CLOSED">>, + <<"LOCAL_EOF", "ReceiveData", "LOCAL_EOF">>, + <<"LOCAL_EOF", "ReceiveEof", "BOTH_EOF">>, + <<"LOCAL_EOF", "ReceiveRequest", "LOCAL_EOF">>, + <<"LOCAL_EOF", "ReceiveWindowAdjust", "LOCAL_EOF">>, + <<"LOCAL_EOF", "SendClose", "CLOSE_SENT">>, + <<"LOCAL_EOF", "SendRequest", "LOCAL_EOF">>, + <<"OPEN", "ReceiveClose", "CLOSED">>, + <<"OPEN", "ReceiveData", "OPEN">>, + <<"OPEN", "ReceiveEof", "REMOTE_EOF">>, + <<"OPEN", "ReceiveRequest", "OPEN">>, + <<"OPEN", "ReceiveWindowAdjust", "OPEN">>, + <<"OPEN", "SendClose", "CLOSE_SENT">>, + <<"OPEN", "SendData", "OPEN">>, + <<"OPEN", "SendEof", "LOCAL_EOF">>, + <<"OPEN", "SendRequest", "OPEN">>, + <<"OPENING", "OpenConfirmed", "OPEN">>, + <<"OPENING", "OpenFailed", "CLOSED">>, + <<"REMOTE_EOF", "ReceiveClose", "CLOSED">>, + <<"REMOTE_EOF", "ReceiveRequest", "REMOTE_EOF">>, + <<"REMOTE_EOF", "ReceiveWindowAdjust", "REMOTE_EOF">>, + <<"REMOTE_EOF", "SendClose", "CLOSE_SENT">>, + <<"REMOTE_EOF", "SendData", "REMOTE_EOF">>, + <<"REMOTE_EOF", "SendEof", "BOTH_EOF">>, + <<"REMOTE_EOF", "SendRequest", "REMOTE_EOF">>, + <<"Unallocated", "AcceptRemoteOpen", "OPEN">>, + <<"Unallocated", "AllocateLocalOpen", "OPENING">> +} +ChannelAuthenticationRequired == { + <<"BOTH_EOF", "ReceiveClose">>, + <<"BOTH_EOF", "ReceiveRequest">>, + <<"BOTH_EOF", "ReceiveWindowAdjust">>, + <<"BOTH_EOF", "SendClose">>, + <<"BOTH_EOF", "SendRequest">>, + <<"CLOSE_SENT", "ReceiveClose">>, + <<"LOCAL_EOF", "ReceiveClose">>, + <<"LOCAL_EOF", "ReceiveData">>, + <<"LOCAL_EOF", "ReceiveEof">>, + <<"LOCAL_EOF", "ReceiveRequest">>, + <<"LOCAL_EOF", "ReceiveWindowAdjust">>, + <<"LOCAL_EOF", "SendClose">>, + <<"LOCAL_EOF", "SendRequest">>, + <<"OPEN", "ReceiveClose">>, + <<"OPEN", "ReceiveData">>, + <<"OPEN", "ReceiveEof">>, + <<"OPEN", "ReceiveRequest">>, + <<"OPEN", "ReceiveWindowAdjust">>, + <<"OPEN", "SendClose">>, + <<"OPEN", "SendData">>, + <<"OPEN", "SendEof">>, + <<"OPEN", "SendRequest">>, + <<"OPENING", "OpenConfirmed">>, + <<"OPENING", "OpenFailed">>, + <<"REMOTE_EOF", "ReceiveClose">>, + <<"REMOTE_EOF", "ReceiveRequest">>, + <<"REMOTE_EOF", "ReceiveWindowAdjust">>, + <<"REMOTE_EOF", "SendClose">>, + <<"REMOTE_EOF", "SendData">>, + <<"REMOTE_EOF", "SendEof">>, + <<"REMOTE_EOF", "SendRequest">>, + <<"Unallocated", "AcceptRemoteOpen">>, + <<"Unallocated", "AllocateLocalOpen">> +} + +ChannelTransitionDefined(channelState, operation) == + \E target \in ChannelStates : <> \in ChannelTransitions + +ChannelTransitionTarget(channelState, operation) == + CHOOSE target \in ChannelStates : <> \in ChannelTransitions + +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 = "SendRequest" -> {"SEND_REQUEST"} + [] /\ channelState = "CLOSE_SENT" /\ operation = "ReceiveClose" -> {"CLOSE_CHANNEL"} + [] /\ 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 = "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 = "SendData" -> {"SEND_DATA"} + [] /\ channelState = "OPEN" /\ operation = "SendEof" -> {"SEND_EOF"} + [] /\ channelState = "OPEN" /\ operation = "SendRequest" -> {"SEND_REQUEST"} + [] /\ channelState = "OPENING" /\ operation = "OpenConfirmed" -> {"COMPLETE_OPEN"} + [] /\ channelState = "OPENING" /\ operation = "OpenFailed" -> {"FAIL_OPEN"} + [] /\ 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 = "SendData" -> {"SEND_DATA"} + [] /\ channelState = "REMOTE_EOF" /\ operation = "SendEof" -> {"SEND_EOF"} + [] /\ channelState = "REMOTE_EOF" /\ operation = "SendRequest" -> {"SEND_REQUEST"} + [] /\ channelState = "Unallocated" /\ operation = "AcceptRemoteOpen" -> {"SEND_OPEN_CONFIRMATION"} + [] /\ channelState = "Unallocated" /\ operation = "AllocateLocalOpen" -> {"SEND_OPEN"} + [] OTHER -> {} + +ChannelOriginFor(operation) == + CASE operation = "ReceiveClose" -> "ParsedPacket" + [] operation = "ReceiveRequest" -> "ParsedPacket" + [] operation = "ReceiveWindowAdjust" -> "ParsedPacket" + [] operation = "SendClose" -> "LocalCommand" + [] operation = "SendRequest" -> "LocalCommand" + [] operation = "ReceiveData" -> "ParsedPacket" + [] operation = "ReceiveEof" -> "ParsedPacket" + [] operation = "SendData" -> "LocalCommand" + [] operation = "SendEof" -> "LocalCommand" + [] operation = "OpenConfirmed" -> "ParsedPacket" + [] operation = "OpenFailed" -> "ParsedPacket" + [] operation = "AcceptRemoteOpen" -> "ParsedPacket" + [] operation = "AllocateLocalOpen" -> "LocalCommand" + [] OTHER -> "None" + +ChannelOperationAllowed(isAuthenticated, connectionState, channelState, operation) == + /\ ChannelTransitionDefined(channelState, operation) + /\ connectionState # "Disconnected" + /\ (<> \notin ChannelAuthenticationRequired + \/ isAuthenticated) + +AttemptChannelOperation == + /\ activeChannel' \in ChannelAttemptIDs + /\ channelEvent' \in ChannelAttemptEvents + /\ channelOrigin' = ChannelOriginFor(channelEvent') + /\ previousChannels' = channels + /\ IF activeChannel' \in ChannelIDs + /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], channelEvent') + THEN + /\ channels' = [channels EXCEPT ![activeChannel'] = ChannelTransitionTarget(channels[activeChannel'], channelEvent')] + /\ channelEffects' = ChannelEffectsFor(channels[activeChannel'], channelEvent') + ELSE + /\ channels' = channels + /\ channelEffects' = {} + /\ UNCHANGED <> + +Init == + /\ state = "Unconnected" + /\ previousState = "Unconnected" + /\ history = "AuthenticationReady" + /\ event = "None" + /\ origin = "Internal" + /\ packetWasParsed = FALSE + /\ effects = {} + /\ rekeying = FALSE + /\ authenticationEstablished = FALSE + /\ initialNewKeysActive = FALSE + /\ authRequestPending = FALSE + /\ previousAuthRequestPending = FALSE + /\ previousChannels = [c \in ChannelIDs |-> "Unallocated"] + /\ activeChannel = 0 + /\ channelEvent = "None" + /\ channelOrigin = "None" + /\ channels = [c \in ChannelIDs |-> "Unallocated"] + /\ channelEffects = {} + +AUTHENTICATION_FAILURE == + /\ state \in {"Authenticating"} + /\ state' = "AuthenticationReady" + /\ previousState' = state + /\ history' = history + /\ event' = "AuthenticationFailure" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"AuthenticationFailure"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +AUTHENTICATION_SUCCESS == + /\ state \in {"Authenticating"} + /\ state' = "Authenticated" + /\ previousState' = state + /\ history' = history + /\ event' = "AuthenticationSuccess" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"AuthenticationSuccess"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = TRUE + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +AUTHORIZE_AUTHENTICATED_PACKET == + /\ state \in {"Authenticated"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "AuthorizeAuthenticatedPacket" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +AUTHORIZE_AUTHENTICATION_PACKET == + /\ state \in {"Authenticating"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "AuthorizeAuthenticationPacket" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +AUTHORIZE_CONNECTION_PACKET == + /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "AuthorizeConnectionPacket" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +AUTHORIZE_POST_AUTH_EXT_INFO == + /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "AuthorizeExtInfo" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +AUTHORIZE_SERVICE_EXT_INFO == + /\ state \in {"WaitService"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "AuthorizeExtInfo" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +BEGIN_AUTHENTICATION == + /\ state \in {"AuthenticationReady"} + /\ ~(authRequestPending) + /\ state' = "Authenticating" + /\ previousState' = state + /\ history' = history + /\ event' = "BeginAuthentication" + /\ origin' = "LocalCommand" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"SendUserauthRequest"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = TRUE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +CONNECT == + /\ state \in {"Unconnected"} + /\ state' = "WaitVersion" + /\ previousState' = state + /\ history' = history + /\ event' = "Connect" + /\ origin' = "LocalCommand" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"SendVersion"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +DISCONNECT == + /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ state' = "Disconnected" + /\ previousState' = state + /\ history' = history + /\ event' = "Disconnect" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Disconnect"} + /\ rekeying' = FALSE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] + /\ channelEffects' = {} + +OPEN_CHANNEL == + /\ state \in {"Authenticated"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "OpenChannel" + /\ origin' = "LocalCommand" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"SendChannelOpen"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' \in ChannelIDs /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], "AllocateLocalOpen") + /\ channelEvent' = "AllocateLocalOpen" + /\ channelOrigin' = ChannelOriginFor("AllocateLocalOpen") + /\ channels' = [channels EXCEPT ![activeChannel'] = ChannelTransitionTarget(channels[activeChannel'], "AllocateLocalOpen")] + /\ channelEffects' = ChannelEffectsFor(channels[activeChannel'], "AllocateLocalOpen") + +RECEIVE_CHANNEL_FAILURE == + /\ state \in {"Authenticated"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveChannelFailure" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveChannelFailure"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_CHANNEL_OPEN_CONFIRMATION == + /\ state \in {"Authenticated"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveChannelOpenConfirmation" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveChannelOpenConfirmation"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' \in ChannelIDs /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], "OpenConfirmed") + /\ channelEvent' = "OpenConfirmed" + /\ channelOrigin' = ChannelOriginFor("OpenConfirmed") + /\ channels' = [channels EXCEPT ![activeChannel'] = ChannelTransitionTarget(channels[activeChannel'], "OpenConfirmed")] + /\ channelEffects' = ChannelEffectsFor(channels[activeChannel'], "OpenConfirmed") + +RECEIVE_CHANNEL_OPEN_FAILURE == + /\ state \in {"Authenticated"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveChannelOpenFailure" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveChannelOpenFailure"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' \in ChannelIDs /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], "OpenFailed") + /\ channelEvent' = "OpenFailed" + /\ channelOrigin' = ChannelOriginFor("OpenFailed") + /\ channels' = [channels EXCEPT ![activeChannel'] = ChannelTransitionTarget(channels[activeChannel'], "OpenFailed")] + /\ channelEffects' = ChannelEffectsFor(channels[activeChannel'], "OpenFailed") + +RECEIVE_CHANNEL_SUCCESS == + /\ state \in {"Authenticated"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveChannelSuccess" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveChannelSuccess"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_DEBUG == + /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveDebug" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Debug"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_GLOBAL_REQUEST == + /\ state \in {"Authenticated"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveGlobalRequest" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveGlobalRequest"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_IGNORE == + /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveIgnore" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Ignore"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_INITIAL_NEW_KEYS == + /\ state \in {"WaitNewKeys"} + /\ ~(rekeying) + /\ state' = "WaitService" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveNewKeys" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ActivateEncryption", "ReceiveNewKeys", "SendClientExtInfo", "SendServiceRequest"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = TRUE + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_KEX_DH_GEX_GROUP == + /\ state \in {"WaitKex"} + /\ state' = "WaitKexDhGexInit" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveKex.DhGexGroup" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"SendKexDhGexInit"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_KEX_DH_GEX_REPLY == + /\ state \in {"WaitKexDhGexInit"} + /\ state' = "WaitNewKeys" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveKex.DhGexReply" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveKexDhGexReply", "SendNewKeys"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_KEX_DH_REPLY == + /\ state \in {"WaitKex"} + /\ state' = "WaitNewKeys" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveKex.DhReply" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveKexDhReply", "SendNewKeys"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_KEX_ECDH_REPLY == + /\ state \in {"WaitKex"} + /\ state' = "WaitNewKeys" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveKex.EcdhReply" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveKexEcdhReply", "SendNewKeys"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_KEX_INIT == + /\ state \in {"WaitKexInit"} + /\ state' = "WaitKex" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveKexInit" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveKexInit", "SendKexExchangeInit"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_REKEY_NEW_KEYS == + /\ state \in {"WaitNewKeys"} + /\ rekeying + /\ state' = history + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveNewKeys" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ActivateEncryption", "ReceiveNewKeys", "RekeyComplete"} + /\ rekeying' = FALSE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = TRUE + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_SERVICE_ACCEPT == + /\ state \in {"WaitService"} + /\ state' = "AuthenticationReady" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveServiceAccept" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveServiceAccept", "StartAuthentication"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_USERAUTH_BANNER_AUTHENTICATING == + /\ state \in {"Authenticating"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveUserauthBanner" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveUserauthBanner"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_USERAUTH_BANNER_READY == + /\ state \in {"AuthenticationReady"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveUserauthBanner" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveUserauthBanner"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_USERAUTH_INFO_REQUEST == + /\ state \in {"Authenticating"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveUserauthInfoRequest" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveUserauthInfoRequest"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_VERSION == + /\ state \in {"WaitVersion"} + /\ state' = "WaitKexInit" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveVersion" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ReceiveVersion", "SendKexInit"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +REKEY_STARTED == + /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady"} + /\ state' = "WaitKexInit" + /\ previousState' = state + /\ history' = state + /\ event' = "RekeyStarted" + /\ origin' \in {"LocalCommand", "ParsedPacket", "Timer"} + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"RekeyStarted", "SendKexInit"} + /\ rekeying' = TRUE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +REPEAT_BEGIN_AUTHENTICATION == + /\ state \in {"Authenticating"} + /\ ~(authRequestPending) + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "BeginAuthentication" + /\ origin' = "LocalCommand" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"SendUserauthRequest"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = TRUE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +SEND_CHANNEL_REQUEST == + /\ state \in {"Authenticated"} + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "SendChannelRequest" + /\ origin' = "LocalCommand" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"SendChannelRequest"} + /\ rekeying' = rekeying + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' \in ChannelIDs /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], "SendRequest") + /\ channelEvent' = "SendRequest" + /\ channelOrigin' = ChannelOriginFor("SendRequest") + /\ channels' = [channels EXCEPT ![activeChannel'] = ChannelTransitionTarget(channels[activeChannel'], "SendRequest")] + /\ channelEffects' = ChannelEffectsFor(channels[activeChannel'], "SendRequest") + +UNEXPECTED_KEX_INIT_WAIT_KEX == + /\ state \in {"WaitKex"} + /\ state' = "Disconnected" + /\ previousState' = state + /\ history' = history + /\ event' = "UnexpectedKexInit" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Disconnect", "SendProtocolError"} + /\ rekeying' = FALSE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] + /\ channelEffects' = {} + +UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT == + /\ state \in {"WaitKexDhGexInit"} + /\ state' = "Disconnected" + /\ previousState' = state + /\ history' = history + /\ event' = "UnexpectedKexInit" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Disconnect", "SendProtocolError"} + /\ rekeying' = FALSE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] + /\ channelEffects' = {} + +UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS == + /\ state \in {"WaitNewKeys"} + /\ state' = "Disconnected" + /\ previousState' = state + /\ history' = history + /\ event' = "UnexpectedKexInit" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Disconnect", "SendProtocolError"} + /\ rekeying' = FALSE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] + /\ channelEffects' = {} + +Next == + \/ AUTHENTICATION_FAILURE + \/ AUTHENTICATION_SUCCESS + \/ AUTHORIZE_AUTHENTICATED_PACKET + \/ AUTHORIZE_AUTHENTICATION_PACKET + \/ AUTHORIZE_CONNECTION_PACKET + \/ AUTHORIZE_POST_AUTH_EXT_INFO + \/ AUTHORIZE_SERVICE_EXT_INFO + \/ BEGIN_AUTHENTICATION + \/ CONNECT + \/ DISCONNECT + \/ OPEN_CHANNEL + \/ RECEIVE_CHANNEL_FAILURE + \/ RECEIVE_CHANNEL_OPEN_CONFIRMATION + \/ RECEIVE_CHANNEL_OPEN_FAILURE + \/ RECEIVE_CHANNEL_SUCCESS + \/ RECEIVE_DEBUG + \/ RECEIVE_GLOBAL_REQUEST + \/ RECEIVE_IGNORE + \/ RECEIVE_INITIAL_NEW_KEYS + \/ RECEIVE_KEX_DH_GEX_GROUP + \/ RECEIVE_KEX_DH_GEX_REPLY + \/ RECEIVE_KEX_DH_REPLY + \/ RECEIVE_KEX_ECDH_REPLY + \/ RECEIVE_KEX_INIT + \/ RECEIVE_REKEY_NEW_KEYS + \/ RECEIVE_SERVICE_ACCEPT + \/ RECEIVE_USERAUTH_BANNER_AUTHENTICATING + \/ RECEIVE_USERAUTH_BANNER_READY + \/ RECEIVE_USERAUTH_INFO_REQUEST + \/ RECEIVE_VERSION + \/ REKEY_STARTED + \/ REPEAT_BEGIN_AUTHENTICATION + \/ SEND_CHANNEL_REQUEST + \/ UNEXPECTED_KEX_INIT_WAIT_KEX + \/ UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT + \/ UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS + \/ AttemptChannelOperation + +Spec == Init /\ [][Next]_vars +====