lockdown mode

Stream: lean4

[(deleted)]

I propose that we have a lockdown mode for Lean 4 and it should be the default. The lockdown mode prevents all side effects from being executed, like filesystem I/O, spawning child processes, accessing the internet, etc. With lockdown mode, Lean 4 becomes a proof assistant only, which is the primary use anyway. While currently mathlib is the only major library in the ecosystem, in the future there can be more mathematical libraries. Lockdown mode ensures that we can safely install additional mathematical libraries to suit our needs without having to risk running untrusted code, getting a virus or having our data exfiltrated.

This is just a proposal. Once there is enough support I can start working on it.

[Henrik Böving]

You can just run a lean process in https://github.com/Zouuup/landrun or any other sandbox that's out there and it's going to be in what you call "lockdown mode".

[Jovan Gerbscheid]

I think the problem is that most Lean users will not use such a sandbox, but they will possibly be running untrusted code. So I think it is a reasonable idea to have this safety net built in for "average" Lean users

[(deleted)]

I agree. This is my primary motivation for making this proposal. I myself run Lean in a sandbox already.

[(deleted)]

Additionally, having the infrastructure in place means that in the future we can make lockdown mode more fine grained. Initially we can start with a blanket lockdown. But in the future lockdown mode could be per package, and each package can explicitly declare the permissions it needs.

[Arthur Paulino]

Not that I oppose to the idea. I think it's reasonable.
But to compare with another language many here may like, Rust's custom build scripts can also cause arbitrary damage to one's system at compile time. At least the risk is more contained there and not spread across the code base.

[Henrik Böving]

Jovan Gerbscheid said:

I think the problem is that most Lean users will not use such a sandbox, but they will possibly be running untrusted code. So I think it is a reasonable idea to have this safety net built in for "average" Lean users

If it is the average Lean user that you are looking for, you quickly run into the issue that this average (likely mathematician) user will probably run Windows and Windows does not have the capabilities to perform privilege drop in the same fashion that Linux (and I guess MacOS? though I don't know) has. You can't just say that some subprocess may not execute a system call to open a network socket on Windows. You might of course reason that the runtime should attempt to enforce this type of stuff but there is nothing stopping an adversarial user from linking in their own C code into say a natively compiled tactic and once that tactic gets called making that piece of C code perform a network request or whatever other system call they want. So you definitely require an OS level mechanism (which again, to the best of my knowledge is not available on Windows) unless you want to somehow add very deep restraints into what lake can do etc. which is likely out of scope for the forseeable future.

[(deleted)]

I mean if Windows didn't have a mechanism for sandboxing Chromium and thus Chrome wouldn't exist... But this is something I'll research more.

[(deleted)]

Looks like there's this mechanism https://learn.microsoft.com/en-us/windows/win32/secauthz/restricted-tokens

[(deleted)]

I initially thought that we could limit the capabilities at the Lean level but now that it's clear an OS level mechanism is required heading in that direction is reasonable too. Let me see what I can do.

[(deleted)]

https://chromium.googlesource.com/chromium/src/+/main/docs/design/sandbox.md#Sandbox-Windows-architecture

[Patrick Massot]

Henrik Böving said:

If it is the average Lean user that you are looking for, you quickly run into the issue that this average (likely mathematician) user will probably run Windows

I think this estimate is extremely unfair to the average mathematician. I don’t know more than a handful of mathematicians using Windows. In my department I was never able to find one when I needed to test Lean installation instructions on Windows before giving them to students.

[(deleted)]

I've identified the lockdown route for both Linux and Windows. For Windows we can use restricted tokens. For Linux we can use namespaces. I don't have a Mac so I have no idea. If maintainers are fine with me using OS level sandboxing mechanisms then I can start working. This is to me the easiest path, compared to modifying how side effects are handled at the Lean level.

From the two links I sent, Windows has adequate sandboxing mechanisms, and we just need to use them.

[Markus Himmel]

Before you start working on this (or any other Lean feature), you should make an RFC to the lean4 repo and wait for feedback (the FRO usually reviews these once per week, but this month there are some availability constraints, so it looks like it will be July until the next time the FRO reviews RFCs).

I can tell you already though, completely independently of the merits of the feature itself, maintaining Lean for our four Tier 1 platforms has already been a struggle for the FRO at times even though there isn't that much platform-specific code in the runtime, so unless you have a very good story for the long-term maintenance of your feature, the RFC is going to have a hard time.

[(deleted)]

Thank you. I plan to pursue another option which requires more upfront work, imposes less maintenance burden and still provides strong isolation.