Java native deserialization of `compiled.bin`/`cache.bin` (object-stream RCE)

Trigger (as reviewed): BinaryLoader.loadImpl creates a raw java.io.ObjectInputStream and calls readObject() with no ObjectInputFilter, no class allow-list and no resolveClass override. It is the single serialization helper for the toolchain and is reached from DefinitionLoadingModule.java:31 (loadOrDie(CompiledDefinition.class, resolveKompiled("compiled.bin"))), KompileFrontEnd.java:109 (write), DefinitionParsing.java:207 and TextDocumentSyncHandler.java:73 (parse cache). An attacker who places a crafted compiled.bin or cache.bin in a *-kompiled directory gets gadget execution when a victim runs kompile/kprove/krun/kast against that directory.

Impact (as reviewed): Arbitrary code execution in the K frontend JVM, i.e. full compromise of the user running kompile/kprove/krun or the language server. The object is cast to CompiledDefinition/Map only after readObject() returns, so any classpath gadget chain runs first. Root cause for both the kompile cache path and the LSP auto-load path.

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

Strongest counterargument found during red-teaming: No weaponizable gadget chain has been demonstrated for this exact classpath (commons-collections4 4.3 and Guava 32.1.3 defeat the classic chains), so the CRITICAL 'arbitrary code execution' claim rests on custom gadget development rather than a proven exploit; without a chain the confirmed impact is attacker-controlled object-graph allocation (DoS) plus class loading, and the LSP kompile path also requires the victim to run K tooling inside an attacker-supplied directory.

Trigger (as reviewed): findCacheFile() recursively walks the opened workspace, selects the shallowest file named cache.bin (Kompile.CACHE_FILE_NAME) and passes it to BinaryLoader.loadCache with no provenance or integrity validation. loadCaches() is re-invoked from KWorkspaceService.didChangeWatchedFiles (KWorkspaceService.java:29). Any repository that ships a cache.bin at its root or under *-kompiled/ is deserialized as soon as the K language server initializes.

Impact (as reviewed): Remote code execution on the developer workstation from merely opening a malicious K project in VS Code or another LSP client. This is the most likely exploitation vector for the deserialization primitive in kfrontend-compile-001 because the attack file arrives with the repository and needs no further user action.

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

Strongest counterargument found during red-teaming: The RCE impact is not established: the commons-collections4 4.3 unsafe-serialization guard blocks the classic transformer chain unless a system property that appears nowhere in the repo is set, JDK 17+ removes the standard JDK gadgets, and no alternative classpath gadget chain was demonstrated. The confirmed impact from this finding alone is deterministic DoS/crash plus the attacker-controlled Source path read, and the trigger is one diagnostic or definition request rather than plain initialization, with client behavior (workspaceFolders, auto-diagnostics, Workspace Trust) outside the audited checkout.

Trigger (as reviewed): loadOrDie (line 46) and loadCache (line 62) both funnel arbitrary files through loadImpl. DefinitionLoadingModule.koreDefinition loads compiled.bin from the resolved -kompiled directory, which is selected from --definition, KRUN_KOMPILED_DIR, or a directory scan. Any definition directory obtained from a tarball, build artifact, shared filesystem, or CI cache is attacker-influenced data, and ObjectInputStream.readObject() executes readObject/readResolve on every class in the stream before the cls.cast check runs.

Impact (as reviewed): Classic Java deserialization RCE: a crafted compiled.bin yields arbitrary code execution with the privileges of kompile/krun/kprove, or at minimum memory exhaustion via deeply nested object graphs. The cls.cast(obj) guard is after-the-fact and provides no protection.

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

Strongest counterargument found during red-teaming: The RCE half of the CRITICAL rating is unproven: commons-collections4 4.3 hardens its transformer chain, and no other confirmed ysoserial-style gadget was identified on the frontend classpath, so in practice the demonstrated impact may be availability-only (StackOverflowError/OutOfMemoryError) rather than code execution. Separately, the primary path requires a victim to load an attacker-controlled definition directory, which is a real but user-mediated trust boundary; however, the LSP workspace scan and the default cwd '*-kompiled' scan make that boundary easy to cross without an explicit flag.

Trigger (as reviewed): loadCache is a second independent entry point into loadImpl. It is intentionally tolerant: any IOException/ClassNotFoundException is downgraded to a warning and null is returned, so a malformed or hostile cache file never stops the pipeline. Caches live under the kompiled/temp directory and are frequently persisted across CI runs.

Impact (as reviewed): Same deserialization RCE primitive as kfrontend-parser-001, reachable through cache files that are more likely to be treated as disposable and less carefully controlled. The error handling guarantees a partially-consumed hostile stream never aborts the load.

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

Strongest counterargument found during red-teaming: The finding's HIGH severity rests on RCE, but no usable gadget chain was demonstrated for this exact classpath (JDK 17, Guava 32.1.3, commons-collections4 4.3, Scala 2.13); and the LSP vector depends on an external IDE client sending workspaceFolders and auto-issuing diagnostics or a user invoking goto-definition, plus any host workspace-trust gating, none of which is verifiable in this checkout. The 'frequently persisted across CI runs' premise and the 'kompiled/temp' wording are also inaccurate for this repository.