----- Forwarded message from "Perry E. Metzger" <perry@piermont.com> ----- Date: Mon, 26 Aug 2013 10:02:54 -0400 From: "Perry E. Metzger" <perry@piermont.com> To: Jerry Leichter <leichter@lrw.com> Cc: cryptography@metzdowd.com, Christian Huitema <huitema@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@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@piermont.com _______________________________________________ The cryptography mailing list cryptography@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