一句话：提出 Refine2Diff，用规约驱动代码精化构造参考实现并生成 PoC，自动检测网络协议规约与实现的不一致性。
检测规约与实现的不一致性至关重要，但自然语言规约与可执行代码之间的语义鸿沟使其十分困难。现有方法通常需要大量人工将规约要求转化为形式化性质，而基于 LLM 的方法虽能自动化该过程，却受幻觉与不可靠推理影响，产生误报。本文提出 Refine2Diff，不依赖 LLM 直接给出二元判定，而是将规约作为指令来精化实现，通过原始实现与精化实现之间可观测的行为差异暴露不一致性。具体地，Refine2Diff 执行上下文感知精化以构造参考实现，并支持精化引导的 PoC 生成：推导触发行为差异的前置条件，并通过规约引导的变异满足这些条件。作者在覆盖六种网络协议的 10 个真实实现上评估，不一致性检测精度为 0.84（最强基线 1.4 倍），经 PoC 确认后提升至 0.98；PoC 生成成功率达 82%，优于所有基线 3–9 倍，且执行次数最多减少 5.7 倍。共发现 30 个此前未知的不一致性缺陷，其中 22 个已被开发者确认。
Detecting specification–implementation inconsistencies is critical and fundamentally challenging due to the semantic gap between natural-language specifications and executable code. Existing approaches often require substantial manual effort to translate specification requirements into formal properties for verification or testing. While recent LLM-based methods have shown promise in automating this process, they suffer from hallucination and unreliable reasoning, producing false positives. To address these limitations, we present Refine2Diff, a novel framework for automatically detecting and validating specification–implementation inconsistencies in network protocols. Rather than relying solely on a direct binary judgment from an LLM, we use the specification as an instruction to refine the implementation, thereby exposing inconsistencies through observable behavioral differences between the original and refined implementations. Specifically, Refine2Diff performs context-aware refinement to construct a reference implementation and supports refinement-guided PoC generation by deriving preconditions that trigger behavioral differences and satisfying them through specification-guided mutation. We evaluate Refine2Diff on 10 real-world implementations spanning six network protocols. For inconsistency detection, Refine2Diff achieves a precision of 0.84 (1.4× higher than the strongest baseline), improving further to 0.98 after the PoC-based confirmation. For PoC generation, Refine2Diff achieves an 82% success rate, outperforming all baselines by 3×–9× while requiring up to 5.7× fewer executions. In total, Refine2Diff uncovers 30 previously unknown inconsistency bugs, 22 confirmed by developers.
@inproceedings{paperbot12257,
title = {Refine2Diff: Detecting Protocol Specification–Implementation Inconsistencies via Specification-Driven Code Refinement},
author = {Yuekun Wang and Lili Quan and Xiaofei Xie},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834437}
}