Skip to content

More TLA+ modeling #234

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kruton merged 4 commits into from
Jul 23, 2026
Merged

More TLA+ modeling #234

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1eaf8f7
test(sftp): add rekey during SFTP tests
kruton Jul 23, 2026
8a606f7
chore(tla+): prove Terrapin is mitigated
kruton Jul 23, 2026
a1ab06a
feat(tla+): model hostile environment
kruton Jul 23, 2026
94c52b2
chore(tla+): make build rules more readable
kruton Jul 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
188 changes: 142 additions & 46 deletions sshlib/build.gradle.kts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@

import com.vanniktech.maven.publish.DeploymentValidation
import org.jetbrains.kotlin.gradle.dsl.JvmTarget
import java.io.ByteArrayOutputStream

plugins {
alias(libs.plugins.kotlin.jvm)
Expand Down Expand Up @@ -69,74 +70,162 @@ tasks.test {

val tlaModelDirectory = layout.projectDirectory.dir("src/test/resources/tla")
val tlaStateDirectory = layout.buildDirectory.dir("tla/states")

tasks.register<JavaExec>("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)
}

tasks.register<JavaExec>("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"))

tasks.register<JavaExec>("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)
listOf(
"Ssh" to ("SshClientStateMachine" to "SshStateMachineTlaGenerator"),
"Sftp" to ("SftpClientStateMachine" to "SftpStateMachineTlaGenerator"),
).forEach { (type, config) ->
val (modelName, generatorClass) = config
tasks.register<JavaExec>("generate${type}StateMachineTla") {
group = "verification"
description = "Regenerates the TLA+ lifecycle model from $modelName"
dependsOn(tasks.testClasses)
classpath = sourceSets.test.get().runtimeClasspath
mainClass.set("org.connectbot.sshlib.protocol.$generatorClass")
args(tlaModelDirectory.file("${modelName}Generated.tla").asFile.absolutePath)
}
}

tasks.register<JavaExec>("checkSftpStateMachineTla") {
fun TaskContainer.registerTlcCheck(
name: String,
description: String,
configFile: String,
tlaFile: String,
stateSubdir: String? = null,
configure: (JavaExec.() -> Unit)? = null,
): TaskProvider<JavaExec> = register<JavaExec>(name) {
group = "verification"
description = "Checks the generated SFTP lifecycle model with TLC"
this.description = description
mainClass.set("tlc2.TLC")
workingDir(tlaModelDirectory)

val metaDir = if (stateSubdir != null) {
tlaStateDirectory.get().dir(stateSubdir).asFile.absolutePath
} else {
tlaStateDirectory.get().asFile.absolutePath
}

args(
"-workers",
"1",
"-metadir",
tlaStateDirectory.get().asFile.absolutePath,
metaDir,
"-config",
"SftpClientStateMachine.cfg",
"SftpClientStateMachine.tla",
configFile,
tlaFile,
)
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)
}

configure?.invoke(this)
}

fun TaskContainer.registerTlcCounterexampleCheck(
name: String,
description: String,
configFile: String,
tlaFile: String,
stateSubdir: String,
expectedViolation: String,
failureMessage: String,
successMessage: String,
): TaskProvider<JavaExec> {
val outputStream = ByteArrayOutputStream()
return registerTlcCheck(
name = name,
description = description,
configFile = configFile,
tlaFile = tlaFile,
stateSubdir = stateSubdir,
) {
standardOutput = outputStream
errorOutput = outputStream
isIgnoreExitValue = true
doFirst {
outputStream.reset()
}
doLast {
val output = outputStream.toString(Charsets.UTF_8)
logger.lifecycle(output)
val exitValue = executionResult.get().exitValue
if (exitValue == 0 || expectedViolation !in output) {
throw GradleException("$failureMessage; exit=$exitValue")
}
logger.lifecycle(successMessage)
}
}
}

tasks.registerTlcCheck(
name = "checkSshStateMachineTla",
description = "Checks the generated SSH lifecycle model with TLC",
configFile = "SshClientStateMachine.cfg",
tlaFile = "SshClientStateMachine.tla",
)

listOf(
"OnPath" to "SshClientStateMachineOnPath.cfg",
"HostilePeer" to "SshClientStateMachineHostilePeer.cfg",
).forEach { (profile, configFile) ->
tasks.registerTlcCheck(
name = "checkSshStateMachine${profile}Tla",
description = "Checks the generated SSH lifecycle model with the $profile hostile environment",
configFile = configFile,
tlaFile = "SshClientStateMachine.tla",
stateSubdir = "ssh-${profile.lowercase()}",
)
}

tasks.registerTlcCounterexampleCheck(
name = "checkSshStateMachineUnsafeProofTla",
description = "Requires TLC to find a hostile KEX counterexample when proof verification is disabled",
configFile = "SshClientStateMachineUnsafeProof.cfg",
tlaFile = "SshClientStateMachine.tla",
stateSubdir = "ssh-unsafe-proof",
expectedViolation = "Invariant HostileKexReplyRequiresPossessionProof is violated",
failureMessage = "Expected TLC to find the disabled-proof counterexample",
successMessage = "Expected disabled-proof counterexample found; treating it as success.",
)

tasks.registerTlcCheck(
name = "checkSftpStateMachineTla",
description = "Checks the generated SFTP lifecycle model with TLC",
configFile = "SftpClientStateMachine.cfg",
tlaFile = "SftpClientStateMachine.tla",
)

val checkSshTerrapinStrictTla = tasks.registerTlcCheck(
name = "checkSshTerrapinStrictTla",
description = "Proves that strict KEX prevents the modeled Terrapin prefix truncation attack",
configFile = "SshTerrapinStrict.cfg",
tlaFile = "SshTerrapin.tla",
stateSubdir = "terrapin-strict",
)

val checkSshTerrapinNonStrictTla = tasks.registerTlcCounterexampleCheck(
name = "checkSshTerrapinNonStrictTla",
description = "Requires TLC to find the modeled Terrapin counterexample without failing the build",
configFile = "SshTerrapinNonStrict.cfg",
tlaFile = "SshTerrapin.tla",
stateSubdir = "terrapin-non-strict",
expectedViolation = "Invariant NoTerrapin is violated",
failureMessage = "Expected TLC to find the non-strict Terrapin counterexample",
successMessage = "Expected non-strict Terrapin counterexample found; treating it as success.",
)

tasks.register("checkSshTerrapinTla") {
group = "verification"
description = "Checks strict Terrapin resistance and the expected non-strict counterexample"
dependsOn(checkSshTerrapinStrictTla, checkSshTerrapinNonStrictTla)
}

tasks.register("generateTla") {
Expand All @@ -148,7 +237,14 @@ tasks.register("generateTla") {
tasks.register("checkTla") {
group = "verification"
description = "Checks all TLA+ formal models (SSH and SFTP) with TLC"
dependsOn("checkSshStateMachineTla", "checkSftpStateMachineTla")
dependsOn(
"checkSshStateMachineTla",
"checkSshStateMachineOnPathTla",
"checkSshStateMachineHostilePeerTla",
"checkSshStateMachineUnsafeProofTla",
"checkSftpStateMachineTla",
"checkSshTerrapinTla",
)
}

java {
Expand Down
Loading
Loading