lake seccomp

Stream: lean4

[Henrik Böving]

This issue was brought up in general https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algorithm.20for.20avoiding.20having.20my.20hard.20drive.20wiped, now what kevin is talking about is most likely a pretty common use case among people that teach with Lean. And for mathematicians it's probably a little bit much to ask them to setup some external sanboxing themselves even if we explain exactly how to do it. My alternative idea would be, that we introduce a flag that can be set in the lakefile which basically makes the build system use seccomp before loading any sort of user code, filtering as many system calls as possible without breaking it. Ideally we could thus lock in the process that is running user code to the point where everything it can do is maybe some printing to stdout or something.

Does this seem doable/reasonable? I'm not entirely familiar with how the LSP and compilation work internally so maybe it actually needs some calls with destructive power that we can simply not seccomp? But if its doable it would be as simple as switching a boolean in lakefile.lean.

[Mac]

At first gloss, I see a few problems with this:

1. seccomp is not cross-platform (i.e., it is Linux-specific), Lake is, so we would need something equivalent for Windows
2. I am not sure how you could feasibly restrict the abilities of the lean process so as to make it secure. In order to compile the file, the lean process needs to be able read, write, memory map, (and, I think, even execute) files so that it can import modules and output the build results. As such, it would be powerful enough to act maliciously as well (e.g., wipe whatever files the user running lake has access to).

[Henrik Böving]

Does Linux have something equivalent to OpenBSDs unveil that would restrict file related system calls to certain directories/files? That way these destructive system calls would not matter.

[Gabriel Ebner]

I'm not sure if you want to write a seccomp sandbox yourself, but it's fairly easy to wrap lake using bubblewrap (only allowing write access to the current directory, but you might also want to consider making .git read-only for obvious security reasons):

bwrap --proc /proc --dev /dev \
  --ro-bind /nix{,} \
  --ro-bind $HOME/.elan{,} \
  --bind $PWD{,} \
  --ro-bind /run/current-system{,} \
  --ro-bind /run/systemd{,} \
  --ro-bind /etc{,} \
  lake build