AI 中文总结
VUPER是生成经验证的ASN.1 UPER解析器的框架，可发现20种现有解析器的不一致问题并演示攻击，提升了相关通信领域的基础设施安全性。
AI 中文摘要
ASN.1是一种广泛使用的接口描述语言，UPER（非对齐打包编码规则）是其关键编码规则之一，尤其在蜂窝网络、车联网（V2X）通信等安全关键领域中应用广泛。为确保这一基础基础设施的正确性与安全性，我们提出了VUPER，这是一个用于生成经过验证的ASN.1 UPER解析器的框架。我们首先形式化定义了位精准解析器的概念，并确定了能证明解析器与序列化器往返一致性的属性，同时考虑了ASN.1的向后/向前兼容性等特性。接着，我们实现并验证了适用于ASN.1基本类型和结构的解析器与序列化器组合子，且严格遵循UPER规范。我们还开发了一个编译器，可将ASN.1定义转换为经过验证的解析器。最后，我们开发了一个以VUPER解析器作为测试预言的动态测试框架。为对我们的方法进行实证评估，我们使用5G和V2X通信协议对7个开源和4个商业ASN.1解析器进行了测试，VUPER在这些流行解析器中发现了20种不一致类型，表现出对ASN.1 UPER标准更严格的合规性，此外，我们还通过利用这些解析器漏洞展示了具体的攻击。
英文摘要
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.
Comments18 pages, 7 figures, 10 tables. Extended version of the paper accepted to ACM CCS 2026
