The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I am a Coq user and also have familiarity configuring and using
sandboxes.  Coincidentally, I am about to set up a firejail sandbox
around Coq, and have previously been using virtual machines for this
purpose. If you'd like some help setting up a container for Coq, I'm
available to help.

-- Jonathan

On Sat, 1 Feb 2020 17:53:35 -0500
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.
> 
> 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.