[Cryptography] Two news items on OpenSSL and formal methods

[Perry E. Metzger]

I find it rather noteworthy that the most recent bug in OpenSSL was
found through the use of formal methods, specifically with the use
of Coq.

I also find it rather noteworthy that Andrew Appel just announced the
formal verification of OpenSSL's SHA-256 implementation, using a
Coq-based separation logic for C.

I've written on this list in the past about the fact that formal
methods are no longer a lab curiosity -- both of these events in the
last week seem like yet more evidence for this contention.

Formal methods can never produce perfection, since we may always make
mistakes in understanding what we wish to prove. However, for a very
wide variety of tasks, they can extirpate the overwhelming bulk of
the bugs we face. Also, unlike test infrastructure, when you
discover you have failed to realize you needed to prove a property,
you can be sure that you'll never face the same bug again, rather
than just being "sorta-kinda sure kinda".

Forwarded Message:

From: "Andrew W. Appel" <appel at cs.Princeton.EDU>
To: coq-club at inria.fr
Subject: [Coq-Club] Verification of OpenSSL SHA-256
Date: Thu, 05 Jun 2014 10:20:29 -0400

Coq-Club members may be interested in this recent result:

Verification of a Cryptographic Primitive: SHA-256
   by Andrew W. Appel
   May 9, 2014

ABSTRACT:
A full formal machine-checked verification of a C program: the
OpenSSL implementation of SHA-256. This is an interactive proof
of functional correctness in the Coq proof assistant, using the
Verifiable C program logic. Verifiable C is a separation logic for the
C language, proved sound w.r.t. the operational semantics for C,
connected to the CompCert verified optimizing C compiler.

www.cs.princeton.edu/~appel/papers/verif-sha.pdf

-- 
Perry E. Metzger		perry at piermont.com