Re: invertible protocol descriptions in Coq

[Prashanth Mundkur <prashanth.mundkur@xxxxxxxxx>]

Interesting, thanks!

Some folks are getting back to even the lexical/parsing aspects of
packet parsing for security:
http://www.cs.dartmouth.edu/~sergey/langsec/

--prashanth

On 11:01 Mon 18 Mar, Anil Madhavapeddy wrote:
> Right, but this is purely about the lexical/parsing problem, which is 
> necessary (but not sufficient) to implement the whole protocol.  I believe 
> Lem/Ott are more appropriate for specifying the dynamic semantic 
> specification of how these 'lexed' packets should be put together.
> 
> *Invertible* parsing is very useful though -- it covers the efficient 
> construction of packets rather than just classification of incoming packets, 
> and reduces code duplication.  This is what MPL solved, as well as 
> Prashanth's follow up FP language [1], and the paper below.
> 
> [1] https://github.com/pmundkur/fp
> 
> -anil
> 
> On 18 Mar 2013, at 06:59, Jon Crowcroft <jon.crowcroft@xxxxxxxxxxxx> wrote:
> 
> > hm - so i think this is a weird paper - the example from eric rescorla's 
> > TLS work is easily sorted with an LALR1 parser and tokenisning the input 
> > stream not at the PACKET level, or byte, but by turning the protocol into a 
> > collection of microprotocols- indeed, this is how most people think about 
> > TCP - tcp is a collection of seperate protocols (state management for 
> > connection setup/teardown; sequenced data delivery; flow control; 
> > congestion control' urgent pointer; etc) living inside one packet format - 
> > don't get hung up on the packet format - that is a mere _lexical_ problem...
> > 
> > On Sat, Mar 16, 2013 at 9:21 PM, Anil Madhavapeddy <anil@xxxxxxxxxx> wrote:
> > Found this very cool paper on specifying invertible protocol descriptions 
> > in Coq:
> > 
> > http://staff.aist.go.jp/reynald.affeldt/documents/plpv2012-preprint.pdf
> > 
> > ..and they cover TLS.  It would be a nice project to extract this to 
> > OCaml/Haskell
> > to guarantee parsing equivalence from the formal spec (this is basically a 
> > much
> > better implementation of MPL or FP, embedded in the Coq proof assistant).
> > 
> > -anil
> > 
> 

-- 
prashanth