krun/kparse source `configVars.sh` from a caller-selectable kompiled directory

Đang mở
  • Có gì không ổn?
#4,973 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Chưa có ai nhận issue này.

Đánh giá

Độ khó
4/5
Thời gian dự kiến
Hơn một tuần
Mức phù hợp với người mới
15/100
Loại issue
Lỗi
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
bash, java
Lĩnh vực
cli, security

Hướng nghiên cứu

The sink is source "$kompiledDir/configVars.sh" in k-distribution/src/main/scripts/bin/krun (around line 498) and kparse (line 183). The generator is initializeConfigurationVariableDefaultSorts in k-frontend/src/main/java/org/kframework/kompile/CompiledDefinition.java (around lines 106-139). Read the generator first to see which values are interpolated unescaped. Done would mean configVars.sh is written with safe quoting or a non-shell format, and the scripts read it without executing it. The trust-model decision in the report needs maintainer input before any patch.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

Summary

source "$kompiledDir/configVars.sh" executes shell from a directory selected by -d, discovered via ./*-kompiled, or produced by kompile with attacker-influenced names (the generator on the Java side interpolates token text into single-quoted shell without escaping).

3 finding(s) (1 HIGH, 1 MEDIUM, 1 LOW) — line-anchor verified at commit 4a46d1231473.

Findings
Severity ID Location Summary
HIGH kfrontend-compile-004 k-frontend/src/main/java/org/kframework/kompile/CompiledDefinition.java:106 Shell injection into the generated configVars.sh sourced by krun
MEDIUM kdist-scripts-015 k-distribution/src/main/scripts/bin/kparse:183 kparse sources the definition's configVars.sh
LOW kdist-scripts-011 k-distribution/src/main/scripts/bin/krun:498 source "$kompiledDir/configVars.sh" executes code from a caller-chosen definition directory
Details
kfrontend-compile-004 — Shell injection into the generated `configVars.sh` sourced by `krun` (k-frontend/src/main/java/org/kframework/kompile/CompiledDefinition.java:106)

Trigger (as reviewed): initializeConfigurationVariableDefaultSorts builds a bash script by interpolating the KConfigVar token text t.s().substring(1), sort.toString(), and (line 134) the parser attribute part[0]/part[1] into single-quoted shell strings without escaping, then writes it with saveToKompiled("configVars.sh", ...) at line 139. The script is sourced by k-distribution/src/main/scripts/bin/krun:498, kparse:183 and kparse-gen:162. The K lexer limits KConfigVar to [A-Z][A-Za-z0-9'_]* so the direct payload is a quote-breakout, but kompile --outer-parsed-json and a crafted compiled.bin bypass the lexer and allow arbitrary token text and sort/module names.

Impact (as reviewed): Code execution in the shell that sources configVars.sh whenever a victim runs krun, kparse or kparse-gen on an attacker-authored definition. Even without the lexer bypass, the unbalanced-quote breakout corrupts the generated script and can alter krun control flow (config-var validation and -c handling). A generated-artifact injection: enquoteCString / enquoteKString are used elsewhere in the codebase but not here.

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

Strongest counterargument found during red-teaming: The plain-.k vector depends on the attacker-controlled parser cell attribute reaching CompiledDefinition.initializeConfigurationVariableDefaultSorts after the backend pipeline; that was verified by code reading (DefinitionParsing adds the production to localSentences; only ModuleToKORE filters FrontendOnly keys, and that runs later) but not by an actual kompile run, since the checkout has no built K toolchain, and the in-repo parseNonPgm regression test does not conclusively prove attribute retention because it would also pass if the attribute were dropped (krun would fall back to kast). If some backend step rewrote cell productions, only the hidden --outer-parsed-json path (code execution

kdist-scripts-015 — `kparse` sources the definition's `configVars.sh` (k-distribution/src/main/scripts/bin/kparse:183)

Trigger (as reviewed): Same primitive as candidate 011 in a different tool: kompiledDir is caller-controlled and configVars.sh from it is executed as shell.

Impact (as reviewed): Arbitrary code execution as the invoking user when kparse is pointed at an untrusted compiled definition.

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

Strongest counterargument found during red-teaming: An attacker-authored *-kompiled directory is executable content by design (kparse itself runs parser_<sort>_<module> from it at kparse:194-196, and krun runs interpreter), so an 'untrusted compiled definition' may already imply code execution and the source sink may add no incremental capability; under that trust model the HIGH severity is overstated.

kdist-scripts-011 — `source "$kompiledDir/configVars.sh"` executes code from a caller-chosen definition directory (k-distribution/src/main/scripts/bin/krun:498)

Trigger (as reviewed): kompiledDir is caller-controlled via -d or discovered from ./*-kompiled in the CWD, and configVars.sh from that directory is executed as shell before any validation.

Impact (as reviewed): Any party supplying or substituting a -kompiled directory achieves arbitrary command execution as the invoking user by running krun against it.

Suggested fix

Emit configVars.sh with proper shell escaping (or a non-shell format, e.g. a key=value data file), and document that a kompiled directory is executable-trusted input; consider refusing to source from directories not created by the current user.

From a static audit of this repository at commit 4a46d1231473b599c699160132fd6e76a5c46406 (master). Every location above was verified against the source at that revision; no exploit code was run against this repository or its infrastructure.

Ngôn ngữ chính
Python
Star
605
Fork
165
Không có pull request nào được merge trong 30 ngày

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của runtimeverification/k

Tất cả issue của runtimeverification/k

Issue tương tự

Thêm issue về Python

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.