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

オープン
  • 何か問題がありますか？
#4,973 コメント 0 件 リアクション 0 件 担当者 0 名 GitHub で見る

まだ誰も着手していません。

評価

難易度
4/5
見積もり時間
1週間以上
初心者へのやさしさ
15/100
issue の種類
バグ
明瞭さ
おおむね明確
活発さ
活発
技術スタック
bash, java
領域
cli, security

調査の方向性

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.

索引モデルが issue の本文から書いたものです。

説明

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.

主要言語
Python
スター
605
フォーク
165
30日以内にマージされた PR はありません

環境構築

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

runtimeverification/k のほかの issue

runtimeverification/k の issue をすべて見る

似ている issue

Python の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。