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

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 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.