[Cryptography] Has formal verification actually been useful in the real world?

[Jim Gettys]

On Sat, Mar 11, 2017 at 1:40 PM, Perry E. Metzger <perry at piermont.com>
wrote:

> On Sat, 11 Mar 2017 07:48:12 -0800 Henry Baker <hbaker1 at pipeline.com>
> wrote:
> > It is my understanding that subsequent to the Intel "Pentium"
> > floating point bug, Intel has always formally verified its
> > arithmetic (at least the floating point arithmetic).
>
> Indeed, they do. My understanding is that they did before the FDIV bug
> as well, abandoned it for that generation, and then learned they
> lesson and always did the verification after that.
>
> > It's also pretty obvious that Intel has NOT been formally verifying
> > its address translation or caching systems, as they have been
> > enabling huge numbers of papers describing attacks on them.
>
> I don't know about address translation, but the cache coherency stuff
> is (to my knowledge) formally verified because it is so tricky and
> cache coherency bugs are so bad. However, as is always the case, which
> properties are formally verified matters -- some properties of
> interest in a security context might not be on their radar.
>
> I believe Intel uses ACL2 for their formal verification work but I
> am working from memory on all of this and might be a bit off.
>
>
​Working from memory: IIRC, one of the first ​uses was to verify that
memory barriers on the Alpha processor worked properly.

And yes, getting that kind of memory system right is "interesting" and
important to get correct....
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20170311/71dbe517/attachment.html>