Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

Update 2025-10-15: Our artifact evaluated by the ACM CCS 2025 AEC (opens in new tab), companion to our paper, has received the ACM CCS 2025 Distinguished Artifact Award (opens in new tab)!

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 other industrial standards. We prove that the deterministic fragment of CBOR is non-malleable and provide EverCBOR, a verified library in both C and Rust to validate, parse, and serialize CBOR objects implemented using PulseParse. Next, we provide the first formalization of CDDL, a schema definition language for CBOR. We identify well-formedness conditions on CDDL definitions to ensure that they yield unambiguous, non-malleable formats, and implement EverCDDL, a tool that checks the well-formedness of a CDDL definition and produces verified parsers and serializers for it.

To evaluate our work, we use EverCDDL to generate verified parsers and serializers for various security-critical applications. Notably, we build a formally verified implementation of COSE signing, a standard for cryptographically signed objects. We also use our toolchain to generate verified code for other standards specified in CDDL, including DICE Protection Environment, a secure boot protocol standard.

We conclude that PulseParse offers a powerful new foundation on which to build verified, secure data formatting tools for a range of applications.

This paper comes with an extended version published on arXiv (opens in new tab), as well as an artifact evaluated by the ACM CCS 2025 AEC (opens in new tab).