[Cryptography] Formal Verification

Phillip Hallam-Baker phill at hallambaker.com
Thu Mar 17 15:44:33 EDT 2016


On Thu, Mar 17, 2016 at 12:18 PM, Jonathan Thornburg
<jthorn at astro.indiana.edu> wrote:
> 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?

My thesis but it is a bit old.

I got distracted by a side project called the Web or something. Only
just got back to it.

> 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?

Not for TCP/IP but if I was going to write a v6 stack I would want to
use the approach.

The tools are here:
https://github.com/hallambaker/PHB-Build-Tools

As I said, they are all open source. I am documenting them as I
document the Mesh.

Unlike traditional formal methods, this is a major productivity
improvement. I can generate a protocol spec from scratch in under a
week elapsed time and no more than about 20 hours work. The LURK
specification I am currently writing for a BOF at IETF95 uses these
tools.


More information about the cryptography mailing list