full-disclosure - OT: best practices in formal verification and security

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]

Message-ID: <20110514172113.GB1888@sivokote.iziade.m$>
Date: Sat, 14 May 2011 20:21:13 +0300
From: Georgi Guninski <guninski@...inski.com>
To: full-disclosure@...ts.grok.org.uk
Subject: OT: best practices in formal verification and
	security

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/