From 686ffeb3765c6bf5edfb3193ac5cb6a46d2ac345 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 23 Sep 2026 12:44:29 +1000 Subject: [PATCH] feat: add `lake-check-sandbox` to make the sandbox startable GitHub-hosted runners restrict the unprivileged user namespaces bubblewrap needs, so `lake-check` cannot run there until something grants them. Making that change means changing the runner, so `lean-action` does not do it uninvited: `lake-check-sandbox` takes "none" (the default), "apparmor", "sysctl" or "setuid", and the chosen setup is applied only when the sandbox is probed and found not to work. "apparmor" is the narrowest and the documented choice. Ubuntu's restriction denies unprivileged user namespaces to programs whose AppArmor profile does not grant `userns`, so a profile covering bubblewrap leaves the restriction in force for everything else, where "sysctl" relaxes it for every program on the runner and "setuid" leaves a setuid binary behind. The privileged operations act only on a root-owned distribution bubblewrap at /usr/bin/bwrap or /bin/bwrap, never on a symlink and never on one named by COMPARATOR_BWRAP: otherwise PATH or that variable would decide which file gets made setuid root or gains a policy. `chmod u+s` on a file owned by the job user grants that user's privileges rather than root's, so refusing a non-root owner also avoids a change that would look like it had worked. None of these are restored afterwards, which the warnings and the documentation say plainly, because on a persistent self-hosted runner they outlive the job. The probe now exercises the namespace and mount operations Lake itself uses rather than a bare bind, since a runner can permit `--ro-bind` and still refuse the sandbox Lake actually builds. --- .../functional_tests/lake_check/action.yml | 6 ++ .github/workflows/functional_tests.yml | 10 ++ CHANGELOG.md | 1 + README.md | 20 +++- action.yml | 21 +++++ scripts/run_lake_check.sh | 94 ++++++++++++++++++- 6 files changed, 147 insertions(+), 5 deletions(-) diff --git a/.github/functional_tests/lake_check/action.yml b/.github/functional_tests/lake_check/action.yml index 94db6e0..91b2778 100644 --- a/.github/functional_tests/lake_check/action.yml +++ b/.github/functional_tests/lake_check/action.yml @@ -4,6 +4,10 @@ inputs: toolchain: description: 'Toolchain to use for the test' required: true + sandbox: + description: 'Value for the `lake-check-sandbox` input. GitHub-hosted runners need one; a privileged Namespace container needs none.' + required: false + default: 'none' runs: using: 'composite' steps: @@ -27,6 +31,7 @@ runs: with: use-github-cache: false lake-check: paranoid + lake-check-sandbox: ${{ inputs.sandbox }} - name: verify lake check success on the clean package env: @@ -50,6 +55,7 @@ runs: with: use-github-cache: false lake-check: paranoid + lake-check-sandbox: ${{ inputs.sandbox }} - name: verify lake check failure once a sorry is introduced env: diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml index dd05f10..0923bbe 100644 --- a/.github/workflows/functional_tests.yml +++ b/.github/workflows/functional_tests.yml @@ -264,6 +264,16 @@ jobs: with: toolchain: ${{ env.lake_check_toolchain }} + lake-check: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + - uses: ./.github/functional_tests/lake_check + with: + toolchain: ${{ env.lake_check_toolchain }} + # GitHub-hosted runners restrict the user namespaces bubblewrap needs. + sandbox: apparmor + # Pinned to a toolchain that predates `lake check`, rather than to the moving default: once the # default supports it, this would otherwise quietly stop testing feature detection. lake-check-unsupported-toolchain: diff --git a/CHANGELOG.md b/CHANGELOG.md index ca4b57a..623003e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - new `lake-check` input to check the project with `lake check`: build it and replay the result through one or more kernels inside a sandbox, erroring on any use of a non-standard axiom. `"true"` uses Lean's own kernel; `"paranoid"` additionally runs every external checker the toolchain bundles (`leanchecker-paranoid`, `lean4lean`, `nanoda`, `con-leche` and `con-ron`), none of which has to be built. Requires a Linux runner, Lean `v4.35.0-rc1` or newer (`"paranoid"` needs `v4.35.0-rc2`), and a runner permitting the user namespaces bubblewrap needs; see the README. Default: false - new `lake-check-status` output parameter +- new `lake-check-sandbox` input (`"none"` | `"apparmor"` | `"sysctl"` | `"setuid"`, default `"none"`) choosing how to make bubblewrap's sandbox able to start on a runner that restricts unprivileged user namespaces, as GitHub-hosted runners do. `"apparmor"` is narrowest: it grants the capability through an AppArmor profile and leaves the restriction in force for everything else. `lean-action` never changes a runner's configuration unless asked, and only when the sandbox is found not to work ## v1.6.0 - 2026-08-22 diff --git a/README.md b/README.md index 7fed88b..4771d86 100644 --- a/README.md +++ b/README.md @@ -420,17 +420,29 @@ adversarial input. bubblewrap needs unprivileged user namespaces, and not every runner permits them. -**GitHub-hosted runners** restrict them, so `lake-check` fails there until you grant them. The -narrowest way is an AppArmor profile covering `bwrap` alone; the blunt way is to lift the -restriction for the whole runner: +**GitHub-hosted runners** restrict them, so `lake-check` fails there until you grant them. Set +`lake-check-sandbox` to have `lean-action` do it: ```yaml -- run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0 - uses: leanprover/lean-action@v1 with: lake-check: "paranoid" + lake-check-sandbox: "apparmor" ``` +| value | effect | +| --- | --- | +| `"none"` (default) | Change nothing. `lake-check` fails if the sandbox cannot start. | +| `"apparmor"` | Install an AppArmor profile granting bubblewrap, and the processes it starts, permission to create user namespaces. The restriction stays in force for everything else, so this is the narrowest option and the usual choice. | +| `"sysctl"` | Relax `kernel.apparmor_restrict_unprivileged_userns`. Affects every program on the runner. | +| `"setuid"` | Install `bwrap` setuid root. | + +All three need passwordless sudo and are applied only when the sandbox is found not to work, so a +runner that already permits user namespaces is left untouched. None of them is undone afterwards: +on a persistent self-hosted runner they outlive the job, so prefer configuring such runners once +yourself and leaving this at `"none"`. `"apparmor"` and `"setuid"` refuse to act on anything but a +root-owned distribution bubblewrap, and never on one named by `COMPARATOR_BWRAP`. + **Namespace runners** fail differently: jobs run in a container whose seccomp profile denies `pivot_root`, for root as well as for the job user, so relaxing user namespaces does not help. Request a privileged container instead, where the `-with-features` suffix on the machine label is diff --git a/action.yml b/action.yml index ddea890..2d45b2f 100644 --- a/action.yml +++ b/action.yml @@ -131,6 +131,26 @@ inputs: Allowed values: "true" | "false" | "paranoid". required: false default: "false" + lake-check-sandbox: + description: | + How to make `lake check`'s bubblewrap sandbox able to start, when it cannot. + GitHub-hosted runners restrict the unprivileged user namespaces bubblewrap needs, so + `lake-check` fails there without one of these. A runner that already permits them, such as + a privileged Namespace container, needs nothing. + "none" changes nothing, and `lake-check` fails with an error naming this input. + "apparmor" installs an AppArmor profile granting bubblewrap, and the processes it starts, + permission to create user namespaces, leaving the runner's restriction in force for + everything else. The narrowest option, and the usual choice on GitHub-hosted runners. + "sysctl" relaxes `kernel.apparmor_restrict_unprivileged_userns`, which affects every + program on the runner. + "setuid" installs `bwrap` setuid root. + All three need passwordless sudo, are applied only when the sandbox is found not to work, + and are not restored afterwards: on a persistent self-hosted runner they outlive the job. + "apparmor" and "setuid" are applied only to a root-owned distribution bubblewrap, never to + one named by COMPARATOR_BWRAP. + Allowed values: "none" | "apparmor" | "sysctl" | "setuid". + required: false + default: "none" nanoda: description: | Check environment with nanoda external type checker. @@ -378,6 +398,7 @@ runs: if: ${{ inputs.lake-check != 'false' }} env: LAKE_CHECK_INPUT: ${{ inputs.lake-check }} + LAKE_CHECK_SANDBOX_INPUT: ${{ inputs.lake-check-sandbox }} run: | : Check the project with lake check ${GITHUB_ACTION_PATH}/scripts/run_lake_check.sh diff --git a/scripts/run_lake_check.sh b/scripts/run_lake_check.sh index 07a76e7..02477a8 100755 --- a/scripts/run_lake_check.sh +++ b/scripts/run_lake_check.sh @@ -35,6 +35,15 @@ case "$mode" in ;; esac +sandbox_setup="${LAKE_CHECK_SANDBOX_INPUT:-none}" +case "$sandbox_setup" in + none | apparmor | sysctl | setuid) ;; + *) + failure_message="\`lake-check-sandbox\` must be \"none\", \"apparmor\", \"sysctl\" or \"setuid\", got \"${sandbox_setup}\"" + exit 1 + ;; +esac + # `lake check` sandboxes the code it checks with bubblewrap, which needs Linux namespaces; Lake # refuses to run anywhere else, so say so here rather than letting it fail further in. runner_os="$(uname -s)" @@ -94,11 +103,94 @@ fi # reported as a setup problem naming the remedy, not as a failed check: `lake check` exits 1 both # when it rejects a project and when bubblewrap fails to start, so by the time it has run the two # are hard to tell apart. +# +# Exercise the namespace and mount operations Lake itself uses, not just a bind: a runner can +# permit `--ro-bind` and still refuse the sandbox Lake actually builds. sandbox_probe_output="" sandbox_works() { - sandbox_probe_output="$("$sandbox_exe" --ro-bind / / true 2>&1)" + sandbox_probe_output="$("$sandbox_exe" --unshare-all --ro-bind / / --proc /proc --dev /dev true 2>&1)" +} + +# Privileged setup is only ever applied to a distribution bubblewrap at a root-owned path. The +# executable to modify would otherwise be decided by PATH or by COMPARATOR_BWRAP, and neither +# establishes that the target is bubblewrap or that modifying it is safe. +assert_trusted_sandbox_exe() { + if [ -n "${COMPARATOR_BWRAP:-}" ]; then + failure_message="\`lake-check-sandbox: ${sandbox_setup}\` will not modify the executable named by COMPARATOR_BWRAP. Provision that sandbox yourself, or unset COMPARATOR_BWRAP to use the distribution's bubblewrap." + exit 2 + fi + if [ -L "$sandbox_exe" ]; then + failure_message="\`lake-check-sandbox: ${sandbox_setup}\` will not modify ${sandbox_exe}, which is a symbolic link; the target it resolves to today need not be the one modified." + exit 2 + fi + case "$sandbox_exe" in + /usr/bin/bwrap | /bin/bwrap) ;; + *) + failure_message="\`lake-check-sandbox: ${sandbox_setup}\` only modifies a distribution bubblewrap at /usr/bin/bwrap or /bin/bwrap, and this runner's is at ${sandbox_exe}. Grant it user namespaces yourself instead." + exit 2 + ;; + esac + if [ "$(stat -c '%U' "$sandbox_exe")" != "root" ]; then + # `chmod u+s` on a file owned by the job user grants that user's own privileges, not + # root's, so it would not make the sandbox work and would not mean what it appears to. + failure_message="\`lake-check-sandbox: ${sandbox_setup}\` will not modify ${sandbox_exe}, which is not owned by root." + exit 2 + fi } +if ! sandbox_works; then + case "$sandbox_setup" in + apparmor) + # Ubuntu's own mechanism: the restriction denies unprivileged user namespaces to + # programs whose AppArmor profile does not grant `userns`. Granting it here covers + # bubblewrap and the processes it starts, which inherit an unconfined profile; it does + # not cover the rest of the runner. + assert_trusted_sandbox_exe + if ! command -v apparmor_parser > /dev/null 2>&1; then + failure_message="\`lake-check-sandbox: apparmor\` needs \`apparmor_parser\`, which is not on this runner. Use \"sysctl\" or \"setuid\" instead." + exit 2 + fi + if [ -e /etc/apparmor.d/bwrap ]; then + failure_message="\`lake-check-sandbox: apparmor\` will not overwrite the existing AppArmor policy at /etc/apparmor.d/bwrap. Remove it, or grant bubblewrap user namespaces yourself." + exit 2 + fi + echo "::warning::\`lake-check-sandbox: apparmor\` is installing an AppArmor profile granting ${sandbox_exe}, and the processes it starts, permission to create user namespaces. The runner's restriction stays in force for everything else. On a persistent self-hosted runner the profile outlives this job." + if ! sudo tee /etc/apparmor.d/lean-action-bwrap > /dev/null <, +include + +profile lean-action-bwrap ${sandbox_exe} flags=(unconfined) { + userns, + include if exists +} +PROFILE + then + failure_message="\`lake-check-sandbox: apparmor\` could not write /etc/apparmor.d/lean-action-bwrap. This runner probably does not offer passwordless sudo." + exit 2 + fi + if ! sudo apparmor_parser -r /etc/apparmor.d/lean-action-bwrap; then + failure_message="\`lake-check-sandbox: apparmor\` could not load the AppArmor profile for ${sandbox_exe}. Use \"sysctl\" or \"setuid\" instead." + exit 2 + fi + ;; + sysctl) + echo "::warning::\`lake-check-sandbox: sysctl\` is relaxing kernel.apparmor_restrict_unprivileged_userns on this runner. This affects every program on the runner, not just bubblewrap, and nothing restores it: on a persistent self-hosted runner it stays relaxed for later jobs too. \`lake-check-sandbox: apparmor\` is narrower." + if ! sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0; then + failure_message="\`lake-check-sandbox: sysctl\` could not set \`kernel.apparmor_restrict_unprivileged_userns\`. This runner either does not have that knob, in which case its sandbox is blocked by something else, or does not offer passwordless sudo." + exit 2 + fi + ;; + setuid) + assert_trusted_sandbox_exe + echo "::warning::\`lake-check-sandbox: setuid\` is installing ${sandbox_exe} setuid root. The setuid bit persists on disk, so on a persistent self-hosted runner it outlives this job." + if ! sudo chmod u+s "$sandbox_exe"; then + failure_message="\`lake-check-sandbox: setuid\` could not make ${sandbox_exe} setuid root. This runner probably does not offer passwordless sudo." + exit 2 + fi + ;; + esac +fi + if ! sandbox_works; then # The remedy depends on which half of the sandbox was refused, so name the one that fits. # A denied uid map means user namespaces are blocked; a denied `pivot_root` means the job is