The Coq mailing list

["Perry E. Metzger" <perry AT piermont.com>]

On Tue, 30 Jul 2013 12:47:22 -0700 t x 
<txrev319 AT gmail.com>
 wrote:
> Hi,
> 
>   I'm working on a Coq GUI in Javascript, where the Gallina / Ltac
> code being executed is untrusted (and possibly malicious).
> 
>   I'm interfacing with Coq via "coqtop.opt -ideslave", where only
> CpdtTactics + standard Coq libraries are provided.
> 
>   Besides denial of service attacks via infinite looping; are there
> any security issues I should be aware of? [For example, reading /
> writing files to the host OS; somehow embedding ocaml code; etc ...
> ]

Depending on the operating system you are running under, you can also
cage the running process in a variety of ways, which is to say,
prevent it from being able to spawn additional processes, open files,
etc. This can help ensure that even if there are bugs in the
underlying OCaml implementation that it is still impossible for an
attacker to break out into the host operating system.

Methods for doing so are sadly quite system dependent at the moment,
and under Linux, one has ones choice of far too many...

Perry
-- 
Perry E. Metzger                
perry AT piermont.com