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

[Ron Garret]

On Mar 18, 2016, at 12:55 AM, Viktor Dukhovni <cryptography at dukhovni.org> wrote:

> 
>> 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?

No, it was the application of formal methods that failed.  But it’s not just a random bit of stupidity, there was an interesting structure to this particular failure.  It was never practical to verify the entire software stack, there was just too much of it.  So we tried to structure the software with a secure, formally verified “core” that was supposed to maintain certain invariants (like no deadlocks).  The theory was that anything built on top of that core would maintain those invariants.  It was a riff on this theme from Perry’s original post:

> However, it is an astonishingly useful *ratchet*. If you verify a
> property, and you specified the property correctly, no new bugs will
> appear of that particular flavor.

It’s a very attractive theory.  I believed it myself.  But I now think that the RAX bug falsified it.

My intent here is not to discourage anyone from applying formal methods, only to caution against being overconfident in their results.

rg