{"id":"34ba9d35-e2a0-4d88-97e7-f016661eeb4a","arxiv_id":"2505.17335","paper_version":2,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":8.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"PulseParse, a separation-logic parser combinator library in F*, yields the first verified formalizations of CBOR, CDDL, and a COSE signing implementation, with non-malleability proofs and C and Rust extraction.","lead":"A Microsoft Research team built PulseParse, a verified parsing and serialization library for the CBOR binary format, its schema language CDDL, and the COSE signing standard, with formal proofs of memory safety and non-malleability. The tools generate C and Rust code, giving security-critical systems parsers that mathematically cannot accept ambiguous or malformed messages.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"CDDL semantics fidelity to RFC 8610 is the weakest load-bearing link; EverCDDL's well-formedness and unambiguity theorems are proven for the paper's own PEG/cut semantics, not for the RFC's prose semantics.","rationale":"The paper's main novelty is a verified toolchain for CBOR/CDDL/COSE with non-malleability proofs. The CBOR formalization (Theorem 3.1) is supported by machine-checked proofs, an explicit data model, and an injective serializer; I do not see a concrete flaw there. The CDDL layer is where the central claim becomes contingent: the paper defines a precise but nonstandard formal semantics (PEG and cuts) and proves unambiguity relative to that semantics. The security-relevant conclusion — that elaborating a CDDL schema yields an unambiguous, non-malleable format — is exactly as strong as the match between that formal semantics and RFC 8610. The paper's own need to correct the COSE CDDL, and its explicit limitations (no recursion, no indefinite-length, no floats), show that this is a genuine assumption rather than a routine equivalence. Still, the paper is transparent about these choices, the formal statements are accurately scoped, and the artifacts are available, so I do not think the reader's ACCEPT verdict should change; I would add the differential/formal cross-check of the semantics as the condition that would make the 'applied to CDDL' claim airtight.","tokens_in":29396,"tokens_out":15635,"duration_ms":131247,"concrete_test":"Run a differential test between EverCDDL-generated parsers and an independent executable semantics of RFC 8610 (e.g., the pycddl validator or a separate formalization in Coq/Isabelle) on the COSE schemas and the RFC 8610 Appendix A examples, with CBOR instances chosen to exercise ':' cuts, '?' under non-backtracking, and concatenations of map groups covered by Theorem 4.2. If EverCDDL accepts or rejects any schema/instance differently from the RFC oracle, the formal semantics is not the RFC semantics; if the verdicts match on the whole corpus, the concern is settled.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim of Section 4 (Theorem 4.4) is conditional on the formal semantics of CDDL chosen in Section 4.1: PEG-style non-backtracking alternatives, an exception-style interpretation of the ':' cut, and the determinism criterion for map groups (Theorem 4.2). RFC 8610 specifies CDDL in prose, not with a formal semantics; the paper itself had to patch the non-normative COSE CDDL to match the normative text (Section 5.2), showing that the RFC-to-model transfer is not automatic. If EverCDDL's reading of ':', '?', or map-group concatenation diverges from RFC 8610's intended semantics, then the tool can reject schemas the standard considers valid or accept schemas whose RFC-level semantics is ambiguous, in which case the generated-parser unambiguity/non-malleability guarantee does not transfer to standard CDDL. The formal theorems are machine-checked and sound for the paper's own semantics; the load-bearing assumption is the faithfulness of that semantics to the standard. This is the weakest link in the central claim; the CBOR result (Theorem 3.1) is independent and on much firmer ground.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":29646,"tokens_out":4498,"duration_ms":37086,"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":[{"comment":"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.","section":"§4.1, Theorem 4.4"},{"comment":"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.","section":"§2.2, §3, footnote 3"},{"comment":"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.","section":"§3.3, Theorem 3.1 and §3.2"}],"minor_comments":[{"comment":"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.","section":"§5.1, Table 1"},{"comment":"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.","section":"Figure 4"},{"comment":"The WebAuthn reference lists the consortium as 'Word Wide Web Consortium'; this should be 'World Wide Web Consortium'.","section":"References"},{"comment":"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.","section":"§5.1, Table 1"}],"recommendation":"major_revision","confidential_remarks":"The paper is technically strong and the machine-checked proofs are a major asset. My main concern is the faithfulness of the CDDL semantics to RFC 8610, which is exactly the kind of standard-interpretation issue that can invalidate a tool's real-world guarantees without invalidating its internal theorems. I would advise the editor to require the authors to add a clear conformance argument or test suite against RFC 8610 examples, and to soften or prove the constant-stack claim, before final acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis is a substantial, machine-checked systems verification paper, and the core is in better shape than most things we see. The genuinely new content is real: PulseParse's separation-logic combinator layer, the recursive parse_rec combinator with constant-stack validation for header-counted formats, and the first CBOR formalization proving deterministic CBOR non-malleable. The CBOR theorem (3.1) is on firm ground, since it is verified in F*/Pulse and the data model is defined from the byte representation upward. EverCDDL's elaboration into deterministic map groups is clever, and the COSE/DPE case studies show the toolchain works at scale, with functional correctness specs that actually say something meaningful about signatures.\n\nNow the soft spots, in proportion. The stress-test note is right: the CDDL results (4.3/4.4) are proven for the paper's own semantics—PEG-style non-backtracking alternatives, cut semantics for ':', and deterministic map groups—not for RFC 8610 prose. The paper is honest about this, and even had to patch the COSE CDDL to match normative prose. So the unambiguity guarantee transfers to standard CDDL only to the extent that their reading matches the RFC. That is a scope caveat, not a hidden flaw, and I don't think it should block publication; a referee should ask for a sharper statement about this transfer rather than new proofs. The other issues are minor: the constant-stack claim is not part of the formal proof (footnote 3 says so), the benchmarks are single runs without error bars, and floating point is unsupported. All disclosed.\n\nThe citation pattern is fine. The reliance on F*, Pulse, EverParse, and HACL* is real, but those are independent machine-checked artifacts; the new results are not circular. No fitted parameters anywhere.\n\nWho is this for: anyone working on verified parsers, binary format security, or protocol implementations in C/Rust. It is a strong candidate for a serious venue, and it deserves a full referee report. I would accept after minor revisions focusing on the CDDL semantics caveat, and perhaps a quick pass to add error bars or say why they were omitted.","headline":"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.","tokens_in":30166,"tokens_out":2389,"would_cite":true,"duration_ms":20195,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["formal verification","separation logic","CBOR","CDDL","COSE","non-malleability","parser combinators","constant-stack parsing"],"falsifier":"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.","tokens_in":29214,"feed_emoji":"🔐","tokens_out":6085,"duration_ms":44992,"temperature":0.7,"pith_summary":"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.","feed_headline":"Deterministic CBOR: one encoding, proven unique","feed_subtitle":"Verified parsers and serializers for CBOR, CDDL, and COSE now ship with machine-checked correctness in C and Rust.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines CBOR and the deterministic encoding subset whose non-malleability the paper proves.","marker":"Bormann and Hoffman 2020"},{"why":"Defines CDDL semantics that the paper formalizes and imposes well-formedness conditions on.","marker":"Birkholz et al. 2019"},{"why":"Supplies the specification combinators and the verified low-level formatting approach that PulseParse extends with separation logic.","marker":"Ramananandro et al. 2019"},{"why":"Provides the separation logic substrate and the prior DPE implementation that the paper's CDDL layer builds on.","marker":"[Ebner et al. 2025]"},{"why":"Gives the parsing expression grammar semantics that CDDL's non-backtracking alternatives are modeled on.","marker":"Ford 2004a"},{"why":"Provides the COSE standard whose CDDL schemas the paper adapts and verifies.","marker":"Schaad 2022"},{"why":"Supplies the verified cryptographic primitives used in the verified COSE signing application.","marker":"Zinzindohoué et al. 2017"}],"fun_headline_variants":["Verified CBOR: one encoding, proven non-malleable","Machine-checked parsers for CBOR, CDDL, and COSE","Non-malleable binary formats, proven in separation logic","Constant-stack parsing for recursive formats, formally verified","From CDDL to verified code: unambiguous, non-malleable"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Verified CBOR: one encoding, proven non-malleable","Machine-checked parsers for CBOR, CDDL, and COSE","Non-malleable binary formats, proven in separation logic","Constant-stack parsing for recursive formats, formally verified","From CDDL to verified code: unambiguous, non-malleable"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00024,"raw_usage":{"total_tokens":1580,"prompt_tokens":1072,"completion_tokens":508,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":688,"completion_tokens_details":{"reasoning_tokens":421}},"tokens_in":688,"tokens_out":508,"duration_ms":3700,"temperature":1.0,"reasoning_tokens":421,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T14:48:31.770938+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}