diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index be26b91..b3c9842 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -77,9 +77,9 @@ jobs: echo "${TLA2TOOLS_SHA256} ${tla2tools_jar}" | sha256sum --check echo "TLA2TOOLS_JAR=${tla2tools_jar}" >> "${GITHUB_ENV}" - - name: Check SSH lifecycle TLA+ model + - name: Check TLA+ models if: matrix.java == '17' - run: ./gradlew :sshlib:checkSshStateMachineTla + run: ./gradlew :sshlib:checkTla - name: Configure Docker mirror run: | diff --git a/sshlib/build.gradle.kts b/sshlib/build.gradle.kts index 5c09d07..b3dffa0 100644 --- a/sshlib/build.gradle.kts +++ b/sshlib/build.gradle.kts @@ -79,6 +79,15 @@ tasks.register("generateSshStateMachineTla") { args(tlaModelDirectory.file("SshClientStateMachineGenerated.tla").asFile.absolutePath) } +tasks.register("generateSftpStateMachineTla") { + group = "verification" + description = "Regenerates the TLA+ lifecycle model from SftpStateMachine" + dependsOn(tasks.testClasses) + classpath = sourceSets.test.get().runtimeClasspath + mainClass.set("org.connectbot.sshlib.protocol.SftpStateMachineTlaGenerator") + args(tlaModelDirectory.file("SftpClientStateMachineGenerated.tla").asFile.absolutePath) +} + val tla2toolsJar = providers.gradleProperty("tla2toolsJar") .orElse(providers.environmentVariable("TLA2TOOLS_JAR")) @@ -106,6 +115,42 @@ tasks.register("checkSshStateMachineTla") { } } +tasks.register("checkSftpStateMachineTla") { + group = "verification" + description = "Checks the generated SFTP lifecycle model with TLC" + mainClass.set("tlc2.TLC") + workingDir(tlaModelDirectory) + args( + "-workers", + "1", + "-metadir", + tlaStateDirectory.get().asFile.absolutePath, + "-config", + "SftpClientStateMachine.cfg", + "SftpClientStateMachine.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) + } +} + +tasks.register("generateTla") { + group = "verification" + description = "Regenerates all TLA+ formal models (SSH and SFTP)" + dependsOn("generateSshStateMachineTla", "generateSftpStateMachineTla") +} + +tasks.register("checkTla") { + group = "verification" + description = "Checks all TLA+ formal models (SSH and SFTP) with TLC" + dependsOn("checkSshStateMachineTla", "checkSftpStateMachineTla") +} + java { withSourcesJar() toolchain { diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/sftp/SftpClientImpl.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/sftp/SftpClientImpl.kt index 426bfea..31fe5a7 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/sftp/SftpClientImpl.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/sftp/SftpClientImpl.kt @@ -21,6 +21,7 @@ import kotlinx.coroutines.CoroutineScope import kotlinx.coroutines.Dispatchers import kotlinx.coroutines.Job import kotlinx.coroutines.SupervisorJob +import kotlinx.coroutines.runBlocking import org.connectbot.sshlib.SftpAttributes import org.connectbot.sshlib.SftpClient import org.connectbot.sshlib.SftpDirectoryEntry @@ -29,9 +30,15 @@ import org.connectbot.sshlib.SftpOpenFlag import org.connectbot.sshlib.SftpResult import org.connectbot.sshlib.SftpStatusCode import org.connectbot.sshlib.SshSession +import org.connectbot.sshlib.protocol.SftpAcceptedTransition +import org.connectbot.sshlib.protocol.SftpState +import org.connectbot.sshlib.protocol.SftpStateMachine import org.slf4j.LoggerFactory import java.nio.ByteBuffer import java.nio.charset.StandardCharsets +import java.util.concurrent.atomic.AtomicBoolean + +private typealias SftpTransition = suspend (suspend (SftpAcceptedTransition) -> Unit) -> Boolean /** * Internal implementation of [SftpClient]. @@ -43,12 +50,13 @@ internal class SftpClientImpl private constructor( private val dispatcher: SftpDispatcher, private val readJob: Job, override val protocolVersion: Int, + private val stateMachine: SftpStateMachine, ) : SftpClient { private val scope = CoroutineScope(Dispatchers.IO + SupervisorJob()) - private var closed = false + private val closed = AtomicBoolean() - override val isOpen: Boolean get() = !closed && session.isOpen + override val isOpen: Boolean get() = !closed.get() && session.isOpen && stateMachine.state == SftpState.READY // --- File I/O --- @@ -62,7 +70,7 @@ internal class SftpClientImpl private constructor( payload.putInt(pflags) payload.put(attrsBytes) - return dispatchRequest(SSH_FXP_OPEN, payload.array()) { response -> + return dispatchRequest(SSH_FXP_OPEN, payload.array(), stateMachine::openFile) { response -> when (response.type) { SSH_FXP_HANDLE -> SftpResult.Success(SftpFileHandle(extractString(ByteBuffer.wrap(response.payload)))) SSH_FXP_STATUS -> decodeStatusError(response.payload) @@ -75,7 +83,7 @@ internal class SftpClientImpl private constructor( val payload = ByteBuffer.allocate(4 + handle.handle.size) putString(payload, handle.handle) - return dispatchRequest(SSH_FXP_CLOSE, payload.array()) { response -> + return dispatchRequest(SSH_FXP_CLOSE, payload.array(), stateMachine::closeHandle) { response -> if (response.type == SSH_FXP_STATUS) { val status = decodeStatus(response.payload) if (status == SftpStatusCode.OK) { @@ -95,7 +103,7 @@ internal class SftpClientImpl private constructor( payload.putLong(offset) payload.putInt(length) - return dispatchRequest(SSH_FXP_READ, payload.array()) { response -> + return dispatchRequest(SSH_FXP_READ, payload.array(), stateMachine::readFile) { response -> when (response.type) { SSH_FXP_DATA -> SftpResult.Success(extractString(ByteBuffer.wrap(response.payload))) @@ -119,7 +127,7 @@ internal class SftpClientImpl private constructor( payload.putLong(offset) putString(payload, data) - return dispatchStatusRequest(SSH_FXP_WRITE, payload.array()) + return dispatchStatusRequest(SSH_FXP_WRITE, payload.array(), stateMachine::writeFile) } // --- Stat operations --- @@ -181,7 +189,7 @@ internal class SftpClientImpl private constructor( val payload = ByteBuffer.allocate(4 + pathBytes.size) putString(payload, pathBytes) - return dispatchRequest(SSH_FXP_OPENDIR, payload.array()) { response -> + return dispatchRequest(SSH_FXP_OPENDIR, payload.array(), stateMachine::openDir) { response -> when (response.type) { SSH_FXP_HANDLE -> SftpResult.Success(SftpFileHandle(extractString(ByteBuffer.wrap(response.payload)))) SSH_FXP_STATUS -> decodeStatusError(response.payload) @@ -194,7 +202,7 @@ internal class SftpClientImpl private constructor( val payload = ByteBuffer.allocate(4 + handle.handle.size) putString(payload, handle.handle) - return dispatchRequest(SSH_FXP_READDIR, payload.array()) { response -> + return dispatchRequest(SSH_FXP_READDIR, payload.array(), stateMachine::readDir) { response -> when (response.type) { SSH_FXP_NAME -> SftpResult.Success(decodeName(response.payload)) @@ -289,10 +297,6 @@ internal class SftpClientImpl private constructor( } override suspend fun symlink(targetPath: String, linkPath: String): SftpResult { - // Note: OpenSSH has a known bug where symlink arguments are reversed - // from the spec. The spec says (targetpath, linkpath) but OpenSSH - // expects (linkpath, targetpath). We follow the OpenSSH convention - // since it's the most common server implementation. val linkBytes = linkPath.toByteArray(StandardCharsets.UTF_8) val targetBytes = targetPath.toByteArray(StandardCharsets.UTF_8) val payload = ByteBuffer.allocate(4 + linkBytes.size + 4 + targetBytes.size) @@ -303,8 +307,10 @@ internal class SftpClientImpl private constructor( } override fun close() { - if (closed) return - closed = true + if (!closed.compareAndSet(false, true)) return + runBlocking { + stateMachine.disconnect { } + } dispatcher.stop() session.close() } @@ -317,8 +323,9 @@ internal class SftpClientImpl private constructor( private suspend fun dispatchRequest( type: Int, payload: ByteArray, + transition: SftpTransition = stateMachine::request, map: (SftpRawPacket) -> SftpResult, - ): SftpResult = when (val result = dispatcher.request(type, payload)) { + ): SftpResult = when (val result = dispatcher.request(type, payload) { action -> transition { action() } }) { is SftpResult.Success -> try { map(result.value) } catch (e: SftpDecodeException) { @@ -335,7 +342,11 @@ internal class SftpClientImpl private constructor( /** * Send a request that expects SSH_FXP_STATUS with OK. */ - private suspend fun dispatchStatusRequest(type: Int, payload: ByteArray): SftpResult = dispatchRequest(type, payload) { response -> + private suspend fun dispatchStatusRequest( + type: Int, + payload: ByteArray, + transition: SftpTransition = stateMachine::request, + ): SftpResult = dispatchRequest(type, payload, transition) { response -> if (response.type == SSH_FXP_STATUS) { val status = decodeStatus(response.payload) if (status == SftpStatusCode.OK) { @@ -395,16 +406,22 @@ internal class SftpClientImpl private constructor( suspend fun create(session: SshSession): SftpResult = create(session, SftpPacketIO(session)) internal suspend fun create(session: SshSession, packetIO: SftpPacketTransport): SftpResult { - val dispatcher = SftpDispatcher(packetIO) + val stateMachine = SftpStateMachine() + val dispatcher = SftpDispatcher(packetIO, stateMachine) // Send SSH_FXP_INIT val initPayload = ByteBuffer.allocate(4) initPayload.putInt(SFTP_VERSION) - when (val w = dispatcher.writeRaw(SSH_FXP_INIT, initPayload.array())) { + var initResult: SftpResult? = null + stateMachine.sendInit { + initResult = dispatcher.writeRaw(SSH_FXP_INIT, initPayload.array()) + } + when (val w = initResult) { is SftpResult.Success -> {} is SftpResult.ServerError -> return w is SftpResult.ProtocolError -> return w is SftpResult.IoError -> return w + null -> return SftpResult.ProtocolError("Failed to send SFTP INIT") } // Read SSH_FXP_VERSION @@ -430,7 +447,7 @@ internal class SftpClientImpl private constructor( val scope = CoroutineScope(Dispatchers.IO + SupervisorJob()) val readJob = dispatcher.startReadLoop(scope) - return SftpResult.Success(SftpClientImpl(session, dispatcher, readJob, negotiatedVersion)) + return SftpResult.Success(SftpClientImpl(session, dispatcher, readJob, negotiatedVersion, stateMachine)) } // --- Wire format helpers --- diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/sftp/SftpDispatcher.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/sftp/SftpDispatcher.kt index 3c95c24..3f135a4 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/sftp/SftpDispatcher.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/sftp/SftpDispatcher.kt @@ -25,6 +25,7 @@ import kotlinx.coroutines.sync.Mutex import kotlinx.coroutines.sync.withLock import kotlinx.coroutines.withTimeout import org.connectbot.sshlib.SftpResult +import org.connectbot.sshlib.protocol.SftpStateMachine import org.slf4j.LoggerFactory import java.nio.ByteBuffer import java.util.concurrent.ConcurrentHashMap @@ -36,7 +37,10 @@ import java.util.concurrent.atomic.AtomicInteger * Each outbound request gets a unique request ID. A background read loop * parses incoming SFTP packets and completes the matching deferred. */ -internal class SftpDispatcher(private val packetIO: SftpPacketTransport) { +internal class SftpDispatcher( + private val packetIO: SftpPacketTransport, + private val stateMachine: SftpStateMachine = SftpStateMachine(), +) { private val nextRequestId = AtomicInteger(1) private val pending = ConcurrentHashMap>() private val writeMutex = Mutex() @@ -50,39 +54,61 @@ internal class SftpDispatcher(private val packetIO: SftpPacketTransport) { * @param timeoutMs Maximum time to wait for a response * @return The raw response packet */ - suspend fun request(type: Int, payload: ByteArray, timeoutMs: Long = 30_000L): SftpResult { - val requestId = nextRequestId.getAndIncrement() - val deferred = CompletableDeferred() - pending[requestId] = deferred - - // Prepend request ID to payload - val fullPayload = ByteBuffer.allocate(4 + payload.size) - fullPayload.putInt(requestId) - fullPayload.put(payload) - - // The framing layer ([packetIO]) now returns sealed SftpResult - // rather than throwing — propagate any error from the write - // straight back to the caller. Timeout / await are still - // exception-paths so they keep the catch. - val writeResult = writeMutex.withLock { - packetIO.writePacket(type, fullPayload.array()) + suspend fun request(type: Int, payload: ByteArray, timeoutMs: Long = 30_000L): SftpResult = request(type, payload, timeoutMs) { action -> + action() + true + } + + /** + * Admit and write a request as one state-machine action, then await its response + * after the state-machine serialization point has been released. + */ + suspend fun request( + type: Int, + payload: ByteArray, + timeoutMs: Long = 30_000L, + authorize: suspend (suspend () -> Unit) -> Boolean, + ): SftpResult { + var requestId = 0 + var deferred: CompletableDeferred? = null + var writeResult: SftpResult? = null + + val authorized = authorize { + requestId = nextRequestId.getAndIncrement() + deferred = CompletableDeferred().also { pending[requestId] = it } + + val fullPayload = ByteBuffer.allocate(4 + payload.size) + fullPayload.putInt(requestId) + fullPayload.put(payload) + + writeResult = writeMutex.withLock { + packetIO.writePacket(type, fullPayload.array()) + } + } + if (!authorized) { + return SftpResult.ProtocolError("SFTP session is not ready") } - if (writeResult is SftpResult.IoError) { + + val response = deferred + ?: return SftpResult.ProtocolError("Authorized SFTP request did not run its action") + val result = writeResult + ?: return SftpResult.ProtocolError("Authorized SFTP request did not produce a write result") + if (result is SftpResult.IoError) { pending.remove(requestId) - return writeResult + return result } - if (writeResult is SftpResult.ProtocolError) { + if (result is SftpResult.ProtocolError) { pending.remove(requestId) - return writeResult + return result } - if (writeResult is SftpResult.ServerError) { + if (result is SftpResult.ServerError) { pending.remove(requestId) - return writeResult + return result } return try { val packet = withTimeout(timeoutMs) { - deferred.await() + response.await() } SftpResult.Success(packet) } catch (e: Exception) { @@ -101,9 +127,14 @@ internal class SftpDispatcher(private val packetIO: SftpPacketTransport) { /** * Read a single raw packet (used for VERSION response during init). - * Just forwards the framing-layer result. */ - suspend fun readRaw(): SftpResult = packetIO.readPacket() + suspend fun readRaw(): SftpResult { + val result = packetIO.readPacket() + if (result is SftpResult.Success && result.value.type == SSH_FXP_VERSION) { + stateMachine.receiveVersion { } + } + return result + } /** * Start the background read loop that routes responses to waiting callers. @@ -117,23 +148,22 @@ internal class SftpDispatcher(private val packetIO: SftpPacketTransport) { is SftpResult.IoError -> { logger.debug("SFTP read loop ended: {}", result.cause.message) - pending.values.forEach { it.completeExceptionally(result.cause) } - pending.clear() + stateMachine.disconnect { failPending(result.cause) } break@loop } is SftpResult.ProtocolError -> { logger.debug("SFTP channel closed: {}", result.message) val err = SftpProtocolException(result.message) - pending.values.forEach { it.completeExceptionally(err) } - pending.clear() + stateMachine.disconnect { failPending(err) } break@loop } is SftpResult.ServerError -> { - // Framing layer never produces ServerError, but the - // sealed exhaustiveness check requires this branch. logger.warn("Unexpected ServerError from packet framing: code={}", result.statusCode) + stateMachine.disconnect { + failPending(SftpProtocolException("Unexpected SFTP framing server error")) + } break@loop } } @@ -144,6 +174,15 @@ internal class SftpDispatcher(private val packetIO: SftpPacketTransport) { continue } + // Notify state machine directly of incoming packet + when (packet.type) { + SSH_FXP_STATUS -> stateMachine.receiveStatus { } + SSH_FXP_HANDLE -> stateMachine.receiveHandle { } + SSH_FXP_DATA -> stateMachine.receiveData { } + SSH_FXP_NAME -> stateMachine.receiveName { } + SSH_FXP_ATTRS -> stateMachine.receiveAttrs { } + } + val requestId = ByteBuffer.wrap(packet.payload, 0, 4).int val responsePayload = packet.payload.copyOfRange(4, packet.payload.size) val responsePacket = SftpRawPacket(packet.type, responsePayload) @@ -156,10 +195,8 @@ internal class SftpDispatcher(private val packetIO: SftpPacketTransport) { } } } catch (e: Exception) { - // Coroutine cancellation or other unexpected error. logger.debug("SFTP read loop ended unexpectedly: {}", e.message) - pending.values.forEach { it.completeExceptionally(e) } - pending.clear() + stateMachine.disconnect { failPending(e) } } } readJob = job @@ -168,13 +205,22 @@ internal class SftpDispatcher(private val packetIO: SftpPacketTransport) { fun stop() { readJob?.cancel() - pending.values.forEach { - it.completeExceptionally(SftpProtocolException("SFTP session closed")) - } + failPending(SftpProtocolException("SFTP session closed")) + } + + private fun failPending(cause: Throwable) { + pending.values.forEach { it.completeExceptionally(cause) } pending.clear() } companion object { private val logger = LoggerFactory.getLogger(SftpDispatcher::class.java) + + private const val SSH_FXP_VERSION = 2 + private const val SSH_FXP_STATUS = 101 + private const val SSH_FXP_HANDLE = 102 + private const val SSH_FXP_DATA = 103 + private const val SSH_FXP_NAME = 104 + private const val SSH_FXP_ATTRS = 105 } } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachine.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachine.kt new file mode 100644 index 0000000..3b8234c --- /dev/null +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachine.kt @@ -0,0 +1,397 @@ +/* + * 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 + +/** + * Protocol lifecycle states for an SFTP session (draft-ietf-secsh-filexfer-02). + */ +internal enum class SftpState { + UNINITIALIZED, + WAIT_VERSION, + READY, + CLOSED, +} + +/** + * Lifecycle states for individual SFTP file/directory handles. + */ +internal enum class SftpHandleState { + Unallocated, + OpenFile, + OpenDir, + Closed, +} + +internal enum class SftpEffect { + SEND_INIT, + RECEIVE_VERSION, + SEND_OPEN_FILE, + SEND_OPEN_DIR, + SEND_READ, + SEND_WRITE, + SEND_READDIR, + SEND_CLOSE_HANDLE, + SEND_REQUEST, + DELIVER_HANDLE, + DELIVER_DATA, + DELIVER_NAME, + DELIVER_ATTRS, + DELIVER_STATUS, + DISCONNECT_SFTP, +} + +internal enum class SftpEventId(val tlaName: String) { + SEND_INIT("SendInit"), + RECEIVE_VERSION("ReceiveVersion"), + OPEN_FILE("OpenFile"), + OPEN_DIR("OpenDir"), + READ_FILE("ReadFile"), + WRITE_FILE("WriteFile"), + READ_DIR("ReadDir"), + CLOSE_HANDLE("CloseHandle"), + REQUEST("Request"), + RECEIVE_HANDLE("ReceiveHandle"), + RECEIVE_DATA("ReceiveData"), + RECEIVE_NAME("ReceiveName"), + RECEIVE_ATTRS("ReceiveAttrs"), + RECEIVE_STATUS("ReceiveStatus"), + DISCONNECT("Disconnect"), +} + +internal enum class SftpEventOrigin { + LOCAL_COMMAND, + PARSED_PACKET, + CONNECTION_CONTROL, +} + +internal enum class SftpTransitionId { + SEND_INIT_UNINITIALIZED, + RECEIVE_VERSION_WAIT_VERSION, + OPEN_FILE_READY, + OPEN_DIR_READY, + READ_FILE_READY, + WRITE_FILE_READY, + READ_DIR_READY, + CLOSE_HANDLE_READY, + REQUEST_READY, + RECEIVE_HANDLE_READY, + RECEIVE_DATA_READY, + RECEIVE_NAME_READY, + RECEIVE_ATTRS_READY, + RECEIVE_STATUS_READY, + DISCONNECT_UNINITIALIZED, + DISCONNECT_WAIT_VERSION, + DISCONNECT_READY, +} + +internal data class SftpTransitionMeta( + val id: SftpTransitionId, + val eventId: SftpEventId, + val source: SftpState, + val target: SftpState, + val effects: Set, + val origin: SftpEventOrigin, + val requiresReadySession: Boolean, +) : MetaInfo + +internal data class SftpAcceptedTransition( + val id: SftpTransitionId, + val effects: Set, + val origin: SftpEventOrigin, +) + +internal data class SftpFormalTransition( + val id: SftpTransitionId, + val eventId: SftpEventId, + val source: SftpState, + val target: SftpState, + val effects: Set, + val origin: SftpEventOrigin, + val requiresReadySession: Boolean, +) + +internal data class SftpFormalModel( + val states: Set, + val transitions: List, +) + +/** + * Source of truth for SFTP Client State Machine. + */ +internal class SftpStateMachine { + private sealed class SftpEvent( + val id: SftpEventId, + val effects: Set, + val origin: SftpEventOrigin, + val action: suspend (SftpAcceptedTransition) -> Unit, + val requiresReadySession: Boolean = true, + ) : Event { + class SendInit(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.SEND_INIT, + setOf(SftpEffect.SEND_INIT), + SftpEventOrigin.LOCAL_COMMAND, + action, + requiresReadySession = false, + ) + + class ReceiveVersion(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.RECEIVE_VERSION, + setOf(SftpEffect.RECEIVE_VERSION), + SftpEventOrigin.PARSED_PACKET, + action, + requiresReadySession = false, + ) + + class OpenFile(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.OPEN_FILE, + setOf(SftpEffect.SEND_OPEN_FILE), + SftpEventOrigin.LOCAL_COMMAND, + action, + ) + + class OpenDir(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.OPEN_DIR, + setOf(SftpEffect.SEND_OPEN_DIR), + SftpEventOrigin.LOCAL_COMMAND, + action, + ) + + class ReadFile(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.READ_FILE, + setOf(SftpEffect.SEND_READ), + SftpEventOrigin.LOCAL_COMMAND, + action, + ) + + class WriteFile(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.WRITE_FILE, + setOf(SftpEffect.SEND_WRITE), + SftpEventOrigin.LOCAL_COMMAND, + action, + ) + + class ReadDir(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.READ_DIR, + setOf(SftpEffect.SEND_READDIR), + SftpEventOrigin.LOCAL_COMMAND, + action, + ) + + class CloseHandle(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.CLOSE_HANDLE, + setOf(SftpEffect.SEND_CLOSE_HANDLE), + SftpEventOrigin.LOCAL_COMMAND, + action, + ) + + class Request(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.REQUEST, + setOf(SftpEffect.SEND_REQUEST), + SftpEventOrigin.LOCAL_COMMAND, + action, + ) + + class ReceiveHandle(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.RECEIVE_HANDLE, + setOf(SftpEffect.DELIVER_HANDLE), + SftpEventOrigin.PARSED_PACKET, + action, + ) + + class ReceiveData(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.RECEIVE_DATA, + setOf(SftpEffect.DELIVER_DATA), + SftpEventOrigin.PARSED_PACKET, + action, + ) + + class ReceiveName(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.RECEIVE_NAME, + setOf(SftpEffect.DELIVER_NAME), + SftpEventOrigin.PARSED_PACKET, + action, + ) + + class ReceiveAttrs(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.RECEIVE_ATTRS, + setOf(SftpEffect.DELIVER_ATTRS), + SftpEventOrigin.PARSED_PACKET, + action, + ) + + class ReceiveStatus(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.RECEIVE_STATUS, + setOf(SftpEffect.DELIVER_STATUS), + SftpEventOrigin.PARSED_PACKET, + action, + ) + + class Disconnect(action: suspend (SftpAcceptedTransition) -> Unit) : + SftpEvent( + SftpEventId.DISCONNECT, + setOf(SftpEffect.DISCONNECT_SFTP), + SftpEventOrigin.CONNECTION_CONTROL, + action, + requiresReadySession = false, + ) + } + + private val mutex = Mutex() + + @Volatile + private var activeState: SftpState = SftpState.UNINITIALIZED + + private val stateMachine: StateMachine = createStdLibStateMachine { + val uninitialized = initialState(SftpState.UNINITIALIZED.name) + val waitVersion = state(SftpState.WAIT_VERSION.name) + val ready = state(SftpState.READY.name) + val closed = finalState(SftpState.CLOSED.name) + + bindState(uninitialized, SftpState.UNINITIALIZED) + bindState(waitVersion, SftpState.WAIT_VERSION) + bindState(ready, SftpState.READY) + bindState(closed, SftpState.CLOSED) + + uninitialized.sftpTransition(SftpEvent.SendInit {}, SftpTransitionId.SEND_INIT_UNINITIALIZED, waitVersion) + waitVersion.sftpTransition(SftpEvent.ReceiveVersion {}, SftpTransitionId.RECEIVE_VERSION_WAIT_VERSION, ready) + + ready.sftpTransition(SftpEvent.OpenFile {}, SftpTransitionId.OPEN_FILE_READY) + ready.sftpTransition(SftpEvent.OpenDir {}, SftpTransitionId.OPEN_DIR_READY) + ready.sftpTransition(SftpEvent.ReadFile {}, SftpTransitionId.READ_FILE_READY) + ready.sftpTransition(SftpEvent.WriteFile {}, SftpTransitionId.WRITE_FILE_READY) + ready.sftpTransition(SftpEvent.ReadDir {}, SftpTransitionId.READ_DIR_READY) + ready.sftpTransition(SftpEvent.CloseHandle {}, SftpTransitionId.CLOSE_HANDLE_READY) + ready.sftpTransition(SftpEvent.Request {}, SftpTransitionId.REQUEST_READY) + + ready.sftpTransition(SftpEvent.ReceiveHandle {}, SftpTransitionId.RECEIVE_HANDLE_READY) + ready.sftpTransition(SftpEvent.ReceiveData {}, SftpTransitionId.RECEIVE_DATA_READY) + ready.sftpTransition(SftpEvent.ReceiveName {}, SftpTransitionId.RECEIVE_NAME_READY) + ready.sftpTransition(SftpEvent.ReceiveAttrs {}, SftpTransitionId.RECEIVE_ATTRS_READY) + ready.sftpTransition(SftpEvent.ReceiveStatus {}, SftpTransitionId.RECEIVE_STATUS_READY) + + uninitialized.sftpTransition(SftpEvent.Disconnect {}, SftpTransitionId.DISCONNECT_UNINITIALIZED, closed) + waitVersion.sftpTransition(SftpEvent.Disconnect {}, SftpTransitionId.DISCONNECT_WAIT_VERSION, closed) + ready.sftpTransition(SftpEvent.Disconnect {}, SftpTransitionId.DISCONNECT_READY, closed) + } + + val state: SftpState get() = activeState + + suspend fun sendInit(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.SendInit(action)) + suspend fun receiveVersion(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.ReceiveVersion(action)) + suspend fun openFile(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.OpenFile(action)) + suspend fun openDir(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.OpenDir(action)) + suspend fun readFile(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.ReadFile(action)) + suspend fun writeFile(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.WriteFile(action)) + suspend fun readDir(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.ReadDir(action)) + suspend fun closeHandle(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.CloseHandle(action)) + suspend fun request(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.Request(action)) + suspend fun receiveHandle(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.ReceiveHandle(action)) + suspend fun receiveData(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.ReceiveData(action)) + suspend fun receiveName(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.ReceiveName(action)) + suspend fun receiveAttrs(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.ReceiveAttrs(action)) + suspend fun receiveStatus(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.ReceiveStatus(action)) + suspend fun disconnect(action: suspend (SftpAcceptedTransition) -> Unit) = process(SftpEvent.Disconnect(action)) + + internal fun formalModel(): SftpFormalModel { + val states = collectStates(stateMachine) + val transitions = states.flatMap { state -> + state.transitions.mapNotNull { transition -> + val meta = transition.metaInfo as? SftpTransitionMeta ?: return@mapNotNull null + SftpFormalTransition( + meta.id, + meta.eventId, + meta.source, + meta.target, + meta.effects, + meta.origin, + meta.requiresReadySession, + ) + } + } + return SftpFormalModel( + states = states.mapNotNullTo(mutableSetOf()) { it.name?.let(SftpState::valueOf) }, + transitions = transitions, + ) + } + + private suspend fun process(event: SftpEvent): Boolean = mutex.withLock { + stateMachine.processEvent(event) == ProcessingResult.PROCESSED + } + + private fun bindState(state: IState, lifecycleState: SftpState) { + state.onEntry { activeState = lifecycleState } + } + + private inline fun IState.sftpTransition( + event: E, + id: SftpTransitionId, + target: State? = null, + effects: Set = event.effects, + ) { + transition(id.name) { + targetState = target + metaInfo = SftpTransitionMeta( + id = id, + eventId = event.id, + source = SftpState.valueOf(requireNotNull(this@sftpTransition.name)), + target = target?.name?.let(SftpState::valueOf) + ?: SftpState.valueOf(requireNotNull(this@sftpTransition.name)), + effects = effects, + origin = event.origin, + requiresReadySession = event.requiresReadySession, + ) + }.onTriggered { + it.event.action(SftpAcceptedTransition(id, effects, event.origin)) + } + } +} + +private fun collectStates(root: IState): List = buildList { + add(root) + root.states.forEach { addAll(collectStates(it)) } +} diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineFormalModel.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineFormalModel.kt new file mode 100644 index 0000000..8b66cd4 --- /dev/null +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineFormalModel.kt @@ -0,0 +1,289 @@ +/* + * 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 java.security.MessageDigest + +internal class SftpStateMachineFormalModel( + val model: SftpFormalModel, +) { + private data class FormalVariable( + val name: String, + val initialValue: String, + val renderNext: (FormalStep) -> String, + ) + + private data class FormalStep( + val transition: SftpFormalTransition, + val handles: String = "handles", + val activeHandle: String = "activeHandle' = 0", + val pendingRequests: String = "pendingRequests", + val activeRequest: String = "activeRequest' = 0", + ) + + fun renderTla(moduleName: String = "SftpClientStateMachineGenerated"): String { + val states = model.states.mapTo(sortedSetOf()) { it.name } + val events = model.transitions.mapTo(sortedSetOf()) { it.eventId.tlaName } + val origins = model.transitions.mapTo(sortedSetOf()) { it.origin.name } + val effects = model.transitions.flatMapTo(sortedSetOf()) { transition -> + transition.effects.map(SftpEffect::name) + } + val handleStates = SftpHandleState.entries.mapTo(sortedSetOf()) { it.name } + val variables = formalVariables() + + val sessionTransitions = model.transitions.filter { + it.eventId in setOf(SftpEventId.SEND_INIT, SftpEventId.RECEIVE_VERSION, SftpEventId.DISCONNECT) + } + val openFile = model.transitionFor(SftpEventId.OPEN_FILE) + val openDir = model.transitionFor(SftpEventId.OPEN_DIR) + val readFile = model.transitionFor(SftpEventId.READ_FILE) + val writeFile = model.transitionFor(SftpEventId.WRITE_FILE) + val readDir = model.transitionFor(SftpEventId.READ_DIR) + val closeHandle = model.transitionFor(SftpEventId.CLOSE_HANDLE) + val request = model.transitionFor(SftpEventId.REQUEST) + val responseTransitions = listOf( + SftpEventId.RECEIVE_HANDLE, + SftpEventId.RECEIVE_DATA, + SftpEventId.RECEIVE_NAME, + SftpEventId.RECEIVE_STATUS, + SftpEventId.RECEIVE_ATTRS, + ).map { model.transitionFor(it) } + + val body = buildString { + appendLine("EXTENDS Naturals") + appendLine() + appendLine("CONSTANT MaxHandles, MaxRequests") + appendLine() + appendLine("HandleIDs == 1..MaxHandles") + appendLine("RequestIDs == 1..MaxRequests") + appendLine() + appendLine("VARIABLES ${variables.joinToString(", ", transform = FormalVariable::name)}") + appendLine() + appendLine("vars == <<${variables.joinToString(", ", transform = FormalVariable::name)}>>") + appendLine() + appendLine("States == ${renderSet(states)}") + appendLine("Events == ${renderSet(events)}") + appendLine("Origins == ${renderSet(origins)}") + appendLine("Effects == ${renderSet(effects)}") + appendLine("HandleStates == ${renderSet(handleStates)}") + appendLine() + appendLine("Init ==") + variables.forEach { variable -> + appendLine(" /\\ ${variable.name} = ${variable.initialValue}") + } + appendLine() + + sessionTransitions.sortedBy { it.id.name }.forEach { transition -> + val disconnect = transition.eventId == SftpEventId.DISCONNECT + appendTransition( + transition.id.name, + FormalStep( + transition = transition, + handles = if (disconnect) { + "[h \\in HandleIDs |-> IF handles[h] = \"Unallocated\" THEN \"Unallocated\" ELSE \"Closed\"]" + } else { + "handles" + }, + pendingRequests = if (disconnect) "[r \\in RequestIDs |-> \"None\"]" else "pendingRequests", + ), + variables, + ) + appendLine() + } + + appendTransition( + "AllocateHandle", + FormalStep( + transition = openFile, + handles = "[handles EXCEPT ![activeHandle'] = \"OpenFile\"]", + activeHandle = "activeHandle' \\in HandleIDs", + pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = \"PendingOpen\"]", + activeRequest = "activeRequest' \\in RequestIDs", + ), + variables, + "handles[activeHandle'] = \"Unallocated\"", + "pendingRequests[activeRequest'] = \"None\"", + ) + appendLine() + + appendTransition( + "AllocateDirHandle", + FormalStep( + transition = openDir, + handles = "[handles EXCEPT ![activeHandle'] = \"OpenDir\"]", + activeHandle = "activeHandle' \\in HandleIDs", + pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = \"PendingOpen\"]", + activeRequest = "activeRequest' \\in RequestIDs", + ), + variables, + "handles[activeHandle'] = \"Unallocated\"", + "pendingRequests[activeRequest'] = \"None\"", + ) + appendLine() + + appendTransition( + "ReadFileOp", + requestStep(readFile, "PendingRead"), + variables, + "handles[activeHandle'] = \"OpenFile\"", + "pendingRequests[activeRequest'] = \"None\"", + ) + appendLine() + + appendTransition( + "WriteFileOp", + requestStep(writeFile, "PendingWrite"), + variables, + "handles[activeHandle'] = \"OpenFile\"", + "pendingRequests[activeRequest'] = \"None\"", + ) + appendLine() + + appendTransition( + "ReadDirOp", + requestStep(readDir, "PendingReadDir"), + variables, + "handles[activeHandle'] = \"OpenDir\"", + "pendingRequests[activeRequest'] = \"None\"", + ) + appendLine() + + appendTransition( + "CloseHandleOp", + requestStep( + transition = closeHandle, + pendingState = "PendingClose", + handles = "[handles EXCEPT ![activeHandle'] = \"Closed\"]", + ), + variables, + "handles[activeHandle'] \\in {\"OpenFile\", \"OpenDir\"}", + "pendingRequests[activeRequest'] = \"None\"", + ) + appendLine() + + appendTransition( + "RequestOp", + FormalStep( + transition = request, + pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = \"PendingRequest\"]", + activeRequest = "activeRequest' \\in RequestIDs", + ), + variables, + "pendingRequests[activeRequest'] = \"None\"", + ) + appendLine() + + appendLine("FulfillResponse ==") + responseTransitions.forEach { transition -> + val step = FormalStep( + transition = transition, + pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = \"None\"]", + activeRequest = "activeRequest' \\in RequestIDs", + ) + appendLine(" \\/ /\\ state = ${quote(transition.source.name)}") + variables.forEach { variable -> + appendLine(" /\\ ${variable.renderNext(step)}") + } + appendLine(" /\\ pendingRequests[activeRequest'] # \"None\"") + } + appendLine() + + appendLine("Next ==") + sessionTransitions.sortedBy { it.id.name }.forEach { transition -> + appendLine(" \\/ ${transition.id.name}") + } + appendLine(" \\/ AllocateHandle") + appendLine(" \\/ AllocateDirHandle") + appendLine(" \\/ ReadFileOp") + appendLine(" \\/ WriteFileOp") + appendLine(" \\/ ReadDirOp") + appendLine(" \\/ CloseHandleOp") + appendLine(" \\/ RequestOp") + appendLine(" \\/ FulfillResponse") + 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 SftpStateMachine. Do not edit.") + appendLine("\\* Model SHA-256: $fingerprint") + append(body) + appendLine("====") + } + } + + private fun StringBuilder.appendTransition( + name: String, + step: FormalStep, + variables: List, + vararg guards: String, + ) { + appendLine("$name ==") + appendLine(" /\\ state = ${quote(step.transition.source.name)}") + variables.forEach { variable -> + appendLine(" /\\ ${variable.renderNext(step)}") + } + guards.forEach { guard -> appendLine(" /\\ $guard") } + } + + private fun requestStep( + transition: SftpFormalTransition, + pendingState: String, + handles: String = "handles", + ) = FormalStep( + transition = transition, + handles = handles, + activeHandle = "activeHandle' \\in HandleIDs", + pendingRequests = "[pendingRequests EXCEPT ![activeRequest'] = ${quote(pendingState)}]", + activeRequest = "activeRequest' \\in RequestIDs", + ) + + private fun formalVariables(): List = listOf( + variable("state", quote(SftpState.UNINITIALIZED.name)) { quote(it.transition.target.name) }, + variable("previousState", quote(SftpState.UNINITIALIZED.name)) { "state" }, + variable("event", quote("None")) { quote(it.transition.eventId.tlaName) }, + variable("origin", quote(SftpEventOrigin.LOCAL_COMMAND.name)) { quote(it.transition.origin.name) }, + variable("effects", "{}") { renderSet(it.transition.effects.map(SftpEffect::name)) }, + variable("previousHandles", "[h \\in HandleIDs |-> \"Unallocated\"]") { "handles" }, + FormalVariable("activeHandle", "0", FormalStep::activeHandle), + variable("handles", "[h \\in HandleIDs |-> \"Unallocated\"]", FormalStep::handles), + variable("previousPendingRequests", "[r \\in RequestIDs |-> \"None\"]") { "pendingRequests" }, + FormalVariable("activeRequest", "0", FormalStep::activeRequest), + variable("pendingRequests", "[r \\in RequestIDs |-> \"None\"]", FormalStep::pendingRequests), + ) + + private fun variable( + name: String, + initialValue: String, + nextValue: (FormalStep) -> String, + ) = FormalVariable(name, initialValue) { step -> "$name' = ${nextValue(step)}" } + + private fun renderSet(values: Collection): String = values + .toSortedSet() + .joinToString(prefix = "{", postfix = "}", transform = ::quote) + + private fun quote(value: String) = "\"${value.replace("\\", "\\\\").replace("\"", "\\\"")}\"" + + private fun SftpFormalModel.transitionFor(eventId: SftpEventId): SftpFormalTransition = transitions.singleOrNull { it.eventId == eventId } + ?: error("Expected exactly one SFTP transition for ${eventId.name}") +} diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientImplTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientImplTest.kt index b9732e9..9621c75 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientImplTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientImplTest.kt @@ -19,7 +19,9 @@ package org.connectbot.sshlib.client.sftp import kotlinx.coroutines.channels.Channel import kotlinx.coroutines.channels.ReceiveChannel +import kotlinx.coroutines.delay import kotlinx.coroutines.runBlocking +import kotlinx.coroutines.withTimeout import org.connectbot.sshlib.SftpAttributes import org.connectbot.sshlib.SftpClient import org.connectbot.sshlib.SftpDirectoryEntry @@ -53,6 +55,23 @@ class SftpClientImplTest { assertEquals(1, session.closeCalls) } + @Test + fun `close cleans up session after read loop already disconnected state machine`() = runBlocking { + val session = FakeSshSession() + val client = createClient(session) + + session.closeReads() + withTimeout(1_000) { + while (client.isOpen) { + delay(1) + } + } + + client.close() + + assertEquals(1, session.closeCalls) + } + @Test fun `create returns protocol errors for malformed version response`() { runBlocking { diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineTest.kt new file mode 100644 index 0000000..720e540 --- /dev/null +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SftpStateMachineTest.kt @@ -0,0 +1,136 @@ +/* + * 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.CompletableDeferred +import kotlinx.coroutines.async +import kotlinx.coroutines.runBlocking +import kotlinx.coroutines.yield +import java.nio.file.Files +import java.nio.file.Path +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +internal object SftpStateMachineTlaGenerator { + @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) + val machine = SftpStateMachine() + val renderer = SftpStateMachineFormalModel(machine.formalModel()) + Files.writeString(output, renderer.renderTla()) + } +} + +class SftpStateMachineTest { + + @Test + fun `formal model captures all transitions`() { + val machine = SftpStateMachine() + val formal = machine.formalModel() + assertEquals(4, formal.states.size) + assertTrue(SftpState.UNINITIALIZED in formal.states) + assertTrue(SftpState.WAIT_VERSION in formal.states) + assertTrue(SftpState.READY in formal.states) + assertTrue(SftpState.CLOSED in formal.states) + } + + @Test + fun `renderTla emits valid module body`() { + val machine = SftpStateMachine() + val model = machine.formalModel() + val renderer = SftpStateMachineFormalModel(model) + val tla = renderer.renderTla() + + assertTrue("---- MODULE SftpClientStateMachineGenerated ----" in tla) + assertTrue("CONSTANT MaxHandles, MaxRequests" in tla) + assertTrue("AllocateHandle ==" in tla) + assertTrue("ReadFileOp ==" in tla) + assertTrue("FulfillResponse ==" in tla) + assertTrue("====" in tla) + } + + @Test + fun `renderer requires runtime transitions for modeled operations`() { + val formal = SftpStateMachine().formalModel() + val missingRead = formal.copy( + transitions = formal.transitions.filterNot { it.eventId == SftpEventId.READ_FILE }, + ) + + assertFailsWith { + SftpStateMachineFormalModel(missingRead).renderTla() + } + } + + @Test + fun `renderer generates declarations initialization and updates from formal variables`() { + val tla = SftpStateMachineFormalModel(SftpStateMachine().formalModel()).renderTla() + val variables = tla.lineSequence() + .single { it.startsWith("VARIABLES ") } + .removePrefix("VARIABLES ") + .split(", ") + val init = tla.substringAfter("Init ==\n").substringBefore("\n\n") + val sendInit = tla.substringAfter("SEND_INIT_UNINITIALIZED ==\n").substringBefore("\n\n") + + variables.forEach { variable -> + assertTrue("/\\ $variable =" in init, "$variable is missing from Init") + assertTrue("$variable'" in sendInit, "$variable is missing from a generated transition") + } + assertTrue("vars == <<${variables.joinToString(", ")}>>" in tla) + } + + @Test + fun `request write action is serialized with disconnect`() = runBlocking { + val machine = SftpStateMachine() + assertTrue(machine.sendInit { }) + assertTrue(machine.receiveVersion { }) + val writeStarted = CompletableDeferred() + val finishWrite = CompletableDeferred() + + val request = async { + machine.request { + writeStarted.complete(Unit) + finishWrite.await() + } + } + writeStarted.await() + val disconnect = async { machine.disconnect { } } + yield() + + assertFalse(disconnect.isCompleted) + finishWrite.complete(Unit) + assertTrue(request.await()) + assertTrue(disconnect.await()) + assertEquals(SftpState.CLOSED, machine.state) + } + + @Test + fun `generated TLA file matches rendered model`() { + val machine = SftpStateMachine() + val renderer = SftpStateMachineFormalModel(machine.formalModel()) + val generatedPath = Path.of("src/test/resources/tla/SftpClientStateMachineGenerated.tla") + if (Files.exists(generatedPath)) { + val fileContent = Files.readString(generatedPath) + assertEquals(renderer.renderTla(), fileContent) + } + } +} diff --git a/sshlib/src/test/resources/tla/SftpClientStateMachine.cfg b/sshlib/src/test/resources/tla/SftpClientStateMachine.cfg new file mode 100644 index 0000000..2402533 --- /dev/null +++ b/sshlib/src/test/resources/tla/SftpClientStateMachine.cfg @@ -0,0 +1,14 @@ +SPECIFICATION Spec +CONSTANT MaxHandles = 2 +CONSTANT MaxRequests = 2 + +VIEW ModelView + +INVARIANT TypeOK +INVARIANT NoOperationsBeforeInitialization +INVARIANT ClosedSessionClosesHandles +INVARIANT HandleTypeOKAndOperationsGuarded +INVARIANT HandleIsolation +INVARIANT RequestCorrelationAndNonInterference + +CHECK_DEADLOCK FALSE diff --git a/sshlib/src/test/resources/tla/SftpClientStateMachine.tla b/sshlib/src/test/resources/tla/SftpClientStateMachine.tla new file mode 100644 index 0000000..6f39937 --- /dev/null +++ b/sshlib/src/test/resources/tla/SftpClientStateMachine.tla @@ -0,0 +1,62 @@ +---- MODULE SftpClientStateMachine ---- +EXTENDS SftpClientStateMachineGenerated + +TypeOK == + /\ state \in States + /\ previousState \in States + /\ event \in Events \cup {"None"} + /\ origin \in Origins + /\ effects \subseteq Effects + /\ handles \in [HandleIDs -> HandleStates] + /\ previousHandles \in [HandleIDs -> HandleStates] + /\ activeHandle \in 0..MaxHandles + /\ pendingRequests \in [RequestIDs -> {"None", "PendingOpen", "PendingRead", "PendingWrite", "PendingReadDir", "PendingClose", "PendingRequest"}] + /\ previousPendingRequests \in [RequestIDs -> {"None", "PendingOpen", "PendingRead", "PendingWrite", "PendingReadDir", "PendingClose", "PendingRequest"}] + /\ activeRequest \in 0..MaxRequests + +\* Invariant 1: Initialization Guard +\* No handle operations or allocated handles are permitted before session reaches READY. +NoOperationsBeforeInitialization == + state \in {"UNINITIALIZED", "WAIT_VERSION"} => + \A h \in HandleIDs : handles[h] = "Unallocated" + +ClosedSessionClosesHandles == + state = "CLOSED" => + \A h \in HandleIDs : handles[h] \in {"Unallocated", "Closed"} + +\* Invariant 2: Handle Safety & Type Guards +\* Read/Write requires OpenFile, ReadDir requires OpenDir, CloseHandle requires OpenFile/OpenDir. +HandleTypeOKAndOperationsGuarded == + /\ (event \in {"ReadFile", "WriteFile"} => activeHandle # 0 /\ previousHandles[activeHandle] = "OpenFile") + /\ (event = "ReadDir" => activeHandle # 0 /\ previousHandles[activeHandle] = "OpenDir") + /\ (event = "CloseHandle" => activeHandle # 0 /\ previousHandles[activeHandle] \in {"OpenFile", "OpenDir"}) + +\* Invariant 3: Handle Isolation +\* Targeted handle operations alter activeHandle while keeping sibling handles unchanged. +HandleIsolation == + activeHandle \in HandleIDs => + \A other \in HandleIDs \ {activeHandle} : + handles[other] = previousHandles[other] + +\* Invariant 4: Request ID Correlation & Non-Interference +\* Response fulfillment targets a specific activeRequest and preserves sibling in-flight requests. +RequestCorrelationAndNonInterference == + (event \in {"ReceiveData", "ReceiveHandle", "ReceiveName", "ReceiveStatus", "ReceiveAttrs"} /\ activeRequest # 0) => + \A other \in RequestIDs \ {activeRequest} : + pendingRequests[other] = previousPendingRequests[other] + +\* ModelView abstraction to reduce state space explosion and keep TLC fast +ModelView == << + state, + handles, + pendingRequests, + activeHandle, + activeRequest, + NoOperationsBeforeInitialization, + ClosedSessionClosesHandles, + HandleTypeOKAndOperationsGuarded, + HandleIsolation, + RequestCorrelationAndNonInterference +>> + +==== diff --git a/sshlib/src/test/resources/tla/SftpClientStateMachineGenerated.tla b/sshlib/src/test/resources/tla/SftpClientStateMachineGenerated.tla new file mode 100644 index 0000000..0313b50 --- /dev/null +++ b/sshlib/src/test/resources/tla/SftpClientStateMachineGenerated.tla @@ -0,0 +1,298 @@ +---- MODULE SftpClientStateMachineGenerated ---- +\* Generated from SftpStateMachine. Do not edit. +\* Model SHA-256: 66c6ecb224482047f6437721e0f69ecc6ad240c631519a17776df4038ef3cff1 +EXTENDS Naturals + +CONSTANT MaxHandles, MaxRequests + +HandleIDs == 1..MaxHandles +RequestIDs == 1..MaxRequests + +VARIABLES state, previousState, event, origin, effects, previousHandles, activeHandle, handles, previousPendingRequests, activeRequest, pendingRequests + +vars == <> + +States == {"CLOSED", "READY", "UNINITIALIZED", "WAIT_VERSION"} +Events == {"CloseHandle", "Disconnect", "OpenDir", "OpenFile", "ReadDir", "ReadFile", "ReceiveAttrs", "ReceiveData", "ReceiveHandle", "ReceiveName", "ReceiveStatus", "ReceiveVersion", "Request", "SendInit", "WriteFile"} +Origins == {"CONNECTION_CONTROL", "LOCAL_COMMAND", "PARSED_PACKET"} +Effects == {"DELIVER_ATTRS", "DELIVER_DATA", "DELIVER_HANDLE", "DELIVER_NAME", "DELIVER_STATUS", "DISCONNECT_SFTP", "RECEIVE_VERSION", "SEND_CLOSE_HANDLE", "SEND_INIT", "SEND_OPEN_DIR", "SEND_OPEN_FILE", "SEND_READ", "SEND_READDIR", "SEND_REQUEST", "SEND_WRITE"} +HandleStates == {"Closed", "OpenDir", "OpenFile", "Unallocated"} + +Init == + /\ state = "UNINITIALIZED" + /\ previousState = "UNINITIALIZED" + /\ event = "None" + /\ origin = "LOCAL_COMMAND" + /\ effects = {} + /\ previousHandles = [h \in HandleIDs |-> "Unallocated"] + /\ activeHandle = 0 + /\ handles = [h \in HandleIDs |-> "Unallocated"] + /\ previousPendingRequests = [r \in RequestIDs |-> "None"] + /\ activeRequest = 0 + /\ pendingRequests = [r \in RequestIDs |-> "None"] + +DISCONNECT_READY == + /\ state = "READY" + /\ state' = "CLOSED" + /\ previousState' = state + /\ event' = "Disconnect" + /\ origin' = "CONNECTION_CONTROL" + /\ effects' = {"DISCONNECT_SFTP"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = [h \in HandleIDs |-> IF handles[h] = "Unallocated" THEN "Unallocated" ELSE "Closed"] + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' = 0 + /\ pendingRequests' = [r \in RequestIDs |-> "None"] + +DISCONNECT_UNINITIALIZED == + /\ state = "UNINITIALIZED" + /\ state' = "CLOSED" + /\ previousState' = state + /\ event' = "Disconnect" + /\ origin' = "CONNECTION_CONTROL" + /\ effects' = {"DISCONNECT_SFTP"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = [h \in HandleIDs |-> IF handles[h] = "Unallocated" THEN "Unallocated" ELSE "Closed"] + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' = 0 + /\ pendingRequests' = [r \in RequestIDs |-> "None"] + +DISCONNECT_WAIT_VERSION == + /\ state = "WAIT_VERSION" + /\ state' = "CLOSED" + /\ previousState' = state + /\ event' = "Disconnect" + /\ origin' = "CONNECTION_CONTROL" + /\ effects' = {"DISCONNECT_SFTP"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = [h \in HandleIDs |-> IF handles[h] = "Unallocated" THEN "Unallocated" ELSE "Closed"] + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' = 0 + /\ pendingRequests' = [r \in RequestIDs |-> "None"] + +RECEIVE_VERSION_WAIT_VERSION == + /\ state = "WAIT_VERSION" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReceiveVersion" + /\ origin' = "PARSED_PACKET" + /\ effects' = {"RECEIVE_VERSION"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' = 0 + /\ pendingRequests' = pendingRequests + +SEND_INIT_UNINITIALIZED == + /\ state = "UNINITIALIZED" + /\ state' = "WAIT_VERSION" + /\ previousState' = state + /\ event' = "SendInit" + /\ origin' = "LOCAL_COMMAND" + /\ effects' = {"SEND_INIT"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' = 0 + /\ pendingRequests' = pendingRequests + +AllocateHandle == + /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "OpenFile" + /\ origin' = "LOCAL_COMMAND" + /\ effects' = {"SEND_OPEN_FILE"} + /\ previousHandles' = handles + /\ activeHandle' \in HandleIDs + /\ handles' = [handles EXCEPT ![activeHandle'] = "OpenFile"] + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingOpen"] + /\ handles[activeHandle'] = "Unallocated" + /\ pendingRequests[activeRequest'] = "None" + +AllocateDirHandle == + /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "OpenDir" + /\ origin' = "LOCAL_COMMAND" + /\ effects' = {"SEND_OPEN_DIR"} + /\ previousHandles' = handles + /\ activeHandle' \in HandleIDs + /\ handles' = [handles EXCEPT ![activeHandle'] = "OpenDir"] + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingOpen"] + /\ handles[activeHandle'] = "Unallocated" + /\ pendingRequests[activeRequest'] = "None" + +ReadFileOp == + /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReadFile" + /\ origin' = "LOCAL_COMMAND" + /\ effects' = {"SEND_READ"} + /\ previousHandles' = handles + /\ activeHandle' \in HandleIDs + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingRead"] + /\ handles[activeHandle'] = "OpenFile" + /\ pendingRequests[activeRequest'] = "None" + +WriteFileOp == + /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "WriteFile" + /\ origin' = "LOCAL_COMMAND" + /\ effects' = {"SEND_WRITE"} + /\ previousHandles' = handles + /\ activeHandle' \in HandleIDs + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingWrite"] + /\ handles[activeHandle'] = "OpenFile" + /\ pendingRequests[activeRequest'] = "None" + +ReadDirOp == + /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReadDir" + /\ origin' = "LOCAL_COMMAND" + /\ effects' = {"SEND_READDIR"} + /\ previousHandles' = handles + /\ activeHandle' \in HandleIDs + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingReadDir"] + /\ handles[activeHandle'] = "OpenDir" + /\ pendingRequests[activeRequest'] = "None" + +CloseHandleOp == + /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "CloseHandle" + /\ origin' = "LOCAL_COMMAND" + /\ effects' = {"SEND_CLOSE_HANDLE"} + /\ previousHandles' = handles + /\ activeHandle' \in HandleIDs + /\ handles' = [handles EXCEPT ![activeHandle'] = "Closed"] + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingClose"] + /\ handles[activeHandle'] \in {"OpenFile", "OpenDir"} + /\ pendingRequests[activeRequest'] = "None" + +RequestOp == + /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "Request" + /\ origin' = "LOCAL_COMMAND" + /\ effects' = {"SEND_REQUEST"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "PendingRequest"] + /\ pendingRequests[activeRequest'] = "None" + +FulfillResponse == + \/ /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReceiveHandle" + /\ origin' = "PARSED_PACKET" + /\ effects' = {"DELIVER_HANDLE"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] + /\ pendingRequests[activeRequest'] # "None" + \/ /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReceiveData" + /\ origin' = "PARSED_PACKET" + /\ effects' = {"DELIVER_DATA"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] + /\ pendingRequests[activeRequest'] # "None" + \/ /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReceiveName" + /\ origin' = "PARSED_PACKET" + /\ effects' = {"DELIVER_NAME"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] + /\ pendingRequests[activeRequest'] # "None" + \/ /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReceiveStatus" + /\ origin' = "PARSED_PACKET" + /\ effects' = {"DELIVER_STATUS"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] + /\ pendingRequests[activeRequest'] # "None" + \/ /\ state = "READY" + /\ state' = "READY" + /\ previousState' = state + /\ event' = "ReceiveAttrs" + /\ origin' = "PARSED_PACKET" + /\ effects' = {"DELIVER_ATTRS"} + /\ previousHandles' = handles + /\ activeHandle' = 0 + /\ handles' = handles + /\ previousPendingRequests' = pendingRequests + /\ activeRequest' \in RequestIDs + /\ pendingRequests' = [pendingRequests EXCEPT ![activeRequest'] = "None"] + /\ pendingRequests[activeRequest'] # "None" + +Next == + \/ DISCONNECT_READY + \/ DISCONNECT_UNINITIALIZED + \/ DISCONNECT_WAIT_VERSION + \/ RECEIVE_VERSION_WAIT_VERSION + \/ SEND_INIT_UNINITIALIZED + \/ AllocateHandle + \/ AllocateDirHandle + \/ ReadFileOp + \/ WriteFileOp + \/ ReadDirOp + \/ CloseHandleOp + \/ RequestOp + \/ FulfillResponse + +Spec == Init /\ [][Next]_vars +====