Build depends on SNAPSHOT artifacts and non-enforced version locks

Trigger (as reviewed): mvn-lock//dependencies-lock.json files (with sha512 integrity fields for every artifact) are checked in, and nix/k.nix / flake.nix only generate them (the k-lock attribute runs dependency-lock-maven-plugin:1.2.2:lock). Grepping the POMs for dependency-lock / dependencies-lock finds no binding the plugin's verify/check goal to a lifecycle phase. Consequently mvn package, as invoked by package/debian//rules.* and package/arch/PKGBUILD, resolves dependencies from remote repositories without consulting the lock.

Impact (as reviewed): The integrity data in mvn-lock/ provides no protection for the ordinary (non-Nix) build paths that produce the released .debs and Arch packages. A compromised or typosquatted artifact at a resolved coordinate is accepted; the checked-in lock is decorative in those paths. A partially applied verification gap: the repo looks locked but the enforcing step is absent.

Deep review: reachability=REACHABLE-FROM-UNTRUSTED; exploitability=EXPLOITABLE; red-team=RED-TEAM-SURVIVED.

Strongest counterargument found during red-teaming: The exploit requires an attacker with write access to runtimeverification.mycloudrepo.io, and the maintainers explicitly documented the lock as informational/best-effort in commit #4820. Whether that documented tradeoff should count as an accepted risk with an owner (lowering or closing this as a finding) is a judgment the code alone cannot settle; the external repository's redeploy/immutability policy for the 1.0.0-SNAPSHOT coordinates is also unverifiable from this checkout.

Trigger (as reviewed): The frontend declares a uexe (native executable) dependency on org.kframework.dependencies:ng at a -SNAPSHOT version, with sibling declarations at 0.9.2-k4.0 for linux (line 161) and windows (line 175). The snapshot repository is enabled (see -006). ng/kserver are the nailgun launchers that the distribution executes (k-distribution/src/main/scripts/lib/checkJava invokes bin/ng), and k-distribution/src/main/assembly/bin.xml copies :uexe: artifacts into lib/kframework/bin.

Impact (as reviewed): An unverifiable, re-publishable native binary is bundled into the shipped distribution and executed on the user's machine. Maven's checksum check only proves consistency with whatever the repository currently serves for that snapshot coordinate, not that the binary is the reviewed one. Direct binary-supply-chain injection point into every K install.

Deep review: reachability=REACHABLE-FROM-UNTRUSTED; exploitability=EXPLOITABLE; red-team=RED-TEAM-INCONCLUSIVE.

Strongest counterargument found during red-teaming: The Nix fixed-output hash fully protects released macOS installations (the only shipped macOS channel) and Linux packages, so an artifact-repository-only attacker cannot reach end users; however the finding still survives in a narrower form: the README-documented mvn package developer build on macOS resolves the mutable snapshot fresh with no enforced digest (the lock file is only generated by the separate k-lock Nix output), and the build/tests plus the resulting local distribution execute lib/kframework/bin/ng, giving RCE on macOS build machines.

Trigger (as reviewed): The parent POM enables snapshot resolution from a third-party host (runtimeverification.mycloudrepo.io) for all modules. The same repository is registered again as a pluginRepository (lines 50-54), so build plugins can also be resolved as snapshots.

Impact (as reviewed): Snapshot artifacts are mutable by design: the same coordinates can be re-published with different bytes. Any module that resolves a -SNAPSHOT coordinate silently picks up re-published content on the next non-offline build. Because the repository is operator-controlled and not central, this is a persistent supply-chain path that survives normal dependency pinning.

Trigger (as reviewed): nailgun-server is a compile-scope dependency at a snapshot version, resolved from runtimeverification.mycloudrepo.io. The lock file records its sha512, but (per -007) the lock is not enforced in the plain Maven build. checkJava in the distribution uses the nailgun server socket (KSERVER_SOCKET, $NG --nailgun-server local:$KSERVER_SOCKET/socket), so this class is loaded into the long-running kserver process.

Impact (as reviewed): Mutable snapshot code runs in the compiler server process that K's tooling talks to. A re-published snapshot (or a repo compromise) substitutes new bytecode with no enforced hash and no signature; because it is compile-scope it also enters the toolchain's classpath at runtime.

Deep review: reachability=REACHABLE-FROM-UNTRUSTED; exploitability=EXPLOITABLE; red-team=RED-TEAM-SURVIVED.

Strongest counterargument found during red-teaming: The attack requires write access to Runtime Verification's own CloudRepo namespace (or a compromise of CloudRepo itself), and the repository is first-party rather than the 'third-party repository' the title claims. Whether CloudRepo permits adding new timestamped snapshots under that coordinate, and whether the release deploy job really executes the integration-test/kserver phase while MAVEN_PASSWORD is in the environment, could not be verified offline. These affect severity and framing, not the existence of the unenforced mutable-snapshot dependency.