The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 05/03/2011 01:49 PM, 
guninski AT guninski.com
 wrote:
> hostile ocaml plugins (possibly disguised as FILE.v) can generate their own 
> .vo
> files (of trivial statements), thus subverting coqchk, and don't give a chance
> of coqc to even see the whole file via the plugin doing exit(2) after writing
> .vo. this scenario seems interesting when validating large archives.

Hello,

Well this is a nice little hack. And it's really a good thing that
some people like you try to challenge Coq and coqchk. But it's not
going to change the hacker reputation of eastern european folks ;-)

Your "attack" uses the fact that people tend to accept that when
successfully compiling a file producing an object file, and the latter
has been accepted by a checker, then the content of the source file is
correctly represented in the object file.

But the checker only validates object (.vo) files, not source (.v)
files, which would need to have a trusted compiler. The problem is
then: how can we access the content of .vo which is not human-readable
? The current answer is: run coqtop, Require fib5, and you can see its
content (and see that fib5.really has type True, not what's in
fib5.v). It's not a fully safe solution since requiring the .vo file
will also require the malicious plugin which could corrupt the
environment of coqtop. And even without malicious plugins, coqtop
could be buggy and display the content in an ambiguous manner.

There are better solutions, like having coqchk display the type
of all constants it verifies. But how should we print the
statements ?  using user notations, this could hide the actual
meaning; and without notations, the statement might then become so
obfuscated (not for Lisp experts though) that you cannot even guess
what it actually means.

You could also say that the content of the .v file should be closer to
that of the .vo file. Well, let me advocate against that. You don't
write a statement in the same way when talking to a believer or a
skeptical person:
- the believer (the code maintainer) want to avoid redundancies (like
  recalling the exact assumptions of a statement) and go directly to
  the point. That's the source code.
- the skeptical person (the code reviewer) also wants access to the
  full details at every step. That's the object file, provided we can
  reliability have access to its content.

Coq's sections are a good tool (when used properly) for the believer
but the skeptical will hate them because it hides the assumptions:

Section S.
  Variable F : False.
(* a lot of code here ... *)
  Lemma L : False.
(* the proof is easy... *)
End S.

You might miss that L depends on F... But you'll see it in the .vo file.

So, the bottom-line of the story is that gaining certainty is not a
matter of pushing a button and waiting for a green light. It's always
a matter of reducing the gap between what has been formally
established and what you think you have proved.

Bruno Barras.