full-disclosure - Re: 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-prev] [day] [month] [year] [list]

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

On Tue, May 03, 2011 at 04:27:29PM +0300, Georgi Guninski wrote:
> 10x.
> 
> what about this scenario, is it reallistic:
> 
> i claim i have a proof of X. the proof is thousands of files. 
> lambda.v is the plugin and coqc is invoked on only top.v ?
> 
>

if i read the fine manual, i would have saved myself the ocaml troubles

  Theorem really: True = False.
  Proof.
    external "/bin/sh" "ESCAPE_SEQ; write_vo_proof; nicely_kill_coq ;" True.
    (* this invokes /bin/sh. suited for formal software verification *)
  Qed.

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