[146474] in cryptography@c2.net mail archive
Re: [Cryptography] The Case for Formal Verification
daemon@ATHENA.MIT.EDU (Phillip Hallam-Baker)
Thu Aug 29 19:20:50 2013
X-Original-To: cryptography@metzdowd.com
In-Reply-To: <20130829164630.3aa90354@jabberwock.cb.piermont.com>
Date: Thu, 29 Aug 2013 19:00:41 -0400
From: Phillip Hallam-Baker <hallam@gmail.com>
To: "Perry E. Metzger" <perry@piermont.com>
Cc: "cryptography@metzdowd.com" <cryptography@metzdowd.com>
Errors-To: cryptography-bounces+crypto.discuss=bloom-picayune.mit.edu@metzdowd.com
--===============5263304265074037730==
Content-Type: multipart/alternative; boundary=001a11c3db743a5abf04e51e1347
--001a11c3db743a5abf04e51e1347
Content-Type: text/plain; charset=ISO-8859-1
On Thu, Aug 29, 2013 at 4:46 PM, Perry E. Metzger <perry@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/
--001a11c3db743a5abf04e51e1347
Content-Type: text/html; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr">On Thu, Aug 29, 2013 at 4:46 PM, Perry E. Metzger <span di=
r=3D"ltr"><<a href=3D"mailto:perry@piermont.com" target=3D"_blank">perry=
@piermont.com</a>></span> wrote:<br><div class=3D"gmail_extra"><div clas=
s=3D"gmail_quote">
<blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1p=
x #ccc solid;padding-left:1ex">Taking a break from our discussion of new pr=
ivacy enhancing protocols,<br>
I thought I'd share something I've been mumbling about in various<b=
r>
private groups for a while. This is almost 100% on the security side<br>
of things, and almost 0% on the cryptography side of things. It is<br>
long, but I promise that I think it is interesting to people doing<br>
security work.<br></blockquote><div><br></div><div>Whitt Diffie was meant t=
o be working on formal methods when he came up with public key crypto...</d=
iv><div><br></div><div>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.</div>
<div><br></div><div>The problemI saw with formal methods was that the skill=
s required were already at the limit of what Oxford University grad student=
s were capable of and building systems large enough to matter looked like i=
t would take tools like category theory which are even more demanding.=A0</=
div>
<div><br></div><div>The code synthesis scheme I developed was an attempt to=
address the scaling problem from the other end. The idea being that to bui=
ld a large system you create a very specific programming language that is t=
argeted at precisely that class of problems. Then you write a back end that=
converts the specification into code for that very restricted domain. If y=
ou want a formal proof you have the synthesizer generate it from the specif=
ication as well. That approach finesses the problem of having to validate t=
he synthesizer (which would likely take category theory) because only the f=
inal target code need be validated.</div>
<div><br></div><div><br></div><div>That is the code I re-implemented in C a=
fter leaving VeriSign and released onto SourceForge earlier this year and t=
he tool I used to build the JSON Schema tool.</div><div><br></div><div>
I would probably have released it earlier only I met this guy at CERN who h=
ad some crazy idea about hypertext.</div><div><br></div></div><div><br></di=
v>-- <br>Website: <a href=3D"http://hallambaker.com/">http://hallambaker.co=
m/</a><br>
</div></div>
--001a11c3db743a5abf04e51e1347--
--===============5263304265074037730==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
_______________________________________________
The cryptography mailing list
cryptography@metzdowd.com
http://www.metzdowd.com/mailman/listinfo/cryptography
--===============5263304265074037730==--
