The Coq mailing list

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

Hi Théo,

Théo Zimmermann 
<theo.zimmi AT gmail.com>
 writes:

> Finally, Emilio, I don't understand what the issue would be with
> providing a `-safe` mode that doesn't allow writing to files? Why do
> you say a complete redesign and rewrite would be necessary? I seem to
> have always heard people be optimistic on this matter (with projects
> such as MetaCoq in particular). Your claim seems a bit at odds with
> this.

Maybe we don't agree on what I consider "adversarial"; indeed, to talk
about "security" of Coq's type checking first we should establish what
power does the adversary have.

It is my impression that most security problems as of today are
partially to blame on people doing too optimistic assumptions about the
adversary.

Can we for example guarantee that a .vo file is not going to be able to
exploit a bug in the OCaml's GC / runtime as to have coqchk accept a
file with a wrong proof?

I'd advocate erring on the safe side here; my opinion is that Coq should
not be used under general adversarial assumptions.

E.