The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

Sorry for my part in any confusion <3

Consider the following workflow:

1. User goes to website and downloads .tgz

2. User extracts .tgz, finds a bunch of .v files

3. README.md says "The safety guarantee is expressed in foo.v"

4. Independent expert in computer science reads foo.v, reads basic_definitions.v, and says "yep: the safety guarantee means what you think it means. if it typechecks, then you're good to go."

5. User runs coqc foo.v

My question was: is this safe for the user to do, or is it possible that coqc foo.v might hack their computer?

The interesting question is whether Coq intentionally has features that can facilitate this: things like the ability to run shell commands, write to files at arbitrary paths, explore the file system in any way, open sockets, run arbitrary ocaml, etc.

[ Ignore memory safety for a moment; I'll assume no one knows if coqc is memory safe for the same reasons no one knows if any program is memory safe (no formal methods - yet!) ]

If so, then (5) is inherently an unsafe thing to do, and in that case I don't see how Coq could be used to certify untrusted code. You'd need to first do a code review of the ltac and everything else to convince yourself that it was safe to compile. IMHO this should change in the future, simply on the appeal of the use case described above. One of Coq's best application domains is the verification of real world computing artifacts, after all.

Again, I don't want people to think I'm raising giant alarm bells here - Coq is undergoing a lot of changes right now as a platform, and I respect the autonomy of the Coq maintainers to decide what problems to tackle and in what order. In my opinion they have shown excellent judgement thus far and I do not seek to interfere in their plans.

On Sat, Feb 1, 2020 at 7:48 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

There's some confusion here, perhaps all mine, about the distinction
between Coq as a system for verifying code (which it can do) vs. Coq
and the environment it runs in as a verified system (which it isn't).
It seems to me that these questions have been mixing those two very
different concepts.

Coq, merely by virtue of it being a system for verifying code, does not
enhance trust of itself and the environment it is run in being safe
to use to check that some other code can be verified.  One level of
trust does not eliminate the need for trusting the other level.

If you run Coq in a way such that something malicious can substitute
'echo "Qed!"' for your Coq prover without you knowing it is
doing so, then there is nothing Coq nor its developers can do to save
you.  Yet I am sure this must be obvious to all, so it must be me that
is still confused about your questions.



On Sun, 2 Feb 2020 15:50:27 +1300
Marco Servetto <marco.servetto AT gmail.com> wrote:

> > Also: "put it in a container" doesn't address the other use case I
> > mentioned above: namely, telling people that they can use Coq to
> > certify the safety/correctness of untrusted code. 
>
> To make this more explicit:
> if there was an online service that gives you "proven correct and
> safe code1" and the corresponding coq proof code2; would running such
> proof be a valid certification that such code1 is
> correct and safe? or, is it possible that during the execution of
> code2 arbitrary behavior makes a "yes" result even if the proof in
> itself if bogus?
> Note how running coq in a container or not does not really change the
> issue here.