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

[Ray Dillinger]

On 03/18/2016 12:55 AM, Viktor Dukhovni 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?
> On the face of it, they were quite successful...
> 

If the system can fail because of something that was not
formally verified, then even if the formal verification
was perfectly implemented and proved perfect compliance
with the specification...

It does not matter because the specification itself
contained a bug.

This is the real issue with formal verification.  You
can prove that software complies with a specification,
but you cannot prove that the specification itself is
bug-free.  The specification is also code and may
also contain bugs.

The benefit is that the specification language is usually
less susceptible to misunderstanding or unsuspected bugs
because it has much cleaner semantics which would take a
compiler at least days to compile code for (and which in
some cases cannot be directly translated into machine
code but which can be checked)  and nobody really cares if
the theorem prover (as opposed to the compiler) runs for
days.  Another benefit is that even if the specification
does contain a bug, a bug in the program being checked
usually does not coincide with it.

But no language has ever been created which makes it
difficult to write buggy code, and that includes the
representations of software specifications that the
formal verification systems prove compliance to.

			Bear

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20160318/3afcec0e/attachment.sig>