<div dir="ltr"><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 20, 2017 at 8:28 AM, 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 Mon, 20 Feb 2017 03:09:23 +0000 Peter Gutmann<br>
<span class=""><<a href="mailto:pgut001@cs.auckland.ac.nz">pgut001@cs.auckland.ac.nz</a>> wrote:<br>
> Perry E. Metzger <<a href="mailto:perry@piermont.com">perry@piermont.com</a>> writes:<br>
><br>
</span><span class="">> >We now have several formally verified microkernels, a formally<br>
> >verified C compiler that also doubles as a proof tool, we nearly<br>
> >have a formally verified TLS stack (Project Everest), etc., etc.<br>
><br>
</span>> None of which are actually used in practice, at least not to any<br>
> noticeable extent.<br>
<br>
Not actually true. seL4 is used in millions of baseband<br>
controllers in mobile phones (to name one example) but I'll agree<br>
that overall, penetration of these tools isn't so great *yet* compared<br>
to everything else out there.<br></blockquote><div><br></div><div><div class="gmail_default" style="font-size:small">​You are conflating two things</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">1) Formal proofs of code correctness</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">2) Formal proofs of algorithm or protocol security</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">I very strongly believe the first is possible. My doctoral thesis is on a formal proof of correctness for a significantly large system.</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">I remain skeptical on the second and suspect that the current state of the art is doing more harm than good.</div><br></div><div> </div></div><br></div></div>