Generic packet descriptions: Verified Parsing and Pretty Printing of Low-Level Data

Marcell van Geest; Wouter Swierstra

doi:10.1145/3122975.3122979

Generic packet descriptions: Verified Parsing and Pretty Printing of Low-Level Data

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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.

Original language	English
Title of host publication	TyDe 2017
Subtitle of host publication	Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development
Publisher	Association for Computing Machinery
Pages	30-40
Number of pages	11
ISBN (Print)	978-1-4503-5183-6
DOIs	https://doi.org/10.1145/3122975.3122979
Publication status	Published - 3 Sept 2017

Keywords

data type generic programming
dependent types
parsing
pretty printing

Access to Document

10.1145/3122975.3122979

7Final published version, 655 KB

Cite this

@inproceedings{05451680b0924b6a9c4e534e48af44e1,

title = "Generic packet descriptions: Verified Parsing and Pretty Printing of Low-Level Data",

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; thecorresponding 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.",

keywords = "data type generic programming, dependent types, parsing, pretty printing",

author = "{van Geest}, Marcell and Wouter Swierstra",

year = "2017",

month = sep,

day = "3",

doi = "10.1145/3122975.3122979",

language = "English",

isbn = "978-1-4503-5183-6",

pages = "30--40",

booktitle = "TyDe 2017",

publisher = "Association for Computing Machinery",

address = "United States",

}

Generic packet descriptions: Verified Parsing and Pretty Printing of Low-Level Data. / van Geest, Marcell; Swierstra, Wouter.
TyDe 2017: Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development. Association for Computing Machinery, 2017. p. 30-40.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Generic packet descriptions

T2 - Verified Parsing and Pretty Printing of Low-Level Data

AU - van Geest, Marcell

AU - Swierstra, Wouter

PY - 2017/9/3

Y1 - 2017/9/3

N2 - 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; thecorresponding 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.

AB - 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; thecorresponding 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.

KW - data type generic programming

KW - dependent types

KW - parsing

KW - pretty printing

U2 - 10.1145/3122975.3122979

DO - 10.1145/3122975.3122979

M3 - Conference contribution

SN - 978-1-4503-5183-6

SP - 30

EP - 40

BT - TyDe 2017

PB - Association for Computing Machinery

ER -

Generic packet descriptions: Verified Parsing and Pretty Printing of Low-Level Data

Abstract

Keywords

Access to Document

Fingerprint

Cite this