The Coq mailing list

[t x <txrev319 AT gmail.com>]

Perry: I like this solution, using kvm/docker.

Nuno: Do you know if coq on top of ocaml on top of js is actually practical?

On Tue, Jul 30, 2013 at 1:49 PM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

Have you consider running Coq at client side via the _javascript_ compiler [1]?

Not sure if someone already tried that --- I don't mean CoqIDE but just coqtop ---, but heh, it sure would be cool and no more concerns about possible DoS attacks or otherwise..

[1] http://ocsigen.org/js_of_ocaml/manual/

2013/7/30 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

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.