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

[Bill Frantz]

On 3/18/16 at 2:33 PM, perry at piermont.com (Perry E. Metzger) wrote:

>Now, on the more general question, although it is true that
>specifications can contain bugs as well, that's not a reason to think
>formal verification isn't exceptionally useful.

...

>And again, the big win is not perfection (which is difficult to
>achieve) but rather the ratchet effect.

Ignoring the ability of  formal methods to actually find bugs, 
they are valuable because they make you look at code and systems 
from a different prospective. This different view will be 
particularly valuable if the system was developed informally 
e.g. using agile methods. Another viewpoint has great value for 
finding bugs.

Cheers - Bill

---------------------------------------------------------------------------
Bill Frantz        |"Web security is like medicine - trying to 
do good for
408-356-8506       |an evolved body of kludges" - Mark Miller
www.pwpconsult.com |