该论文提出了 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 标准更严格的合规性。此外，他们还通过利用这些解析器漏洞展示了具体攻击。该研究的主要贡献在于提出了一种可能的方法来生成验证过的解析器，并揭示了现有解析器实现中的大量缺陷，为相关安全加固提供了基础。适合编译器、形式化验证、协议安全及通信系统安全领域的研究人员和工程师阅读。

解析（parsing）在软件项目中无处不在，从小型命令行工具到高安全性的网络客户端，再到大型编译器，都离不开解析器。然而，解析库的实现缺陷可能导致生成不正确的解析器，进而被恶意输入利用，引发系统崩溃或安全漏洞。本文提出了一种轻量级的验证框架Bohemia，旨在帮助解析库开发者将其作为集成测试的工具箱中的一员。该框架基于 Equivalence Modulo Inputs (EMI) 的概念，通过变异输入语法来对解析库进行压力测试。作者在多个采用不同解析算法的解析库上评估了Bohemia，发现了若干缺陷，其中一些已被开发者确认并修复。论文详细阐述了Bohemia的设计原理、实现方式以及实验结果，展示了其在提升解析库鲁棒性方面的潜力。读者可以从中了解一种基于语法变异的解析库测试方法，以及如何利用EMI技术挖掘潜在的解析器缺陷。