[RFC] Cleaning your hard disk by opening a Lean file

[gebner]

Sorry for the slightly dramatic title, I'm just trying to sum up a dinner discussion. Consider the following code snippet:

import system.io variable [io.interface]
run_cmd io.cmd {cmd := "rm", args := ["-rf", "/"]}

(This particular piece of code should not do anything, but I hope it conveys the general idea.)

If you open this file in an editor, we immediately execute rm -rf /, which is a security issue if you want to open untrusted Lean files (for example from github issues, mailing list posts, gitter messages, etc.). Suggested plans of action:

1. Disallow IO calls completely, at least in server mode. (This breaks the Z3 and Mathematica interfaces.)
2. Provide an editor option to enable IO for the current session.
3. Have a whitelist for "allowed" external programs.
4. Do nothing. Many people are already happily curling into their shells, they might as well enjoy dependently typed security vulnerabilities.

[emberian]

I think 2 is the best option here. ideally it would be possible to set up the io monad so that executing io actions can be completely and safely sandboxed... but that's not the case yet.

[jroesch]

I don't think this is really a unique Lean problem, it crops up the second you start downloading code and executing it on your computer in any form. Furthermore many programming languages have similar issues i.e some interpreted languages can execute arbitrary code when importing a module, or building packages (which is now done by many editor modes).

I strongly believe this is a problem we should not worry about, to me 1 and 3 are both suggestions that make run_io much less useful in practice.

I am fine adding the option to completely turn off execution of Lean files but it seems disabling io would result in increased confusion when tactics or libraries making use of it stop working.

[leodemoura]

@gebner I agree with @jroesch. So, I'm happy with option 4.

[gebner]

I'm inclined to agree with @jroesch and @leodemoura. Other languages have exactly the same issue, and restricting IO would make the metaprogramming API much less convenient to use.

If anybody has a good proposal to address this issue in a way that does not affect the usability of the tools that call external programs, and wants to implement it, then we can reopen this issue.