krun/kparse source `configVars.sh` from a caller-selectable kompiled directory
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 4/5
- Tiempo estimado
- Más de una semana
- Aptitud para principiantes
- 15/100
Línea de trabajo
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.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
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.
- Lenguaje dominante
- Python
- Estrellas
- 605
- Forks
- 165
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Preparar el entorno
- Sin Dockerfile ni archivo de Docker Compose
- Sin plantilla de pull request
- Leer la guía de contribución
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de runtimeverification/k
-
Dificultad 4/5 3-5 días Aptitud para principiantes 15/100
runtimeverification/k#4972 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 22/100
runtimeverification/k#4971 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 15/100
runtimeverification/k#4970 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 15/100
runtimeverification/k#4969 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 18/100
runtimeverification/k#4968 ·
Todos los issues de runtimeverification/k
Issues similares
-
[BUG]: Compliance rules never see Unity Catalog views as viewsPosiblemente ocupada @wagnercsantos la tomó hoy. Abierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
databrickslabs/ontos#1348 ·
Los mantenedores suelen responder en 3 días
-
`forum_pr_poster` action will always return `none` when checking for pre-existing feedback threads, even if a feedback thread already exists.Posiblemente ocupada @pgmzeta la tomó hoy. AbiertoE-Verified P-Major
Dificultad 2/5 1-3 horas Aptitud para principiantes 79/100
goonstation/goonstation#28259 ·
Los mantenedores suelen responder en 2 días
-
enhancement
Dificultad 2/5 1-3 horas Aptitud para principiantes 65/100
woonstadrotterdam/monumenten#70 ·
Los mantenedores suelen responder en 15 días
-
binding:python bug
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
Los mantenedores suelen responder en 1 día
-
The Browser tab fails with a Wayland error when Open Terminal runs from a Wayland desktop sessionAbierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
open-webui/open-terminal#210 ·