[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

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.

So what?

Imagine it was 1970 and someone said that writing operating systems in
high level languages was the future and you said "meh, other than a
couple of experiments (Multics) I don't know of any that have been
done that way and it certainly isn't the future." You would have been
absolutely correct about the present and absolutely incorrect about
the future.

It has been possible to formally verify significant pieces of software
*at all* for, what, ten years at this point? What fraction of the
programmers out there working on mission critical systems even know it
is possible at this point?

Give it another decade or two.

> CompCert is nice, but can't reach anywhere near the code quality of
> any standard C compiler,

On the contrary, it is the only compiler out there where you can feel
reasonably safe that the output is correct!

If you're talking about performance, well, that's a reasonable
concern. But, for many purposes, I'd rather be safe than fast, and
we'll get fast eventually. It's all very new. Give it time.

(BTW, if you don't believe people often prefer characteristics other
than fast, I'll note that there are huge web applications out there
written in Ruby and Python right now.)

Anyway, with time, other compilers are likely to benefit from formal
verification, too. The LLVM world now has VeLLVM, which is a project
to produce a formal definition of the LLVM intermediate
representation, and they've demonstrated the ability to plug formally
verified optimizations in to LLVM and have them work. The fact that
LLVM is fully modular means you can replace parts with formally
verified replacements without having to toss the whole thing at once.

> miTLS is a cool project, but I don't know of anyone using it in
> production,

So yes, there are all these tools, and they're brand new, and in a
world of many millions of software artifacts, there are now a couple
dozen verified ones that not many people are using yet.

So, give it time.

> Note that I'm not trying to bash any of L4, CompCert, miTLS, etc.
> They're all extremely useful... well OK, I don't know how useful L4
> is but CompCert and miTLS certainly are.  However, they're
> specialised, craftsman's tools, not something you bake into a
> shipping product, in the same way that you don't use a McLaren to
> deliver UPS packages.

Patience.

> >I disagree. Much of the difficulty in using a system like Coq now
> >lies in problems we understand how to solve, like terrible error
> >messages and terrible UI
>
> It's not the error messages that are the problem, it's the learning
> cliff (not a curve, a vertical cliff).  I've played with some tools
> built around Coq, and even with my somewhat elevated level of
> masochism for doing code analysis and lack of
> the-boss-wants-it-by-Tuesday constraints, it was just too painful
> to continue.

The cliff is there because the UI sucks, the documentation is
mediocre, and you need to understand a bunch of type theory and formal
logic in order to make progress. Patience. Things will get better.

> >I entirely disagree. I suspect that we're going to see serious
> >mainstream acceptance of the tools for high value products inside
> >of ten years,
>
> Again, we'll have to disagree on this, I see no sign of formal
> methods going mainstream not just in ten years but ever.

All the serious operating system guys said no one would ever use high
level languages for kernels, too, until suddenly everyone
did. And all the IBM people assured me that microcomputers were never
going to replace the mainframes. (To their credit, the mainframes
still, weirdly, sell, though they clearly are no longer even vaguely
dominant.)

> Better yet, if in ten years they've gone mainstream, I'll buy you
> dinner at Tony's Steak House in Victoria St, Auckland.  If not, you
> owe me dinner at the same venue.

We can discuss terms. I think the location is not exactly optimized
for a fair bet given that we're on exactly opposite sides of the
world, and that I'm not a steak person. We'll take that bit offline.

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