[Cryptography] Formal Verification (was Re: Email and IM are ideal candidates for mix networks)

[Eugen Leitl]

----- Forwarded message from "Perry E. Metzger" <perry at piermont.com> -----

Date: Mon, 26 Aug 2013 10:02:54 -0400
From: "Perry E. Metzger" <perry at piermont.com>
To: Jerry Leichter <leichter at lrw.com>
Cc: cryptography at metzdowd.com, Christian Huitema <huitema at huitema.net>
Subject: [Cryptography] Formal Verification (was Re: Email and IM are ideal candidates for mix networks)
X-Mailer: Claws Mail 3.9.0 (GTK+ 2.24.20; x86_64-apple-darwin12.4.0)

On Sun, 25 Aug 2013 23:32:32 -0400 Jerry Leichter <leichter at lrw.com>
wrote:
> I think the goal to aim for is no patches!  Keep the device and its
> interfaces simple enough that you can get a decent formal proof of
> correctness, along with a ton of careful review and testing (per
> Don Knuth's comment somewhere to "Be careful of the following code,
> I've only proved it correct, not tested it") and then *leave it
> alone*.

I'd like to point out that this is no longer a pipe dream. The formal
verification of seL4, CompCert and other substantial pieces of code in
recent years shows the technology has improved a lot. Quark (the web
browser verified by the use of a "shim") has shown one can get
enormous leverage by formally verifying only tiny fractions of an
overall system comprising millions of lines of code, which is an
especially interesting technique in the context of existing large code
bases.

Formal verification is not a panacea. One has to know what to verify,
for example, and if you verify the wrong properties, you've gained
little. However, unlike current methods, if you discover you have
failed to verify a needed property, adding a theorem to your
development fixes that hole _completely_ and _forever_.

(Yes, you also need a verified toolchain, but given things like
CompCert, that is now doable.)

I'm something of a recent arrival to the world that developed the most
widely used tools for formal verification (like Coq), and so I'm in a
better position than most to explain how to learn about them.

I would be happy to produce an extended post on how to learn about
what is out there for people who are interested.

Warning: although in the long term there is no reason the tools cannot
be made very user friendly and easy to use, right now that is not the
case. This is not inherently so, it is just a feature of the
development history of the tools. Error messages tend to be pretty
poor, as is documentation, and the learning curve is steep. However,
in the long run, I'll state very directly I think the recent advances
in the state of the art in proof assistants are the most significant
new development in software quality in decades. The user
unfriendliness could be fixed by a new generation of users and
developers who started "further away from the problem".

Perry
-- 
Perry E. Metzger		perry at piermont.com
_______________________________________________
The cryptography mailing list
cryptography at metzdowd.com
http://www.metzdowd.com/mailman/listinfo/cryptography

----- End forwarded message -----
-- 
Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org
______________________________________________________________
ICBM: 48.07100, 11.36820 http://ativel.com http://postbiota.org
AC894EC5: 38A5 5F46 A4FF 59B8 336B  47EE F46E 3489 AC89 4EC5