[prev in list] [next in list] [prev in thread] [next in thread] 

List:       full-disclosure
Subject:    Re: [Full-disclosure] OT: best practices in formal verification and
From:       Georgi Guninski <guninski () guninski ! com>
Date:       2011-05-30 14:09:14
Message-ID: 20110530140914.GH8415 () sivokote ! iziade ! m$
[Download RAW message or body]

coq developers appear to do forensics this way:
http://article.gmane.org/gmane.science.mathematics.logic.coq.club/6228


the academic approach (detached from current implementations imho) is:

How to Believe a Machine-Checked Proof, Robert Pollack
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.72.7610&rep=rep1&type=pdf


On Sat, May 14, 2011 at 08:21:13PM +0300, Georgi Guninski wrote:
> sorry for OT.
> 
> i am trying to convince a client a bit counterintuitive Coq proof about security is \
> valid. 
> i can make Coq generate .vo certificates that match the source (human forensic \
> would be happy with this part i suppose). 
> how do i mitigate human forensic analysis of the proof, what the human forensics \
> will look for? any introductory books? 
> what if the proof is big (about 3GB) and computer generated?
> 
> 10x.
> 
> _______________________________________________
> Full-Disclosure - We believe in it.
> Charter: http://lists.grok.org.uk/full-disclosure-charter.html
> Hosted and sponsored by Secunia - http://secunia.com/

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


[prev in list] [next in list] [prev in thread] [next in thread]