<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Tue, May 19, 2015 at 8:11 AM, Henry Baker <span dir="ltr"><<a href="mailto:hbaker1@pipeline.com" target="_blank">hbaker1@pipeline.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span class="">At 01:26 PM 5/18/2015, Steve Weis wrote:<br>>For those who aren't familiar with SGX, see the links below.  Some pros and cons that I see:<br>
>+ You can run code in a "secure enclave" that is not accessible from either ring-0 code or SMM.<br>
<br>
</span>Mathematical proof?<br></blockquote><div><br></div><div>SGX is implemented through hardware mechanisms, not through cryptography or anything with a mathematical proof that would satisfy you. Yes, you do need to trust Intel to implement it correctly and yes, Intel certainly ships hardware with hundreds of errata.<br></div><div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span class="">>+ Secure enclaves are backed by physically encrypted memory, and thus not exposed to cold boot attacks or non-volatile RAM.<br>
<br>
</span>Mathematical proof?</blockquote><div><br></div><div><div>You want a mathematical proof that a physical attack against hardware is impossible? Or that memory is actually being encrypted as advertised? The latter is easy to verify.</div><div><br></div><div>The closest model I can think of is physically observable cryptography: <a href="http://www.cs.bu.edu/fac/reyzin/papers/physec.pdf">http://www.cs.bu.edu/fac/reyzin/papers/physec.pdf</a></div></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span class="">>+ Enclaves should be remotely attestable with CPU-bound public keys using anonymized or pseudonymized signatures.<br>
<br>
</span>Mathematical proof?<br></blockquote><div><br></div><div>EPID paper is here: <a href="https://eprint.iacr.org/2009/095.pdf">https://eprint.iacr.org/2009/095.pdf</a></div><div><br></div><div>I doubt that will satisfy you.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">If Intel can't provide sound & complete & public proofs for their wet dreams, then these technologies are simply more BS for the pile.<br>
<br>
In the absence of such mathematical proofs, Intel SGX is providing more "security through obscurity" than true security.<br></blockquote><div><br></div><div>You seem to be asking for formal proofs of both the correctness of the architecture design and that a hardware implementation properly embodies the design. I can't think of any hardware which would satisfy your criteria.</div><div><br></div><div>DARPA's TRUST and CRASH programs may be of interest:</div><div><a href="http://www.darpa.mil/opencatalog/CRASH.html">http://www.darpa.mil/opencatalog/CRASH.html</a><br></div><div><a href="http://www.darpa.mil/Our_Work/MTO/Programs/Trusted_Integrated_Circuits_%28TRUST%29.aspx">http://www.darpa.mil/Our_Work/MTO/Programs/Trusted_Integrated_Circuits_%28TRUST%29.aspx</a><br></div></div></div></div>