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

[Perry E. Metzger]

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.

Perry
-- 
Perry E. Metzger		perry at piermont.com