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

[Ron Garret]

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.)

There’s no getting around the GIGO problem.

rg