<div dir="ltr">On Thu, Aug 29, 2013 at 4:46 PM, Perry E. Metzger <span dir="ltr"><<a href="mailto:perry@piermont.com" target="_blank">perry@piermont.com</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Taking a break from our discussion of new privacy enhancing protocols,<br>
I thought I'd share something I've been mumbling about in various<br>
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 to be working on formal methods when he came up with public key crypto...</div><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 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. </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 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.</div>
<div><br></div><div><br></div><div>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.</div><div><br></div><div>
I would probably have released it earlier only I met this guy at CERN who had some crazy idea about hypertext.</div><div><br></div></div><div><br></div>-- <br>Website: <a href="http://hallambaker.com/">http://hallambaker.com/</a><br>

</div></div>