[Cryptography] Formal Verification

Jonathan Thornburg jthorn at astro.indiana.edu
Thu Mar 17 12:18:20 EDT 2016


On Thu, Mar 17, 2016 at 09:42:47AM -0400, Phillip Hallam-Baker wrote:
> There is another approach that I developed in my doctoral thesis 25
> odd years ago.
> 
> First you develop a language that is precisely targeted to your problem domain.
> 
> Then you develop a code generator for that language to your target language.
> 
> Finally, you augment the code generator to generate the proof as well.
> 
> 
> C and C# are general purpose languages that talk about what the
> machine should do. If you are writing a communication protocol you
> have a collection of finite state machines at various levels. Some are
> used to map bits to data structures, others orchestrate the state at
> the protocol ends, etc. etc. C and C# require the programer to do the
> mental map from the problem domain to the target.
> 
> With the Goedel meta-synthesizer, you can quickly develop a
> mini-language that describes a ridiculously specific language and
> create a code synthesizer for that domain. So instead of a completely
> unrestricted parser generator like yacc, a Goedel generated parser
> would only work for RFC822 style message headers.

Is there a published paper describing this work?

I wonder why none of the big secure-mailer projects (e.g. postfix, qmail,
opensmtp, etc) are using this type of technique?

Indeed, it would seem to provide an interesting vehicle for producing
a formally-verified TCP/IP stack.  Has anyone tried this?



More information about the cryptography mailing list