pyk: path traversal family (kcfg ids, proof ids, requires, kbuild targets)

Trigger (as reviewed): KCFGStore.read_cfg_data parses kcfg.json with json.loads (no schema validation) and iterates dct.get('nodes'), feeding every element straight into read_node_data(node_id) with no type or range check. read_node_data (kcfg/kcfg.py:110) calls kcfg_node_path, which builds self.kcfg_node_dir / f'{node_id}.json' (kcfg/kcfg.py:71). Because node_id is interpolated into a Path component, values such as '../../../../etc/shadow' or an absolute path escape the store directory; the .json suffix only constrains the target filename. KCFG.read_cfg_data(cfg_dir) (kcfg/kcfg.py:1298) exposes this to callers loading a KCFG from a directory they did not create (e.g. a downloaded/shared proof-artifact directory).

Impact (as reviewed): Arbitrary read of any *.json file the pyk process can read, with the parsed content then fed into KCFG.from_dict / CTerm.from_dict. Chained with 002/007 this yields local file disclosure plus attacker-selected JSON entering the deserializer.

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

Strongest counterargument found during red-teaming: The only durable doubt is operational rather than technical: default pyk runs never read a proof directory (save_directory defaults to None), so exploitation needs a victim who loads a directory the attacker can write, and general content disclosure additionally needs the target to be *.json and its content to be surfaced in output or logs. No code-level sanitizer or type barrier mitigates the traversal once that precondition holds.

Trigger (as reviewed): The id-hashed variant immediately above (proof.py:108) is safe, but proof_data_exists and the parallel read_proof_data (proof.py:245-259, proof/implies.py:187-191) interpolate the raw proof id as a path segment: proof_dir / id / 'proof.json'. A caller- or file-supplied id such as '../../../../tmp/x' resolves outside proof_dir. Proof.read_proof_data (line 250) also builds proof_dir / id / 'proof.json', and fetch_subproof_data (line 169) drives it from subproof_ids read out of proof JSON.

Impact (as reviewed): Arbitrary read of any proof.json on the host, and (via sibling write_proof_data paths) potential writes outside the intended proof directory. Proof ids also flow into locals()[proof_type] dispatch (006), so hostile artifacts control both the file read and the deserializer entry point.

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

Strongest counterargument found during red-teaming: The exploit needs a victim workflow that both sets --save-directory and treats the .k spec (or save-dir contents) as untrusted; this checkout has no such CI usage, effects are same-user, reads are limited to files named proof.json, and the Java frontend step was verified statically rather than executed end-to-end. The 'HIGH' severity is therefore arguable, but the unsafe path interpolation is confirmed and no sanitizer exists.

Trigger (as reviewed): OuterParser.require() (kast/outer_parser.py:121-124) parses the requires "PATH" string out of a .k/.md definition with no sanitization into Require(path). slurp_definitions (kast/utils.py:42-67) then calls _resolve_require, which joins the raw string onto the definition directory and every include dir. require.path == '../../../etc/passwd' (or an absolute path) is accepted, resolved, and read by _parse_file (kast/utils.py:70-78) and parsed as K source. Nothing restricts the result to include_dirs or a project subtree.

Impact (as reviewed): When pyk parses an untrusted K definition (parse_outer, kprove, CI import of third-party specs), the attacker-chosen file is read off disk and its contents surfaced in parser error messages. Local file disclosure plus arbitrary-text-as-K-source ingestion.

Trigger (as reviewed): target_name reaches definition_dir directly from the CLI (pyk/src/pyk/kbuild/main.py:35) and from do_which. No valid_id-style validation is applied; Project.get_target only compares names for equality. A value such as ../../../../tmp/owned resolves the output definition directory outside kdist_dir.

Impact (as reviewed): KBuild.kompile passes the resolved directory to kompile(output_dir=...), which invokes the K compiler with --output-definition . An attacker who can influence target_name causes the toolchain to create and populate a kompiled definition tree at an arbitrary writable path: an arbitrary-directory-write primitive.

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

Strongest counterargument found during red-teaming: The write requires attacker control of kbuild.toml; with that control the attacker also chooses main-file and ccopts, which reach the backend compiler via -ccopt, so the directory-write primitive may add no capability beyond the hostile-build-configuration model, and the .. variant fails to populate on a fresh tree because kdist/<version> does not exist. The absolute-target-name variant nevertheless yields a verified create-and-populate primitive.

Trigger (as reviewed): check_relative_path rejects only absolute paths, so main-file = '../../../../etc/foo.k' passes. KBuildEnv._kompile_args (pyk/src/pyk/kbuild/kbuild.py:132) then computes self._source_dir(self.project) / args['main_file'], escaping the synced project tree. If args['main-file'] is missing the code raises KeyError; if empty/None, main_file is never assigned and line 72 raises UnboundLocalError.

Impact (as reviewed): A malicious or careless kbuild.toml in a cloned repository can point main-file at an arbitrary .k/.md file on the host, pulling it into the kompiled artifact and escaping the intended project sandbox. The unbound-variable branch masks the validation failure.

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

Strongest counterargument found during red-teaming: The exploit's practical impact is narrower than the finding's wording: the victim must run kbuild kompile against attacker-influenced configuration, the target must already exist as a regular file, and clean artifact inclusion requires the target to parse as K or markdown; non-K files yield only an error-message oracle. A sibling weakness (source = '../..' via relative_path, which also only rejects absolute paths) may provide an equivalent or easier read path, suggesting this may be one instance of a broader validation gap rather than a unique traversal. Additionally, the UnboundLocalError/KeyError branch is only a configuration-triggered crash, not part of the read exploit.

Trigger (as reviewed): The regex capture group resource is \S+, which matches literal ../../. _resource_dir (pyk/src/pyk/kbuild/kbuild.py:112) does self.path / project.name / 'resource' / resource_name with no normalization or containment check, so {{ p:../../../../etc/passwd }} in a target ccopts resolves out of tree.

Impact (as reviewed): The resolved path is returned into ccopts and forwarded verbatim to the LLVM backend as -ccopt . An attacker-controlled kbuild.toml can cause compiler/linker arguments to reference arbitrary host paths, enabling out-of-tree file reads and making the build depend on attacker-selected files. The exists() check only confirms existence.

Trigger (as reviewed): relative_path rejects absolute paths only. source = '../../../../' and resources = {r = '../../../../etc'} in a kbuild.toml are accepted as long as the resolved directory exists. The resulting source_dir is used by source_files (rglob('.k')/rglob('.md')) and by KBuildEnv._sync_project, which copies matched files into the build sandbox.

Impact (as reviewed): An untrusted project definition can make pyk walk and copy arbitrary host directories into the kompiled output and include them in the build: an out-of-sandbox read primitive and a way to pull host content into a distributable artifact. check_dir_path merely verifies existence and is not containment.

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

Strongest counterargument found during red-teaming: The impact overstates what is proven: copied files are staged in a TemporaryDirectory that is deleted after env.kompile, and -I does not obviously copy them into the final definition. kbuild.toml is also effectively executable build configuration (post_process/ccopts), so an untrusted config may already run arbitrary commands; that makes the traversal less of a boundary crossing even though the code path itself is real.

Trigger (as reviewed): file_names is a plain Iterable[str] public parameter. Current in-tree callers pass values computed via Path.relative_to (pyk/src/pyk/kbuild/project.py:175, :189), which cannot contain '..'; however the function performs no containment check on either source_file or target_file, and it is exported for reuse. A file_name of '../../../../tmp/owned' writes outside target_dir and reads outside source_dir.

Impact (as reviewed): Latent arbitrary-file-write/read via the kbuild sync primitive. LOW because present call sites are safe, but the missing guard is a half-applied sanitizer and any new caller passing config-derived names would immediately be exploitable.