南京大学 | SPAR：用对抗式LLM交互从RFC中萃取精确的网络协议格式规范

原创

陈怡璇
陈怡璇

安全学术圈

2026年10月23日 21:30
四川

去阅读

原文标题：Generating Precise Format Specification for Network Protocols Through Adversarial LLM Interactions
原文作者：Hengdi Ye, Bing Shui, Jielun Wu, Yufan Zhou, Baowen Xu, Qingkai Shi                 发表会议：35th USENIX Security Symposium (USENIX Security '26), August 12–14, 2026, Baltimore, MD, USA
笔记作者：陈怡璇@安全学术圈
主编：黄诚@安全学术圈

1、背景介绍

网络协议是跨系统通信的\"语言\"，而协议的格式规范就是这门语言的语法书，它规定两件事：一是语法结构，即一个报文由哪些字段、以什么顺序拼成；二是语义依赖，即字段之间的约束关系。后者才是安全的关键——比如\"当 AE 字段等于 3 时，Omitted 字段必须为 0\"这类跨字段约束，一旦被实现忽略，攻击者就可能伪造路由、劫持会话。因此，精确的格式规范是网络模糊测试 [21, 39, 51, 80]、入侵检测 [17, 23, 24, 40]、协议验证 [2–5] 等一系列安全任务的前提。

但\"精确\"极难达成。现有工作分两条路线，各有硬伤。第一条以协议实现为输入（源码 [53, 55] 或二进制 [6, 7, 13, 27, 33, 34, 66]），用程序分析反推格式，其致命缺陷是继承实现的缺陷：实现本身漏掉的约束，学到的规范也会同样漏掉——于是它对自己本该发现的 bug 天生\"盲视\"。差分分析（如 ParDiff [77]）试图用多个独立实现交叉验证来摆脱偏置，但工程上往往拿不到多个实现，换一种编程语言还得重新适配。第二条引入大语言模型直接读 RFC 文档（[19, 52, 63, 78]），绕开了\"坏实现\"，在语法上表现很好，但受幻觉拖累，在跨字段语义约束上普遍不合格。论文给了一个很扎眼的实测：ParCleanse [78] 推断语法结构的精度和召回几乎接近 100%，但对很多协议一条跨字段约束都推不出来。注意作者对\"幻觉\"做了宽泛定义——不只是凭空编造，也包括遗漏关键信息。

本文的切入点是两个观察：其一，LLM 在规范推断 [31, 36, 48, 79] 与代码生成 [16, 38, 42, 62] 两类任务上都已经很强；其二，两个不同的 LLM 任务不太可能独立地产生完全相同的幻觉——因为幻觉通常源于输入的模棱两可或信息不足。基于此，作者提出 SPAR：仅凭 RFC 文档，就能自动生成语法与语义双精确的格式规范。

2、Motivation：藏在\"错误字段\"下的约束

论文用 RFC 8966（BABEL 路由协议）的一个片段说明问题。

这段自然语言描述了 BABEL 的 \"Update\" 报文：语法上由一串字段组成（8 位的 Type、Length、AE，16 位的 Interval、Seqno 等）；语义上规定 Type 必须为 8，且若 AE 等于 3，则 Omitted 必须为 0。作者点出自然语言规范的两个固有缺陷：一是取值范围要靠上下文补全——AE 和 Plen 的合法区间在这段里根本没写，它们出现在更早的正文中；二是约束被写在了\"不对\"的字段下面——AE 与 Omitted 的依赖关系并不是写在 AE 或 Omitted 的描述里，而是藏在 Plen 的描述里。

把它写成形式化规范，跨字段依赖就变成了显式公式：

UINT8 AE      { AE >= 0 && AE <= 3 };
UINT8 Omitted { (AE == 3 && Omitted == 0)
             || (AE != 3 && Omitted <= ((Plen + 7) / 8)) };

有了这份规范，藏在实现里的 bug 就浮出来了：FRRouting [10]（Linux/Unix 上广泛部署的开源路由套件）的 BABEL 解析函数完全没检查 AE 与 Omitted 的依赖，论文的修复只有三行——if (packet[2] == 3 && packet[5] != 0) { ... goto fail; }。由于 BABEL 用这两个字段配合 Prefix 计算有效网络地址，漏掉这个检查会导致地址算错，让路由器把包转到次优甚至拥塞的路径上，甚至可被用来对关键网络服务发起基于流量的拒绝服务攻击。作者强调，这类 bug 既没有内存破坏，也几乎不崩溃，所以传统静态分析 [54, 60] 和模糊测试 [20, 74] 都很难抓到——这正是\"先建立规范、再拿规范校验实现\"的价值，而前提是规范必须真把字段间的依赖写对。

3、本文方法：SPAR 的对抗式双向精化

SPAR 的骨架是一个双向对抗循环：从 LLM 依据 RFC 生成的初始格式规范与初始解析器出发，交替地（2）以格式规范为预言机精化解析器、（3）以解析器为预言机精化格式规范，直到双方收敛到不动点——此时规范与参考解析器互相一致，再无精化余地。支撑这一循环的两个洞见是：洞见一，LLM 在两个任务上都能产出质量尚可的初稿；洞见二，两个不同的 LLM 任务不太可能独立地犯下同一个幻觉——这正是对抗循环能压制幻觉的根本原因。

四步走下来是这样的：

步骤一，从 RFC 构建初始规范与解析器。 采用分而治之策略（沿用先前工作 [78] 的做法）：先把 RFC 组织成目录树（每个节点对应目录中的一节），让 LLM 逐节解释、生成局部的子格式/子解析器，最后按树自底向上合并。这样 LLM 每次只聚焦相关章节，避免注意力被稀释。作者坦承这一步不是本文的核心贡献，因此不展开。

步骤二，以格式为预言机精化解析器。 从规范中抽出字段约束，交给 Z3 约束求解器 [14] 生成正例报文（满足全部约束）与反例报文（至少违反一条约束），拿去测解析器。如果解析器接受了反例、或拒绝了正例，就把相关代码片段与对应 RFC 章节交给 LLM 复查修正。

步骤三，以解析器为预言机精化格式。 反方向更难，因为从解析器生成报文比从规范生成更难——解析器的代码结构远比声明式的格式复杂。SPAR 改用混合模糊测试 [59, 73, 75]（灰盒模糊测试 + 符号执行）生成被解析器接受/拒绝的报文。若被接受的报文违反了规范、或被拒绝的报文反而满足规范，就说明规范漏了约束，同样定位出片段与 RFC 章节交给 LLM 修正。回到动机示例：混合模糊测试器生成了一个被拒绝的反例（AE = 3 && Omitted = 1），但比对规范时发现它居然满足规范里的所有约束——规范并不认为它非法，说明规范漏了东西，于是 AE、Omitted 连同相关 RFC 章节被送去让 LLM 补上。

步骤四，用规范去挖洞。 与步骤二同理，用最终规范生成正/反例报文去模糊测试有缺陷的实现，那个违反跨字段约束的反例会被漏检的实现照单全收，bug 就此暴露。

这套流程还要解决两个挑战：挑战一是报文组合爆炸——n 个字段、每个 m 种取值就有 mⁿ 个报文，全枚举不可行；挑战二是注意力分散——喂给 LLM 的输入应该\"恰好\"包含全部且仅有相关的 RFC 片段，给少了切不中要害，给整篇又会稀释注意力、反而引入新幻觉，甚至把本来正确的部分改坏。

对应地，论文给了三个优化。优化一\"路径覆盖\"：SPAR 先把规范转成有向无环的报文格式图（PFG），图上每条路径对应一种报文布局；由于路径数量常呈指数级、而每处格式与解析器的不一致都要调一次 LLM（论文实测：几千条路径就会把流程拖到数小时），SPAR 只要求每个顶点至少被一条正例报文覆盖，用线性时间的贪心算法近似最小路径覆盖，把指数复杂度压成线性。优化二\"线性取反\"：若允许任意组合地取反子约束会得到 2ⁿ 个反例，SPAR 改为每个字段的约束只取反一次，只产生 n 个反例报文，既保证每个字段都被正反各验一遍，又让第 i 个反例专门检验第 i 个约束（且必须按序测试，否则解析器会因前面字段不满足而提前拒绝，使反例失去针对性）。优化三\"程序切片\"：图 11 的例子说明了为什么不能只喂\"生成该字段的那一节 RFC\"——规范里 IHU 的 AE 约束漏掉了 AE=0 和 AE=2，而定义 AE 完整取值的章节（4.1.4）并不在生成 IHU 的 4.6.6 里，只看 4.6.6 无解。SPAR 于是用数据依赖切片找出与字段 f 相关的所有字段，把\"相关 RFC 章节\"取为 M(f) ∪ ⋃M(fᵢ)，从而把 4.1.4 一并纳入，LLM 就能补上缺失的两种情形。

4、评估

4.1 实验设置

实现与配置。 SPAR 构建在 AutoGen [49]（面向 LLM 交互的智能体编程框架）之上，报文生成依托 Z3 [14]；模型温度设为 0 以降低随机性。协议与基准答案。 共 8 个协议：BFD、BGPv4、BABEL 三个来自 ParCleanse [78]，另选 IGMPv3、HTTP2、DNS、NTP、SCTP 五个，理由是它们含有复杂的跨字段约束，恰好能凸显 SPAR 的强项与现有工作的短板（八个协议都是树状、非递归格式，这一限制在 §6 讨论）。RFC 平均 84 页（49–152 页），平均 83 个字段（24–148 个）、18 条单字段约束（2–42 条）、12 条跨字段约束（2–32 条）；由于缺少公开 ground truth，两名作者独立手工从 RFC 抽取、分歧协商解决，并把基准答案公开。对比基线。 ParCleanse [78] 与 ChatAFL [39]——两者都是\"用 LLM 从 RFC 获取形式化规范\"的近期工作，但都没有对抗式交互；3DGEN [19] 因未公开可用而不做对比。LLM 与环境。 默认 GPT-4.1 [45]，另验证 Gemini-2.0-Flash [22]、Claude-3.5-Sonnet [46]、Qwen3-Coder [69]；实验跑在 64 核 / 128 线程 / 3.4 GHz / 256 GB 内存、Ubuntu 22.04 的服务器上。

4.2 有效性：跨字段约束是分水岭

评估维度与规范结构一一对应：字段名与字段类型反映语法准确度，单字段约束与跨字段约束反映语义依赖。判定相当严格——字段名须经人工确认语义等价，复杂类型要求递归匹配，约束通过 SMT 求解器做逻辑等价判定。八协议平均结果（精度/召回）：

语法层面三家都做得不错、精度普遍接近 100%，但 ChatAFL 召回明显偏低——它只为一部分报文类型生成规范（如 BABEL 的大量报文类型被直接漏掉）。语义层面的分水岭出现在跨字段约束：SPAR 平均召回 \\98%\\，ParCleanse \\23%\\，ChatAFL \\2%\\，相对前者提升 \\326%\\、相对后者提升 4800%。这组数字几乎就是论文的结论本身——对抗式 LLM 交互带来的收益，几乎全部体现在跨字段语义约束上，而那恰恰是漏洞检测最需要的信息。

4.3 效率与消融

论文对每个协议各跑 100 次取平均：总耗时从 378.42 秒（IGMPv3）到 5412.90 秒（BABEL，约 1.5 小时），而 SMT 求解器开销只占 1.15%–5.38%——求解器被\"圈\"在可控范围内，是轻量的校验引擎而非计算瓶颈，这正说明优化一、二有效。精化轮数介于 3.51 轮（BFD）到 18.05 轮（BABEL），轮数有界说明对抗交互收敛到不动点而非陷入无限循环；LLM API 成本从 $0.72（BFD）到 $14.05（SCTP），是一次性投入。

消融实验证实了每个组件都不可或缺：去掉 RFC 输入后，单字段约束召回跌到 35%（字段类型 94/47），跨字段约束一条都推不出（记为 -/0）；去掉对抗式精化后，跨字段约束降到 91/22；去掉优化三后降到 93/74。整体看，单字段约束的下降幅度为 5%–67%，跨字段约束为 25%–100%。而优化一、二虽然\"只管效率\"，却直接决定可行性——关掉任何一个，多数协议在 12 小时内根本跑不完，而完整的 SPAR 始终能在至多 1.5 小时内收敛。换用 Gemini-2.0-Flash、Claude-3.5-Sonnet、Qwen3-Coder 后，精度与召回波动都在 8% 以内，说明 SPAR 的有效性不依赖特定 LLM。

4.4 有用性：24 个 0-day

作者用规范去审计 FRRouting [10]（广泛部署于 Linux）与 Holo [11]（面向大规模自动化网络的 Rust 协议套件），做法与精化时一致：用 Z3 依据规范生成正/反例报文打它们的解析器，正例被拒、或反例通过即判定实现有缺陷。结果共发现 24 个 0-day 漏洞，全部依赖正确推断出的约束，且均已被开发者确认或修复——其中 BABEL/FRRouting 13 个（未强制 ae=3, omitted=0、Router-ID 检查缺失、保留位被错误拒绝、子 TLV 处理缺失等）、BFD/FRRouting 4 个、BFD/Holo 7 个（版本检查、状态检查、判别符检查等都发生在查表之后）。论文强调，这 24 个只是能力的\"验证样本\"，真正的价值在于：有了精确规范，就能做形式化验证、自动化一致性测试、甚至生成更安全的解析器，从而降低整个路由生态长期出现实现缺陷的概率。

5、Case Study

论文挑了两个漏洞深入剖析，两者都在代码里藏了 6 年以上（结论章表述为\"最长藏了 9 年\"），共同说明跨字段约束的识别才是发现这类漏洞的关键。

Case 1：BFD 实现——既误检、又漏检。 代码里 cp 表示一个 BFD 报文。问题有两处：一是误检，原代码把 cp->len 当单字段约束检查，但它本该是跨字段约束——cp->len 的合法下限与 cp->flags 中的某一位有关（GETABIT(cp->flags) ? BFD_PKT_LEN+2 : BFD_PKT_LEN）；二是漏检，缺少会话 ID 与协议状态之间的检查——会话 ID 映射到字段 cp->discrs.remote_discr，协议状态映射到 cp->flags，约束是若会话 ID 为 0，协议状态必须是 DOWN 或 ADMIN\_DOWN。作者解释了为什么这条至关重要：BFD 用会话 ID 定位远端会话，并把值为 0 的会话 ID 当作通配符——漏掉检查，攻击者无需猜中随机的 32 位会话 ID 就能伪造网络会话，进而可能导致盲报文注入与拒绝服务。

Case 2：BABEL 实现——Router-ID 检查缺失。 报文字段 Prefix（对应变量 prefix）承载 Update 消息中宣告的地址前缀；当报文里的 Router ID 标志位（packet[3] & 0x40）被置位时，实现会从 prefix 里派生出局部变量 router_id，而另一个字段 AE（packet[2]）决定从 prefix 的哪一段来构造它。论文的修复补上了检查：router_id不能全 0 也不能全 1——这两个保留值分别代表\"未指定\"与\"广播\"地址，无法唯一标识一台路由器。因此这里存在一条横跨 Router ID 标志、AE、Prefix 三个字段的约束：标志位被置位时，由 AE 指定的那一段 Prefix 不得全 0 或全 1。违反它，攻击者就能用一个保留的全 0 标识符绕过内部安全过滤，向路由表注入伪造路由，导致数据被截获、流量被黑洞化或拒绝服务。论文明确指出，ParCleanse 与 ChatAFL 都难以推断出这些跨字段约束，因而无法发现这两处缺失的检查。

值得一提的是，SPAR 的用途不止于网络模糊测试：在 Wireshark [68] 这类流量审计工具里，开发者历来靠手工编写报文解析器，SPAR 可把这一步自动化；用于 Snort [58] 这类 IDS 时，则能把僵硬的字节序列匹配升级为结构感知的规则（例如拿长度头核对实际载荷大小），从而抵御分片、混淆、对齐偏移等规避手段。

6、总结与展望

SPAR 的核心主张可以浓缩为一句话：把\"规范推断\"与\"参考解析器生成\"这两件 LLM 都擅长、但都会幻觉的事，放进一个互为预言机的对抗循环里互相纠错，直到收敛到不动点。 其结果与价值主张也很清晰——把规范推断与有缺陷的实现解耦，绕开\"实现漏检则规范也漏检\"的先天盲视；用对抗式交互纠正幻觉，补上跨字段语义约束这块最大短板（相对 ParCleanse 提升 326%、相对 ChatAFL 提升 4800%）；成本控制在至多 1.5 小时、$15 以内；最终在 FRRouting 与 Holo 两个广泛部署的路由套件中挖出 24 个 0-day。

作者对边界也相当坦诚：为避免报文爆炸而用的路径覆盖与线性取反不保证穷尽覆盖（这是有意为之的取舍，未来可引入组合测试提升覆盖）；目前只处理单一 RFC 定义的协议；受 3D 语言限制，只支持树状格式，无法处理递归/非线性格式，也不强制跨结构的全局约束；此外 RFC 本身还存在语言歧义（\"typically\"\"should\"这类措辞）与未定义行为（规定了约束违背该怎样、却没定义违背后如何处理）。在伦理层面，为不压垮志愿者驱动的开源社区，研究团队自己编写并验证了每个漏洞的修复、打包成 PR 提交，截至成文 20 个补丁已合入主分支，其余在审查中；为缓解\"精确规范等于高保真攻击面地图\"的双重用途风险，作者刻意未公开漏洞检测与测试框架，只发布规范生成器源码（MIT 协议，归档于 Zenodo [71]）。

作者团队介绍

• 论文作者Hengdi Ye、Bing Shui、Jielun Wu、Yufan Zhou、Baowen Xu、Qingkai Shi，均来自南京大学计算机软件新技术全国重点实验室（State Key Laboratory of Novel Software Technology, Nanjing University），通讯作者为 Qingkai Shi。
• 团队长期从事程序分析与软件安全、网络协议逆向与验证、模糊测试、大语言模型辅助程序分析等方向研究，成果见于 USENIX Security、CCS、PLDI、OOPSLA、ISSTA 等顶级会议。本文的多项前置工作也出自该团队：基于实现提取协议格式规范（CCS '23 [53]、USENIX Security '23 [55]）、用可追溯 RFC 解析验证协议解析器的 ParCleanse（ISSTA 2025 [78]）、协议解析器静态差分分析 ParDiff（OOPSLA '24 [77]）——SPAR 正是这条脉络的自然延伸。

安全学术圈 | 投稿须知
有兴趣加入学术圈的请联系 secdr#qq.com

---