The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Hi Timothy,

Timothy Carstens 
<intoverflow AT gmail.com>
 writes:

> Suppose a super-intelligent malevolent AI hands me a collection of .v files
> and asks me to compile them.
>
> Is there *any* mechanism built into coqc which could be used by this evil
> oracle to hack my computer? Examples: ability to run shell commands,
> ability to write to disk, ability to detect whether or not a file at an
> arbitrary path exists or is readable, etc.
>
> I *assume* the answer is "no, coqc is safe to run on untrusted .v from
> Internet," but I've been burned by that before (other languages) so I
> thought I'd better ask.
>
> If the answer is "no," has that been the case for a nice long time, or is
> it only recently "no?" (Trying to gauge likelihood of bugs)

In my opinion the is answer is indeed a strong "no"; sadly, Coq wasn't
designed to be used with adversarial `.v` and `.vo` files. Thus, you
need to trust the good faith of the proof sources.

I would also assume that arbitrary code execution is possible from a
`.v` file, indeed you can likely inject code into files such as
`.bashrc`, etc...

Unfortunately I think that making a system such as Coq
adversarial-resistant would require a complete redesign and rewrite, so
this doesn't seem like something that will be attempted soon.

Then, you would have to worry about the OCaml compiler and runtime, tho
I'm not sure OCaml would be the language of choice for such a project.

> Sorry if this question is answered elsewhere; I searched but wasn't sure
> how to phrase the query

Maybe this question should be added to Coq's F.A.Q.

E.