[Cryptography] Formal Verification

Phillip Hallam-Baker phill at hallambaker.com
Thu Mar 17 09:42:47 EDT 2016


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.

Using this style of coding removes a vast amount of the cruft that
clutters up traditional implementations. In my experience, the largest
number of coding errors come from the mismatch between the problem
domain and the implementation and that applies to formal methods as
well. A broken specification is as much a bug as a broken program.
Which is why I originally started looking at this approach in the
first place.

But if you want to use Goedel to develop a formal proof of
correctness, you can do that as well by generating the proof just like
you would generate any other bit of code.


I recently cleaned up all the code so that I could use this to build
the Mathematical Mesh. The code is on SourceForge and GitHub under an
MIT license. You can get there from http://prismproof.org.

The tools are available as standalone tools or integrated into Visual
Studio as VSIX extensions.

If you use them to develop protocols, there is a set of other support
tools that allows the entire production chain to be automated. If you
look at my Internet Drafts for the Mesh, all the examples are
generated from running code that was generated from the protocol
specification by a generator. The reference sections for the draft
come from the same source. This ensures that all my examples match the
reference section.


Now I am not currently using this system to develop formal proofs, I
do not have time to go down that route at present. But it would
provide a good platform for that approach.


More information about the cryptography mailing list