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

[Viktor Dukhovni]

On Fri, Mar 18, 2016 at 11:45:59AM -0700, Ray Dillinger wrote:

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

In this case only a part of the system was formally verified,
failure to verify more of the code was not a result of an incomplete
specification, it simply was not done.

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

There was no bug.  Just verification of a part of a system.  A
verified wheel on a car does not prevent fatal accidents, but that's
not a bug a formal verification of wheels.

-- 
	Viktor.