The Coq mailing list

[Jay Kruer <kruerj AT reed.edu>]

Compiling a .v file can run arbitrary OCaml plugin code which can do anything the coqc process has permissions to do.

Unsure if anyone has exploited it, but this might also be interesting to you: https://github.com/coq/coq/issues/11170

On Feb 1, 2020, at 2:32 PM, Timothy Carstens <intoverflow AT gmail.com> wrote:

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)

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

-t