[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

[Perry E. Metzger]

Not to disagree with most of what you wrote, but as an aside:

On Wed, 16 Mar 2016 09:07:59 -0700 Henry Baker <hbaker1 at pipeline.com>
wrote:
> Even though I'm a formalist by nature & training,
> I can see that formal methods are not going to be
> sufficient to solve most of the problems in computer
> security today.

Most, no, but I've become a convert to formal methods in the last few
years. Until quite recently it was impossible to do real formal
verification work on programs of significant size, but that has
completely changed.

Two decades ago you couldn't have dreamed of writing a verified
program of any significant size, and now we have worked examples of
quite large formally verified artifact, including compilers, large
chunks of microprocessors, a microkernel, etc. etc.

> Part/most of the reasons have to do with the fact
> that we're trying to replace the engine & wings on
> a plane that's already flying with billions of folks
> aboard.

Ah, there, I would direct people to the work done on the Quark
formally verified browser. The key insight in the Quark browser work
was that you can protecting a few million lines of crappy code by
caging it behind a small amount of formally verified code that
firewalls it from the world. Such formally verified software firewalls
are a really useful trick, and I expect them to play a big role in
remediating legacy systems.

Formal verification is not a panacea, will never be something we can
use for every program, and has serious limitations, but it is already
a really serious tool in the security world. A number of recent TLS
vulns were found via formal methods.

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