厦门大学系统与网络团队的一项研究成果被网络领域最具影响力的会议ACM SIGCOMM’23 (CCF-A)录用，提出了一种分布式网络设备数据平面自验证框架。SIGCOMM是ACM组织的网络通信领域旗舰型会议，第37届SIGCOMM将于2023年9月10日至14日在美国纽约市举行。本次会议共录用71篇论文，录用率为22% (71/323)。该成果是SNGroup继2022年发表厦门大学首篇通讯单位SIGCOMM论文后，连续第二年在SIGCOMM发表论文，也是厦门大学首篇以第一单位发表的SIGCOMM论文。

具体论文信息如下

Qiao Xiang（厦门大学SNG）, Chenyang Huang (厦门大学SNG二年级硕士生), Ridi Wen (厦门大学SNG二年级硕士生), Yuxin Wang(厦门大学SNG二年级硕士生), Xiwen Fan(厦门大学SNG一年级硕士生), Zaoxing Liu (波士顿大学), Linghe Kong (上海交通大学), Dennis Duan (耶鲁大学毕业生), Franck Le(IBM Research), Wei Sun(得克萨斯大学奥斯汀分校博士生)

Beyond a Centralized Verifier: Scaling Data Plane Checking via Distributed, On-Device Verification(SIGCOMM’23)

【论文简介】

已有的数据平面验证工具均采用集中式架构，将网络设备的数据平面信息收集到集中验证器上进行验证计算。这样的架构不仅需要一个可以时刻保持验证器与网络之间可靠互联的管理网络，同时，集中验证器也会成为性能瓶颈与单一故障点，因此集中式数据平面验证工具无法适用于数据中心、环球广域网等大规模网络。为此，本文提出了一种分布式的网络设备数据平面自验证 (distributed data plane verification，简称DDPV) 框架，其核心思想是将复杂的数据平面验证问题转化为有向无环图上的简单计数问题，从而将算力/内存密集型的集中式验证计算分解为轻量的设备级验证子任务，并下放到网络设备上分布式执行，从而实现对任意规模网络的快速、高效数据平面网内自验证。本框架由四个核心部件构成，如图1所示：

（1）基于正则表达式的高级声明式网络不变量规格语言(invariant specification language)：支持管理员高效且灵活地表达常见的网络不变量规格；

（2）验证规划器：将管理员指定的网络不变量与网络拓扑进行有限自动状态机乘法，得到有向无环图DVNet，并以此系统地将复杂的全局验证任务分解为设备上的轻量级计数子任务；

（3）分布式验证消息协议：定义相邻的网络设备间如何有效、可靠地交换各自的计数子任务结果，从而实现网络不变量快速、高效的网内自验证；

（4）不变量容错验证机制：通过在DVNet计算过程中引入链路失效场景预计算，在最小化验证规划器重新规划频率的同时，实现链路失效场景下的网络不变量快速分布式网内自验证。

实验结果表明：

实验结果表明，本框架能够在41秒内对一个拥有超过6000台交换机的大型数据中心网络完成全量验证，比目前最快的集中式验证工具Flash快了7.4倍。同时，在80%的增量验证实验中，本框架与最快的集中式验证工具相比，最高可以实现2355倍的验证加速。

在进行理论创新与广泛实验的基础上，我们还在开源网络操作系统SONiC社区上提出将这一分布式网络设备数据平面自验证框架融入SONiC生态。目前该提案的high-level design (HLD)正在接受审核。

同时，在多款商用交换机实机上进行的测试表明，本框架所提出的设备级验证器仅需消耗极低的CPU和内存即可高效运行。本框架的源代码将会在SIGCOMM’23会议举行前公开，敬请关注。

本工作是厦门大学系统与网络课题组在网络与形式化方法方面的进一步探索，之前的研究工作包括控制平面验证加速Solvability Digraph [INFOCOM’21], 数据平面验证加速Flash [SIGCOMM’22],分布式数据平面验证Coral [HotNets’22], 网络配置诊断修复Scalpel [APNet’23]和域间网络配置验证InCV [APNet’23]，更多内容可访问：

视频展示: https://distributeddpvdemo.tech/

功能展示: https://www.distributeddpchecking.com/

厦门大学系统与网络课题组主页:

http://sngroup.org.cn/