该论文提出了 VUPER，一个用于生成经过形式化验证的 ASN.1 UPER（非对齐压缩编码规则）解析器的框架。ASN.1 是一种广泛使用的接口描述语言，而 UPER 是其中关键的编码规则之一，尤其在蜂窝网络和车联网（V2X）通信等安全关键领域应用广泛。为保证这一基础基础设施的正确性和安全性，作者首先形式化了位精确解析器的概念，并识别出能够证明解析器与序列化器往返一致性的属性，同时考虑了 ASN.1 的向后/向前兼容性等特性。接着，他们按照 UPER 规范，为 ASN.1 基本类型和结构实现并验证了解析器和序列化器组合子。他们还开发了一个编译器，能够将 ASN.1 定义转换为经过验证的解析器。最后，他们构建了一个以 VUPER 解析器为测试基准的动态测试框架。为了实证评估，作者使用 5G 和 V2X 通信协议测试了 7 个开源和 4 个商业 ASN.1 解析器。VUPER 在流行解析器中发现了 20 种类型的不一致，并展示了对 ASN.1 UPER 标准更严格的合规性。此外，他们还通过利用这些解析器漏洞展示了具体攻击。该研究的主要贡献在于提出了一种可能的方法来生成验证过的解析器，并揭示了现有解析器实现中的大量缺陷，为相关安全加固提供了基础。适合编译器、形式化验证、协议安全及通信系统安全领域的研究人员和工程师阅读。