@inproceedings{ramananandro2025secure,
author = {Ramananandro, Tahina and Ebner, Gabriel and Martínez, Guido and Swamy, Nikhil},
title = {Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE},
organization = {ACM SIGSAC},
booktitle = {2025 Computer and Communications Security},
year = {2025},
month = {October},
abstract = {Update 2025-10-15: Our artifact evaluated by the ACM CCS 2025 AEC, companion to our paper, has received the ACM CCS 2025 Distinguished Artifact Award!

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, as well as an artifact evaluated by the ACM CCS 2025 AEC.},
url = {http://approjects.co.za/?big=en-us/research/publication/evercbor/},
}