research-article

Generic packet descriptions: verified parsing and pretty printing of low-level data

Authors:

Marcell van Geest,

Wouter SwierstraAuthors Info & Claims

TyDe 2017: Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development

Pages 30 - 40

https://doi.org/10.1145/3122975.3122979

Published: 03 September 2017 Publication History

Abstract

Complex protocols describing the communication or storage of binary data are difficult to describe precisely. This paper presents a collection of data types for describing a binary data formats; the corresponding parser and pretty printer are generated automatically from a data description. By embedding these data types in a general purpose dependently typed programming language, we can verify once and for all that the parsers and pretty printers generated in this style are correct by construction. To validate our results, we show how to write a verified parser of the IPv4 network protocol.

References

[1]

Thorsten Altenkirch and Conor McBride. 2003. Generic programming within dependently typed programming. In Generic Programming. Springer, 1–20.

Digital Library

[2]

Thorsten Altenkirch, Conor McBride, and Peter Morris. 2007. Generic programming with dependent types. In Datatype-Generic Programming. Springer, 209–257.

Digital Library

[3]

Roland Backhouse, Patrik Jansson, Johan Jeuring, and Lambert Meertens. 1998. Generic programming. In International School on Advanced Functional Programming. Springer, 28–115.

[4]

Ana Bove, Peter Dybjer, and Ulf Norell. 2009. A brief overview of Agda–a functional language with dependent types. In International Conference on Theorem Proving in Higher Order Logics. Springer, 73–78.

Digital Library

[5]

Edwin Brady. 2011. Idris: systems programming meets full dependent types. In Proceedings of the 5th ACM workshop on Programming languages meets program verification. ACM, 43–54.

Digital Library

[6]

Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 05 (2013), 552– 593.

[7]

Pierre-Evariste Dagand. 2013. A Cosmology of Datatypes. Ph.D. Dissertation. University of Strathclyde.

[8]

Nils Anders Danielsson. 2013. Correct-by-construction Pretty-printing. In Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-typed Programming. ACM, 1–12.

Digital Library

[9]

Ben Delaware. 2017. Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. (2017). Unpublished draft.

[10]

Dominique Devriese and Frank Piessens. 2011. On the Bright Side of Type Classes: Instance Arguments in Agda. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP ’11). 143–155.

Digital Library

[11]

Peter Dybjer and Anton Setzer. 1999. A finite axiomatization of inductive-recursive definitions. In International Conference on Typed Lambda Calculi and Applications. Springer, 129–146.

Digital Library

[12]

Kathleen Fisher, Yitzhak Mandelbaum, and David Walker. 2006. The next 700 data description languages. In POPL’06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 2–15.

Digital Library

[13]

Pepijn Kokke and Wouter Swierstra. 2015. Auto in Agda: programming proof search. In International Conference on Mathematics of Program Construction. Springer, 276– 301.

[14]

Per Martin-Löf. 1984. Intuitionistic type theory. Vol. 9. Bibliopolis Napoli.

[15]

The Coq development team. 2004. The Coq proof assistant reference manual. LogiCal Project. http://coq.inria.fr Version 8.0.

[16]

Conor McBride. 2010. Ornamental algebras, algebraic ornaments. Journal of functional programming (2010).

[17]

Conor McBride and Ross Paterson. 2008. Applicative programming with effects. Journal of functional programming 18, 01 (2008), 1–13.

Digital Library

[18]

Peter J McCann and Satish Chandra. 2000. Packet types: abstract specification of network protocol messages. ACM SIGCOMM Computer Communication Review 30, 4 (2000), 321–333.

Digital Library

[19]

Fabrice Mérillon, Laurent Réveillère, Charles Consel, Renaud Marlet, and Gilles Muller. 2000. Devil: An IDL for hardware programming. In Proceedings of the 4th conference on Symposium on Operating System Design & Implementation-Volume 4. USENIX Association, 2–2.

Digital Library

[20]

Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers University of Technology.

[21]

Nicolas Oury and Wouter Swierstra. 2008. The power of Pi. In ACM Sigplan Notices, Vol. 43. ACM, 39–50.

Digital Library

[22]

Tillmann Rendel and Klaus Ostermann. 2010. Invertible syntax descriptions: unifying parsing and pretty printing. In ACM Sigplan Notices, Vol. 45. ACM, 1–12.

Digital Library

[23]

Paul Van Der Walt and Wouter Swierstra. 2012. Engineering proof by reflection in Agda. In Symposium on Implementation and Application of Functional Languages. Springer, 157–173.

[24]

Yan Wang and Verónica Gaspes. 2008. A Library for Processing Ad hoc Data in Haskell - Embedding a Data Description Language. In Implementation and Application of Functional Languages - 20th International Symposium, IFL 2008, Hatfield, UK, September 10-12, 2008. Revised Selected Papers. 174–191.

Digital Library

Cited By

Shankar NLucas Z(2024)Robust Verification of PEG Parser Interpreters2024 IEEE Security and Privacy Workshops (SPW)10.1109/SPW63631.2024.00022(180-191)Online publication date: 23-May-2024
https://doi.org/10.1109/SPW63631.2024.00022
Wallez TProtzenko JBhargavan KMeng WJensen CCremers CKirda E(2023)Comparse: Provably Secure Formats for Cryptographic ProtocolsProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623201(564-578)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623201
Chen ZLafont AO'Connor LKeller GMcLaughlin CJackson VRizkallah C(2023)Dargent: A Silver Bullet for Verified Data Layout RefinementProceedings of the ACM on Programming Languages10.1145/35712407:POPL(1369-1395)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571240
Show More Cited By

Index Terms

Generic packet descriptions: verified parsing and pretty printing of low-level data
1. Software and its engineering
  1. Software notations and tools
    1. Context specific languages
      1. Domain specific languages
    2. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Logic
    1. Type theory

Recommendations

Generic constructors and eliminators from descriptions: type theory as a dependently typed internal DSL
WGP '14: Proceedings of the 10th ACM SIGPLAN workshop on Generic programming

Dependently typed languages with an "open" type theory introduce new datatypes using an axiomatic approach. Each new datatype introduces axioms for constructing values of the datatype, and an elimination axiom (which we call the standard eliminator) for ...
The next 700 data description languages

In the spirit of Landin, we present a calculus of dependent types to serve as the semantic foundation for a family of languages called data description languages. Such languages, which include pads, datascript, and packettypes, are designed to ...
Left recursion in Parsing Expression Grammars

Parsing Expression Grammars (PEGs) are a formalism that can describe all deterministic context-free languages through a set of rules that specify a top-down parser for some language. PEGs are easy to use, and there are efficient implementations of PEG ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

TyDe 2017: Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development

September 2017

40 pages

ISBN:9781450351836

DOI:10.1145/3122975

General Chairs:
Sam Lindley,
Brent Yorgey

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 September 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '17

Sponsor:

SIGPLAN

ICFP '17: ACM SIGPLAN International Conference on Functional Programming

September 3, 2017

Oxford, UK

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
116
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)1

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shankar NLucas Z(2024)Robust Verification of PEG Parser Interpreters2024 IEEE Security and Privacy Workshops (SPW)10.1109/SPW63631.2024.00022(180-191)Online publication date: 23-May-2024
https://doi.org/10.1109/SPW63631.2024.00022
Wallez TProtzenko JBhargavan KMeng WJensen CCremers CKirda E(2023)Comparse: Provably Secure Formats for Cryptographic ProtocolsProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623201(564-578)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623201
Chen ZLafont AO'Connor LKeller GMcLaughlin CJackson VRizkallah C(2023)Dargent: A Silver Bullet for Verified Data Layout RefinementProceedings of the ACM on Programming Languages10.1145/35712407:POPL(1369-1395)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571240
Egolf DLasser SFisher KPopescu AZdancewic S(2022)Verbatim++: verified, optimized, and semantically rich lexing with derivativesProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503694(27-39)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503694
Lucas ZLiu JAnantharaman PSmith S(2021)Research Report: Parsing PEGs with Length Fields in Software and Hardware2021 IEEE Security and Privacy Workshops (SPW)10.1109/SPW53761.2021.00026(128-133)Online publication date: May-2021
https://doi.org/10.1109/SPW53761.2021.00026
Xu XWu JWang YYin ZLi P(2021)Automatic Generation and Validation of Instruction Encoders and DecodersComputer Aided Verification10.1007/978-3-030-81688-9_34(728-751)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_34
Olmos SFernández MSteinberg MGadea AGunther EPagano MCavalcante EDantas FBatista T(2020)A formalisation of LEGv8 in AgdaProceedings of the 24th Brazilian Symposium on Context-Oriented Programming and Advanced Modularity10.1145/3427081.3427086(33-39)Online publication date: 19-Oct-2020
https://dl.acm.org/doi/10.1145/3427081.3427086
Blaudeau CShankar NBlanchette JHriţcu C(2020)A verified packrat parser interpreter for parsing expression grammarsProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373836(3-17)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373836
Delaware BSuriyakarn SPit-Claudel CYe QChlipala A(2019)Narcissus: correct-by-construction derivation of decoders and encoders from binary formatsProceedings of the ACM on Programming Languages10.1145/33416863:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341686
Ye QDelaware BMahboubi AMyreen M(2019)A verified protocol buffer compilerProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294105(222-233)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294105

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents