VUPER: Verified ASN.1 UPER Parser
本文介绍了 VUPER，这是一个能够生成经过形式化验证且位精确（bit-precise）的 ASN.1 UPER 解析器与序列化器的框架，该框架通过对 5G 和 V2X 协议进行动态测试，被用于发现流行开源及商业解析器中存在的 20 类不一致性与具体的安全漏洞。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，互联网和我们的手机就像一座巨大且繁忙的城市，数以十亿计的消息每秒钟都在建筑之间穿梭。为了让这座城市正常运转，这些消息需要一种通用的语言，这样纽约的手机才能与东京的基站进行通信而不会产生混乱。这种语言被称为 ASN.1，它就像是语法和词汇，告诉计算机如何精确地将信息打包进微小、高效的数字盒子中。但棘手之处在于，为了节省空间并提高速度，这些盒子的打包极其紧凑，甚至没有对齐到整齐的字节行（即标准的计算机字长）；相反，它们被压缩到了每一个 位（bit），即数据的最小单位。这种特定的、超紧凑的打包方法被称为 UPER。
问题在于，编写一个用于拆解这些微小、位级盒子的“翻译器”（或称“解析器”）是非常困难的。如果翻译器出了哪怕一点点差错——比如读错了一个位，或者忘记了如何处理新出现的未知信息——都可能导致整个系统崩溃、泄露秘密，甚至让黑客潜入。多年来，工程师们一直试图通过用数百万条随机消息来测试这些翻译器来修复这些错误，希望能抓到漏洞。但这就像是通过摇晃干草堆来寻找针头一样——你可能会找到一些针，但你永远无法确定是否已经找到了所有的针，也无法确定你找到的是不是真正的目标。
VUPER 登场了。这是由宾夕法尼亚州立大学的研究人员开发的一种新工具，它改变了游戏规则。VUPER 不仅仅是在摇晃干草堆，它从零开始构建了一个在数学上完美的翻译器。你可以把它想象成创建了一本“金标准”字典和语法书，其正确性得到了计算机数学家的证明，是 100% 正确的。研究人员使用这个完美的翻译器测试了其他 11 个在现实世界 5G 网络和车联网（V2X）系统中广泛使用的解析器。他们发现，许多这些广泛使用的翻译器实际上并不合规，遗漏了 20 种不同类型的规则。在某些情况下，这种不合规性允许黑客导致手机崩溃，或诱导网络发送未加密的消息。VUPER 证明了，虽然我们不能总是信任现有的翻译器，但我们现在可以构建在数学上保证安全的翻译器，并利用它们来修复那些有缺陷的程序。
VUPER 的故事：构建完美的翻译器
在计算机网络的世界里，数据就像流经管道的长流之水。为了发送一条消息，计算机会对数据进行“序列化”，将数据挤压成紧凑的位流。为了接收它，另一台计算机会对这个位流进行“解析”，将这些位重新挤压回可读的消息。在 5G 蜂窝网络和车联网（V2X）通信的高风险领域，这个过程使用了一套特定的规则，称为 UPER（非对齐打包编码规则）。它被称为“非对齐”，是因为它不在乎整齐的字节边界；它将数据尽可能紧密地打包，逐位进行，以节省带宽。
挑战在于，UPER 的官方规则手册是用晦涩的描述性文本编写的，而不是代码。这使得工程师只能靠猜测来执行规则，从而导致微妙的错误。开发 VUPER 的研究人员决定不再靠猜。他们构建了一个能够从形式上证明解析器正确性的框架。他们不仅仅是编写代码并寄希望于其有效，而是使用了一种强大的数学工具——Rocq 证明器，来验证逻辑中的每一个步骤。
“往返”测试
要理解 VUPER 如何工作，想象你有一个神奇的翻译器，能把一本书变成密码，又能把密码变回书。所谓的“往返”测试意味着：你拿出一句话，将其转化为代码，然后再将该代码转回句子。如果你得到了完全相同的句子，说明翻译器工作正常。
然而，UPER 有一个特别的转折：扩展（extensions）。随着技术演进（例如从 4G 转向 5G），消息中会加入新功能。旧的翻译器需要能够读取新消息，忽略它不理解的新部分，并依然能理解旧的部分。这被称为前向兼容性。VUPER 通过证明两件事来处理这个问题：
- 严格往返（Strict Round-Trip）： 如果消息来自同一个版本，翻译器必须将其还原为完全相同的位模式。不能有多余的位，也不能缺少位。
- 弱往返（Weak Round-Trip）： 如果消息包含新的、未知的扩展，翻译器可以跳过它们，但它必须仍能将已知的部分还原为有效的消息。它不需要与原始数据实现位对位的完全匹配（因为未知部分已经消失了），但它绝不能损坏剩余部分。
寻找 Bug
研究人员构建了一个“受信任的先知”（trusted oracle）——即由 VUPER 生成的完美解析器——并用它来测试其他 11 个解析器。这些解析器包括 7 个开源工具（如 asn1c 和 pycrate）以及 4 个用于真实 4G 和 5G 基站（连接手机到网络的硬件）的商业解析器。
他们并没有发送随机的垃圾数据；而是使用了一个理解消息结构的智能“模糊测试器（fuzzer）”来创建数百万个棘手的测试用例。当他们对比结果时，发现了 20 种不同类型的差异。
以下是一些最有趣的发现：
- “过长”问题： 一些解析器接受了超出分配空间的数值，或者长度与数据不匹配。这就像一名邮递员接受了一封信，信上写着“我有 5 页”，但实际却有 100 页，导致邮箱溢出并崩溃。
- “未知扩展”引起的混乱： 当消息包含旧解析器不认识的新功能时，一些解析器会陷入混乱，开始错误地读取消息的其他部分，误以为那是别的东西。这就像一个翻译员看到外语中的新单词后感到困惑，然后把句子的其余部分也翻译错了。
- “默认值”错误： 规则规定，如果某个值是“默认值”，为了节省空间，则不应发送该值。但有些解析器仍然会发送它，或者无法识别它缺失的情况。
现实世界的危险
该论文并不仅仅发现了理论上的 Bug；它展示了这些 Bug 如何被利用。研究人员演示了 四种具体的攻击方式：
- 导致手机崩溃： 通过发送一个包含略长于限制范围的网络 ID 列表的消息（违反了约束条件），导致手机软件崩溃，造成拒绝服务（DoS）攻击。
- 导致基站崩溃： 一个被攻破的基站可以向另一个基站发送畸形消息，导致第二个基站在处理该消息时崩溃。
- 泄露秘密： 如果解析器由于未知扩展而误读了消息，它可能会认为某个安全设置是“关闭”的，而实际上它是“开启”的，反之亦然。这可能导致一种情况：手机认为自己正在进行安全通信，但网络实际上正在发送明文数据，从而允许窃听者读取。
- 设备指纹识别： 由于不同的解析器处理错误的方式不同，黑客可以发送特定的“陷阱”消息并观察设备的反应。如果设备接受了一个奇怪的消息，黑客就知道它使用的是特定品牌的硬件（例如三星基带），从而针对该特定设备发动已知的攻击。
性能与未来
研究人员承认，他们那个完美的、经过数学验证的解析器并不是目前市面上最快的。它比目前工业界使用的经过高度优化的 C 语言库慢大约 4 倍。然而，它比基于 Python 的解析器快 4 倍。
VUPER 的目标并非立即取代这些快速的解析器，而是作为一种参考实现（reference implementation）。正如一位名厨可以通过品尝菜肴来准确指出食谱中的错误一样，VUPER 可以告诉工程师他们的解析器究竟在哪里失败了。研究人员希望通过使用 VUPER 来发现并修复这些 Bug，行业最终能够构建出既快速又在数学上保证安全的解析器。
最后，VUPER 表明，在 5G 及更高速度的复杂世界中，我们不能再仅仅依赖“足够好”的测试。我们需要经过数学证明的翻译器，来守护我们的数字城市安全、可靠且顺畅地运行。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。