fix: contain sandbox descendants with util-linux

.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: |

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

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

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.

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