paperbot · PL 论文追踪

全部论文 待读 收藏

P1 Spec2Code: Mapping Protocol Specification to Function-Level Code Implementation

Spec2Code:将协议规范映射到函数级代码实现
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 7/10 · 该工作属于用户画像中'AI→PL'方向:用 LLM 自动化协议规范(RFC)到函数级实现的一致性映射,并配合轻量级一致性验证器发现真实 bug,本质上是 LLM 辅助的程序验证/一致性检查。在真实工业代码库(Nginx、OpenSSL、FRRouting 等)上验证、发现被开发者确认的不一致 bug,契合用户对工业落地与问题驱动研究的偏好;但与用户更核心的静态分析(尤其 Agentic 程序分析、浮点/贝叶斯程序分析)以及理论形式化深度仍有距离,且方法主要是 LLM 匹配流程而非新的分析理论。引用 0 inbox
Yuekun Wang, Lili Quan, Xiaofei Xie, Junjie Wang, Jianjun Chen
crossref: 2026-09-12

AI 速览

一句话:提出首个LLM驱动的函数级协议规范到代码映射框架,支持细粒度一致性检查并发现真实不一致。

协议规范(RFC)到实现的映射多依赖人工且仅到文件级,难以支持函数级一致性检查。Spec2Code 是首个 LLM 驱动的细粒度映射框架:先提取结构化规范需求与函数级代码表示及依赖上下文;再用相关性过滤和聚类组织缩减候选对;最后对候选 SR-函数对做约束级匹配,判定完全、部分或无关。在 HTTP、TLS、BFD 的真实实现(Apache Httpd、Nginx、OpenSSL、BoringSSL、FRRouting、BIRD)上,其精确率、召回率和 F1 较四个基线最多提升 49%、66%、66%,并恢复 16 个已知不一致、发现 11 个新不一致,5 个获开发者确认。

问题
规范与实现之间的函数级映射缺失,现有方法多靠人工且只到文件级,妨碍细粒度一致性检查。
方法
使用 LLM 驱动:预处理提取结构化规范需求与函数级代码表示,经相关性过滤和聚类缩减候选,再进行约束级匹配判定函数与 SR 的关系。
评估
在 HTTP、TLS、BFD 的六个真实代码库上与四个基线比较,并集成轻量一致性验证器检测已知与未知不一致。
原文摘要(Abstract)

Protocol specifications, defined in Request for Comments (RFCs), play a critical role in ensuring the correctness of protocol software systems. To check consistency, specification–implementation pairs are essential for testing and verification. However, existing efforts in specification-to-code mapping remain largely manual and are typically limited to the file level, lacking the fine-grained granularity needed for function-level analysis, which is crucial for effective consistency checking. To address this gap, we present Spec2Code, the first LLM-driven framework that automates fine-grained mapping from protocol specifications to function implementations.Given a RFC document and a protocol codebase, Spec2Code first performs preprocessing to extract structured specification requirements (SRs) and function-level code representations, along with contextual and dependency information. To ensure scalability, Spec2Code employs a two-stage process comprising relevance filtering and clustering-based SR organization to reduce the candidate pairs. For accuracy, Spec2Code performs fine-grained constraint-level matching on each candidate SR–function pair using LLMs, leveraging enriched context to determine whether a function fully, partially, or does not relate to an SR.We evaluate Spec2Code on real-world implementations of HTTP, TLS and BFD protocols, including Apache Httpd, Nginx, OpenSSL, BoringSSL, FRRouting, and BIRD. Experimental results show that Spec2Code outperforms four state-of-the-art baselines, achieving up to 49%, 66%, and 66% improvement in precision, recall, and F1, respectively. Additionally, Spec2Code successfully recovers the mappings for 16 known inconsistency bugs and discovers 11 previously unreported inconsistencies using an integrated lightweight consistency verifier, 5 of which have been confirmed by project developers.

链接与引用

DOI 原文 ·

BibTeX
@inproceedings{paperbot9238,
  title = {Spec2Code: Mapping Protocol Specification to Function-Level Code Implementation},
  author = {Yuekun Wang and Lili Quan and Xiaofei Xie and Junjie Wang and Jianjun Chen},
  booktitle = {ASE},
  year = {2025},
  doi = {10.1109/ase63991.2025.00174}
}