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

• URL: http://arxiv.org/abs/2505.17335v2
• Date: Thu, 17 Jul 2025 15:50:49 GMT
• Title: Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
• Abstract summary: We present PulseParse, a library of verified and serializers for non-malleable binary formats.<n>We use PulseParse at scale by providing the first formalization of CBOR, a binary data format standard.<n>We show how to parse formats with only a constant amount of stack space.
• Score: 1.2419340000421064
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• SeriCrypt: An LLM-Driven Context-Aware Serialization Framework for Cryptographic Protocols [3.5793925951831125]
  SeriCrypt is an LLM-driven, context-aware serialization framework for cryptographic protocols.<n>It employs a large language model to extract field constraints, state dependencies, and cryptographic computation rules from unstructured protocol specifications.<n>A protocol-agnostic execution engine parses CDSL declarations, automating field value resolution, cryptographic primitive invocation, and stream serialization.
  arXiv  Detail & Related papers  (2026-08-25T12:46:34Z)
• VUPER: Verified ASN.1 UPER Parser [19.74234190254681]
  We present VUPER, a framework for generating verified ASN.1 UPERs.<n>VUPER uncovers 20 types of inconsistencies in popular compilers and demonstrates stricter compliance with ASN.1 UPER standards.<n>We demonstrate concrete attacks by exploiting these vulnerabilities.
  arXiv  Detail & Related papers  (2026-08-10T03:47:38Z)
• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• Misquoted No More: Securely Extracting F* Programs with IO [0.3848364262836075]
  Shallow embeddings that use monads to represent effects are popular in proof-oriented languages.<n>Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C.<n>We build on this idea, but limit the use of translation validation to a first extraction step.
  arXiv  Detail & Related papers  (2026-02-23T15:37:18Z)
• Residual Context Diffusion Language Models [90.07635240595926]
  Residual Context Diffusion (RCD) is a module that converts discarded token representations into contextual residuals and injects them back for the next denoising step.<n>RCD consistently improves frontier dLLMs by 5-10 points in accuracy with minimal extra computation overhead.
  arXiv  Detail & Related papers  (2026-01-30T13:16:32Z)
• Text2Mem: A Unified Memory Operation Language for Memory Operating System [59.082901444153684]
  We introduce Text2Mem, a unified memory operation language for model agents.<n>Text2Mem provides a standardized pathway from natural correctness reliable execution.
  arXiv  Detail & Related papers  (2025-09-14T07:30:09Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
  arXiv  Detail & Related papers  (2025-06-24T13:42:59Z)
• Large Language Models for Validating Network Protocol Parsers [8.007994733372675]
  Protocol standards are typically written in natural language, whereas implementations are in source code.<n>We propose PARVAL, a framework built on large language models (LLMs)<n>It transforms both protocol standards and their implementations into a unified intermediate representation, referred to as format specifications.<n>It successfully identifies inconsistencies between the implementation and its RFC standard, achieving a low false positive rate of 5.6%.
  arXiv  Detail & Related papers  (2025-04-18T07:09:56Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  We introduce a type-constrained decoding approach that leverages type systems to guide code generation.<n>For this purpose, we develop novel prefix automata and a search over inhabitable types, forming a sound approach to enforce well-typedness on LLM-generated code.<n>Our approach reduces compilation errors by more than half and significantly increases functional correctness in code synthesis, translation, and repair tasks.
  arXiv  Detail & Related papers  (2025-04-12T15:03:00Z)
• Verified invertible lexer using regular expressions and DFAs [0.0]
  In this project, we explore the concept of invertibility applied to serialisation and lexing frameworks.<n>While serialisation is the process of taking a data structure and writing it to a bit array, lexing is the process of reading a stream of characters and splitting them into tokens.
  arXiv  Detail & Related papers  (2024-12-18T08:03:17Z)
• Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study [0.0]
  ASN.1 is a language for describing data structures widely employed in ground and space telecommunications.<n>ACN can be used along ASN.1 to describe complex binary formats and legacy protocols.<n>We show how to port an ASN.1/ACN code generator to generate Scala code.<n>We then enhance the generator to emit not only the executable code but also strong enough pre-conditions, post-conditions, and lemmas for inductive proofs.
  arXiv  Detail & Related papers  (2024-12-10T06:54:42Z)
• SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
  We propose SVTRv2, a CTC model endowed with the ability to handle text irregularities and model linguistic context.<n>We extensively evaluate SVTRv2 in both standard and recent challenging benchmarks.<n> SVTRv2 surpasses most EDTRs across the scenarios in terms of accuracy and inference speed.
  arXiv  Detail & Related papers  (2024-11-24T14:21:35Z)
• StrTune: Data Dependence-based Code Slicing for Binary Similarity Detection with Fine-tuned Representation [5.41477941455399]
  BCSD can address binary tasks such as malicious code snippets identification and binary patch analysis by comparing code patterns. Because binaries are compiled with different compilation configurations, existing approaches still face notable limitations when comparing binary similarity. We propose StrTune, which slices binary code based on data dependence and perform slice-level fine-tuning.
  arXiv  Detail & Related papers  (2024-11-19T12:20:08Z)
• 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers [5.102523342662388]
  3DGen is a framework that makes use of AI agents to transform mixed informal input into format specifications in a language called 3D. 3DGen produces a 3D specification that conforms to a test suite, and which yields safe, efficient, provably correct, parsing code in C.
  arXiv  Detail & Related papers  (2024-04-16T07:53:28Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  We propose a novel framework called FoC to Figure out the Cryptographic functions in stripped binaries.<n>We first build a binary large language model (FoC-BinLLM) to summarize the semantics of cryptographic functions in natural language.<n>We then build a binary code similarity model (FoC-Sim) upon the FoC-BinLLM to create change-sensitive representations and use it to retrieve similar implementations of unknown cryptographic functions in a database.
  arXiv  Detail & Related papers  (2024-03-27T09:45:33Z)
• Blind Evaluation Framework for Fully Homomorphic Encryption and Privacy-Preserving Machine Learning [0.0]
  Blind Evaluation Framework (BEF) is a cryptographically secure programming framework. It enables blind, but correct, execution of programming logic without Interactive Rounds of Decryption and Evaluation (IRDE) This is the first framework to enable both training and inference of machine learning models with FHE without decryption rounds.
  arXiv  Detail & Related papers  (2023-10-19T20:33:02Z)
• Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
  We study cross-lingual semantic parsing as a zero-shot problem without parallel data for 7 test languages. We propose a multi-task encoder-decoder model to transfer parsing knowledge to additional languages using only English-Logical form paired data. Our system frames zero-shot parsing as a latent-space alignment problem and finds that pre-trained models can be improved to generate logical forms with minimal cross-lingual transfer penalty.
  arXiv  Detail & Related papers  (2021-04-15T16:08:43Z)
• Towards Instance-Level Parser Selection for Cross-Lingual Transfer of Dependency Parsers [59.345145623931636]
  We argue for a novel cross-lingual transfer paradigm: instance-level selection (ILPS) We present a proof-of-concept study focused on instance-level selection in the framework of delexicalized transfer.
  arXiv  Detail & Related papers  (2020-04-16T13:18:55Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.