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

Perry E. Metzger perry at piermont.com
Fri Mar 18 19:52:58 EDT 2016


On Fri, 18 Mar 2016 23:18:29 +0000 Peter Gutmann
<pgut001 at cs.auckland.ac.nz> wrote:
> Perry E. Metzger <perry at piermont.com> writes:
> 
> >I will also point out that mere model checking isn't the state of
> >the art -- we can now do far better. CompCert, for example, is
> >written completely in Coq and then extracted into OCaml.  
> 
> Which leads to a variant of the Gnu problem in which, to build
> Gnu-anything, you first need Gnu-everything-else.  I started
> playing with the CompCert rabbit hole a few days ago when you first
> mentioned it, but now I'm waiting for the proverbial rainy weekend
> to keep going...

You will find that much of the current Coq ecosystem is hard to use.
This isn't because the technology is inherently difficult to use but
because the people who have worked on all these tools to date have
been doctoral students and the like and have been more interested in
adding features than documentation, good error reporting, etc.

The error messages in Coq are particularly terrible. At the point in
a proof development where a tactic fails, the system has more than
enough information to tell you exactly what failed, which would help
you a lot with figuring out how to tweak what you're doing. However,
the system generally just tells you "that didn't work", which isn't
useful.

As these technologies become more widespread, I'm expecting to see a
lot of work on making them more usable by ordinary engineers as well.


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


More information about the cryptography mailing list