[Cryptography] Security proofs prove non-failproof

Phillip Hallam-Baker phill at hallambaker.com
Mon Feb 20 11:59:11 EST 2017


On Mon, Feb 20, 2017 at 8:28 AM, Perry E. Metzger <perry at piermont.com>
wrote:

> On Mon, 20 Feb 2017 03:09:23 +0000 Peter Gutmann
> <pgut001 at cs.auckland.ac.nz> wrote:
> > Perry E. Metzger <perry at piermont.com> writes:
> >
> > >We now have several formally verified microkernels, a formally
> > >verified C compiler that also doubles as a proof tool, we nearly
> > >have a formally verified TLS stack (Project Everest), etc., etc.
> >
> > None of which are actually used in practice, at least not to any
> > noticeable extent.
>
> Not actually true. seL4 is used in millions of baseband
> controllers in mobile phones (to name one example) but I'll agree
> that overall, penetration of these tools isn't so great *yet* compared
> to everything else out there.
>

​You are conflating two things

1) Formal proofs of code correctness

2) Formal proofs of algorithm or protocol security

I very strongly believe the first is possible. My doctoral thesis is on a
formal proof of correctness for a significantly large system.

I remain skeptical on the second and suspect that the current state of the
art is doing more harm than good.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20170220/3cef6467/attachment.html>


More information about the cryptography mailing list