LIPIcs.ITP.2021.30.pdf
- Filesize: 0.62 MB
- 17 pages
Document
Specifying Message Formats with Contiguity Types
Author
-
Part of:
Volume:
12th International Conference on Interactive Theorem Proving (ITP 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-06-21
File
Document Identifiers
Acknowledgements
This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA). The views, opinions and/or findings expressed are those of the author and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. Discussions with Robby, Luke Ryon, Dave Greve, David Hardin, Magnus Myreen, and Michael Norrish have greatly improved this work.
Cite As Get BibTex
Konrad Slind. Specifying Message Formats with Contiguity Types. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.30
Abstract
We introduce Contiguity Types, a formalism for network message formats, aimed especially at self-describing formats. Contiguity types provide an intermediate layer between programming language data structures and messages, offering a helpful setting from which to automatically generate decoders, filters, and message generators. The syntax and semantics of contiguity types are defined and used to prove the correctness of a matching algorithm which has the flavour of a parser generator. The matcher has been used to enforce semantic well-formedness conditions on complex message formats for an autonomous unmanned avionics system.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
Keywords
- Logic
- verification
- formal language theory
- message format languages
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
Supplementary Materials
- HOL4 formalization may be found at:
-
Model
https://github.com/loonwerks/splat/blob/monitors/contig/abscontigScript.sml
browse
archived version
References
-
Franz Baader and Tobias Nipkow. Term Rewriting and all that. Cambridge University Press, 1998.
- Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala. Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang., 3(ICFP):82:1-82:29, 2019. URL: https://doi.org/10.1145/3341686.
-
Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. CACM, 22(8):465-476, 1979.
- Kathleen Fisher, Yitzhak Mandelbaum, and David Walker. The next 700 data description languages. J. ACM, 57(2), 2010. URL: https://doi.org/10.1145/1667053.1667059.
- David S. Hardin, Konrad Slind, Mark Bortz, James Potts, and Scott Owens. A high-assurance, high-performance hardware-based cross-domain system. In Amund Skavhaug, Jérémie Guiochet, and Friedemann Bitsch, editors, Computer Safety, Reliability, and Security - 35th International Conference, SAFECOMP 2016, Trondheim, Norway, September 21-23, 2016, Proceedings, volume 9922 of Lecture Notes in Computer Science, pages 102-113. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-45477-1_9.
-
John Harrison. Inductive definitions: automation and application. In E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, editors, Proceedings of the 1995 International Workshop on Higher Order Logic theorem proving and its applications, number 971 in LNCS, pages 200-213, Aspen Grove, Utah, 1995. Springer-Verlag.
- Trevor Jim and Yitzhak Mandelbaum. A new method for dependent parsing. In Gilles Barthe, editor, Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6602 of Lecture Notes in Computer Science, pages 378-397. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19718-5_20.
-
Donald E. Knuth. Semantics of context-free languages. In In Mathematical Systems Theory, pages 127-145, 1968.
- Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179-191. ACM Press, 2014. URL: https://doi.org/10.1145/2535838.2535841.
- Prashanth Mundkur, Linda Briesemeister, Natarajan Shankar, Prashant Anantharaman, Sameed Ali, Zephyr Lucas, and Sean Smith. Research report: The parsley data format definition language. In 2020 IEEE Security and Privacy Workshops (SPW), pages 300-307, 2020. URL: https://doi.org/10.1109/SPW50608.2020.00064.
- Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. Everparse: Verified secure zero-copy parsers for authenticated message formats. In Nadia Heninger and Patrick Traynor, editors, 28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019, pages 1465-1482. USENIX Association, 2019. URL: https://www.usenix.org/conference/usenixsecurity19/presentation/delignat-lavaud.
-
Dennis Ritchie. The development of the C language. https://www.bell-labs.com/usr/dmr/www/chist.html.
- Christopher Strachey. Fundamental concepts in programming languages. High. Order Symb. Comput., 13(1/2):11-49, 2000. URL: https://doi.org/10.1023/A:1010000313106.