[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

[Perry E. Metzger]

On Thu, 17 Mar 2016 23:51:35 -0700 Ron Garret <ron at flownet.com> wrote:
> On Mar 16, 2016, at 7:00 PM, Perry E. Metzger <perry at piermont.com>
> wrote:
> 
> > Formal verification is not a panacea  
> 
> Indeed not.
> 
> http://spinroot.com/spin/Doc/rax.pdf
> 
> TL;DR: In the 1990s we formally verified the a portion of the
> flight software for an unmanned spacecraft.  Despite this, and
> despite extensive ground testing, the software nonetheless failed
> in flight.  (Happily, the failure was not catastrophic.)

The flaw was not in the formally verified portion of the flight
software, so this wasn't a flaw in formal verification, rather, it
was the lack of formal verification throughout the stack. The
formally verified portions were fine.

I will also point out that mere model checking isn't the state of the
art -- we can now do far better. CompCert, for example, is written
completely in Coq and then extracted into OCaml. One can (accurately)
claim that the fact that the OCaml implementation is not verified
creates a hole in the toolchain, but people are working to create
formally verified ML implementations.

Perry
-- 
Perry E. Metzger		perry at piermont.com