The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

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.

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.

On Sat, Feb 1, 2020 at 5:44 PM Andres Erbsen <andreser AT mit.edu> wrote:

Redirect and Extraction commands write to the disk by spec. I reported it a while back and was told that I shouldn't expect coqc on unknown code to be safe in any sense.