可扩展的网络验证技术：研究现状与发展趋势

黄翰林; 徐恪; 李琦; 李彤; 付松涛; 高翔宇

doi:10.12263/DZXB.20230682

您当前的位置：

首页 >

文章列表页 >

可扩展的网络验证技术：研究现状与发展趋势

中国电子学会科学技术奖特约专栏 | 更新时间：2025-12-08

- 可扩展的网络验证技术：研究现状与发展趋势
- Scalable Network Verification Technologies: State of the Art and Future
- 电子学报 2024年52卷第4期页码：1083-1102
- 作者机构：
  
  1.清华大学计算机科学与技术系,北京 100084
  2.北京信息科学与技术国家研究中心,北京 100084
  3.中关村实验室,北京 100094
  4.清华大学网络科学与网络空间研究院,北京 100084
  5.数据工程与知识工程教育部重点实验室(中国人民大学),北京 100872
- 作者简介：
  
  [ "黄翰林男，1998年7月出生于河南省信阳市.清华大学计算机系博士研究生.主要研究方向为网络验证和网络安全.E-mail: hhl21@mails.tsinghua.edu.cn" ]
  [ "徐恪男，1974年12月出生于江苏省淮安市.现为清华大学计算机系教授、博士生导师.获得国家技术发明奖二等奖1项，国家科技进步奖二等奖1项，省部级特等奖1项，省部级一等奖5项.主要研究方向新一代互联网体系结构、网络空间安全、区块链系统.中国电子学会会员编号：E190008630F.E-mail: xuke@mail.tsinghua.edu.cn" ]
  [ "李琦男，1979年1月出生于浙江省长兴县.现为清华大学网络研究院副教授、博士生导师.主要研究方向为互联网安全.中国电子学会会员编号：E190026656S.E-mail: qli01@tsinghua.edu.cn" ]
  [ "李彤男，1989年9月出生于湖南省涟源市.现为中国人民大学副教授、杰出学者、硕士生导师.主要研究方向为新一代互联网体系结构、分布式系统、大数据.E-mail: tong.li@ruc.edu.cn" ]
  [ "付松涛男，1982年2月出生于贵州省遵义市.2023年获清华大学计算机系博士学位.现为卫星通信中心工程师.主要研究方向为计算机网络、卫星通信.中国电子学会会员编号：E190024348A.E-mail: fust18@tinghua.org.cn" ]
  [ "高翔宇男，1999年5月出生于辽宁省沈阳市.清华大学网络研究院硕士研究生.主要研究方向为计算机网络和网络安全.中国电子学会会员编号：E190028664A.E-mail: gaoxy21@mails.tsinghua.edu.cn" ]
- 基金信息：
  
  国家重点研发计划(2022YFB3102300;2022YFB3102301);国家自然科学基金(61932016;62132011;62202473;U22B2031;61825204);北京高校卓越青年科学家计划(BJJWZYJH01201910003011);Beijing Outstanding Young Scientist Program(BJJWZYJH01201910003011)
- DOI：10.12263/DZXB.20230682
  中图分类号： TP393;
- 收稿：2023-07-21，
  
  修回：2023-11-18，
  
  纸质出版：2024-04-25
- 稿件说明：
移动端阅览
黄翰林,徐恪,李琦,等.可扩展的网络验证技术：研究现状与发展趋势[J].电子学报,2024,52(04):1083-1102.

HUANG Han-lin, XU Ke, LI Qi, et al.Scalable Network Verification Technologies: State of the Art and Future[J].Acta Electronica Sinica, 2024, 52(04): 1083-1102.
黄翰林,徐恪,李琦,等.可扩展的网络验证技术：研究现状与发展趋势[J].电子学报,2024,52(04):1083-1102. DOI：10.12263/DZXB.20230682

HUANG Han-lin, XU Ke, LI Qi, et al.Scalable Network Verification Technologies: State of the Art and Future[J].Acta Electronica Sinica, 2024, 52(04): 1083-1102. DOI：10.12263/DZXB.20230682

摘要

互联网作为国家信息基础设施的重要组成部分，已经在各个领域发挥着巨大的作用.随着其规模不断扩大和应用持续深入，我们也面临着意图不一致的网络行为可能导致的灾难性危害.为了确保互联网的正常运行和网络行为的一致性，我们迫切需要可部署的网络验证技术，以确保网络运行时的行为与网络运维人员的意图一致.当前已经有许多关于网络验证技术的研究，这些研究帮助用户实现自动检测网络错误，并进一步分析错误产生的原因.然而，为了满足互联网规模不断扩大的需求，可扩展性问题成为在互联网部署网络验证技术的一项重要挑战.即如何在满足时间和空间复杂度约束的前提下，快速发现并排查网络策略的错误，真正将网络验证技术应用于实际，成为一个研究热点.本文从数据面验证和控制面验证两个方面出发，深入研究和总结了现有的网络验证研究工作，并探索了基于时空优化的可扩展性技术，对这些方案的特点进行了系统性分析.最后，本文总结和展望了网络验证可扩展技术的未来研究趋势，为该领域的研究人员提供一定的参考.

Abstract

The Internet

as a critical component of a nation's information infrastructure

has played a significant role in various domains. However

as its scale continues to expand and its applications deepen

we also face the potential catastrophic consequences of inconsistent network behaviors. To ensure the normal operation of the Internet and the consistency of network behaviors

there is an urgent need for deployable network verification technologies that align network operations with the intentions of network operators. Extensive research has been conducted on network verification technologies

assisting users in automating the detection of network errors and analyzing their root causes. However

to meet the increasing demands of the expanding Internet

scalability has become a crucial challenge in deploying network verification technologies. Specifically

how to quickly identify and diagnose errors in network policies

while satisfying time and space complexity constraints

has become a research hotspot in effectively applying network verification technologies in practice. To address this problem

this paper delves into and summarizes cutting-edge research on the temporal and spatial scalability of network verification. It begins by introducing the background knowledge related to network verification and then describes the current issues and challenges faced in network verification. Focusing on the core issue of scalability

the paper thoroughly analyzes existing work in achieving scalable verification from both the data plane and control plane perspectives. It provides a systematic analysis of the characteristics of these approaches

showcasing the distinctions and connections among related studies. According to the existing researches

we find that: (1) The scalability of data plane verification is primarily constrained by header space and forwarding matching rules

while the scalability of control plane verification is mainly limited by the complexity of multiple protocols and policies. (2) Although both data plane and control plane research employ similar scalable verification techniques

they address different but interconnected targets. For example

incremental computation in the data plane primarily focuses on updating packet equivalence classes

while incremental computation in the control plane primarily deals with network models affected by configuration changes. When applying network slicing techniques

both data plane and control plane independently validate the network by dividing it into multiple segments. (3) Compared to spatial scalability

current research places greater emphasis on temporal scalability

where reducing verification time overhead appears to be the primary pursuit of verification tools. (4) Previous research predominantly adopted a centralized verification approach

which involved collecting control plane or data plane information and then performing centralized analysis and verification. However

there has been a recent trend towards distributed verification

such as Coral and Tulkun in control plane verification. Lastly

based on the current research landscape

the paper concludes by summarizing and forecasting the research trends in scalable network verification technologies

offering valuable insights for researchers in this field. In conclusion

this paper presents a comprehensive review and outlook on the topic of scalability in network verification. It emphasizes the importance of aligning network behaviors with the intentions of network operators to ensure the reliable and consistent operation of the Internet. By addressing the challenges of scalability

researchers can advance the development of network verification technologies that can effectively verify large-scale networks within the constraints of time and space complexity. Ultimately

this contributes to enhancing the reliability and security of the Internet as a critical information infrastructure.

关键词

Keywords

references

JANGJOU M , SOHRABI M K . A comprehensive survey on security challenges in different network layers in cloud computing [J ] . Archives of Computational Methods in Engineering , 2022 , 29 ( 6 ): 3587 - 3608 .

DHATRAK A , SARKAR A , GORE A , et al . Cyber security threats and vulnerabilities in IoT [J ] . International Research Journal of Engineering and Technology , 2020 , 7 ( 3 ): 2921 - 2925 .

DEB R , ROY S . Dynamic vulnerability assessments of software-defined networks [J ] . Innovations in Systems and Software Engineering , 2020 , 16 ( 1 ): 45 - 51 .

PAN L , QIU R , WANG A , et al . Measuring the resolution resiliency of second-level domain name [C ] // InScience and Information Conference . Cham : Springer , 2022 : 742 - 755 .

ABHASHKUMAR A , GEMBER-JACOBSON A , AKELLA A . Tiramisu: Fast multilayer network verification [C ] // Proceedings of the 17th USENIX Conference on Networked Systems Design and Implementation . New York : ACM , 2020 : 201 - 220 .

LI Y , YIN X , WANG Z , et al . A survey on network verification and testing with formal methods: Approaches and challenges [J ] . IEEE Communications Surveys & Tutorials , 2018 , PP(99): 1.

ZHANG X , WANG C , LI Q , et al . Toward comprehensive network verification: Practices, challenges and beyond [J ] . IEEE Network , 2020 , 34 ( 1 ): 108 - 115 .

方星 , 胡波 , 马超 , 等 . 网络验证研究综述 [J ] . 软件学报 , 2023 , 34 ( 1 ): 351 - 380 .

FANG X , HU B , MA C , et al . Survey on network verification [J ] . Journal of Software , 2023 , 34 ( 1 ): 351 - 380 . (in Chinese)

PRABHU S , CHOU KY , KHERADMAND A , et al . Plankton: Scalable network configuration verification through model checking [C ] // Proceedings of the 17th USENIX Conference on Networked Systems Design and Implementation . New York : ACM , 2020 : 953 - 968 .

SHAO X , GAO L . Verifying policy-based routing at internet scale [C ] // Proceedings of IEEE International Conference on Computer Communications (INFOCOM) . Piscataway : IEEE , 2020 : 2293 - 2302 .

YUAN Y , MOON SJ , UPPAL S , et al . NetSMC: A custom symbolic model checker for stateful network verification [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2020 : 181 - 200 .

NELSON T , FERGUSON AD , SCHEER MJ , KRISHNAMURTHI S . Tierless programming and reasoning for software-defined networks [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2014 : 519 - 531 .

YANG R , XING F , LIZHAO Y , et al . Diagnosing distributed routing configurations using sequential program analysis [C ] // Proceedings of the Asia-Pacific Workshop on Networking (APNet) . New York : ACM , 2023 : 34 - 40 .

KAZEMIAN P , GEORGE V , NICK M . Header space analysis: Static checking for networks [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2012 : 113 - 126 .

RUCHANSKY N , PROSERPIO D , CANINI M , et al . A nice way to test openflow applications [C ] // Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2012 : 127 - 140 .

GEMBER-JACOBSON A , VISWANATHAN R , AKELLA A , MAHAJAN R , et al . Fast control plane analysis using an abstract representation [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2016 : 300 - 313 .

TANG A L , BECKETT R , BENALOH S , et al . Lightyear: Using modularity to scale bgp control plane verification [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2023 : 94 - 107 .

FAYAZ S K , SHARMA T , FOGEL A , et al . Efficient network reachability analysis using a succinct control plane representation [C ] // Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI) . New York : ACM , 2016 : 217 - 232 .

ZHANG P , WANG D , GEMBER-JACOBSON A . Symbolic router execution [C ] // Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2022 : 336 - 349 .

XIANG Q , HUANG C Y , WEN R D , et al . Beyond a centralized verifier: Scaling data plane checking via distributed, on-device verification [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2023 : 152 - 166 .

GUHA , A , REITBLATT M , FOSTER N . Machine-verified network controllers [J ] . ACM SIGPLAN Notices , 2013 , 48 ( 6 ): 483 - 494 .

BALL T , BJØRNER N , GEMBER A , et al . VeriCon: Towards verifying controller programs in software-defined networks [C ] // Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation . New York : ACM , 2014 : 282 - 293 .

ANDERSON C J , FOSTER N , GUHA A , et al . NetKAT: semantic foundations for networks [C ] // Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation . New York : ACM , 2014 : 113 - 126 .

PANDA A , LAHAV O , ARGYRAKI K , et al . Verifying reachability in networks with mutable datapaths [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2017 : 699 - 718 .

MAI H , KHURSHID A , AGARWAL R , et al . Debugging the data plane with anteater [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2011 : 290 - 301 .

YE F , YU D , ZHAI E , et al . Accuracy, scalability, coverage: A practical configuration verifier on a global WAN [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2020 : 599 - 614 .

WEBSTER M , WESTERN D , ARAIZA-ILLAN D , et al . A corroborative approach to verification and validation of human-robot teams [J ] . The International Journal of Robotics Research , 2020 , 39 ( 1 ): 73 - 99 .

DANIEL LA , BARDIN S , REZK T . Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level [C ] // Proceedings of the IEEE Symposium on Security and Privacy (SP) . Piscataway : IEEE , 2020 : 1021 - 1038 .

HANDIGOL N . Intent-based verification leading a new wave of network automation [EB/OL ] . ( 2019-05-21 ) [ 2023-07-01 ] . https://www.networkcomputing.com/networking/intent-based-verification-leading-new-wave-network-automation https://www.networkcomputing.com/networking/intent-based-verification-leading-new-wave-network-automation .

BECKETT R , GUPTA A , MAHAJAN R , et al . A general approach to network configuration verification [C ] // Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2017 : 155 - 168 .

ZENG H Y , ZHANG S D , YE F , et al . Libra: Divide and conquer to verify forwarding tables in huge networks [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2014 : 87 - 99 .

ZHANG P , LIU X , YANG H , et al . APKeep: Realtime verification for real networks [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2020 : 241 - 255 .

AWEYA J . IP Routing Protocols: Link-State and Path-Vector Routing Protocols [M ] . First edition . Boca Raton : CRC Press , 2021 .

PLOTKIN G D , BJØRNER N , LOPES N P , et al . Scaling network verification using symmetry and surgery [J ] . ACM SIGPLAN Notices , 2016 , 51 ( 1 ): 69 - 83 .

AL-FARES M , LOUKISSAS A , VAHDAT A . A scalable, commodity data center network architecture [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2008 : 63 - 74 .

ABDALLA H B , AHMED A M , SIBAHEE MA A L . Optimization driven mapreduce framework for indexing and retrieval of big data [J ] . KSII Transactions on Internet and Information Systems , 2020 , 14 ( 5 ): 1886 - 1908 .

GUO D , CHEN S S , GAO K , et al . Flash: Fast, consistent data plane verification for large-scale network settings [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2022 : 314 - 335 .

HORN A , KHERADMAND A , PRASAD M R . Delta-net: Real-time network verification using atoms [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2017 : 735 - 749 .

FAYAZ S K , YU T L , TOBIOKA Y , et al . BUZZ: Testing context-dependent policies in stateful networks [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2016 : 275 - 289 .

ZENG H Y , KAZEMIAN P , VARGHESE G , et al . Automatic test packet generation [C ] // Proceedings of the International Conference on Emerging Networking Experiments and Technologies (CoNEXT) . New York : ACM , 2012 : 241 - 252 .

KHURSHID A , ZOU X , ZHOU W X , et al . VeriFlow: Verifying network-wide invariants in real time [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2013 : 15 - 28 .

ZHANG K Y , ZHUO D Y , AKELLA A , et al . Automated verification of customizable middlebox properties with gravel [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2020 : 221 - 240 .

The P 4 Language Consortium . P 4 portable NIC architecture[EB/OL ] . ( 2021-05-18 )[ 2023-11-28 ] . https://p4.org/p4-spec/docs/PNA.html https://p4.org/p4-spec/docs/PNA.html .

ZHANG Y C . SONiC system architecture [EB/OL ] . ( 2022-07-21 )[ 2023-11-28 ] . https://github.com/sonic-net/SONiC/wiki/Architecture https://github.com/sonic-net/SONiC/wiki/Architecture .

YANG H K , LAM S S . Real-time verification of network properties using atomic predicates [J ] . IEEE/ACM Transactions on Networking , 2015 , 24 ( 2 ): 887 - 900 .

WANG H Z , QIAN C , YU Y , et al . Practical network-wide packet behavior identification by AP classifier [J ] . IEEE/ACM Transactions on Networking , 2017 , 25 ( 5 ): 2886 - 2899 .

BECKETT R , GUPTA A . Katra: Realtime verification for multilayer networks [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2022 : 617 - 634 .

MAHALINGAM M , DUTT D , DUDA K , et al . Virtual eXtensible Local Area Network (VXLAN): A Framework for Overlaying Virtualized Layer 2 Networks over Layer 3 Networks:RFC 7348:2014 [S/OL ] .( 2020-01-21 )[ 2023-12-20 ] . https: //doi.org/10.17487/RFC7348 https://doi.org/10.17487/RFC7348 .

LI J Q , ZHOU M . Research on VPN in experimental simulation environment based on GRE and IPSec [C ] // Proceedings of the International Conference on Robotics and Artificial Intelligence . New York : ACM , 2020 : 220 - 224 .

RENGANATHAN S , RUBIN B , KIM H , et al . Hydra: Effective runtime network verification [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2023 : 182 - 194 .

XIANG Q , WEN R D , HUANG C Y , et al . Network can check itself: Scaling data plane checking via distributed, on-device verification [C ] // Proceedings of the ACM Workshop on Hot Topics in Networks (HotNets) . New York : ACM , 2022 : 85 - 92 .

FOGEL A , FUNG S , PEDROSA L , et al . A general approach to network configuration analysis [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2015 : 469 - 483 .

RUMREICH L . The Binary Decision Diagram: Formal Verification of a Reference Implementation [R ] . Columbus : The Ohio State University , 2021 .

BECKETT R , GUPTA A , MAHAJAN R , et al . Control plane compression [C ] // Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2018 : 476 - 489 .

THIJM T A , BECKETT R , GUPTA A , et al . Kirigami, the verifiable art of network cutting [C ] // Proceedings of the IEEE International Conference on Network Protocols (ICNP) . Piscataway : IEEE , 2022 : 1 - 12 .

ZHANG P , HUANG Y H , GEMBER-JACOBSON A , et al . Incremental network configuration verification [C ] // Proceedings of the ACM Workshop on Hot Topics in Networks . New York : ACM , 2020 : 81 - 87 .

ZHANG P , GEMBER-JACOBSON A , ZUO Y , et al . Differential network analysis [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2022 : 601 - 615 .

STEFFEN S , GEHR T , TSANKOV P , et al . Probabilistic verification of network configurations [C ] // Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2020 : 750 - 764 .

SCHNEIDER T , BIRKNER R , VANBEVER L . Snowcap: Synthesizing network-wide configuration updates [C ] // Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2021 : 33 - 49 .

CHLIPALA A . Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant [M ] . Cambridge : MIT Press , 2022 .

MCKEOWN N , ANDERSON T , BALAKRISHNAN H , et al . OpenFlow: Enabling innovation in campus networks [C ] // Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM) . New York : ACM , 2008 : 69 - 74 .

BERDE P , GEROLA M , HART J , et al . ONOS: Towards an open, distributed SDN OS [C ] // Proceedings of the Third Workshop on Hot Topics in Software Defined Networking (HotSDN) . New York : ACM , 2014 : 1 - 6 .

MORALES LV , MURILLO AF , RUEDA SJ . Extending the floodlight controller [C ] // Proceedings of the IEEE International Symposium on Network Computing and Applications (NCA) . Piscataway : IEEE , 2015 : 126 - 133 .

RAMANATHAN S , ZHANG Y , GAWISH M , et al . Practical intent-driven routing configuration synthesis [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2023 : 629 - 644 .

KIM H , REICH J , GUPTA A , et al . Kinetic: Verifiable dynamic network control [C ] // Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI) . New York : ACM , 2015 : 59 - 72 .

XU H , QIN Q , FANG X , et al . Toward privacy-preserving interdomain configuration verification via multi-party computation [C ] // Proceedings of the Asia-Pacific Workshop on Networking (APNet) . New York : ACM , 2023 : 28 - 33 .

LOPES NP , RYBALCHENKO A . Fast BGP simulation of large datacenters [C ] // International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) . Cham : Springer , 2019 : 386 - 408 .

饶琛琳 . 大模型在运维领域的应用展望 [EB/OL ] . ( 2023-08-10 ) [ 2023-11-28 ] . https://mp.weixin.qq.com/s/ewuSv2wX0uouyg9JOQDIMA https://mp.weixin.qq.com/s/ewuSv2wX0uouyg9JOQDIMA .

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于大语言模型的SDN网络自动化配置研究

基于分片技术的区块链可扩展性研究综述

一种具有O信息复杂度的高速crossbar调度算法

基于TCAD与DNN的FinFET器件辐射总剂量效应模型

基于加权优先级与数据包到达时间的MP-QUIC调度算法