From 5846789249283e94ee0564dd86d02da6f440c1d4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 20 Aug 2026 12:48:18 +0000 Subject: [PATCH] feat: verify Landrun enforcement in fail-closed mode --- Comparator/Landlock.lean | 86 +++++++++++++++++++ Main.lean | 15 +++- README.md | 21 +++++ runtests.lean | 19 +++- tests/Landlock.lean | 18 ++++ .../projects/fail_closed_match/Challenge.lean | 2 + .../projects/fail_closed_match/Solution.lean | 2 + tests/projects/fail_closed_match/config.json | 7 ++ tests/projects/fail_closed_match/test.json | 4 + 9 files changed, 169 insertions(+), 5 deletions(-) create mode 100644 Comparator/Landlock.lean create mode 100644 tests/Landlock.lean create mode 100644 tests/projects/fail_closed_match/Challenge.lean create mode 100644 tests/projects/fail_closed_match/Solution.lean create mode 100644 tests/projects/fail_closed_match/config.json create mode 100644 tests/projects/fail_closed_match/test.json diff --git a/Comparator/Landlock.lean b/Comparator/Landlock.lean new file mode 100644 index 0000000..32abe24 --- /dev/null +++ b/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 diff --git a/Main.lean b/Main.lean index 95c18e1..fed985c 100644 --- a/Main.lean +++ b/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 diff --git a/README.md b/README.md index e1d67f6..2c04d5f 100644 --- a/README.md +++ b/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 diff --git a/runtests.lean b/runtests.lean index 0d722fc..e918cb4 100644 --- a/runtests.lean +++ b/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" diff --git a/tests/Landlock.lean b/tests/Landlock.lean new file mode 100644 index 0000000..92de7c3 --- /dev/null +++ b/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 diff --git a/tests/projects/fail_closed_match/Challenge.lean b/tests/projects/fail_closed_match/Challenge.lean new file mode 100644 index 0000000..b45c299 --- /dev/null +++ b/tests/projects/fail_closed_match/Challenge.lean @@ -0,0 +1,2 @@ +theorem comm (n m : Nat) : n + m = m + n := by + sorry diff --git a/tests/projects/fail_closed_match/Solution.lean b/tests/projects/fail_closed_match/Solution.lean new file mode 100644 index 0000000..bd29d73 --- /dev/null +++ b/tests/projects/fail_closed_match/Solution.lean @@ -0,0 +1,2 @@ +theorem comm (n m : Nat) : n + m = m + n := by + grind diff --git a/tests/projects/fail_closed_match/config.json b/tests/projects/fail_closed_match/config.json new file mode 100644 index 0000000..82cf6bd --- /dev/null +++ b/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 +} diff --git a/tests/projects/fail_closed_match/test.json b/tests/projects/fail_closed_match/test.json new file mode 100644 index 0000000..d7580c0 --- /dev/null +++ b/tests/projects/fail_closed_match/test.json @@ -0,0 +1,4 @@ +{ + "exit_code": 0, + "linux_only": true +}