research-article

A verified protocol buffer compiler

Authors:

Benjamin DelawareAuthors Info & Claims

CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 222 - 233

https://doi.org/10.1145/3293880.3294105

Published: 14 January 2019 Publication History

Abstract

The code responsible for serializing and deserializing untrusted external data is a vital component of any software that communicates with the outside world, as any bugs in these components can compromise the entire system. This is particularly true for verified systems which rely on trusted code to process external data, as any defects in the parsing code can invalidate any formal proofs about the system. One way to reduce the trusted code base of these systems is to use interface generators like Protocol Buffer and ASN.1 to generate serializers and deserializers from data descriptors. Of course, these generators are not immune to bugs.

In this work, we formally verify a compiler for a realistic subset of the popular Protocol Buffer serialization format using the Coq proof assistant, proving once and for all the correctness of every generated serializer and deserializer. One of the challenges we had to overcome was the extreme flexibility of the Protocol Buffer format: the same source data can be encoded in an infinite number of ways, and the deserializer must faithfully recover the original source value from each. We have validated our verified system using the official conformance tests.

References

[1]

2016. CVE-2016-5080. Available from MITRE, CVE-ID CVE-2016-5080. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2016-5080

[2]

2017. CVE-2017-9023. Available from MITRE, CVE-ID CVE-2017-9023. https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2017-9023

[3]

2018. CVE-2018-11058. Available from MITRE, CVE-ID CVE-2018-11058. https://cve.mitre.org/cgi-bin/cvename.cgi?name= CVE-2018-11058

[4]

Apache Software Foundation. 2016. Apache Avro 1.8.0 Documentation. http://avro.apache.org/docs/current/ {Accessed May 04, 2016}.

[5]

Aditi Barthwal and Michael Norrish. 2009. Verified, Executable Parsing. In Programming Languages and Systems, Giuseppe Castagna (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 160–174.

Digital Library

[6]

Tim Bray. 2017. The JavaScript Object Notation (JSON) Data Interchange Format. RFC 8259.

[7]

Tim Bray, Jean Paoli, C Michael Sperberg-McQueen, Eve Maler, and François Yergeau. 1997. Extensible Markup Language (XML). World Wide Web Journal 2, 4 (1997), 27–66.

Digital Library

[8]

Adam Chlipala. 2013. Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant. MIT Press.

Digital Library

[9]

Nathan Collins, Mark Tullsen, Aaron Tomb, and Lee Pike. 2017. Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System. In Embedded Security in Cars (ESCARS).

[10]

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala. {n. d.}. NARCISSUS: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. arXiv: 1803.04870

[11]

Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb. 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench. In Verified Software. Theories, Tools, and Experiments, Sandrine Blazy and Marsha Chechik (Eds.). Springer International Publishing, Cham, 56–72.

[12]

Olivier Dubuisson. 2001. ASN. 1: communication between heterogeneous systems. Morgan Kaufmann.

Digital Library

[13]

Pedro Fonseca, Kaiyuan Zhang, Xi Wang, and Arvind Krishnamurthy. 2017. An Empirical Study on the Correctness of Formally Verified Distributed Systems. In Proceedings of the Twelfth European Conference on Computer Systems (EuroSys ’17). ACM, New York, NY, USA, 328–343.

Digital Library

[14]

Python Software Foundation. 2018. Pickle - Python object serialization. https://docs.python.org/3/library/pickle.html

[15]

Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. 2012. Validating LR(1) Parsers. In Programming Languages and Systems, Helmut Seidl (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 397–416.

Digital Library

[16]

Adam Koprowski and Henri Binsztok. 2011. TRX: A Formally Verified Parser Interpreter. Logical Methods in Computer Science 7, 2 (2011).

[17]

Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. 2018. The OCaml system release 4.07 Documentation and user’s manual - Module Marshal. https://caml. inria.fr/pub/docs/manual-ocaml/libref/Marshal.html

[18]

P. Mockapetris. 1987. Domain names - implementation and specification. RFC 1035.

Digital Library

[19]

Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, and Edward Gan. 2012. RockSalt: Better, Faster, Stronger SFI for the x86. SIGPLAN Not. 47, 6 (June 2012), 395–404.

Digital Library

[20]

Jon Postel. 1981. Internet Protocol. RFC 791.

[21]

Jon Postel. 1981. Transmission Control Protocol. RFC 793.

[22]

Keith Simmons. 2016. Cheerios. (2016). courses.cs.washington.edu/courses/cse599w/16sp/projects/cheerios.pdf.

[23]

Raj Srinivasan. 1995. XDR: External data representation standard. Technical Report.

Digital Library

[24]

Gang Tan and Greg Morrisett. 2018. Bidirectional Grammars for Machine-Code Decoding and Encoding. Journal of Automated Reasoning 60, 3 (01 Mar 2018), 257–277.

Digital Library

[25]

The Coq Development Team. 2018. The Coq proof assistant reference manual, version 8.8.1. (2018).

[26]

Marcell van Geest and Wouter Swierstra. 2017. Generic Packet Descriptions: Verified Parsing and Pretty Printing of Low-Level Data. In Proceedings of the 2Nd ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2017). ACM, 30–40.

Digital Library

[27]

James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: A Framework for Implementing and Formally Verifying Distributed Systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM, New York, NY, USA, 357–368.

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
Ciobâcă ŞGratie D(2024)Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case StudyIntegrated Formal Methods10.1007/978-3-031-76554-4_3(35-52)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_3
Nepiyushchikh DBlekanov ITarasov NMaksimov A(2024)Methods of User Opinion Data Crawling in Web 2.0 Social Network DiscussionsSocial Computing and Social Media10.1007/978-3-031-61281-7_5(72-81)Online publication date: 1-Jun-2024
https://doi.org/10.1007/978-3-031-61281-7_5
Show More Cited By

Index Terms

A verified protocol buffer compiler
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Source code generation
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Software verification
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Tactics for Proving Separation Logic Assertion in Coq Proof Assistant
ICVISP 2019: Proceedings of the 3rd International Conference on Vision, Image and Signal Processing

The verification of the correctness of large programs, particularly operating systems is an unmanageable but important endeavor. we are interested in verifying C programs with formal methods, the logic is separation logic, a Hoare-style program logic. ...
Verified peephole optimizations for CompCert
PLDI '16

Transformations over assembly code are common in many compilers. These transformations are also some of the most bug-dense compiler components. Such bugs could be elim- inated by formally verifying the compiler, but state-of-the- art formally verified ...
Verifying verified code
Abstract
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow-up case study that explores the methodology from the perspective of three research ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2019

261 pages

ISBN:9781450362221

DOI:10.1145/3293880

Program Chairs:
Assia Mahboubi
INRIA, France
,
Magnus O. Myreen
Chalmers University of Technology, Sweden

Copyright © 2019 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 ACM 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

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Available

Author Tags

Qualifiers

Research-article

Conference

CPP '19

Sponsor:

SIGPLAN

CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 14 - 15, 2019

Cascais, Portugal

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
224
Total Downloads

Downloads (Last 12 months)37
Downloads (Last 6 weeks)5

Reflects downloads up to 14 Dec 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
Ciobâcă ŞGratie D(2024)Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case StudyIntegrated Formal Methods10.1007/978-3-031-76554-4_3(35-52)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_3
Nepiyushchikh DBlekanov ITarasov NMaksimov A(2024)Methods of User Opinion Data Crawling in Web 2.0 Social Network DiscussionsSocial Computing and Social Media10.1007/978-3-031-61281-7_5(72-81)Online publication date: 1-Jun-2024
https://doi.org/10.1007/978-3-031-61281-7_5
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
Ni HDelignat-Lavaud AFournet CRamananandro TSwamy NKrebbers RTraytel DPientka BZdancewic S(2023)ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DERProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575684(275-289)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575684
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
Swamy NRamananandro TRastogi ASpiridonova INi HMalloy DVazquez JTang MCardona OGupta AJhala RDillig I(2022)Hardening attack surfaces with formally proven binary format parsersProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523708(31-45)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523708
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
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
Ramananandro TDelignat-Lavaud AFournet CSwamy NChajed TKobeissi NProtzenko JHeninger NTraynor P(2019)EverparseProceedings of the 28th USENIX Conference on Security Symposium10.5555/3361338.3361440(1465-1482)Online publication date: 14-Aug-2019
https://dl.acm.org/doi/10.5555/3361338.3361440
Show More Cited By

View Options

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