今天为大家介绍清华大学计算机系徐恪教授团队发表于安全领域顶级会议 USENIX Security 2026 的论文 WAVED: Principled Identification of Off-Path Exploitable Weak Verifications within the TCP/IP Protocol Suite。该工作针对 TCP/IP 协议栈中隐蔽且危害巨大的“弱验证”（Weak Verification）问题，首次提出系统性的自动化检测框架 WAVED。通过创新性的方向敏感污点分析技术，WAVED 能够对复杂内核代码中的路径约束强度进行建模，并精准识别旁路攻击者可利用的脆弱路径。研究团队利用该工具在 Linux 和 FreeBSD 内核中发现 19 个可被旁路攻击的漏洞，其中 14 个为此前从未报告的新问题；所有发现均已向内核社区报送，并被分配 1 个 CVE 编号。

源代码与论文仓库：https://github.com/Internet-Architecture-and-Security/WAVED

01

研究背景

TCP/IP 协议栈是互联网基础设施的基石，为了确保通信的安全与稳定，协议栈在接收数据包时，必须验证其合法性，以区分正常流量与攻击者伪造的恶意流量。然而，由于无状态协议的语义缺失或内核开发者实现上的疏忽，协议栈在执行某些敏感操作前（如修改next hop PMTU导致报文分片）并未经过充分的校验，致使旁路攻击者可以利用这些“弱验证”漏洞欺骗协议栈执行恶意操作，并最终实现流量投毒、连接劫持或拒绝服务。因此，亟需设计一个能够有效地对协议栈到达敏感操作的路径约束进行建模并筛选这类弱验证路径的自动化工具。

02

研究动机与挑战

核心动机：基于“猜测成本”的安全性建模

WAVED 的核心思想源于对旁路攻击本质的重新思考。旁路攻击者不在通信链路中间，无法窃听流量。他们攻击的唯一方式，就是“盲猜”——伪造一个数据包，试图骗过协议栈的检查。因此，一条路径是否安全，取决于攻击者为了通过检查，必须掌握多少正确知识（这里可以表示为猜对多少个字节）。

然而，并不是所有分支检查都会实质对攻击难度产生贡献：类似不等号检查或者单边比较（>或<）的无界约束（如要求序列号在窗口外或者要求pmtu更新时需比原pmtu更小）往往能让攻击者通过填充一个较小值或较大值轻易绕过，而类似等式检查或者区间检查的有界约束（如要求序列号精确命中或在窗口内）才能有效增加旁路攻击者的盲注开销。< p="">

因此，路径约束强度建模不仅需要知道“哪些报文字节影响了分支”，还需要知道约束方向。被有界约束的字节越多，旁路攻击者需要掌握的知识通常越多。基于此，WAVED 提出了一种全新的建模标准：使用有界约束的字节集合表征路径约束强度。该集合的大小可以作为攻击者所需要的必要知识量的有效衡量，同时其中是否包含高安全性字段（如TCP序列号和确认号）也能作为判断弱验证路径的重要依据。

WAVED引入了一种将约束方向包含进污点信息的思路，并称之为方向敏感性（Direction-Sensitivity），并形成了一种基于方向敏感污点分析的路径约束强度建模与弱验证路径筛选方法。

核心挑战与现有工作不足

要从真实内核中自动识别弱验证，分析方法必须同时具备三项能力：(1) 精确恢复跨函数、指针密集的真实代码路径；(2) 量化各条路径所施加的约束强度；(3) 在完整协议栈规模上控制分析成本。现有方法各有贡献，却很难同时满足这三点。

基于静态分析的PacketGuardian 使用隐式污点分析寻找由报文输入影响的危险路径，但复杂分支仍需要人工结合上下文判断；基于模型检查的SCENT 通过模型检查分析协议行为，却需要专家预先抽象模型，模型与真实实现能否保持相同路径约束难以严格保证。基于符号执行的SCAD 使用选择性符号执行检测 non-interference violation，关注两条可观察行为不同的路径是否同时存在。即使只分析 TCP 与 UDP 的有限范围，仍超过 1000 CPU 小时，也不直接回答“一条路径已有的校验究竟有多强”。

WAVED 的目标不是全面替代这些方法，而是在克服以上挑战的同时，补全弱验证路径识别场景下真实实现中的路径强度建模与规模化筛选。

03

WAVED 系统设计

WAVED 的核心是一个包含四个阶段的深度静态分析流水线，为了在数百万行代码中精准捕捉“弱验证”逻辑，WAVED 设计了四个环环相扣的分析阶段：(1) 首先通过指针分析理清内核复杂的内存引用关系；(2) 接着构建字节粒度污点图，精确追踪攻击者输入的每一个字节流向；(3) 核心的分支影响求解器负责“读懂”代码中的检查逻辑，量化约束强度；(4) 最后由弱验证识别器在全路径上进行搜索与过滤，输出最终的漏洞报告。

WAVED的完整系统总共包括四个模块：面向内核协议的指针分析 (Protocol-Oriented Pointer Analysis)、字节粒度污点分析 (Byte-Granularity Taint Analysis)、分支影响求解器 (Branch Impact Calculator)和弱验证路径识别器 (Weak Path Identifier)。

面向内核协议的指针分析

为将指针分析覆盖完整协议栈，WAVED面向内核协议栈源代码拓展SVF静态分析工具进行了全程序分析，同时向稀疏值流图（Sparse Value-Flow Graph，SVFG）中引入了上下文敏感性以支持复杂的跨函数调用分析。此外，注意到目前大部分静态分析工具在处理获取元素指针（GEP）指令时常采用基于字段下标的方式来索引结构体成员，这种方式可以有效的处理由父结构体指针往内访问子结构体指针的行为，但是无法解析子结构体往外访问父结构体或是同级结构体之间互相索引的行为，而这些行为在内核实现中经常出现（如Linux中的container_of宏），WAVED因此在指针分析中实现了一种基于物理字节偏移的索引方式，解决了这一问题并达到了更高的精度。

字节粒度污点分析

为辅助后续模块计算， WAVED在此阶段中通过建立污点传播图（Taint Propagation Graph，TPG）表示协议栈实现中全量的字节粒度数据流传播关系。污点传播图为实现字节敏感，扩展了上下文敏感的SVFG，每个点表示一个LLVM Value，每条边上附带了一个8×8的位图map，其中map[i][j]=1表示该边起点的第i个字节的污点可以传播到该边终点的第j个字节。WAVED针对LLVM IR中的各类指令分别建模了共计7类污点传播边，通过类似矩阵乘法的传播计算，WAVED 可以高效地计算出跨越多个指令的复合污点传播关系。为加速计算，WAVED采用了一种所有路径交汇（Meet-Over-All-Paths，MOP）的计算方式，在标记污点源后运行Tabulation算法以保证上下文无关文法可达性（CFL-Reachability），达到较高的精度。

分支影响求解器

本模块为计算方向敏感污点的核心模块，WAVED在其中扩展了传统的污点表示，提出了方向敏感污点元组（Taint Tuple），其包含了当前位置的所有受约束输入字节，并将其分为了三个子集合：L集合，G集合和E集合。其中L集合表示受到上界约束的字节集合，G集合表示受到下界约束的字节集合，E集合表示受到有界约束的字节集合。当两个污点元组需要同时满足，即进行逻辑与运算时，可以理解为各约束集合的求并。

当一个字节同时受到上界约束和下界约束时，其相当于受到了区间约束（即有界约束），即在每次求或后，污点元组必须进行如下归约：

由于污点元组之间的逻辑与无法直接使用约束集合的运算得到，WAVED显式定义了分支约束（Branch Impact），表示若干污点元组的逻辑与，并分别定义了分支影响的逻辑或与运算规则，至此分支影响可以完整表示一个分支跳转处的方向敏感约束。

为了精准区分条件跳转处 True 与 False 分支的约束差异，并解决内核中广泛存在的“隐式污点”问题，WAVED 设计了一套隐式污点分析与高效求解算法：

1. 隐式污点的二元状态建模

内核协议栈常将控制流约束“隐藏”在辅助函数（Helper Function）的返回值中（例如返回 0 代表成功，NULL 代表失败）。为了读懂这种隐式逻辑，WAVED 对每个 LLVM Value 维护了一对分支影响，分别表征其取 “零值/空值” 与 “非零值/非空值” 时所需的路径约束。这种二元建模精准捕获了隐藏在数据流中的控制流信息。

2. 基于拓扑序的按需迭代求解

为了兼顾精度与效率，WAVED 摒弃了盲目的全量传播，而是采用了一种基于拓扑序的迭代求解算法：

（1）遍历策略：算法在去除控制流环后，严格按照拓扑顺序依次遍历函数内的每个基本块。

（2）逆向计算与摘要更新：在遍历过程中，WAVED 同时执行两项任务：

① 分支影响计算：仅在遇到条件跳转指令（即需求点）时，根据预定义的 7 类指令逆向规则，解析当前 Value 的分支影响。

② 函数摘要更新：同步计算并更新当前函数的摘要。该摘要通过对路径上所有控制依赖的分支影响进行逻辑与运算获得，最终记录了从函数入口到当前点的所有可能跳转路径及其约束。

弱验证路径识别器

基于预求解的函数摘要，WAVED建立了函数摘要图（Summary Graph），以表示协议栈的跨过程控制流及其路径约束，并保持了上下文敏感性。在标记需要分析的敏感操作后，WAVED在函数摘要图上从协议栈入口函数进行到达所有敏感操作的深度优先搜索并合并函数摘要中的路径约束，同时动态过滤出所有可能的弱验证路径。在其中，为提高分析精度和降低最终的人工分析量，WAVED开启了三种优化机制。

  1. 首部激活 (Header Activation)：因为上下文敏感分析的精度与维护的调用栈深度有关，对于某些较深的函数调用污点分析可能会产生误报，当且仅当到达一个协议的入口处理函数时才会激活该首部的污点追踪。

  2. 约束去重 (Constraint Deduplication)：由于内核协议栈中复杂的快速/慢速路径实现，许多函数内路径会呈现出相同的约束，为了缓解此问题与隐式污点分析带来的大量误报，如果一个新到达的分支跳转并不会更新当前路径的累计分支影响的值，其不会被用作路径去重的依据，因此所有包含相同路径约束前缀且最终约束相同的函数内路径会被去重。

  3. 强度过滤 (Strength Filtering)：根据方向敏感污点的定义，如果一条路径约束的分支影响中存在一个污点元组的E集合大小小于一个设定的阈值（预设为8，参考内嵌UDP的ICMP Redirect攻击），且不包含任何高安全性字段（如TCP/DCCP序列号/确认号，SCTP验证标签），那么其会被标记为弱验证并报告给用户。

04

实验验证与漏洞发现

研究团队标记了两类敏感操作——缓存投毒和报文注入，利用 WAVED 对 Linux 5.15、Linux 6.8 和 FreeBSD 14.1 的内核IPv4/IPv6协议栈进行了检测，涵盖ICMP、TCP、UDP、SCTP、DCCP协议实现。其中，分析Linux 5.15的IPv4/IPv6协议栈分别花费了22和30分钟，分析Linux 6.8分别花费了11和21分钟，分析FreeBSD 14.1分别花费了42和125分钟，得益于各类加速优化，相比现有自动化工作达到了较高的效率。

WAVED总共报告了31个TP和12个FP，达到了72%的准确率，经团队手动分析发现，这些FP均是由底层静态分析无法分析程序运行时具体值的局限性导致的，与WAVED中实现的机制无关，由于这些FP大多有相似的结构，并不会为后续人工排查带来过多的影响。

团队同样进行了消融实验，以研究WAVED在减少路径空间的效果。分别对比了WAVED的完整实现和使用传统隐式污点分析（w/o DT）以及关闭强度过滤（w/o SF）两类情况的报告路径总量。实验表明，相比与传统污点分析，WAVED在各种类型下平均降低了89.3%的报告路径总量，在约束去重后开启强度过滤使得WAVED在各种类型下平均过滤了53.6%的待选路径，这些路径均受到了鲁棒的约束使得旁路攻击者难以绕过。

WAVED总共发现了19个可被旁路攻击的弱验证漏洞，其中14 个新漏洞，并被分配一个CVE编号(CVE-2026-46266)。关于算法、实验和漏洞细节，欢迎阅读完整版论文。

05

结语

WAVED 是首个针对 TCP/IP 协议栈弱验证问题进行系统性建模和检测的框架。该工作揭示了即便是成熟的操作系统内核协议栈，在处理报文或异常流程时，依然面临着严峻的逻辑安全风险。研究团队呼吁开发者在实现网络协议时，应审慎对待无状态协议和快速/慢速路径的处理逻辑，引入更严格的验证机制并确保每条路径都得到了充分逻辑校验，以抵御旁路攻击。WAVED所采用的方法可以被迁移至更多协议和更多系统（如网络中间件）的安全研究中，为网络安全建设添砖加瓦。

在大模型也开始参与漏洞挖掘的今天，这类程序分析方法仍有其独特价值，能够以明确的机制、可追踪的证据和可复现的结果，为漏洞研究提供可靠的科学依据。

声明：本文来自赛博新经济，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。