The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  I guess we could ask for a "Coq inspector" utility that would implement 
only the printing and notation-handling commands of Coq, and would not load 
plug-ins.
Also coqchk should have an option to trace the assumptions under which the 
file is checked. Otherwise you could have a plugin that creates a hidden .vo 
file (say, under .svn) containing Axiom XXX_subproof : False (where XXX is 
some obscure Unicode letter), inserts a Require for it, then overrides the 
vernacular Print Assumptions command so that it does not display that axiom, 
and overrides some innocuous tactic (say, auto) so that it provides a 
trapdoor to the axiom. 
   Of course it would also be good if Print Assumptions did not display 
constants and theorems whose definition/proofs have been hidden by module 
signature ascription, since this makes it pretty hard to figure out if a 
development really depends on axioms...

Georges

-----Original Message-----
From: Bruno Barras 
[mailto:bruno.barras AT inria.fr]
 
Sent: 03 May 2011 19:57
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs 
can subvert "coqchk" and prove anything

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.