[Cryptography] The Case for Formal Verification

[Phillip Hallam-Baker]

On Thu, Aug 29, 2013 at 4:46 PM, Perry E. Metzger <perry at piermont.com>wrote:

> Taking a break from our discussion of new privacy enhancing protocols,
> I thought I'd share something I've been mumbling about in various
> private groups for a while. This is almost 100% on the security side
> of things, and almost 0% on the cryptography side of things. It is
> long, but I promise that I think it is interesting to people doing
> security work.
>

Whitt Diffie was meant to be working on formal methods when he came up with
public key crypto...

My D.Phil Thesis was on applying formal methods to a large, non trivial
real time system (raw input bandwidth was 6Tb/sec, the immediate
fore-runner to the LHC data acquisition scheme). My college tutor was Tony
Hoare but I was in the nuclear physics dept because they had the money to
build the machine.

The problemI saw with formal methods was that the skills required were
already at the limit of what Oxford University grad students were capable
of and building systems large enough to matter looked like it would take
tools like category theory which are even more demanding.

The code synthesis scheme I developed was an attempt to address the scaling
problem from the other end. The idea being that to build a large system you
create a very specific programming language that is targeted at precisely
that class of problems. Then you write a back end that converts the
specification into code for that very restricted domain. If you want a
formal proof you have the synthesizer generate it from the specification as
well. That approach finesses the problem of having to validate the
synthesizer (which would likely take category theory) because only the
final target code need be validated.


That is the code I re-implemented in C after leaving VeriSign and released
onto SourceForge earlier this year and the tool I used to build the JSON
Schema tool.

I would probably have released it earlier only I met this guy at CERN who
had some crazy idea about hypertext.


-- 
Website: http://hallambaker.com/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20130829/71294247/attachment.html>