The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

On Sat, Feb 1, 2020 at 2:54 PM Tej Chajed <tchajed AT mit.edu> wrote:

I think you should assume that it's unsafe unless you run it in a carefully-designed sandbox. At the very least one can easily write files which take huge amounts of time, memory, or disk space while compiling.

That assumption is why I asked the Q :) As for resource usage, I can set ulimits. That's the easy part. But it's harder for me to anticipate the consequences of arbitrary OCaml. I could selinux everything but that's also a ton of hassle in practice. No, I think the right way to go is for the type checking to be a pure operation :), modulo disk reads for .v and disk writes for compiled output.

 

For some idea of some of the issues, see this thread on a similar question for compiling C: https://security.stackexchange.com/questions/138881/is-it-dangerous-to-compile-arbitrary-c. In particular see Matt G's answer, since he runs a site that compiles arbitrary C. Essentially he runs the whole thing in a VM that doesn't have secrets, and then has extra mitigations to give nicer error messages when people try to exploit the compiler.

I respect Matt G's approach but I lack his confidence. A VM with no secrets is a beautiful ideal but in practice this is a giant hassle to actually implement and maintain. For instance, a VM with no secrets has no IAM role. It has no GitHub keys. It also has no route to the Internet, lest it be used as a staging box for other hacks.

Don't get me wrong - there are ways to approach this ideal. But they require as much engineering as the collaborative system I'd like to toss together:

Sorry if I sound obstinate on this point; my professional work is in computer security and when my clients go the sandbox route we put a *lot* of work into making sure it's done right - more than I can do by myself for this project.

-t