Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL and COSE
Tahina Ramananandro (RiSE: Research
in Software Engineering, Microsoft Research, Redmond, WA, USA)
Gabriel Ebner
(RiSE)
Guido Martínez
(RiSE)
Nikhil Swamy
(RiSE)
- Artifact
evaluated by the ACM CCS 2025 Artifact
Evaluation Committee.
We received the Distinguished Artifact Award! - Source code of the artifact, on GitHub
- Authors' version at arXiv
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 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 that ensure that they yield unambiguous, non-malleable formats, and implement EverCDDL, a tool that checks that a CDDL definition is well-formed, and then 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.