feat: sandbox lake challenge with bwrap instead of landrun - #15005
Draft
Kha wants to merge 1 commit into
Draft
Conversation
This PR builds and exports the code `lake challenge` judges inside a `bubblewrap` sandbox rather than a `landrun` one, which stops that code from reading the invoking user's files and gives the steps that must not reach the network no network at all. `/` is bound read-only and the home directories are then covered, so the project still builds against the system it expects while `~/.ssh`, credentials and caches are simply absent; only `.lake` is writable; and only dependency resolution, which has to fetch git dependencies, gets a network namespace. `COMPARATOR_LANDRUN` becomes `COMPARATOR_BWRAP`. Landlock could not express either property. Its rules only ever grant, so nothing can be carved out of the `--ro /` the toolchain needs, and its network rules cover TCP alone, so a build could open a UDP socket and send what it had read; a namespace has neither gap. The cost is that `bwrap` cannot narrow a network to particular ports, so resolution gets all of one rather than TCP 443 and 22. A dependency reachable only with the user's own credentials is now out of reach, which is the point. `bwrap` runs either through unprivileged user namespaces or installed setuid root, and distributions that disable the former ship the latter. `--unshare-all` expands to `--unshare-user-try`, which skips the user namespace rather than failing when it cannot be created, and none of `--userns`, `--disable-userns` or the overlay options, the ones bubblewrap does not support setuid, are used. `readablePaths` becomes load-bearing, since a path the run needs has to be bound back over those covers: the toolchain, which an `elan` install puts under the home directory, along with the project, the exporter and any external kernel binary. External kernels are resolved through `PATH` before the sandbox starts for that reason. `tests/lake/tests/fake-bwrap.sh` replaces `fake-landrun.sh` and now honours `--clearenv` and `--setenv`, which `landrun`'s `--env` got for free from the parent environment. Co-Authored-By: Claude <noreply@anthropic.com>
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
leanprover-bot
added
the
breaks-manual
Collaborator
|
Reference manual CI status:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR builds and exports the code
lake challengejudges inside a further restrictedbubblewrapsandbox rather thanlandrun, which stops that code from being able to access the invoking user's files and gives the steps that must not reach the network no network at all./is bound read-only and the home directories are then covered, so the project still builds against the system it expects while~/.ssh, credentials and caches are simply absent; only.lakeis writable; and only dependency resolution, which has to fetch git dependencies, gets a network namespace.COMPARATOR_LANDRUNbecomesCOMPARATOR_BWRAP.Landlock could not express either property. Its rules only ever grant, so nothing can be carved out of the
--ro /the toolchain needs, and its network rules cover TCP alone, so a build could open a UDP socket and send what it had read; a namespace has neither gap. The cost is thatbwrapcannot narrow a network to particular ports, so resolution gets all of one rather than TCP 443 and 22. A dependency reachable only with the user's own credentials is now out of reach, which is the point.bwrapruns either through unprivileged user namespaces or installed setuid root, and distributions that disable the former usually ship the latter.--unshare-allexpands to--unshare-user-try, which skips the user namespace rather than failing when it cannot be created, and none of--userns,--disable-usernsor the overlay options, the ones bubblewrap does not support setuid, are used.readablePathsbecomes more critical, since a path the run needs has to be bound back over those covers: the toolchain, which anelaninstall puts under the home directory, along with the project, the exporter and any external kernel binary. External kernels are resolved throughPATHbefore the sandbox starts for that reason.tests/lake/tests/fake-bwrap.shreplacesfake-landrun.shand now honors--clearenvand--setenv, whichlandrun's--envgot for free from the parent environment.