publication . Preprint . 2018

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats

Delaware, Benjamin; Suriyakarn, Sorawit; Pit--Claudel, Clément; Ye, Qianchuan; Chlipala, Adam;
Open Access English
  • Published: 13 Mar 2018
Abstract
It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more work, the same combinator program can denote both a decoder and an encoder. Unfortunately, the real world is full of gnarly formats, as with the packet formats that make up the standard Internet protocol stack. Most past parser-combinator approaches cannot handle these formats, and the few exceptions require redundancy -- one part of the natural grammar needs to be hand-translated into hints in multiple parts of a parser program. We show how to recover very natural and nonredundant format...
Subjects
free text keywords: Computer Science - Programming Languages
Related Organizations
Download from
21 references, page 1 of 2

[1] Apache Software Foundation. Apache Avro 1.8.0 documentation, 2016. [Accessed May 04, 2016].

[2] Godmar Back. Datascript - a specification and scripting language for binary data. In Proceedings of the 1st ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering, GPCE '02, pages 66-77, London, UK, UK, 2002. Springer-Verlag.

[3] Ralph-JR Back. A calculus of refinements for program derivations. Acta Informatica, 25(6):593-624, 1988.

[4] Julian Bangert and Nickolai Zeldovich. Nail: A Practical Tool for Parsing and Generating Data Formats. In OSDI, pages 615-628. USENIX Association, 2014. [OpenAIRE]

[5] Benjamin Delaware, Cle´ment Pit-Claudel, Jason Gross, and Adam Chlipala. Fiat: Deductive synthesis of abstract data types in a proof assistant. In Proc. POPL, 2015.

[6] Edsger W. Dijkstra. A constructive approach to the problem of program correctness. Circulated privately, August 1967.

[7] Olivier Dubuisson. ASN. 1: communication between heterogeneous systems. Morgan Kaufmann, 2001.

[8] Kathleen Fisher and Robert Gruber. Pads: a domain-specific language for processing ad hoc data. ACM Sigplan Notices, 40(6):295-304, 2005.

[9] Kathleen Fisher, Yitzhak Mandelbaum, and David Walker. The next 700 data description languages. SIGPLAN Not., 41(1):2- 15, January 2006.

[10] Stephen C. Johnson. Yacc: Yet another compiler-compiler. Technical report, 1979.

[11] Peter Lammich and Thomas Tuerk. Applying data refinement for monadic programs to hopcroft's algorithm. In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, volume 7406 of Lecture Notes in Computer Science, pages 166-182. Springer Berlin Heidelberg, 2012.

[12] Anil Madhavapeddy, Richard Mortier, Charalampos Rotsos, David Scott, Balraj Singh, Thomas Gazagnaire, Steven Smith, Steven Hand, and Jon Crowcroft. Unikernels: Library operating systems for the cloud. In Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '13, pages 461-472, New York, NY, USA, 2013. ACM.

[13] Peter J. McCann and Satish Chandra. Packet types: Abstract specification of network protocol messages. In Proceedings of the Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM '00, pages 321-333, New York, NY, USA, 2000. ACM.

[14] P. Mockapetris. Domain names - implementation and specification. RFC 1035, November 1987.

[15] Ruoming Pang, Vern Paxson, Robin Sommer, and Larry Peterson. binpac: A yacc for writing application protocol parsers. In Proceedings of the 6th ACM SIGCOMM conference on Internet measurement, pages 289-300. ACM, 2006.

21 references, page 1 of 2
Abstract
It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more work, the same combinator program can denote both a decoder and an encoder. Unfortunately, the real world is full of gnarly formats, as with the packet formats that make up the standard Internet protocol stack. Most past parser-combinator approaches cannot handle these formats, and the few exceptions require redundancy -- one part of the natural grammar needs to be hand-translated into hints in multiple parts of a parser program. We show how to recover very natural and nonredundant format...
Subjects
free text keywords: Computer Science - Programming Languages
Related Organizations
Download from
21 references, page 1 of 2

[1] Apache Software Foundation. Apache Avro 1.8.0 documentation, 2016. [Accessed May 04, 2016].

[2] Godmar Back. Datascript - a specification and scripting language for binary data. In Proceedings of the 1st ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering, GPCE '02, pages 66-77, London, UK, UK, 2002. Springer-Verlag.

[3] Ralph-JR Back. A calculus of refinements for program derivations. Acta Informatica, 25(6):593-624, 1988.

[4] Julian Bangert and Nickolai Zeldovich. Nail: A Practical Tool for Parsing and Generating Data Formats. In OSDI, pages 615-628. USENIX Association, 2014. [OpenAIRE]

[5] Benjamin Delaware, Cle´ment Pit-Claudel, Jason Gross, and Adam Chlipala. Fiat: Deductive synthesis of abstract data types in a proof assistant. In Proc. POPL, 2015.

[6] Edsger W. Dijkstra. A constructive approach to the problem of program correctness. Circulated privately, August 1967.

[7] Olivier Dubuisson. ASN. 1: communication between heterogeneous systems. Morgan Kaufmann, 2001.

[8] Kathleen Fisher and Robert Gruber. Pads: a domain-specific language for processing ad hoc data. ACM Sigplan Notices, 40(6):295-304, 2005.

[9] Kathleen Fisher, Yitzhak Mandelbaum, and David Walker. The next 700 data description languages. SIGPLAN Not., 41(1):2- 15, January 2006.

[10] Stephen C. Johnson. Yacc: Yet another compiler-compiler. Technical report, 1979.

[11] Peter Lammich and Thomas Tuerk. Applying data refinement for monadic programs to hopcroft's algorithm. In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, volume 7406 of Lecture Notes in Computer Science, pages 166-182. Springer Berlin Heidelberg, 2012.

[12] Anil Madhavapeddy, Richard Mortier, Charalampos Rotsos, David Scott, Balraj Singh, Thomas Gazagnaire, Steven Smith, Steven Hand, and Jon Crowcroft. Unikernels: Library operating systems for the cloud. In Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '13, pages 461-472, New York, NY, USA, 2013. ACM.

[13] Peter J. McCann and Satish Chandra. Packet types: Abstract specification of network protocol messages. In Proceedings of the Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM '00, pages 321-333, New York, NY, USA, 2000. ACM.

[14] P. Mockapetris. Domain names - implementation and specification. RFC 1035, November 1987.

[15] Ruoming Pang, Vern Paxson, Robin Sommer, and Larry Peterson. binpac: A yacc for writing application protocol parsers. In Proceedings of the 6th ACM SIGCOMM conference on Internet measurement, pages 289-300. ACM, 2006.

21 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue