Untrusted descendants can outlive `safeLakeBuild`

runSandBoxed spawns landrun and waits for it, but nothing kills descendants that outlive it. A Submission.lean initialize block can leave a child running into safeExport, so the artifact comparator exports is not necessarily the artifact it built.

The argument against this has been the exec allowlist: safeLakeBuild --rox-whitelists only leanPrefix and gitLocation, so sh, setsid, bash and env cannot be exec'd, and a detached daemon is therefore impossible. That does not hold. lean is on the allowlist and is a general-purpose interpreter, and IO.Process.SpawnArgs has a native setsid : Bool field (Init/System/IO.lean, v4.32.2), so untrusted Lean can detach a lean child with no external binary involved. Children are reparented rather than killed when the landrun child exits.

Two smaller things in the same area: executablePaths := #[leanPrefix, gitLocation] grants exec across the whole Lean prefix, so lake, clang, ld.lld and leanc are all exec'able rather than just lean; and -ldd exec-allows the dynamic loader, which can load a readable ELF that is not itself exec-allowed.

I have no working exploit, so this is an unsound argument rather than a demonstrated attack. Containment looks cheaper than establishing that no exploit exists: run the sandboxed child in its own PID namespace and let PID 1 die, or in a delegated cgroup and cgroup.kill it, so safeLakeBuild cannot return while descendants are still alive.

lean-eval depends on the current argument explicitly, in its SECURITY.md, so we will correct that on our side either way.

Start with runSandBoxed and safeLakeBuild, then read the referenced Init/System/IO.lean SpawnArgs definition and SECURITY.md. Trace how the sandboxed process reaches safeExport, and evaluate the proposed PID-namespace or delegated-cgroup containment; done means descendants cannot remain running when safeLakeBuild returns and the executable allowlist does not broaden the issue.