feat: verify Landrun enforcement in fail-closed mode

Comparator/Landlock.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+namespace Comparator.Landlock
+
+/-- The Landrun policy shared by Comparator workloads and the enforcement probe. -/
+def baseArgs : Array String :=
+  #["--best-effort", "--ro", "/", "--rw", "/dev", "-ldd", "-add-exec"]
+
+private def probeContents := "comparator-landlock-enforcement-probe"
+private def replacementContents := "landlock-did-not-deny-this-write"
+private def probeSuccess := "comparator-landlock-enforcement-ok"
+private def permissionDenied : UInt32 := 13
+
+/--
+Internal child mode for the end-to-end Landrun probe. The probe file is writable by the user but
+must be read-only under Comparator's Landrun policy.
+-/
+def runProbeChild (path : System.FilePath) : IO Unit := do
+  let contents ← IO.FS.readFile path
+  unless contents == probeContents do
+    throw <| .userError "The Landlock enforcement probe could not read its input file"
+
+  let writeWasDenied ←
+    try
+      IO.FS.writeFile path replacementContents
+      pure false
+    catch e =>
+      match e with
+      | .permissionDenied _ code _ =>
+        if code == permissionDenied then
+          pure true
+        else
+          throw e
+      | _ =>
+        throw e
+
+  unless writeWasDenied do
+    throw <| .userError "The Landlock enforcement probe unexpectedly wrote its read-only file"
+  unless (← IO.FS.readFile path) == probeContents do
+    throw <| .userError "The Landlock enforcement probe file was modified"
+  IO.println probeSuccess
+
+private def failureMessage (details : String) : String :=
+  let details := details.trimAscii.toString
+  let details := if details.isEmpty then "no diagnostic was produced" else details
+  s!"The installed Landrun did not enforce Comparator's read-only filesystem policy ({details}); \
+fail_closed is enabled, so no workload command was started"
+
+/--
+Run the installed Landrun around a child Comparator process and verify that Comparator's policy
+denies a write to a file which is writable outside the sandbox. This detects unavailable or disabled
+Landlock and an accidentally configured no-op Landrun shim before any workload command starts.
+-/
+def requireEnforcement (landrunPath : String) (comparatorPath cwd : System.FilePath) : IO Unit :=
+  try
+    IO.FS.withTempFile fun handle probePath => do
+      let probePathString := probePath.toString
+      if System.Platform.isLinux &&
+          (probePathString == "/dev" || probePathString.startsWith "/dev/") then
+        let message :=
+          s!"The Landlock enforcement probe cannot use {probePath} because Comparator's policy \
+makes /dev writable. Set TMPDIR to a directory outside /dev; fail_closed is enabled, so no \
+workload command was started"
+        throw <| .userError message
+      handle.putStr probeContents
+      handle.flush
+      let { stdout, stderr, exitCode } ← IO.Process.output {
+        cmd := landrunPath
+        args := baseArgs ++ #[
+          "--", comparatorPath.toString, "--landlock-enforcement-probe", probePath.toString
+        ]
+        cwd := cwd
+      }
+      let contents ← IO.FS.readFile probePath
+      unless exitCode == 0 && stdout.trimAscii.toString == probeSuccess &&
+          contents == probeContents do
+        throw <| .userError (failureMessage stderr)
+  catch e =>
+    if e.toString.contains "fail_closed is enabled" then
+      throw e
+    throw <| .userError (failureMessage e.toString)
+
+end Comparator.Landlock

Main.lean

@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 import Lean
 import Comparator
+import Comparator.Landlock
 import Export.Parse
 
 namespace Comparator
@@ -78,7 +79,7 @@ def queryLeanPrefix (projectDir : System.FilePath) : IO System.FilePath := do
   return out.trimAscii.toString
 
 def buildLandrunArgs (spawnArgs : LandrunArgs) : Array String :=
-  let args := #["--best-effort", "--ro", "/", "--rw", "/dev", "-ldd", "-add-exec"]
+  let args := Landlock.baseArgs
   let args := spawnArgs.envPass.foldl (init := args) (fun acc env => acc ++ #["--env", env])
   let args := spawnArgs.readablePaths.foldl (init := args) (fun acc path => acc ++ #["--ro", path.toString])
   let args := spawnArgs.writablePaths.foldl (init := args) (fun acc path => acc ++ #["--rwx", path.toString])
@@ -316,14 +317,19 @@ structure Config where
   permitted_axioms : Array String
   enable_nanoda? : Option Bool
   external_kernels? : Option (Std.TreeMap String (Array String))
+  /-- Verify that Landrun enforces Comparator's filesystem policy before starting any workload.
+  Defaults to `false`. -/
+  fail_closed? : Option Bool
   deriving Lean.FromJson, Lean.ToJson, Repr
 
 def M.run (x : M α) (cfg : Config) : IO α := do
   let cwd ← IO.Process.getCurrentDir
+  let whichLandrun := (← IO.getEnv "COMPARATOR_LANDRUN").getD "landrun"
+  if cfg.fail_closed?.getD false then
+    Landlock.requireEnforcement whichLandrun (← IO.appPath) cwd
   let leanPrefix ← queryLeanPrefix cwd
   let gitLocation ← queryGitLocation
   let whichLean4Export := (← IO.getEnv "COMPARATOR_LEAN4EXPORT").getD "lean4export"
-  let whichLandrun := (← IO.getEnv "COMPARATOR_LANDRUN").getD "landrun"
   let mut externalKernels := cfg.external_kernels?.getD {}
   let defaultNanoda := "nanoda_bin"
   let nanodaOverride? ← IO.getEnv "COMPARATOR_NANODA"
@@ -358,6 +364,11 @@ def M.run (x : M α) (cfg : Config) : IO α := do
 end Comparator
 
 def main (args : List String) : IO Unit := do
+  if args.head? == some "--landlock-enforcement-probe" then
+    let some (path : String) := args[1]?
+      | throw <| .userError "The Landlock enforcement probe expected a file path"
+    Comparator.Landlock.runProbeChild path
+    return
   let some (configPath : String) := args[0]?
     | throw <| .userError "Expected config file path as first argument."
   let content ← IO.FS.readFile configPath

README.md

@@ -85,6 +85,27 @@ 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
+
+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
+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:
+
+```
+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`.
+
 ## Definition Holes
 Sometimes challenges want to leave open definitions for solutions to fill in. This can range from
 simple things like filling in a `Prop` valued definition to resolve whether a conjecture is true or

runtests.lean

@@ -25,6 +25,7 @@ open Lean System.FilePath IO.FS IO.Process System
 
 structure TestConfig where
   exit_code : Nat
+  linux_only : Option Bool := none
   deriving FromJson, ToJson
 
 inductive TestResult
@@ -86,12 +87,15 @@ def readTestConfig (configPath : FilePath) : IO TestConfig := do
 def getTempDir : IO FilePath := do
   return "/tmp" / s!"lean_test_{← IO.rand 0 999999}"
 
-def runTestProject (projectPath : FilePath) (projectName : String) (testsDir : FilePath)
+def runTestProject (projectPath : FilePath) (projectName : String) (_testsDir : FilePath)
     (comparatorPath : FilePath) : IO TestResult := do
   try
     let configPath := projectPath / "test.json"
     let config ← readTestConfig configPath
 
+    if config.linux_only.getD false && !System.Platform.isLinux then
+      return TestResult.success projectName
+
     let tempDir ← getTempDir
     IO.FS.createDirAll tempDir
 
@@ -140,6 +144,13 @@ def printTestResult (result : TestResult) : IO Unit := do
   | .error name msg =>
     IO.println s!"✗ {name}: ERROR - {msg}"
 
+def runLandlockTests (comparatorPath : FilePath) : IO TestResult := do
+  let exitCode ← runCommandInDir "." "lake"
+    #["env", "lean", "--run", "tests/Landlock.lean", comparatorPath.toString]
+  if exitCode == 0 then
+    return .success "landlock_hardening"
+  return .failure "landlock_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
@@ -164,8 +175,10 @@ def main (args : List String) : IO UInt32 := do
 
   let comparatorPath ← IO.FS.realPath <| ".lake" / "build" / "bin" / "comparator"
 
-  let mut allPassed := true
-  let mut results := #[]
+  let mut results := #[← runLandlockTests comparatorPath]
+  let mut allPassed := results.all fun
+    | .success _ => true
+    | _ => false
   for projectPath in projects do
     let projectName := projectPath.fileName.get!
     IO.println s!"\n## Running test: {projectName}\n"

tests/Landlock.lean

@@ -0,0 +1,18 @@
+import Comparator.Landlock
+
+open System
+
+def main (args : List String) : IO UInt32 := do
+  let some (comparatorPath : String) := args[0]?
+    | throw <| .userError "expected the Comparator executable path"
+  let cwd ← IO.Process.getCurrentDir
+  let fakeLandrun ← IO.FS.realPath <| "scripts" / "fake-landrun.sh"
+  let rejected ←
+    try
+      Comparator.Landlock.requireEnforcement fakeLandrun.toString comparatorPath cwd
+      pure false
+    catch _ =>
+      pure true
+  unless rejected do
+    throw <| .userError "the insecure Landrun shim passed the enforcement probe"
+  return 0

tests/projects/fail_closed_match/Challenge.lean

@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  sorry

tests/projects/fail_closed_match/Solution.lean

@@ -0,0 +1,2 @@
+theorem comm (n m : Nat) : n + m = m + n := by
+  grind

tests/projects/fail_closed_match/config.json

@@ -0,0 +1,7 @@
+{
+  "challenge_module": "Challenge",
+  "solution_module": "Solution",
+  "theorem_names": ["comm"],
+  "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+  "fail_closed": true
+}

tests/projects/fail_closed_match/test.json

@@ -0,0 +1,4 @@
+{
+  "exit_code": 0,
+  "linux_only": true
+}