| 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
| ||
|
Message-ID: <20110530140914.GH8415@sivokote.iziade.m$> Date: Mon, 30 May 2011 17:09:14 +0300 From: Georgi Guninski <guninski@...inski.com> To: full-disclosure@...ts.grok.org.uk Subject: Re: OT: best practices in formal verification and security 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/
Powered by blists - more mailing lists