信息学院陈浩贤课题组在可解释网络验证领域取得研究进展

随着网络规模不断扩大、配置复杂度不断提升，网络运维人员越来越难以快速判断网络配置是否符合既定设计意图。然而，现有网络验证工具通常只能判断网络配置是否满足预期要求，难以解释“为什么”得到这样的结果，使得工程师在维护、修改或审计网络配置时，仍需手动分析复杂配置与网络行为之间的关联。

针对上述问题，上海科技大学信息科学与技术学院陈浩贤课题组提出了一种基于局部子规约（localized subspecification，subspec）的可解释网络验证框架 SpecLens。该框架能够针对网络配置中的具体字段和配置行生成对应的局部子规约，刻画其对网络设计意图的约束条件，从而帮助运维人员理解配置与网络行为之间的联系。相关研究成果以“Explainable Network Verification via Localized Subspecification”为题发表于计算机网络领域会议ACM SIGCOMM 2026（CCF-A）。

图1：不同粒度的 subspec

为了生成不同粒度的解释，SpecLens 首先基于已验证配置所对应的稳定控制平面状态，提取每个路由器需要保持的功能行为，并构造设备级局部子规约（router-level functional subspecification）。随后针对每个路由器提取其局部配置片段（router-local configuration slice），通过符号化编码与基于 SMT 的常量传播约束化简，将设备级功能约束进一步细化为配置行级和字段级子规约（line-level and field-level subspecifications）。

图2：用户研究界面及 line-level subspec 的提示框。

为了评估subspec 的可解释性，用户研究邀请了网络工程师和计算机网络方向的研究生完成网络维护任务，并比较不提供 subspec 与提供 subspec 两种情况下的任务表现。结果表明，subspec 能够显著提升用户对网络配置的理解，参与者准确率提升了 52%，完成时间缩短了 23%，且 70% 的参与者表示愿意在日常网络运维中参考 subspec。这些结果表明，subspec 具有良好的可解释性和实际应用价值。

同时，研究还进一步验证了框架的可扩展性。实验结果表明，SpecLens 能够在真实网络 Internet2 配置上约 10 分钟内完成配置行和配置字段子规约生成，并可扩展至包含 1,280 台路由器的 FatTree 网络，生成时间约为 25 分钟。这些结果表明，SpecLens 不仅能够提升网络验证结果的可解释性，也具备面向实际网络运维场景的扩展潜力。

上海科技大学为该工作的第一署名单位，合作单位还有南加州大学和西安交通大学。论文第一作者为上海科技大学2024级硕士研究生张永政，陈浩贤教授为通讯作者，上科大2025级硕士研究生林亚旋、2024级本科生马锐泽也参与了该项研究。

SpecLens 的主页：https://declarative-systems-lab.github.io/SpecLens 

用户研究的页面：https://declarative-systems-lab.github.io/SpecLens/userstudy