Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

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

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper proves that Deterministically Encoded CBOR has a unique byte representation and builds verified parsers and serializers for CBOR, CDDL, and COSE using separation logic.

desk verdict A machine-checked, artifact-backed verification paper whose CBOR result is rock-solid and whose CDDL result is proven for the authors' own semantics—a transparent scope caveat, not a fatal flaw. read the letter →

arxiv 2505.17335 v2 pith:ONPHLDV2 submitted 2025-05-22 cs.CR cs.PL

Tahina Ramananandro , Gabriel Ebner , Guido Martínez , Nikhil Swamy This is my paper · ORCID
classification cs.CRcs.PL
keywords formalverificationseparationlogicCBORCDDLCOSEnon-malleabilityparsercombinatorsconstant-stackparsing
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to make parsing and serializing security-critical binary formats provably safe, even in low-level languages like C and Rust. It presents PulseParse, a verified library of parser and serializer combinators written in separation logic, and uses it to formalize CBOR, the IETF binary data format. The central claims are that Deterministically Encoded CBOR has a unique byte representation for every CBOR value, and that a class of CDDL schema definitions can be checked for well-formedness so that any generated parser and serializer pair is unambiguous and non-malleable. These results matter because malleable encodings and parser ambiguities have caused real signature-forgery and confusion attacks in cryptographic protocols. The paper backs the claims with mechanically checked proofs and working code generation to C and Rust, applied to COSE signing and DICE attestation.

What carries the argument

The load-bearing mechanism is the parse_rec combinator, which turns a format into a header parser plus a child-count function and validates recursion with a counter loop rather than a call stack, enabling constant-stack validation of CBOR. Around it, PulseParse's separation-logic combinators use the predicate $ser\ s\ a\ v$ (byte array $a$ contains the serialization of $v$) and the magic-wand pattern $A \mathrel{\ast\!\!\rightarrow} B$ to give zero-copy accessors and copy writers without offset arithmetic. For CDDL, the key machinery is an elaboration algorithm that rewrites map groups into deterministic form, annotates tables with excluded key sets, checks disjointness of alternatives and footprints, and thereby guarantees the parser is injective and a serializer exists.

What would settle it

Compile a corpus of CDDL schemas that the IETF and other standards bodies actually publish, run the paper's tool on each, and compare against hand-written validators; finding a schema that the RFC's own prose treats as valid but the tool rejects as ambiguous, or two distinct byte strings that parse to the same high-level value through a generated parser, would refute the claim that elaboration captures the standard.

Watch

Extended reading notes

Core claim

On its own terms, the paper establishes Theorem 3.1: given any total strict order on raw CBOR bytes, the subset of raw CBOR data with minimal integer byte representations and map entries sorted by that order forms a data model for CBOR that is in bijection with a recursive view type of CBOR items, and because the serializer for that representation is injective, Deterministically Encoded CBOR is non-malleable. It also establishes Theorem 4.4: for any CDDL type whose elaboration is defined by the paper's algorithm, the associated parser specification is injective and a serializer specification exists, so the CDDL definition yields an unambiguous, non-malleable format. The same development proves a structural class of recursive formats can be validated in constant stack space, and reports verified implementations, extracted to C and safe Rust, for CBOR, for CDDL-generated schemas, and for COSE signature objects.

Load-bearing premise

The paper's formal semantics for CDDL—PEG-style non-backtracking alternatives, cut semantics for ':' labels, and the determinism conditions of Theorem 4.2—must match the intended meaning of RFC 8610; the authors had to patch the COSE CDDL to align with its normative prose, showing the mapping is not automatic.

Editorial extensions

If this is right

  • Deterministically Encoded CBOR can be safely used in protocols that sign or hash byte representations, since each CBOR value has exactly one encoding within that subset.
  • Protocol schemas written in CDDL and accepted by the paper's tool can be compiled to C or safe Rust parsers and serializers whose memory safety, arithmetic safety, and functional correctness are machine-checked.
  • Recursive formats that satisfy the header-determined child count condition, like CBOR, can be validated in constant stack space, removing a class of memory-exhaustion attacks.
  • Existing security standards expressed in CDDL, such as COSE and DPE, can be adapted with minor edits to obtain verified implementations.
  • The paper's COSE integration shows the verified toolchain composes with verified cryptography, producing end-to-end guarantees that a signature's payload matches the to-be-signed bytes.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same elaboration approach could be applied to other PEG-like schema languages for JSON or ASN.1, since non-malleability and unambiguity conditions are format-independent once a canonical encoding exists.
  • The paper's choice to reject indefinite-length CBOR and recursion beyond fixed unrolling is a design position: the toolchain trades standards completeness for constant-stack security, and a future extension could support bounded recursion with depth tracking.
  • If the CDDL semantics diverge from RFC 8610 in cut placement or determinism, the tool would be a stricter validator than the standard, which could wrongly reject interoperable schemas; testing against a corpus of deployed CDDL schemas would reveal how often this matters.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents PulseParse, a verified parser/serializer combinator library in F* and Pulse, and uses it to build EverCBOR, a verified CBOR validator/parser/serializer, and EverCDDL, a tool that checks CDDL schemas for well-formedness and generates verified parsers and serializers. The central formal results are that deterministically encoded CBOR is non-malleable (Theorem 3.1) and that elaborated CDDL types yield injective parsers with corresponding serializers (Theorem 4.4). The paper also reports on generated C and Rust code, evaluates performance against QCBOR and TinyCBOR, and applies the toolchain to COSE signing and DPE message handling. All theorems are machine-checked in F*/Pulse, and the code artifacts are integrated into EverParse.

Significance. If the results stand, this is a substantial contribution to verified low-level parsing: it provides the first mechanized formalization of CBOR's deterministic encoding, the first formal account of CDDL's ambiguity conditions, and a credible path from standard prose to verified C/Rust code. The paper's strengths include machine-checked proofs, user-visible code artifacts, and a concrete integration with HACL* to obtain a verified COSE signing path. The benchmarks, while preliminary, show that verified code can be competitive with unverified CBOR libraries. The main caveat is that the CDDL theorems are proven for the paper's own formal semantics, not for the RFC 8610 prose semantics, so the transfer to the standard is a non-automatic step that needs explicit justification.

major comments (3)
  1. [§4.1, Theorem 4.4] The central CDDL guarantee is conditional on the formal semantics chosen in §4.1: PEG-style non-backtracking alternatives, the exception-style reading of the ':' cut, and the determinism condition for map groups in Theorem 4.2. RFC 8610 describes CDDL in prose, not with these constructs. The paper itself reports in §5.2 that the non-normative COSE CDDL had to be modified to match the normative prose, which shows that the RFC-to-model transfer is not automatic. To make the claim that EverCDDL produces unambiguous, non-malleable parsers for CDDL, the authors need to provide explicit evidence that their semantics agrees with the intended semantics of RFC 8610 on the relevant constructs. A concrete test would be to run EverCDDL over the examples and corner cases in RFC 8610 and to list any schemas for which the tool's accepted/rejected behavior differs from the RFC's intended meaning. Without such evidence, Theorem 4.4 is sound for the authors' dialect but does not yet transfer to standard CDDL.
  2. [§2.2, §3, footnote 3] The abstract and §2 claim that recursive formats such as CBOR can be parsed and validated in constant stack space, and this is presented as a security property against adversarial inputs. Footnote 3 correctly states that stack-space usage is outside the scope of the formal proof because the logic does not provide a way to specify it. Since the constant-stack claim is a load-bearing part of the security story, the paper should either formalize a stack bound for the generated code or explicitly scope the claim as an informal, implementation-level observation based on the absence of recursive calls. As written, the reader may infer that the constant-stack property is machine-checked, which it is not.
  3. [§3.3, Theorem 3.1 and §3.2] Theorem 3.1 is stated for an arbitrary total strict order on raw CBOR data, and the paper then instantiates it with the lexicographic byte order. The non-malleability guarantee for 'Deterministically Encoded CBOR' therefore depends on whether this lexicographic byte order is exactly the order mandated by RFC 8949's deterministic encoding rules, including the treatment of keys with different lengths. The paper's brief comparison with the 'length-first' ordering of RFC 7049 is helpful, but it would strengthen the paper to quote the RFC's ordering rule and state explicitly why the lexicographic byte order satisfies it. If the two orders disagree in some corner case, the generated serializer could emit CBOR that is not compliant with the deterministic encoding, even though it is non-malleable with respect to the paper's own order.
minor comments (4)
  1. [§5.1, Table 1] The benchmark table reports single values per configuration without repetitions, error bars, or variance information. The qualitative conclusions may be correct, but the quantitative comparisons should be labeled as preliminary single-run measurements.
  2. [Figure 4] The figure and the surrounding text use both 'synth_cbor' and 'synth_payload' for the same function, and the earlier snippet says 'count_payload' while the later snippet defines 'count_payload' differently; please unify the notation.
  3. [References] The WebAuthn reference lists the consortium as 'Word Wide Web Consortium'; this should be 'World Wide Web Consortium'.
  4. [§5.1, Table 1] For the Map benchmark row, the table shows three numbers but the column headers ('V/P', 'S') do not make clear which value corresponds to which library or whether these are lookup times; please clarify the table caption and column semantics.

Circularity Check

0 steps flagged · score 0.0 of 10

No meaningful circularity; the formal theorems are proved for explicitly stated semantics, and toolchain self-citations are to independently verified artifacts.

full rationale

All central results are proven in F*/Pulse against definitions given in the paper. Theorem 3.1 is not a renaming: cbor is defined as raw_data satisfying minimal-integer and sorted-map constraints, and the bijection with the view type is shown by induction on sizes, with a size function ruling out cycles. Non-malleability follows from injectivity of the serializer, not from an imported uniqueness theorem. In Section 4, CDDL's semantics (PEG non-backtracking, cut-as-exception, deterministic map groups) are explicitly chosen and formalized, and Theorem 4.4 is a machine-checked property of that formal model. The fidelity of these choices to RFC 8610 is an explicit assumption, not a conclusion, so a mismatch would be a correctness or soundness risk rather than circularity. The paper's self-citations (EverParse combinators, Pulse, F*, Karamel, HACL*) are to machine-checked or code-reproduced artifacts, and none is used to import an unverified premise that equals the target result. The stated limitations (no floats, no recursive CDDL, deterministic-CBOR-only parser, stack usage outside the formal proof) narrow the claims honestly and do not hide a fitted parameter or a definitional equivalence.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The central results introduce no fitted numerical parameters and no new physical or abstract entities. The main unproved premises are toolchain soundness and fidelity of the formal model to the IETF standards; the paper explicitly scopes out floats, indefinite-length CBOR, and recursive CDDL.

assumptions (3)
  • domain assumption Soundness of F*, Pulse, Karamel, and the F* standard library.
    All machine-checked guarantees rely on the trusted base of the proof assistant and the code generator to C and Rust; a soundness bug would invalidate the verified claims.
  • ad hoc to paper Theorem 2.1 generalizes to the CBOR and CDDL validators with constant stack usage.
    The paper states this theorem and validates it by design of the loop-based validator in Appendix B, but footnote 3 admits stack usage is outside the formal proof.
  • domain assumption The formal semantics of CBOR and CDDL match the corresponding IETF RFCs.
    The theorems prove properties of the authors' formal model, not of the English standard text; mismatches (floats, indefinite lengths, recursive CDDL) are deliberately excluded or adapted.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE." pith.science (2026). https://pith.science/paper/ONPHLDV2

@misc{pith2026250517335,
  author       = {Pith},
  title        = {Pith review of: Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ONPHLDV2}},
  note         = {Machine review of arXiv:2505.17335}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2505.17335 by the authors.

Figure 1
Figure 1. Architecture of our contributions In this context, formally proven parser generators have been used to secure critical, commercial software including in Microsoft’s OS and cloud infrastructure [Swamy et al. 2022]. However, such uses have focused primarily on validating flat, tag-length-value encodings of network packet formats. We aim to broaden the scope of secure, low-level binary formatting tools, enabling them t… view at source ↗
Figure 2
Figure 2. The data model for CBOR items We now turn to our formalization of CBOR, making essential use of PulseParse’s support for recursion, and abstract separation logic specifications. 3 EverCBOR: A Verified Generic CBOR Parser and Serializer JSON is a ubiquitous textual representation of data. However, it comes with a vast collection of issues, some related to efficiency (whitespace, decimal integers, etc.), others relate… view at source ↗
Figure 3
Figure 3. Representing CBOR items as bytes 3 bits of which describe the type of the CBOR item. The remaining 5 bits, called “additional information”, encode an integer from 0 to 31: additional info 0 to 23 encode a nonnegative integer (or a simple value) of this value. For 64-bit integers, info 24, 25, 26 and 27 encode the fact that the integer is encoded in the next 1, 2, 4 and 8 bytes respectively. Thus, integers are encode… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: F★ inductive type for raw CBOR data The we apply parse_rec to raw CBOR bytes, where count_payload reads the header to compute the number of items of each case; parse_header is a simple parser for the header bytes, and synth_payload constructs a raw_data from the list o…
Figure 5
Figure 5. Figure 5: Annotating map group tables with excluded sets of keys. For two [PITH_FULL_IMAGE:figures/full_fig_p011_5.png]
Figure 6
Figure 6. Figure 6: C validator for raw CBOR bytes This datatype extracts to C as a tagged union, with ref and narray extracting as C pointer types. Then, using the copy writer combinators we defined in PulseParse, we implement a recursive serializer from values of this datatype. The impl…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Canonicalization Failures as a Recurring Vulnerability Class: Representation Divergence in Cryptographic Systems and Its Avoidance

    cs.CR 2026-08 conditional novelty 4.0 of 10

    A cross-ecosystem taxonomy unifies canonicalization failures into one violated uniqueness condition with two break directions, plus a review checklist.

Reference graph

Works this paper leans on

3 extracted references · cited by 1 Pith paper

  1. [1482]

    Reynolds

    https://www.usenix.org/conference/usenixsecurity19/presentation/delignat- lavaud John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS ’02). IEEE Computer Society, USA, 55–74. Jim Schaad. 2022. CBOR Object Signing and Encryption (COSE): Stru...

    doi:10.17487/rfc9052 2002

  2. [2016]

    In 43rd ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL)

    Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 256–270. https://www.fstar-lang.org/papers/mumon/ Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, and Arti Gupta. 2022. Hardenin...

    arXiv 2022

  3. [2024]

    In 2024 IEEE Symposium on Security and Privacy (SP)

    ARMOR: A Formally Verified Implementation of X.509 Certificate Chain Validation. In 2024 IEEE Symposium on Security and Privacy (SP) . 1462–1480. doi:10. 1109/SP54263.2024.00220 Christian Decker and Roger Wattenhofer. 2014. Bitcoin transaction malleability and MtGox. In European Symposium on Research in Computer Security. Springer, 313–326. Benjamin Delaw...

    arXiv 2019

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.