The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I believe compiling coq with js_of_ocaml may run into trouble with tail calls. _javascript_ doesn't eliminate tail calls, so js_of_ocaml tries to figure out some patterns and manually optimise them. It doesn't always work well, and Coq is big and full of tricks. I wouldn't be surprise to observe a lot of stack overflows in _javascript_. (though it's definitely something that should be tried).

For the client/server approach, you should definitely sandbox your server, you never know. You have to be careful of the command Drop, in bytecode mode, which opens a ocaml toplevel (can run arbitrary code). I'm not sure you can send it in -ideslave mode, though. You should also probably forbid the Declare ML Module command, and command about loadpath like Add Rec LoadPath. I don't see anything else, but you may want to browse the command index of the reference manual for something suspicious.

Another thing to bear in mind is proofweb ( http://prover.cs.ru.nl/login.php ) which does something like you're trying to do. You might want to drop the authors a mail for them to share the challenges they faced with you.

On 31 July 2013 08:45, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

Well, as I said "not sure if someone already tried it" meaning I don't know if it is practical (or even possible... maybe some missing features in the compiler would not allow it.. ?)

Anyway, people at OCamlPro already made a very cool thing with it: http://try.ocamlpro.com/

So this thread made me think that probably it is also possible to do so for Coq. Perhaps the people around OCamlPro can give more info on that...

2013/7/31 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.

--
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.