<div dir="ltr"><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Mar 11, 2017 at 1:40 PM, Perry E. Metzger <span dir="ltr"><<a href="mailto:perry@piermont.com" target="_blank">perry@piermont.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Sat, 11 Mar 2017 07:48:12 -0800 Henry Baker <<a href="mailto:hbaker1@pipeline.com">hbaker1@pipeline.com</a>><br>
wrote:<br>
<span class="">> It is my understanding that subsequent to the Intel "Pentium"<br>
> floating point bug, Intel has always formally verified its<br>
> arithmetic (at least the floating point arithmetic).<br>
<br>
</span>Indeed, they do. My understanding is that they did before the FDIV bug<br>
as well, abandoned it for that generation, and then learned they<br>
lesson and always did the verification after that.<br>
<span class=""><br>
> It's also pretty obvious that Intel has NOT been formally verifying<br>
> its address translation or caching systems, as they have been<br>
> enabling huge numbers of papers describing attacks on them.<br>
<br>
</span>I don't know about address translation, but the cache coherency stuff<br>
is (to my knowledge) formally verified because it is so tricky and<br>
cache coherency bugs are so bad. However, as is always the case, which<br>
properties are formally verified matters -- some properties of<br>
interest in a security context might not be on their radar.<br>
<br>
I believe Intel uses ACL2 for their formal verification work but I<br>
am working from memory on all of this and might be a bit off.<br>
<span class="im HOEnZb"><br></span></blockquote><div><br></div><div class="gmail_default" style="font-size:small">​Working from memory: IIRC, one of the first ​uses was to verify that memory barriers on the Alpha processor worked properly.</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">And yes, getting that kind of memory system right is "interesting" and important to get correct....</div><div class="gmail_default" style="font-size:small"><br></div></div></div></div>