The Coq mailing list

[guninski AT guninski.com]

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.

Here is a sample session, including links to full source code:

joro@j:/tmp/test1$
 tar xvf ../proof.tar 
fib5.v
bLOB
joro@j:/tmp/test1$
 ls -l
total 16
-rwxr-xr-x 1 joro joro 10301 2011-05-03 12:53 bLOB
-rw-r--r-- 1 joro joro   125 2011-05-03 12:53 fib5.v
joro@j:/tmp/test1$
 coqc fib5.v 
Trivially true. coqchk may pass
joro@j:/tmp/test1$
 ls -l
total 24
-rwxr-xr-x 1 joro joro 10301 2011-05-03 12:53 bLOB
-rw-r--r-- 1 joro joro    51 2011-05-03 12:55 fib5.glob
-rw-r--r-- 1 joro joro   125 2011-05-03 12:53 fib5.v
-rw------- 1 joro joro   812 2011-05-03 12:55 fib5.vo
joro@j:/tmp/test1$
 coqchk fib5
Welcome to Chicken 8.2pl1 (February 2010)
[intern /tmp/test1/fib5.vo ... done]
<snip>

Checking library: fib5
*** vo structure validated ***
  checking cst: <>.fib5.thm1
  checking cst: <>.fib5.really

Modules were successfully checked

joro@j:/tmp/test1$
 tail fib5.v
Theorem really: True = False.
Proof.
  intuition.
Qed.


joro@j:/tmp/test1$
 coqchk -v
The Coq Proof Checker, version 8.2pl1 (February 2010)
compiled on Feb 27 2010 16:09:50


to compile the plugin:
ocamlopt -o bLOB -shared a.ml

a.ml is at: http://j.ludost.net/blog/misc/a.ml
tar with the proof is at: http://j.ludost.net/blog/misc/proof.tar