发表机构
UCLA; University of California, Riverside（加州大学洛杉矶分校; 加州大学河滨分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出SpecLens，利用语言模型作为脚手架，通过将协议规范中的语义欠规范视为部分指定通信状态机的缺口或分叉，有效发现RFC规范中的歧义，并在5G和DNS协议上验证了其高准确率与实用性。
AI 中文摘要
以RFC形式编写的互联网协议规范存在歧义和多种解释，可能导致互操作性失败。虽然这些问题在多年经验积累后可能已得到澄清，但此类歧义仍会困扰5G等新协议的采用。5G规范将形式化消息语法（ASN.1）与用自然语言编写的消息处理程序配对，这造成了语义欠规范：一条语法上有效的消息可能到达一个其程序从未说明如何处理的状态，因此符合标准的实现会产生分歧。我们将此视为部分指定的通信状态机中的缺口或分叉，并提出了SpecLens，它将这种视图作为脚手架呈现给语言模型。更强的模型并不能消除对它的需求：它们扩大了搜索范围却不加以约束，其发现中不到一半能通过检查。在来自六个3GPP和O-RAN协议的36个程序中，专家接受了197个SpecLens发现中的185个，其中60个在差分测试下驱动了OpenAirInterface和srsRAN实现之间的可观察分歧。虽然我们将5G作为新协议的典型示例，但我们也展示了更成熟的DNS协议的歧义结果。
英文摘要
Internet protocol specifications written in RFCs are subject to ambiguities and multiple interpretations that can cause interoperability failure. While these have presumably cleared up after years of experience, such ambiguities can bedevil the adoption of newer protocols like 5G. The 5G specifications pair a formal message syntax (ASN.1) with message-handling procedures written in natural language. This creates semantic underspecification: a syntactically valid message can reach a state whose procedures never say how to handle it, so standard-compliant implementations diverge. We frame this as a gap or a fork in a partially specified communicating state machine, and present SpecLens, which puts that view in front of a language model as a scaffold. Stronger models do not remove the need for it: they broaden the search without disciplining it, and fewer than half their findings survive inspection. Across 36 procedures from six 3GPP and O-RAN protocols, experts accept 185 of 197 SpecLens findings, and 60 drive observable divergence between the OpenAirInterface and srsRAN implementations under differential test. While we use 5G as a canonical example of a newer protocol, we also show ambiguity results for the more mature DNS protocol.
