diff --git a/SECURITY.md b/SECURITY.md index 48df230bd..c1cc2a00c 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -136,7 +136,7 @@ documents the rule and the regression history (commit `3474943` violated it in 2026-04, reverted in #92 in 2026-05). `lake update` and `lake exe cache get` are the only shell-outs allowed. -**Writable `.lake/`, and why the obvious tampering attack does not work.** +**Writable `.lake/` self-tampering is a known limitation.** Comparator gives `safeLakeBuild` `--rwx /.lake`, which is necessary because lake writes its build outputs there. The natural attack to consider is: a `Submission.lean` `initialize` block spawns a @@ -147,24 +147,16 @@ to PID 1, not killed), and races to overwrite `Solution.olean` between reading it — getting comparator to verify against an attacker-controlled olean. -We ran [scripts/security_probes/artifact_tamper_probe.py](scripts/security_probes/artifact_tamper_probe.py) -on Linux (kernel 6.12 + Lean v4.32.2 + landrun 5ed4a3db + comparator -71b52ec) on 2026-07-29. Inside the sandbox, `IO.Process.spawn` succeeds -for the whitelisted `lean` and `git` binaries; `sh`, `setsid`, `bash`, -`cp`, `/bin/sh`, and `/usr/bin/env` all return exit 255 ("could not -execute external process"). Phase B confirmed by SHA-256 that the -deliberately distinct prepared olean was not installed. - -**We previously concluded from this that the attack is structurally -impossible at the spawn step. That conclusion was wrong** (2026-08-20), -and the probe result above is what shows it: `lean` spawns successfully. -`lean` is a general-purpose interpreter, so the daemon does not need -`sh` or `setsid` — it can be another `lean` running an attacker-written -`initialize` block. Detaching it needs no external binary either: -`IO.Process.SpawnArgs` has a native `setsid : Bool` field -(`Init/System/IO.lean`, v4.32.2). Orphaned children are reparented -rather than killed when the landrun child exits. Two further holes in -the same argument: `executablePaths := #[leanPrefix, gitLocation]` +[scripts/security_probes/artifact_tamper_probe.py](scripts/security_probes/artifact_tamper_probe.py) +shows that `IO.Process.spawn` succeeds for the whitelisted `lean` and +`git` binaries while `sh`, `setsid`, `bash`, `cp`, `/bin/sh`, and +`/usr/bin/env` are denied. Phase B verifies by SHA-256 that its deliberately +distinct prepared olean is not installed. Neither result rules out the attack: +`lean` is a general-purpose interpreter, so the daemon can be another `lean` +running an attacker-written `initialize` block. Detaching it needs no external +binary because `IO.Process.SpawnArgs` has a native `setsid : Bool` field. +Orphaned children are reparented rather than killed when the landrun child +exits. In addition, `executablePaths := #[leanPrefix, gitLocation]` whitelists exec across the *entire* Lean prefix (`lake`, `clang`, `ld.lld`, `leanc`, ...), not just `lean`; and comparator passes `-ldd`, which whitelists the dynamic loader, and a permitted loader can load a @@ -175,15 +167,12 @@ So the premise that no persistent child is possible does not hold, and `safeLakeBuild` produced. We have no working exploit, so this is an unsound argument rather than a demonstrated attack, and note that any substituted olean is still replayed through the kernel and -`external_kernels`. Tracked upstream at +`external_kernels`. This known limitation is tracked upstream at https://github.com/leanprover/comparator/issues/77, with a proposed fix in https://github.com/leanprover/comparator/pull/78 that runs each landrun invocation as PID 1 of a fresh PID namespace, so the kernel -tears down any survivors before comparator proceeds. Note that the -obvious cheaper fixes do not work: copying the olean out before -exporting, hashing it, or renaming its directory all still race a -daemon that rewrites in a loop, and `killpg` misses exactly the process -that called `setsid`. Update this section when that PR lands. +tears down any survivors before comparator proceeds. The current pin does not +contain that proposed fix. This applies to every runner we use today; it has nothing to do with any particular kernel. Re-derive it after any landrun, comparator, or @@ -329,11 +318,9 @@ escaping, the triage gate) are in the submissions repo's `SECURITY.md`. Re-run the probe by hand on a clean Linux box after any landrun bump. 2. **Writable-`.lake` self-tampering** (Section 3). **Not currently - mitigated.** We used to claim landrun's exec restriction ruled out - the daemon this attack needs; it does not, because the daemon can be - `lean`, which is whitelisted. Nothing stops a descendant outliving - `safeLakeBuild` and racing `safeExport`. No working exploit is known, - and a substituted olean is still kernel-checked. Tracked at + mitigated at the pinned comparator commit.** A `lean` descendant can + outlive `safeLakeBuild` and race `safeExport`. No working exploit is + known, and a substituted olean is still kernel-checked. Tracked at https://github.com/leanprover/comparator/issues/77; proposed fix in https://github.com/leanprover/comparator/pull/78. 3. **`lake env` behaviour across lake versions.** The `lake_env_probe` diff --git a/scripts/aristotle/poll_queue.py b/scripts/aristotle/poll_queue.py deleted file mode 100755 index c12e2b70b..000000000 --- a/scripts/aristotle/poll_queue.py +++ /dev/null @@ -1,317 +0,0 @@ -#!/Users/kim/.local/share/uv/tools/aristotlelib/bin/python -"""Manage the Aristotle negation queue. - -One iteration: - 1. Poll every entry in `aristotle-negations/state.json` whose status is - `submitted`. If Aristotle reports COMPLETE, download and classify the - result as `broken` / `verified` / `inconclusive`. - 2. Submit up to (5 - in-flight) entries currently `ready_to_submit`. - 3. Print a summary; surface any newly-`broken` problems with a loud banner - so the loop driver (Claude or a human) can act on it. - -Drive with `/loop 10m scripts/aristotle/poll_queue.py` once seeded. - -state.json schema (per problem id): - - { - "status": "ready_to_submit" | "submitted" | "complete" - | "broken" | "verified" | "inconclusive" - | "skipped" | "error", - "prompt": str, # only meaningful while ready_to_submit - "project_id": str | None, - "submitted_at": ISO-8601 str | None, - "completed_at": ISO-8601 str | None, - "skip_reason": str | None, - "notes": str | None, - "notified": bool, # true once Claude/human has seen this break - } -""" - -from __future__ import annotations - -import asyncio -import datetime as dt -import json -import os -import re -import shutil -import subprocess -import sys -import tarfile -from pathlib import Path - -import aristotlelib - -REPO_ROOT = Path(__file__).resolve().parent.parent.parent -NEG_ROOT = REPO_ROOT / "aristotle-negations" -STATE_PATH = NEG_ROOT / "state.json" -RESULTS_ROOT = NEG_ROOT / "results" -FINDINGS_ROOT = NEG_ROOT / "findings" -SUMMARY_PATH = FINDINGS_ROOT / "SUMMARY.md" - -MAX_INFLIGHT = 5 - -# A distinctive substring Aristotle leaves in the output when it determined -# the submitted statement (here: a *negation*) is itself false. For us that -# means "Aristotle could not falsify the original" — boring but reassuring. -ARISTOTLE_FALSE_MARKER = "Aristotle found this block to be false" - - -def now_iso() -> str: - return dt.datetime.now(dt.timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ") - - -def load_state() -> dict: - if not STATE_PATH.exists(): - return {} - return json.loads(STATE_PATH.read_text()) - - -def save_state(state: dict) -> None: - tmp = STATE_PATH.with_suffix(".json.tmp") - tmp.write_text(json.dumps(state, indent=2, sort_keys=True)) - tmp.replace(STATE_PATH) - - -def workspace_for(problem_id: str) -> Path: - return NEG_ROOT / problem_id - - -def submit(problem_id: str, prompt: str) -> str: - """Run `aristotle submit` and return the new project_id. - - The CLI prints `Project created: ` on success. We capture stdout and - pull the id back out of it. - """ - proj_dir = workspace_for(problem_id) - if not proj_dir.is_dir(): - raise RuntimeError(f"workspace missing: {proj_dir}") - cmd = [ - "aristotle", "submit", prompt, - "--project-dir", str(proj_dir), - ] - result = subprocess.run(cmd, capture_output=True, text=True, check=True) - out = result.stdout + result.stderr - m = re.search(r"Project created:\s*(\S+)", out) - if not m: - raise RuntimeError(f"could not parse project id from aristotle output:\n{out}") - return m.group(1) - - -async def fetch_project(project_id: str): - return await aristotlelib.Project.from_id(project_id) - - -def aristotle_status_to_label(status) -> str: - """Map aristotlelib.ProjectStatus -> our short string.""" - return getattr(status, "value", str(status)).upper() - - -def extract_result_archive(result_path: Path) -> Path: - """`aristotle result` writes a single tar.gz archive at --destination. - Extract it next to the archive (sibling dir) and return that dir.""" - if result_path.is_dir(): - return result_path - extract_dir = result_path.parent / (result_path.name + "_extracted") - if extract_dir.exists(): - shutil.rmtree(extract_dir) - extract_dir.mkdir(parents=True) - with tarfile.open(result_path, "r:gz") as tf: - tf.extractall(extract_dir) - return extract_dir - - -def classify_result_dir(result_dir: Path) -> str: - """Return one of 'broken', 'verified', 'inconclusive'. - - Strategy: read every .lean file Aristotle handed back; if any of them - contain ARISTOTLE_FALSE_MARKER, the *negation* was determined false and - we conclude `verified` (the original is true). Otherwise, if any file - contains a real (non-`sorry`/`admit`) proof body for a `*_negation` - theorem, the negation was proved -- the original is `broken`. Otherwise - we have no useful signal -> `inconclusive`. - """ - result_dir = extract_result_archive(result_dir) - lean_files = list(result_dir.rglob("*.lean")) - saw_proof = False - for lf in lean_files: - try: - text = lf.read_text() - except Exception: - continue - if ARISTOTLE_FALSE_MARKER in text: - return "verified" - # Look for a *_negation theorem with a non-sorry body. We're lenient - # here: anything that isn't just `by sorry` / `by admit` counts as a - # proof. Aristotle wraps proofs in `by ...` blocks, sometimes long. - # Locate each `theorem foo_negation ... :=` and grab everything - # after the `:=` up to the next top-level decl or end-of-file. - for m in re.finditer(r"theorem\s+(\w+_negation)\b", text): - after = text[m.end():] - # The theorem-body delimiter is the LAST top-level `:= ...` before - # the next top-level decl or EOF (signature can contain nested - # `haveI : ... := ...`, hence not the first `:=`). - end_match = re.search(r"\n(?:theorem|lemma|def|instance|example|namespace|end\b|/-)", after) - scope = after[: end_match.start()] if end_match else after - seps = list(re.finditer(r":=\s*", scope)) - if not seps: - continue - body_start = seps[-1].end() - body = scope[body_start:].strip() - # Strip Lean line comments (`-- ...`) and block comments (`/- ... -/`), - # plus the leading `by`, so we can reliably tell whether what's left - # is just `sorry`/`admit` or a genuine proof. - cleaned = re.sub(r"/-[\s\S]*?-/", "", body) - cleaned = re.sub(r"--[^\n]*", "", cleaned) - cleaned = re.sub(r"^\s*by\b", "", cleaned).strip() - if cleaned and not re.fullmatch(r"(sorry|admit)\s*", cleaned): - saw_proof = True - break - if saw_proof: - break - return "broken" if saw_proof else "inconclusive" - - -async def poll_one(problem_id: str, entry: dict) -> dict: - """Update `entry` in place by polling Aristotle. Return entry.""" - pid = entry.get("project_id") - if not pid: - return entry - project = await fetch_project(pid) - status = aristotle_status_to_label(project.status) - # `COMPLETE` and `COMPLETE_WITH_ERRORS` are both terminal — Aristotle - # publishes whatever progress it made and we can download + classify. - terminal = {"COMPLETE", "COMPLETE_WITH_ERRORS"} - if status not in terminal: - # Still in flight; record the latest observation in `notes`. - entry["notes"] = f"aristotle status: {status} ({getattr(project, 'percent_complete', '?')}%)" - return entry - # Complete. Download. `aristotle result` REQUIRES destination to not - # already exist, so we make sure it doesn't (idempotent across reruns). - result_dir = RESULTS_ROOT / problem_id - if result_dir.exists(): - shutil.rmtree(result_dir) - RESULTS_ROOT.mkdir(parents=True, exist_ok=True) - cmd = ["aristotle", "result", pid, "--destination", str(result_dir)] - subprocess.run(cmd, check=True, capture_output=True, text=True) - label = classify_result_dir(result_dir) - entry["status"] = label - entry["completed_at"] = now_iso() - entry["notes"] = f"classified as {label}" - if label == "broken": - write_finding(problem_id, result_dir, entry) - return entry - - -def write_finding(problem_id: str, result_dir: Path, entry: dict) -> None: - FINDINGS_ROOT.mkdir(parents=True, exist_ok=True) - finding = FINDINGS_ROOT / f"{problem_id}.md" - proof_excerpt = "" - for lf in sorted(result_dir.rglob("*_aristotle.lean")) or sorted(result_dir.rglob("*.lean")): - try: - proof_excerpt = lf.read_text() - break - except Exception: - continue - finding.write_text( - f"# Counterexample for `{problem_id}`\n\n" - f"Aristotle proved the negation of this leaderboard problem. The original\n" - f"statement is therefore broken.\n\n" - f"- project_id: `{entry.get('project_id')}`\n" - f"- submitted_at: {entry.get('submitted_at')}\n" - f"- completed_at: {entry.get('completed_at')}\n\n" - f"## Aristotle's proof of the negation\n\n```lean\n{proof_excerpt}\n```\n" - ) - # Append a one-liner to SUMMARY.md. - line = f"- [{problem_id}]({problem_id}.md) (project `{entry.get('project_id')}`, completed {entry.get('completed_at')})\n" - if SUMMARY_PATH.exists(): - SUMMARY_PATH.write_text(SUMMARY_PATH.read_text() + line) - else: - SUMMARY_PATH.write_text("# Broken leaderboard problems\n\n" + line) - - -def submit_refill(state: dict) -> list[str]: - """Submit up to (MAX_INFLIGHT - in-flight) ready problems. Return ids submitted.""" - inflight = sum(1 for e in state.values() if e.get("status") == "submitted") - slots = MAX_INFLIGHT - inflight - if slots <= 0: - return [] - ready = sorted( - ((pid, e) for pid, e in state.items() if e.get("status") == "ready_to_submit"), - key=lambda kv: kv[1].get("queued_at", ""), - ) - submitted = [] - for problem_id, entry in ready[:slots]: - prompt = entry.get("prompt") or "Try to find a counterexample to this theorem; replace the sorry with a proof only if you do." - try: - project_id = submit(problem_id, prompt) - except Exception as e: - entry["status"] = "error" - entry["notes"] = f"submit failed: {e}" - continue - entry["status"] = "submitted" - entry["project_id"] = project_id - entry["submitted_at"] = now_iso() - submitted.append(problem_id) - return submitted - - -async def main() -> int: - if not STATE_PATH.exists(): - print(f"no state file at {STATE_PATH}; nothing to do") - return 0 - state = load_state() - - # 1. Poll in-flight. - polled = [] - for problem_id, entry in state.items(): - if entry.get("status") == "submitted": - polled.append(problem_id) - try: - await poll_one(problem_id, entry) - except Exception as e: - entry["notes"] = f"poll failed: {e}" - - # 2. Refill. - submitted = submit_refill(state) - - save_state(state) - - # 3. Summarise. - counts = {} - for e in state.values(): - counts[e.get("status", "?")] = counts.get(e.get("status", "?"), 0) + 1 - print("== Aristotle negation queue ==") - for k in sorted(counts): - print(f" {k:18s} {counts[k]}") - if submitted: - print(f"\nsubmitted {len(submitted)}: {', '.join(submitted)}") - if polled: - print(f"polled {len(polled)}: {', '.join(polled)}") - - # 4. Surface any new BROKEN. - new_broken = [pid for pid, e in state.items() - if e.get("status") == "broken" and not e.get("notified")] - if new_broken: - banner = "!" * 78 - print(f"\n{banner}") - for pid in new_broken: - print(f"NEW BROKEN: {pid} -> aristotle-negations/findings/{pid}.md") - print(f"{banner}\n") - # Also fire a desktop notification if we can. - try: - subprocess.run([ - "osascript", "-e", - f'display notification "{len(new_broken)} broken: {", ".join(new_broken)[:120]}" with title "Aristotle counterexample"' - ], check=False) - except FileNotFoundError: - pass - # Mark notified so we don't re-bang next iteration. - for pid in new_broken: - state[pid]["notified"] = True - save_state(state) - return 0 - - -if __name__ == "__main__": - sys.exit(asyncio.run(main())) diff --git a/scripts/aristotle/record_ready.py b/scripts/aristotle/record_ready.py deleted file mode 100755 index 120282aa6..000000000 --- a/scripts/aristotle/record_ready.py +++ /dev/null @@ -1,51 +0,0 @@ -#!/Users/kim/.local/share/uv/tools/aristotlelib/bin/python -"""Record a curated negation as ready_to_submit in state.json. - -Usage: record_ready.py - -If is "-", read prompt from stdin. -Idempotent: if the entry already exists, only update prompt + queued_at if it -is still in `ready_to_submit` state. Refuses to overwrite a submitted/complete -entry. -""" -import datetime as dt -import json -import sys -from pathlib import Path - -REPO_ROOT = Path(__file__).resolve().parent.parent.parent -STATE_PATH = REPO_ROOT / "aristotle-negations" / "state.json" - - -def main() -> int: - if len(sys.argv) != 3: - print(__doc__, file=sys.stderr) - return 2 - pid, prompt = sys.argv[1], sys.argv[2] - if prompt == "-": - prompt = sys.stdin.read() - state = json.loads(STATE_PATH.read_text()) - existing = state.get(pid) - if existing and existing.get("status") not in (None, "ready_to_submit", "skipped", "error"): - print(f"refusing to overwrite {pid} (status={existing.get('status')})", file=sys.stderr) - return 1 - now = dt.datetime.now(dt.timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ") - state[pid] = { - "status": "ready_to_submit", - "prompt": prompt, - "queued_at": now, - "project_id": None, - "submitted_at": None, - "completed_at": None, - "skip_reason": None, - "notes": None, - } - tmp = STATE_PATH.with_suffix(".json.tmp") - tmp.write_text(json.dumps(state, indent=2, sort_keys=True)) - tmp.replace(STATE_PATH) - print(f"recorded {pid} as ready_to_submit") - return 0 - - -if __name__ == "__main__": - sys.exit(main()) diff --git a/scripts/aristotle/stage.sh b/scripts/aristotle/stage.sh deleted file mode 100755 index de0af4108..000000000 --- a/scripts/aristotle/stage.sh +++ /dev/null @@ -1,33 +0,0 @@ -#!/bin/bash -# Stage an Aristotle-negation workspace for problem $1. -# Copies lean-toolchain and ChallengeDeps.lean (if present), writes a -# minimal lakefile.toml. Does NOT touch Negation.lean — that's hand-written. -set -euo pipefail -pid="$1" -src="generated/$pid" -dst="aristotle-negations/$pid" -[ -d "$src" ] || { echo "no such problem: $pid" >&2; exit 1; } -mkdir -p "$dst" -cp "$src/lean-toolchain" "$dst/lean-toolchain" -extra_libs="" -if [ -f "$src/ChallengeDeps.lean" ]; then - cp "$src/ChallengeDeps.lean" "$dst/ChallengeDeps.lean" - extra_libs=$'\n[[lean_lib]]\nname = "ChallengeDeps"' -fi -# Read the Mathlib rev from the source lakefile so we keep the toolchain pin. -rev=$(awk '/^rev = /{gsub(/[" ]/,""); split($0,a,"="); print a[2]}' "$src/lakefile.toml") -cat > "$dst/lakefile.toml" < Now click this to install on the repo (1 click + select repo + confirm):") print(f" {html_url}/installations/new") print( - f"\n=> When done, tell Claude the App ID is {app_id} " - f"and the Client ID is {client_id}." + f"\n=> Record the App ID {app_id} and Client ID {client_id} " + "for the repository configuration." ) diff --git a/scripts/security_probes/artifact_tamper_probe.py b/scripts/security_probes/artifact_tamper_probe.py index bb0816cb0..3702176a0 100644 --- a/scripts/security_probes/artifact_tamper_probe.py +++ b/scripts/security_probes/artifact_tamper_probe.py @@ -10,8 +10,8 @@ 1. Spawn a daemon during Submission's elaboration. Daemon inherits landrun's filesystem rules (which permit writes under `.lake/`). - 2. Daemon detaches via setsid + double-fork, surviving the parent - `lake build Solution` exit (and thus surviving comparator's + 2. Daemon detaches via `IO.Process.SpawnArgs.setsid`, surviving the + parent `lake build Solution` exit (and thus surviving comparator's landrun child). 3. Daemon races to overwrite `.lake/build/lib/lean/Solution.olean` with a pre-prepared olean whose theorem statement matches Challenge but @@ -20,9 +20,6 @@ attacker's olean rather than the legitimate one. `verifyMatch` succeeds because the statement type matches Challenge. -Codex flagged this attack class in the second-opinion pass. SECURITY.md -must explicitly cite the result of this probe. - Phases: --phase=A Establish whether landrun children survive parent exit. @@ -34,27 +31,15 @@ --phase=both (default) Run A then B, report both. -LIMITATION (2026-08-20): the exec-allowlist half of this probe does not -establish what we once read it as establishing. It shows `sh`, `setsid`, -`bash`, `cp` and `env` are denied, and we concluded from that that no -daemon can be spawned. But the probe's own `want_ok` case shows `lean` -spawning successfully, and `lean` is a general-purpose interpreter: the -daemon can simply be another `lean`. It needs no external `setsid` -either, since `IO.Process.SpawnArgs` has a native `setsid : Bool` field. -Step 2 above should be read as "detaches via `SpawnArgs.setsid`", not as -requiring the `setsid` binary. Extending this probe to attempt that is -the obvious next step; see -https://github.com/leanprover/comparator/issues/77. - -This probe does NOT have a CI mode that asserts "no exploit" by default. -Note also that the mitigations once sketched here (setsid + killpg -around landrun, or copying the olean out before export) do not work: a -daemon rewriting in a loop races the copy just as it raced the export, -and `killpg` misses a process that called `setsid` itself. The remedy -under discussion upstream is for comparator to detect surviving -descendants and fail, rather than to try to win the race; see -leanprover/comparator#78. Once a mitigation is in place, add a CI -assertion that Phase B reports REJECTED. +LIMITATION: the exec-allowlist half of this probe does not establish that a +daemon cannot be spawned. It denies `sh`, `setsid`, `bash`, `cp`, and `env`, +but permits `lean`. Another Lean process can detach without an external binary +because `IO.Process.SpawnArgs` has a native `setsid : Bool` field. This probe +does not have a CI mode that asserts "no exploit" by default. The current +comparator pin does not guarantee that descendants cannot survive between +`safeLakeBuild` and `safeExport`; this limitation is tracked in +https://github.com/leanprover/comparator/issues/77, with a proposed fix in +https://github.com/leanprover/comparator/pull/78. """ from __future__ import annotations diff --git a/scripts/security_probes/env_dump_probe.py b/scripts/security_probes/env_dump_probe.py index 80e859bdd..801d5806d 100644 --- a/scripts/security_probes/env_dump_probe.py +++ b/scripts/security_probes/env_dump_probe.py @@ -4,12 +4,10 @@ allowlist we expect to user-controlled Submission elaboration — no more, no less. -Codex correctly pushed back on a spot-check probe ("does GH_TOKEN leak? -does ANTHROPIC_API_KEY leak?") because spot checks miss the next -unknown token class. This probe is allowlist-based: the parent shell -sets a battery of decoy-secret env vars, the Submission's initialize -block dumps every env var visible to it, and the probe asserts the -visible set is exactly: +Spot checks for named credentials miss unknown token classes. This probe is +allowlist-based: the parent shell sets a battery of decoy-secret env vars, the +Submission's initialize block dumps every env var visible to it, and the probe +asserts the visible set is exactly: {PATH, HOME, LEAN_ABORT_ON_PANIC}