Document Open Access Logo

Specifying Message Formats with Contiguity Types

Author Konrad Slind

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2021.30.pdf
  • Filesize: 0.62 MB
  • 17 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

Konrad Slind
  • Trusted Systems Group, Collins Aerospace, USA

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.

Supplementary Materials

References

  1. Franz Baader and Tobias Nipkow. Term Rewriting and all that. Cambridge University Press, 1998. Google Scholar
  2. 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.
  3. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. CACM, 22(8):465-476, 1979. Google Scholar
  4. 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.
  5. 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.
  6. 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. Google Scholar
  7. 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.
  8. Donald E. Knuth. Semantics of context-free languages. In In Mathematical Systems Theory, pages 127-145, 1968. Google Scholar
  9. 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.
  10. 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.
  11. 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.
  12. Dennis Ritchie. The development of the C language. https://www.bell-labs.com/usr/dmr/www/chist.html. Google Scholar
  13. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact