[Cryptography] Has formal verification actually been useful in the real world?

[Perry E. Metzger]

On Sat, 11 Mar 2017 15:28:18 +1000 "James A. Donald"
<jamesd at echeque.com> wrote:
> Has a complete formally verified system been deployed anywhere?

In terms of *complete* systems, a few have, though I think mostly in
avionics. There are published papers on the topic.

> Is there one keeping the electricity grid up?

Not to my knowledge.

> Or a formally verified browser?

There isn't one that has been deployed, but an experimental formally
verified browser called Quark was built at UCSD. It hasn't been
deployed and isn't maintained, but it was a very interesting
demonstration because it showed how to use a small formally verified
"software firewall" to contain millions of lines of very bad code that
constituted the bulk of the browser.

http://goto.ucsd.edu/quark/

> Or even software for converting graphics files to images
> on the screen so that a broken image will not take control of your
> computer?

I know of no formally verified image libraries at this time, but
formal verification of something like libtiff or other image libraries
should be feasible at this point using Princeton's VST

http://vst.cs.princeton.edu/

Note that currently it would be a lot of effort, but with every
passing few months new tricks are learned about how to reduce the
effort of such work. I would say that it is worthwhile for someone to
attempt this.

It might or might not be easier to rewrite the code for such a
library from scratch in order to reduce the proof burden. One
approach, for example, might be to go for extraction from Coq or
F*. See the Project Everest effort for information on that approach:

https://project-everest.github.io/

which uses an F* to C conversion.

> Back in the days of usenet there used to be an old and obscure unix
> based usenet browser that would crash on unusual control character
> sequences and start executing usenet post text as machine code.  Is
> there any proof that that cannot happen with unusual html or
> graphics?

There have been numerous attacks that exploit graphics
vulnerabilities. There was a long while, as I recall, where most iOS
exploits were graphics library problems.

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