VUPER: Verified ASN.1 UPER Parser
2026-08-10 • Cryptography and Security
Cryptography and SecurityProgramming Languages
AI summaryⓘ
The authors developed VUPER, a tool that creates reliable and secure parsers to read data encoded with ASN.1 using UPER, which is important for communication systems like 5G and vehicle networks. They defined precise rules to ensure that data can be correctly encoded and decoded without errors, even when old and new versions are used. Their tool can automatically generate these verified parsers from ASN.1 specifications and test existing parsers for mistakes. Testing revealed many errors in popular decoders, which the authors showed could lead to real attacks. This work helps improve the safety and correctness of critical communication systems.
ASN.1UPERparserserializerbit-precise parsing5G communicationV2X communicationround-trip consistencyinterface description languagecompiler
Authors
Xiaotian Zhou, Kai Tu, Ali Ranjbar, Yilu Dong, Gang Tan, Syed Rafiul Hussain
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.