[Cryptography] Security proofs prove non-failproof

[Bill Frantz]

On 2/16/17 at 5:58 PM, perry at piermont.com (Perry E. Metzger) wrote:

>The big change in formal methods happened only in the last decade. We
>now have several formally verified microkernels, a formally verified C
>compiler that also doubles as a proof tool, we nearly have a formally
>verified TLS stack (Project Everest), etc., etc. ...

It will be interesting to see what kind of bugs show up in these 
formally verified systems over years of use.

It is clear there may still be bugs in the verification 
methodology as well as in the choice of what to verify.

>...

>You can run Coverity over a program every day and not find serious
>problems in it that a formal verification will utterly
>eliminate. Static analysis simply isn't able to do a lot of this
>stuff. Yes, static analysis is great, but it isn't the same thing.

The real value today of formal methods is that they force people 
to take a different view of their programs. Looking at things 
from a different viewpoint frequently shows things you didn't 
see before. This feature alone makes them worthwhile. Making 
them easier to use will spread this advantage.

Cheers - Bill



---------------------------------------------------------------------------
Bill Frantz        | If you want total security, go to prison. 
There you're
408-356-8506       | fed, clothed, given medical care and so on. 
The only
www.pwpconsult.com | thing lacking is freedom. - Dwight D. Eisenhower