Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Security concerning executing untrusted Coq Code

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Security concerning executing untrusted Coq Code


Chronological Thread 
  • 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!



Archive powered by MHonArc 2.6.18.

Top of Page