coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Security concerning executing untrusted Coq Code

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