arXiv:2504.18050v1 类别: cross 摘要：验证网络协议实现的正确性极为具有挑战性，主要原因在于 oracle 和可追溯性问题。前者决定了何时可以认为协议实现存在缺陷，尤其是在这些缺陷不会引发任何可观察症状的情况下。后者使得开发人员能够理解实施如何违反协议规范，从而便于进行缺陷修复。不同于现有工作很少同时考虑这两种问题，这项工作同时考虑了两者，并利用最新的大型语言模型（LLMs）进展提供了一个有效的解决方案。我们的关键观察是，网络协议通常伴随着结构化的规范文档，即 RFC 文档，这些文档可以系统地通过 LLMs 翻译为形式化的协议消息规范。此类规范可能因 LLM 的幻觉而含有错误，但它们被用作一种准 oracle 来验证协议解析器，而验证结果反过来逐步完善 oracle。由于 oracle 是从文档中派生出来的，因此在协议实现中发现的任何缺陷都可以追溯到文档本身，从而解决了可追溯性问题。我们使用九种网络协议及其用 C、Python 和 Go 编写的实现进行了广泛的评估。结果显示，我们的方法优于最先进的方法，共检测到了 69 个缺陷，其中有 36 个被确认。该项目还展示了基于自然语言规范完全自动化软件验证的潜力，一个以前主要依赖手动过程来理解规范文档并为测试输入生成预期输出的过程。