TL;DR
This paper introduces PulseParse, a verified library for secure parsing and serialization of binary data formats like CBOR, CDDL, and COSE, ensuring non-malleability and security in low-level languages.
Contribution
It presents PulseParse, a separation logic-based verified parser library supporting recursive formats, and formalizes CBOR and CDDL, enabling verified implementations of standards like COSE.
Findings
PulseParse supports recursive formats with constant stack space.
CBOR's deterministic fragment is proven non-malleable.
Verified parsers for COSE and DICE protocols are generated.
Abstract
Incorrect handling of security-critical data formats, particularly in low-level languages, are the root cause of many security vulnerabilities. Provably correct parsing and serialization tools that target languages like C can help. Towards this end, we present PulseParse, a library of verified parser and serializer combinators for non-malleable binary formats. Specifications and proofs in PulseParse are in separation logic, offering a more abstract and compositional interface, with full support for data validation, parsing, and serialization. PulseParse also supports a class of recursive formats -- with a focus on security and handling adversarial inputs, we show how to parse such formats with only a constant amount of stack space. We use PulseParse at scale by providing the first formalization of CBOR, a recursive, binary data format standard, with growing adoption in various…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
