From edc19abec99c591e992324ef53934977985f5769 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 20 Aug 2026 12:55:28 +0000 Subject: [PATCH 1/2] fix: contain sandbox descendants with util-linux --- Comparator/Namespace.lean | 110 ++++++++++++++++++++++++++++++++++++++ Main.lean | 32 ++++++++--- README.md | 50 +++++++++++++---- 3 files changed, 174 insertions(+), 18 deletions(-) create mode 100644 Comparator/Namespace.lean diff --git a/Comparator/Namespace.lean b/Comparator/Namespace.lean new file mode 100644 index 0000000..1e0e797 --- /dev/null +++ b/Comparator/Namespace.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ + +namespace Comparator.Namespace + +structure Tools where + setpriv : String + unshare : String + deriving Repr + +def configuredTools : IO Tools := do + return { + setpriv := (← IO.getEnv "COMPARATOR_SETPRIV").getD "setpriv" + unshare := (← IO.getEnv "COMPARATOR_UNSHARE").getD "unshare" + } + +private def probeSuccess := "comparator-namespace-probe-ok" + +/-- Build the util-linux supervisor invocation used for every sandboxed command. -/ +def wrap (tools : Tools) (cmd : String) (args : Array String) : String × Array String := + (tools.setpriv, #[ + "--pdeathsig", "SIGKILL", + tools.unshare, + "--user", "--map-current-user", + "--pid", "--fork", "--kill-child=SIGKILL", + "--mount-proc", "--", + cmd + ] ++ args) + +/-- Internal child mode used to verify that the namespace has a private procfs and no capabilities. -/ +def runProbeChild : IO Unit := do + let stat ← IO.FS.readFile "/proc/self/stat" + unless stat.takeWhile (fun c => c != ' ') == "1" do + throw <| .userError "The namespace probe is not PID 1 in its procfs view" + let status ← IO.FS.readFile "/proc/self/status" + unless status.contains "CapEff:\t0000000000000000" do + throw <| .userError "The namespace probe retained effective capabilities" + IO.println probeSuccess + +private def readSetting (path : System.FilePath) : IO (Option String) := + try + return some (← IO.FS.readFile path).trimAscii.toString + catch _ => + return none + +private def explainFailure (problem : String) : IO String := do + let maxUserNamespaces ← readSetting "/proc/sys/user/max_user_namespaces" + let unprivilegedClone ← readSetting "/proc/sys/kernel/unprivileged_userns_clone" + let apparmorRestriction ← + readSetting "/proc/sys/kernel/apparmor_restrict_unprivileged_userns" + + let problem := problem.trimAscii.toString + let problem := if problem.isEmpty then "no diagnostic was produced" else problem + let mut lines := #[s!"Namespace setup failed: {problem}"] + lines := lines.push + "Comparator needs util-linux versions of setpriv and unshare with --pdeathsig, --map-current-user, --kill-child, and --mount-proc support. Install or update util-linux if either command or option is missing." + if maxUserNamespaces == some "0" then + lines := lines.push + "user.max_user_namespaces is 0. On a dedicated runner, an administrator can enable it with: sudo sysctl -w user.max_user_namespaces=15000" + if unprivilegedClone == some "0" then + lines := lines.push + "kernel.unprivileged_userns_clone is 0. On a dedicated runner, an administrator can enable it with: sudo sysctl -w kernel.unprivileged_userns_clone=1" + if apparmorRestriction == some "1" then + lines := lines.push + "Ubuntu AppArmor is restricting unprivileged user namespaces. On a disposable CI runner, enable them with: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0" + if problem.contains "mount" || problem.contains "proc" then + lines := lines.push + "The host or container may forbid mounting a private /proc. Use a runner whose container policy permits unprivileged user, PID, and mount namespaces." + lines := lines.push + "These sysctl changes affect the host. Do not apply them blindly on a shared machine; ask its administrator or use a compatible runner." + return String.intercalate "\n" lines.toList + +private def probe (tools : Tools) (comparatorPath cwd : System.FilePath) : IO (Except String Unit) := do + let (cmd, args) := wrap tools comparatorPath.toString #["--namespace-probe"] + try + let { stdout, stderr, exitCode } ← IO.Process.output { cmd, args, cwd := cwd } + if exitCode == 0 && stdout.trimAscii.toString == probeSuccess then + return .ok () + let output := if stderr.trimAscii.isEmpty then stdout else stderr + return .error output + catch e => + return .error e.toString + +/-- +Check namespace support before any workload starts. Returns whether subsequent sandbox invocations +must use the namespace supervisor. Non-strict mode warns once when containment is unavailable. +-/ +def select (failClosed : Bool) (tools : Tools) (comparatorPath cwd : System.FilePath) : IO Bool := do + if !System.Platform.isLinux then + let details := "Namespace descendant containment is only available on Linux." + if failClosed then + throw <| .userError s!"{details}\nfail_closed is enabled; no workload command was started." + IO.eprintln s!"WARNING: {details}\nContinuing without descendant containment; do not use this \ +fallback for untrusted workloads." + return false + + let result ← probe tools comparatorPath cwd + match result with + | .ok () => + return true + | .error problem => + let details ← explainFailure problem + if failClosed then + throw <| .userError s!"{details}\nfail_closed is enabled; no workload command was started." + IO.eprintln s!"WARNING: {details}\nContinuing without descendant containment; do not use this fallback for untrusted workloads." + return false + +end Comparator.Namespace diff --git a/Main.lean b/Main.lean index fed985c..e12496e 100644 --- a/Main.lean +++ b/Main.lean @@ -6,6 +6,7 @@ Authors: Henrik Böving import Lean import Comparator import Comparator.Landlock +import Comparator.Namespace import Export.Parse namespace Comparator @@ -22,6 +23,8 @@ structure Context where whichLandrun : String whichLean4Export : String externalKernels : (Std.TreeMap String (Array String)) + namespaceTools : Namespace.Tools + namespaceEnabled : Bool abbrev M := ReaderT Context IO @@ -86,10 +89,17 @@ def buildLandrunArgs (spawnArgs : LandrunArgs) : Array String := let args := spawnArgs.executablePaths.foldl (init := args) (fun acc path => acc ++ #["--rox", path.toString]) args ++ #["--", spawnArgs.cmd] ++ spawnArgs.args -def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do +def buildSandboxInvocation (spawnArgs : LandrunArgs) : M (String × Array String) := do + let landrun := (← read).whichLandrun let args := buildLandrunArgs spawnArgs + if (← read).namespaceEnabled then + return Namespace.wrap (← read).namespaceTools landrun args + return (landrun, args) + +def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do + let (cmd, args) ← buildSandboxInvocation spawnArgs let { stdout, stderr, exitCode } ← IO.Process.output { - cmd := (← read).whichLandrun, + cmd, args, env := spawnArgs.envOverride cwd := (← getProjectDir) @@ -101,9 +111,9 @@ def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do def runSandBoxed (spawnArgs : LandrunArgs) : M Unit := do - let args := buildLandrunArgs spawnArgs + let (cmd, args) ← buildSandboxInvocation spawnArgs let proc ← IO.Process.spawn { - cmd := (← read).whichLandrun, + cmd, args, env := spawnArgs.envOverride cwd := (← getProjectDir) @@ -184,11 +194,11 @@ def runExternalKernel (kernelName : String) (kernelCommand : Array String) writablePaths := #[] executablePaths := #[] } - let args := buildLandrunArgs spawnArgs + let (cmd, args) ← buildSandboxInvocation spawnArgs try let proc ← IO.Process.spawn { - cmd := (← read).whichLandrun, + cmd, args, env := spawnArgs.envOverride cwd := (← getProjectDir) @@ -324,9 +334,12 @@ structure Config where def M.run (x : M α) (cfg : Config) : IO α := do let cwd ← IO.Process.getCurrentDir + let comparatorPath ← IO.appPath + let namespaceTools ← Namespace.configuredTools + let namespaceEnabled ← Namespace.select (cfg.fail_closed?.getD false) namespaceTools comparatorPath cwd let whichLandrun := (← IO.getEnv "COMPARATOR_LANDRUN").getD "landrun" if cfg.fail_closed?.getD false then - Landlock.requireEnforcement whichLandrun (← IO.appPath) cwd + Landlock.requireEnforcement whichLandrun comparatorPath cwd let leanPrefix ← queryLeanPrefix cwd let gitLocation ← queryGitLocation let whichLean4Export := (← IO.getEnv "COMPARATOR_LEAN4EXPORT").getD "lean4export" @@ -358,6 +371,8 @@ def M.run (x : M α) (cfg : Config) : IO α := do gitLocation := gitLocation, whichLean4Export := whichLean4Export, whichLandrun := whichLandrun, + namespaceTools := namespaceTools, + namespaceEnabled := namespaceEnabled, externalKernels := externalKernels } @@ -369,6 +384,9 @@ def main (args : List String) : IO Unit := do | throw <| .userError "The Landlock enforcement probe expected a file path" Comparator.Landlock.runProbeChild path return + if args.head? == some "--namespace-probe" then + Comparator.Namespace.runProbeChild + return let some (configPath : String) := args[0]? | throw <| .userError "Expected config file path as first argument." let content ← IO.FS.readFile configPath diff --git a/README.md b/README.md index 2c04d5f..d942873 100644 --- a/README.md +++ b/README.md @@ -3,14 +3,16 @@ Comparator is a trustworthy judge for Lean proofs. It relies on having an existi well as: 1. [`landrun`](https://github.com/Zouuup/landrun), compiled from the `main` branch's source, present in `PATH` 2. [`lean4export`](https://github.com/leanprover/lean4export/), at a version that is compatible with whatever Lean version your project is targeting, present in `PATH` -3. (optional) [nanoda](https://github.com/ammkrn/nanoda_lib/), compiled with a recent version of Rust. +3. On Linux, util-linux versions of `setpriv` and `unshare` present in `PATH` +4. (optional) [nanoda](https://github.com/ammkrn/nanoda_lib/), compiled with a recent version of Rust. This is only necessary if you want to check with the nanoda kernel in addition to the builtin one. `cargo build --release` will place `nanoda_bin` in the `target/release` directory of the checked-out directory, this directory must be present in `PATH` > [!NOTE] > Alternatively full paths to these binaries can be specified using the environment variables -> `COMPARATOR_LANDRUN`, `COMPARATOR_LEAN4EXPORT`, and `COMPARATOR_NANODA` when invoking Comparator. +> `COMPARATOR_LANDRUN`, `COMPARATOR_LEAN4EXPORT`, `COMPARATOR_NANODA`, `COMPARATOR_SETPRIV`, and +> `COMPARATOR_UNSHARE` when invoking Comparator. Comparator is configured through a JSON file: ``` @@ -37,6 +39,8 @@ Given the following assumptions: 5. The Lean kernel is correct (with `external_kernels` this can be reduced to "At least one of the Lean kernel or the `external_kernels` is correct") 6. You are not running this under a privileged user +7. The host permits unprivileged user, PID, and mount namespaces, unless Comparator reports that it + is falling back without descendant containment If the following command succeeds: ``` @@ -86,14 +90,15 @@ moves toward having an option to receive the input file as a `CLI` argument. For development purposes, comparator supports overriding `nanoda` specifically using the `COMPARATOR_NANODA` environment variable. -## Refusing to Run Without an Enforced Landlock Sandbox +## Refusing to Run Without Sandboxing and Descendant Containment Comparator invokes Landrun with `--best-effort` so that the installed Landrun can use the best Landlock ABI available on the running kernel. This also means Landrun may run without applying a policy when Landlock is unavailable. That remains the backwards-compatible default. Set `"fail_closed": true` in the configuration when silently running without filesystem sandboxing -is unacceptable. Before starting any workload command, Comparator then runs its own executable +or descendant containment is unacceptable. Before starting any workload command, Comparator runs a +namespace preflight and then runs its own executable through Landrun and verifies that the normal Comparator policy denies a write to a file which is writable outside the sandbox. If Landlock is unavailable or disabled, Landrun is missing, or a no-op Landrun shim is configured, Comparator exits with an error ending in: @@ -104,7 +109,28 @@ fail_closed is enabled, so no workload command was started This is an end-to-end check for basic filesystem enforcement, not a check for a particular Landlock ABI or every access right. Landrun and the kernel remain trusted to enforce the requested policy. -The default is `false`. + +When the namespace preflight succeeds, every workload Landrun command is supervised by `setpriv` and +`unshare` in a fresh user, PID, and mount namespace with a private `/proc`. Remaining descendants are +killed when the command or Comparator dies. If the preflight fails and `fail_closed` is `false`, +Comparator warns once and runs Landrun without descendant containment. It never retries a workload +command. + +The error includes the failing command's diagnostic and relevant sysctl suggestions. For example, +current disposable Ubuntu CI runners may require: + +```sh +sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0 +``` + +Depending on the reported setting, a dedicated runner may instead require +`sudo sysctl -w user.max_user_namespaces=15000` or +`sudo sysctl -w kernel.unprivileged_userns_clone=1`. These settings affect the host: do not apply +them blindly on a shared machine. Ask its administrator or use a compatible runner. A container +which forbids mounting a private `/proc` cannot provide strict descendant containment. + +The default is `false`, preserving compatibility with an explicit warning when containment is +unavailable. ## Definition Holes Sometimes challenges want to leave open definitions for solutions to fill in. This can range from @@ -197,19 +223,21 @@ We generally adopt a policy of not loading olean files as they just get mmaped i space and then dereferenced and are as such a potential point of attack for sophisticated adversaries. The comparator performs the following steps to ensure these properties: -1. Build `Challenge` using `lake` in a `landrun` sandbox that has: +1. Preflight user, PID, and mount namespaces. When available, supervise every sandboxed command in a + fresh PID namespace so its remaining descendants are killed before Comparator continues. +2. Build `Challenge` using `lake` in a `landrun` sandbox that has: - read access to the entire file system and write access to `/dev` - write access to the `.lake` directory of the project -2. Run `lean4export` on the produced `Challenge.olean` in a `landrun` sandbox that has: +3. Run `lean4export` on the produced `Challenge.olean` in a `landrun` sandbox that has: - read access to the entire file system and write access to `/dev` -3. Repeat the same build sandboxed and export sandboxed steps with `Solution` -4. Verify that all declarations used in the statement of all relevant theorems in `Challenge` +4. Repeat the same build sandboxed and export sandboxed steps with `Solution` +5. Verify that all declarations used in the statement of all relevant theorems in `Challenge` are the same as in the `Solution` environment. This always includes the declarations from `Init` with special meaning to the kernel. Both `Challenge` and `Solution` therefore need to import the default prelude. -5. Verify that the body of all relevant theorems in the `Solution` environment only uses axioms +6. Verify that the body of all relevant theorems in the `Solution` environment only uses axioms listed in `permitted_axioms` -6. Replay the `Solution` environment into the Lean kernel. Doing this within the same process as the +7. Replay the `Solution` environment into the Lean kernel. Doing this within the same process as the comparator should be safe as the worst thing that can happen at this point is an exploit that makes the kernel accept when it should reject and that same exploit should also be applicable from within an external process. From 14b5039e0b6a5171afa160920984e521817d4138 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 20 Aug 2026 12:55:28 +0000 Subject: [PATCH 2/2] test: cover namespace setup and descendant cleanup --- .github/workflows/lean_action_ci.yml | 23 +++++++++++++ runtests.lean | 26 ++++++++++++++- tests/Namespace.lean | 33 +++++++++++++++++++ .../descendant_cleanup/Challenge.lean | 2 ++ .../projects/descendant_cleanup/Solution.lean | 27 +++++++++++++++ tests/projects/descendant_cleanup/config.json | 7 ++++ tests/projects/descendant_cleanup/test.json | 8 +++++ 7 files changed, 125 insertions(+), 1 deletion(-) create mode 100644 tests/Namespace.lean create mode 100644 tests/projects/descendant_cleanup/Challenge.lean create mode 100644 tests/projects/descendant_cleanup/Solution.lean create mode 100644 tests/projects/descendant_cleanup/config.json create mode 100644 tests/projects/descendant_cleanup/test.json diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index b863382..b4721b5 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -49,6 +49,29 @@ jobs: working-directory: lean4export run: lake build + - name: Test informative strict-mode failure + working-directory: comparator + run: | + if COMPARATOR_UNSHARE=/bin/false .lake/build/bin/comparator tests/projects/fail_closed_match/config.json >namespace-error.log 2>&1; then + echo "Strict namespace preflight unexpectedly succeeded." + exit 1 + fi + grep -F "util-linux" namespace-error.log + grep -F "no workload command was started" namespace-error.log + + - name: Enable unprivileged user namespaces + run: | + if [[ -e /proc/sys/user/max_user_namespaces ]] && + [[ "$(sysctl -n user.max_user_namespaces)" == 0 ]]; then + sudo sysctl -w user.max_user_namespaces=15000 + fi + if [[ -e /proc/sys/kernel/unprivileged_userns_clone ]]; then + sudo sysctl -w kernel.unprivileged_userns_clone=1 + fi + if [[ -e /proc/sys/kernel/apparmor_restrict_unprivileged_userns ]]; then + sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0 + fi + - name: Run comparator tests working-directory: comparator run: | diff --git a/runtests.lean b/runtests.lean index e918cb4..265c548 100644 --- a/runtests.lean +++ b/runtests.lean @@ -25,6 +25,10 @@ open Lean System.FilePath IO.FS IO.Process System structure TestConfig where exit_code : Nat + required_path : Option String := none + release_path : Option String := none + forbidden_path : Option String := none + settle_ms : Option Nat := none linux_only : Option Bool := none deriving FromJson, ToJson @@ -107,6 +111,19 @@ def runTestProject (projectPath : FilePath) (projectName : String) (_testsDir : let exitCode ← runCommandInDir tempDir "lake" #["env", comparatorPath.toString, "config.json"] + if let some requiredPath := config.required_path then + if !(← (tempDir / requiredPath).pathExists) then + IO.FS.removeDirAll tempDir + return TestResult.error projectName s!"required path was not created: {requiredPath}" + if let some releasePath := config.release_path then + IO.FS.writeFile (tempDir / releasePath) "" + if let some settleMs := config.settle_ms then + IO.sleep settleMs.toUInt32 + if let some forbiddenPath := config.forbidden_path then + if ← (tempDir / forbiddenPath).pathExists then + IO.FS.removeDirAll tempDir + return TestResult.error projectName s!"forbidden path was created: {forbiddenPath}" + IO.FS.removeDirAll tempDir if exitCode == config.exit_code then @@ -151,6 +168,13 @@ def runLandlockTests (comparatorPath : FilePath) : IO TestResult := do return .success "landlock_hardening" return .failure "landlock_hardening" 0 exitCode +def runNamespaceTests (comparatorPath : FilePath) : IO TestResult := do + let exitCode ← runCommandInDir "." "lake" + #["env", "lean", "--run", "tests/Namespace.lean", comparatorPath.toString] + if exitCode == 0 then + return .success "namespace_hardening" + return .failure "namespace_hardening" 0 exitCode + /-- Run comparator integration tests. When `args` is non-empty, only tests whose project name contains one of the given strings (as a substring) are executed. -/ def main (args : List String) : IO UInt32 := do @@ -175,7 +199,7 @@ def main (args : List String) : IO UInt32 := do let comparatorPath ← IO.FS.realPath <| ".lake" / "build" / "bin" / "comparator" - let mut results := #[← runLandlockTests comparatorPath] + let mut results := #[← runLandlockTests comparatorPath, ← runNamespaceTests comparatorPath] let mut allPassed := results.all fun | .success _ => true | _ => false diff --git a/tests/Namespace.lean b/tests/Namespace.lean new file mode 100644 index 0000000..e08eb56 --- /dev/null +++ b/tests/Namespace.lean @@ -0,0 +1,33 @@ +import Comparator.Namespace + +open System + +def wrapperIsExact : Bool := + Comparator.Namespace.wrap + { setpriv := "setpriv-test", unshare := "unshare-test" } + "landrun-test" #["landrun-arg"] == + ("setpriv-test", #[ + "--pdeathsig", "SIGKILL", "unshare-test", + "--user", "--map-current-user", + "--pid", "--fork", "--kill-child=SIGKILL", + "--mount-proc", "--", "landrun-test", "landrun-arg" + ]) + +def main (args : List String) : IO UInt32 := do + unless wrapperIsExact do + throw <| .userError "the namespace supervisor invocation changed unexpectedly" + let some (comparatorPath : String) := args[0]? + | throw <| .userError "expected the Comparator executable path" + let cwd ← IO.Process.getCurrentDir + let unavailableTools : Comparator.Namespace.Tools := { setpriv := "false", unshare := "false" } + if ← Comparator.Namespace.select false unavailableTools comparatorPath cwd then + throw <| .userError "non-strict namespace selection did not fall back" + let strictRejected ← + try + discard <| Comparator.Namespace.select true unavailableTools comparatorPath cwd + pure false + catch e => + pure <| e.toString.contains "no workload command was started" + unless strictRejected do + throw <| .userError "strict namespace selection did not fail informatively" + return 0 diff --git a/tests/projects/descendant_cleanup/Challenge.lean b/tests/projects/descendant_cleanup/Challenge.lean new file mode 100644 index 0000000..bab3e97 --- /dev/null +++ b/tests/projects/descendant_cleanup/Challenge.lean @@ -0,0 +1,2 @@ +theorem cleanupTest : True := by + trivial diff --git a/tests/projects/descendant_cleanup/Solution.lean b/tests/projects/descendant_cleanup/Solution.lean new file mode 100644 index 0000000..1aa46a0 --- /dev/null +++ b/tests/projects/descendant_cleanup/Solution.lean @@ -0,0 +1,27 @@ +import Lean + +private def waitForStart (path : System.FilePath) : Nat → IO Unit + | 0 => throw <| .userError "descendant did not start within 30 seconds" + | remaining + 1 => do + if ← path.pathExists then + return + IO.sleep 10 + waitForStart path remaining + +theorem cleanupTest : True := by + run_tac + let childSource := + "def waitForRelease : Nat → IO Unit\n | 0 => pure ()\n | remaining + 1 => do\n if ← System.FilePath.pathExists \".lake/release-descendant\" then\n IO.FS.writeFile \".lake/descendant-survived\" \"\"\n else\n IO.sleep 10\n waitForRelease remaining\n\ndef main : IO Unit := do\n IO.FS.writeFile \".lake/descendant-started\" \"\"\n waitForRelease 6000\n" + let childPath : System.FilePath := ".lake" / "detached_child.lean" + let startedPath : System.FilePath := ".lake" / "descendant-started" + IO.FS.writeFile childPath childSource + discard <| IO.Process.spawn { + cmd := "lean" + args := #["--run", childPath.toString] + stdin := .null + stdout := .null + stderr := .null + setsid := true + } + waitForStart startedPath 3000 + trivial diff --git a/tests/projects/descendant_cleanup/config.json b/tests/projects/descendant_cleanup/config.json new file mode 100644 index 0000000..345884a --- /dev/null +++ b/tests/projects/descendant_cleanup/config.json @@ -0,0 +1,7 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["cleanupTest"], + "permitted_axioms": [], + "fail_closed": true +} diff --git a/tests/projects/descendant_cleanup/test.json b/tests/projects/descendant_cleanup/test.json new file mode 100644 index 0000000..daed364 --- /dev/null +++ b/tests/projects/descendant_cleanup/test.json @@ -0,0 +1,8 @@ +{ + "exit_code": 0, + "required_path": ".lake/descendant-started", + "release_path": ".lake/release-descendant", + "forbidden_path": ".lake/descendant-survived", + "settle_ms": 500, + "linux_only": true +}