VUPER: Verified ASN.1 UPER Parser

• URL: http://arxiv.org/abs/2608.09094v1
• Date: Mon, 10 Aug 2026 03:47:38 GMT
• Title: VUPER: Verified ASN.1 UPER Parser
• Abstract summary: 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.
• Score: 19.74234190254681
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: ASN.1 is a widely used interface description language, and UPER (Unaligned Packed Encoding Rules) is one of its key encoding rules, particularly popular in security-critical domains such as cellular networks and vehicle-to-everything (V2X) communication. To ensure the correctness and security of this foundational infrastructure, we present VUPER, a framework for generating verified ASN.1 UPER parsers. We first formalize the notion of a bit-precise parser and identify properties that prove round-trip consistency for parsers and serializers, while accounting for ASN.1 features such as backward/forward compatibility. We then implement and verify parser and serializer combinators for ASN.1 basic types and structures, while adhering to the UPER specification. We also develop a compiler that translates ASN.1 definitions into verified parsers. Finally, we develop a dynamic testing framework using the VUPER parser as a test oracle. To empirically evaluate our approach, we test 7 open-source and 4 commercial ASN.1 parsers using 5G and V2X communication protocols. VUPER uncovers 20 types of inconsistencies in popular parsers and demonstrates stricter compliance with ASN.1 UPER standards. Additionally, we demonstrate concrete attacks by exploiting these parser vulnerabilities.

Related papers

• 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)
• Protocol Testing with I/O Grammars [45.68497486907946]
  We propose a novel approach to protocol testing that combines input generation and output checking in a single framework.<n>We demonstrate that I/O grammars can specify advanced protocol features correctly and completely, while also enabling output validation of the programs under test.
  arXiv  Detail & Related papers  (2025-09-24T16:41:04Z)
• XML Prompting as Grammar-Constrained Interaction: Fixed-Point Semantics, Convergence Guarantees, and Human-AI Protocols [0.2864713389096699]
  We develop a logic-first treatment of XML prompting that unifies (i) grammar-constrained decoding, (ii) fixed-point semantics over lattices of hierarchical prompts, and (iii) convergent human-AI interaction loops.<n>We provide mathematically complete proofs and tie our framework to recent advances in grammar-aligned decoding, chain-of-verification, and programmatic prompting.
  arXiv  Detail & Related papers  (2025-09-09T23:03:53Z)
• Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE [1.2419340000421064]
  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.
  arXiv  Detail & Related papers  (2025-05-22T23:12:03Z)
• 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)
• 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)
• Cross-domain Chinese Sentence Pattern Parsing [67.1381983012038]
  Sentence Pattern Structure (SPS) parsing is a syntactic analysis method primarily employed in language teaching. Existing SPSs rely heavily on textbook corpora for training, lacking cross-domain capability. This paper proposes an innovative approach leveraging large language models (LLMs) within a self-training framework.
  arXiv  Detail & Related papers  (2024-02-26T05:30:48Z)
• Compositional Program Generation for Few-Shot Systematic Generalization [59.57656559816271]
  This study on a neuro-symbolic architecture called the Compositional Program Generator (CPG) CPG has three key features: textitmodularity, textitcomposition, and textitabstraction, in the form of grammar rules. It perfect achieves generalization on both the SCAN and COGS benchmarks using just 14 examples for SCAN and 22 examples for COGS.
  arXiv  Detail & Related papers  (2023-09-28T14:33:20Z)
• 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.