full-disclosure - proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [thread-next>] [day] [month] [year] [list]

Date: Tue, 3 May 2011 13:34:16 +0300
From: Georgi Guninski <guninski@...inski.com>
To: full-disclosure@...ts.grok.org.uk
Subject: proving _anything_ in the Coq proof assistant (in
 addition to code execution). ``coqchk'' passes too

proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too

if some poor soul needs help with a coq [1] homework, this may help.

if some poor AV vendor need a proof his solution is bullet proof this may help too...

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

[1] http://coq.inria.fr/

_______________________________________________
Full-Disclosure - We believe in it.
Charter: http://lists.grok.org.uk/full-disclosure-charter.html
Hosted and sponsored by Secunia - http://secunia.com/