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

[Viktor Dukhovni]

> On Mar 18, 2016, at 2:51 AM, Ron Garret <ron at flownet.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.

I'm confused.  Are you claiming that formal methods failed here?
On the face of it, they were quite successful...

  Introduction:
  ... In 1999 the flight software flew on a space mission, and a
  deadlock occurred in a *sibling* subsystem to the one which was
  the focus of the first verification effort. ...

  Conclusion:

  This paper describes two major verification efforts carried out within
  the Automated Software Engineering Group at NASA Ames Research Center.
  The first effort consisted of analyzing part of the RA autonomous
  space craft software using the SPIN model checker. One of the errors
  found with SPIN, a missing critical section around a conditional wait
  statement, was in fact reintroduced in a *different* subsystem that was
  not verified in this first pre-flight effort. This error caused a real
  deadlock in the RA during flight in space. ...

The software that failed was not verified, and contained a bug isomorphic to
the one that the verifier found.  Had it been verified, the bug would have
been avoided.

-- 
	Viktor.