VUPER: Verified ASN.1 UPER Parser

VUPER is a framework for generating verified ASN.1 UPER (Unaligned Packed Encoding Rules) parsers, designed to address the correctness and security challenges in security-critical domains such as cellular networks and vehicle-to-everything (V2X) communication. The paper formalizes the notion of a bit-precise parser and identifies properties that prove round-trip consistency for parsers and serializers, while accounting for ASN.1 features such as backward/forward compatibility. The framework implements and verifies parser and serializer combinators for ASN.1 basic types and structures, adhering to the UPER specification, and includes a compiler that translates ASN.1 definitions into verified parsers. Additionally, a dynamic testing framework is developed using the VUPER parser as a test oracle. The evaluation tested 7 open-source and 4 commercial ASN.1 parsers using 5G and V2X communication protocols, uncovering 20 types of inconsistencies in popular parsers and demonstrating stricter compliance with ASN.1 UPER standards, with concrete attacks demonstrated by exploiting these parser vulnerabilities.

The motivation for VUPER stems from the prevalence and complexity of UPER implementations, which remain under-investigated and lead to critical vulnerabilities, ranging from safety violations to subtle logic bugs. The ASN.1 standard exists only as descriptive text, lacking a precise reference implementation, and the intricate nature of ASN.1—including support for various primitive types and combinators, ranges, optional fields, extensions, and bit-level precision—makes it difficult to derive a fully correct implementation. Prior work on securing parsers has focused on testing and fuzzing, which cannot provide formal guarantees that eliminate entire classes of errors. Previous efforts on verifying binary formats cover both generic formats and specific formats such as ASN.1 DER and Protocol Buffer, but when it comes to ASN.1 UPER, prior approaches have critical limitations: specifying the correctness property for UPER is complicated by the protocol’s flexibility, most frameworks are byte-oriented creating a mismatch with bit-precise UPER, and most existing ASN.1 formalizations focus on DER, with the only prior work on UPER lacking support for critical features such as CHOICE types and extensions while imposing hard-coded limits on input.

VUPER addresses these gaps by using a bitstream model that disregards byte alignment, maintaining reasonable performance. It guarantees a nuanced round-trip property between its parser and serializer to account for forward and backward compatibility. For messages without unknown extensions, a strict injection property ensures full non-malleability. Conversely, for messages with unknown extensions, the weak-injection property applies a more relaxed criterion: the parsed message can be successfully re-encoded, without insisting that the output exactly match the input. These properties demonstrate that the parser rejects malformed or malicious inputs and remains correct with respect to the serializer. Auxiliary properties essential for building other guarantees, including local write and encode-consistency, are also proven. The framework adopts a modular parser-combinator approach, developing a family of parsers and serializers ranging from bit-level manipulation to structural types like CHOICE and SEQUENCE, with each component formally verified to ensure round-trip consistency. A compiler automatically transforms ASN.1 definitions into verified parser/serializer pairs.

The testing framework uses the formally verified VUPER parser (extracted from Rocq to OCaml) as a trusted oracle, systematically uncovering discrepancies in other ASN.1 implementations. Grammar-aware mutation is used by incorporating ASNFuzzGen into the fuzzing loop, and the JSON Encoding Rules (JER) are utilized to normalize and compare values produced by each parser. The evaluation of 11 parser libraries using uplink and downlink messages from 5G and Intelligent Transport Systems (ITS) protocols found that VUPER enforces stricter compliance than most existing implementations and uncovers 20 types of inconsistencies, including lenient constraint checks, value corruption, and deviations from the UPER standard. Four concrete attacks are demonstrated against two widely used open-source 4G/5G stacks, including DoS via unfiltered inputs and cryptographic key misconfigurations due to parser misinterpretation. The performance of the VUPER-generated parser on 5G messages is on average 4 times slower than C libraries and 4 times faster than Python libraries, which is expected as VUPER prioritizes formal correctness over efficiency and is intended to be used as a reference implementation for testing other ASN.1 parsers and fixing bugs.

The contributions of the paper are: designing VUPER, an automated, bit-precise, and correct-by-construction ASN.1 UPER parser and serializer library; proving and implementing round-trip properties for extensions and basic and ASN.1 parser combinators; developing a testing framework based on VUPER as a trusted oracle to effectively validate existing UPER parsers; and evaluating 7 open-source and 4 commercial parser implementations, uncovering 20 types of non-compliance that can lead to sensitive information exposure and DoS.

The design principles of VUPER begin with the parser’s round-trip properties. Parser security is framed in terms of surjection and injection properties. Surjection ensures that a parser is a surjective inverse of a serializer, meaning for any message, parsing the serialized message returns the original message, and no two distinct messages share the same encoding. Injection requires that the serializer recovers exactly the original encoding whenever parsing succeeds, implying non-malleability. These properties align with Canonical UPER, which enforces a strict bijective mapping of values and bitstrings. Termination is also crucial for program reliability, and side-channel security is excluded as enforcing constant-time execution is impractical for ASN.1 UPER.

The challenges UPER poses for formal specification and verification include backward/forward compatibility with extensions, bit-level precision in a majority byte-aligned world, explicit and implicit constraints, and encoding Open Type fields. Extensions break the injection property as they require the parser to accept messages from different versions. Bit-level precision makes implementation and formal verification more complex, and most parser frameworks operate on byte-aligned formats. Constraints are essential for efficient serialization but complicate verification, with explicit constraints like INTEGER (1..8) easily formalized while implicit constraints add complexity. Open Type fields create a circular dependency where the number of bits used for the length prefix depends on the total length of the value, requiring dynamic memory allocation and multi-pass encoding.

VUPER’s design philosophy focuses on formally verifying the correctness of ASN.1 parser and serializer implementations, distinguishing this from efforts that develop a formal model of the ASN.1 language itself. The framework uses the Rocq prover, with termination ensured by Rocq’s type checker. The extended round-trip property is chosen over verifying both parser and serializer against a formal specification defined as a relation between a value and its encoding, as UPER does not involve one-to-many encodings.

The VUPER workflow starts with formalizing parser/serializer round-trip consistency properties, then develops verified basic combinators serving as the foundation for ASN.1 primitive types, constructs structural combinators like SEQUENCE and proves their correctness, and implements a compiler that generates data types and verified parsers/serializers from any ASN.1 definition. The verified parser works as a trusted test oracle, enabling rigorous conformance testing of other parsers.

The serializer and parser definitions operate directly on a byte array treated as a continuous bitstream, using a precise bit position indicator representing a byte index and bit offset. The parser takes a buffer and starting bit position, returning upon success a tuple containing the parsed value with a proof it satisfies the condition, the new bit position, and a versioning flag. The serializer takes a buffer, starting position, and value to write, returning the updated buffer, new bit position, and proof that the value satisfies the required condition. Both functions are wrapped in an option type to handle errors.

To solve the challenge of forward/backward compatibility, VUPER adopts a flag-based version detection mechanism and a corresponding Weak-Injection property. The parser sets a flag if it encounters an unexpected number of extensions, signaling a version mismatch. Correctness guarantees are two-tiered: the standard Injection property applies when versions match, while the Weak-Injection property applies in all cases, ensuring the serializer can handle any output from the parser and that even when re-encoding does not produce an identical bitstring, the resulting value remains valid and constrained.

For bit-level precision, VUPER utilizes direct, efficient bit-level manipulation, operating directly on a bitstream while tracking the current bit offset, naturally supporting arbitrary bit alignment without requiring repeated shifting or copying. Parser combinators are used to modularly construct data types, parser/serializers, and proofs, tackling ASN.1’s complexities and enabling scalability of the verification process. For explicit constraints, combinators like restrict layer value constraints over other parsers, while implicit constraints are handled by composing basic verified parser combinators. For Open Type fields, a separate length function is defined, and the length is calculated beforehand by keeping a separate length function, eliminating the need for a temporary buffer and copy operation.

The correctness guarantees include surjection, strong-injection, weak-injection, local write, encode-invariance, decode-invariance, and length-consistency properties. Surjection ensures that encoding a value and then decoding the result returns the same value and position. Strong-injection requires that if a buffer decodes to some value, re-encoding that value should yield the same buffer, with equivalence between buffers defined via bitwise equivalence between buffer slices. Non-malleability is implied by a combination of strong-injection and encode-invariance, which ensures the serializer produces a canonical bit-level representation for any value. Local write ensures that encoding into a buffer does not modify bits outside the encoded range, crucial for composing serializers and parsers. Weak-injection establishes that if a buffer decodes to a value, that value can be encoded into another buffer provided sufficient space. Length-consistency ensures the length function accurately computes the encoding length as the difference between final and initial positions.

The verified parser combinators include basic bit formats, map, dependent append, list, CHOICE, and SEQUENCE combinators. The basic bit format acts as the direct interface between the byte array and the data type, enabling basic bit-level read/write operations. The map combinator transforms an existing format into a new data type with the same binary representation. The dependent append combinator formats a pair where the format for the second element depends on the value of the first element. The list combinator formats a fixed-length list of elements. The CHOICE combinator formats a tagged union representing a value that can be one of several predefined types. The SEQUENCE combinator maps an ordered list of fields marked as normal, OPTIONAL, or DEFAULT to a right-nested tuple, with field types adjusted based on their modifiers.

The SEQUENCE combinator handles the complex extension mechanisms of ASN.1, with proofs of round-trip consistency handled by proving components separately: the round-trip consistency of the bitmap, field consistency by parameterizing the parser with the decoded bitmap, and a prepend correctness property formally linking these separate proofs. For sequence extensions, a valid-encoding property is defined to ensure that any value satisfying a specific refinement condition has a valid encoding, proven for the length determinant and list combinator.

The compiler translates ASN.1 definitions into verified Rocq code, recursively generating types and formats using the verified combinators, mapping SEQUENCE to a Record type instead of a nested product, and generating helpful lemmas and proof obligations.

The testing framework extracts the verified parser into OCaml via extraction in Rocq, with the Trusted Computing Base including Rocq, the OCaml compiler, and the OCaml Bigarray library. Structure-aware fuzzing is implemented by incorporating ASNFuzzGen, which linearizes ASN.1 messages to an internal byte-level abstraction, mutates the resulting byte buffer, and delinearizes to reconstruct the final ASN.1 message. Output normalization uses the JSON Encoding Rules (JER) to standardize outputs, with the verified parser’s JER serialization automated using the ppx deriving preprocessor. For baseband targets where reverse engineering internal data formats is impractical, the number of bits each parser consumes is used as a simpler metric.

The implementation details estimate 12k lines of code (LoC) Rocq framework and 1.8k LoC OCaml compiler, taking 4-5 person-months. Supported features include ASN.1 structures such as SEQUENCE, CHOICE, and SEQ-OF with extensions, terminal types including BOOLEAN, INTEGER, ENUMERATED, BIT/OCTET STRING, and special strings including UTF8String and IA5String, length determinants, and Open Type Fields. SET-OF and fragmentation are omitted as they are barely used in practice, and certain high-level language abstractions like CLASS are omitted as they do not appear in target protocols.

The evaluation targets RRC messages in 4G/5G and V2X messages from the ETSI ITS standard. The targeted ASN.1 systems include 7 open-source tools (lionet asn1c, pycrate, asn1tools, TITAN, two parsers from srsRAN, and rasn) and 4 proprietary ones (Objective Systems’ ASN1C, two versions of ProASN extracted from Samsung S21 and Google Pixel 6 basebands, and ffasn1). A dual-input evaluation strategy validates practical utility and capability of finding non-compliance: testing the verified parser against a real-world dataset of 5G RRC traces and evaluating parsers-under-test using fuzzing with a verified oracle.

VUPER accuracy is evaluated with real-world datasets and fuzzer-generated datasets. On real-world data, all baseline parsers accepted every collected message, while VUPER rejected a specific subset containing explicitly encoded DEFAULT values, which per X.691 should always be absent if the value is the default value of a simple type. This indicates non-compliant encoders by the specific network operator, correctly identified by VUPER while other parsers overlook it. On fuzzer-generated traffic, over 99% of generated inputs produced no discrepancies, confirming VUPER is largely conformant with standard implementations. Forward/backward compatibility tests show most messages are accepted by both implementations, with the Rel-16 parser appropriately marking DiffVer to denote unknown extensions, confirming forward compatibility.

The root cause analysis strategy retrofits the verified OCaml parser to emit semantic error codes for Class I errors, performs manual triage by dissecting bit-packets for Class II and III discrepancies, and conducts targeted case studies by injecting a single type of non-compliance into minimal ASN.1 definitions. False positives stem from padding bits within Open Type fields, where the standard does not explicitly require redundant bits to be 0, so parsers that omit this check are not considered inherently non-compliant.

The evaluation identified 20 types of non-compliance categorized by their respective correctness property violation. Four classes of non-compliances occur in all parsers tested, which standard differential fuzzing relying on consensus among existing UPER parsers would fai…

Based on the paper, here are the specific improvements to AI systems and what the improved systems can do:

1. Formal Verification for AI-Generated Code Parsers

• Improvement: Integrate VUPER’s verified parser combinators and round-trip properties (surjection, strong/weak injection) into AI code-generation pipelines for network protocol parsers.

• Capability: AI systems can automatically generate bit-precise, formally verified ASN.1 UPER parsers/serializers, eliminating entire classes of memory corruption, DoS, and logic bugs without relying on fuzzing or testing.

2. AI-Driven Protocol Conformance Testing with a Trusted Oracle

• Improvement: Use the VUPER parser (extracted to OCaml) as a ground-truth oracle in AI-based differential testing frameworks, replacing consensus-based oracles.

• Capability: AI systems can systematically discover non-compliance in any UPER parser (e.g., 20 types found here), including bugs shared by all parsers, by comparing outputs against VUPER’s formally verified behavior, not against other buggy implementations.

3. AI-Assisted Vulnerability Discovery and Attack Generation

• Improvement: Train AI models to generate grammar-aware mutations (like ASNFuzzGen) and target specific correctness properties (weak-injection, surjection, strong-injection) that VUPER identifies.

• Capability: AI systems can automatically craft malicious 5G/V2X messages (e.g., oversized PLMN lists, constraint-violating handover messages) that trigger crashes, key misconfigurations, or interop failures in real-world stacks, as demonstrated in the four proof-of-concept attacks.

4. AI for Formal Specification of Complex Encoding Rules

• Improvement: Apply VUPER’s approach (bitstream model, flag-based version detection, weak-injection for extensions) to other encoding rules (e.g., APER, DER) or binary formats.

• Capability: AI systems can formally specify and verify parsers for protocols with backward/forward compatibility, optional fields, and open types, ensuring non-malleability and termination—beyond what byte-oriented frameworks can handle.

5. AI-Enhanced Compiler Correctness

• Improvement: Incorporate VUPER’s compiler (ASN.1 to verified Rocq code) as a reference in AI-based compiler testing or code synthesis.

• Capability: AI systems can validate or generate compilers that translate high-level protocol definitions into verified, bit-precise implementations, catching subtle errors in extension handling, length determinants, and constraint checks that human-written compilers miss.

6. AI for Security-Aware Protocol Design

• Improvement: Use VUPER’s correctness properties (e.g., strong-injection for non-malleability) as training signals for AI models that design or modify protocol specifications.

• Capability: AI systems can propose protocol changes that preserve round-trip consistency, reject ambiguous encodings, and prevent device fingerprinting or downgrade attacks, based on formal guarantees rather than heuristics.

7. AI-Powered Root Cause Analysis for Parser Bugs

• Improvement: Leverage VUPER’s semantic error codes and bit-level dissection to train AI models for automated triage of parser discrepancies.

• Capability: AI systems can classify bugs into categories (e.g., missing constraint checks, overlong encodings, extension-count errors) and suggest precise fixes, reducing manual analysis time from days to minutes.

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.