coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: t x <txrev319 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Security concerning executing untrusted Coq Code
- Date: Tue, 30 Jul 2013 12:47:22 -0700
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 ... ]
Thanks!
- [Coq-Club] Security concerning executing untrusted Coq Code, t x, 07/30/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, Perry E. Metzger, 07/30/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, Nuno Gaspar, 07/30/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, t x, 07/31/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, Nuno Gaspar, 07/31/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, Arnaud Spiwack, 07/31/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, Nuno Gaspar, 07/31/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, t x, 07/31/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, Nuno Gaspar, 07/30/2013
- Re: [Coq-Club] Security concerning executing untrusted Coq Code, Perry E. Metzger, 07/30/2013
Archive powered by MHonArc 2.6.18.