research-article

Beyond a Centralized Verifier: Scaling Data Plane Checking via Distributed, On-Device Verification

Authors:

Chenyang Huang,

Wei SunAuthors Info & Claims

ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference

Pages 152 - 166

https://doi.org/10.1145/3603269.3604843

Published: 01 September 2023 Publication History

Abstract

Centralized data plane verification (DPV) faces significant scalability issues in large networks (i.e., the verifier being a performance bottleneck and single point of failure and requiring a reliable management network). We tackle this scalability challenge by introducing Tulkun, a distributed, on-device DPV framework. Our key insight is that DPV can be transformed into a counting problem on a directed acyclic graph, which can be naturally decomposed into lightweight tasks executed at network devices, enabling fast data plane checking in networks of various scales and types. With this insight, Tulkun consists of (1) a declarative invariant specification language, (2) a planner that employs a novel data structure DPVNet to systematically decompose global verification into on-device counting tasks, (3) a distributed verification messaging (DVM) protocol that specifies how on-device verifiers efficiently communicate task results to jointly verify the invariants, and (4) a mechanism to verify invariant fault-tolerance with minimal involvement of the planner. Extensive experiments with real-world datasets (WAN/LAN/DC) show that Tulkun verifies a real, large DC in 41 seconds while others tools need minutes or up to tens of hours, and shows an up to 2355× speed up on 80% quantile of incremental verification with small overhead on commodity network devices.

References

[1]

Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast Multilayer Network Verification. In NSDI'20. USENIX, 201--219.

[2]

Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. 2008. A Scalable, Commodity Data Center Network Architecture. In SIGCOMM'08. ACM, 63--74.

[3]

Ehab Al-Shaer and Saeed Al-Haj. 2010. FlowChecker: Configuration Analysis and Verification of Federated OpenFlow Infrastructures. In SafeConfig'10. ACM, 37--44.

[4]

Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks. Acm sigplan notices 49, 1 (2014), 113--126.

Digital Library

[5]

Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, and Asaf Valadarsky. 2014. Vericon: Towards Verifying Controller Programs in Software-Defined Networks. In SIGPLAN'14. ACM, 282--293.

Digital Library

[6]

Barefoot. 2019. UfiSpace S9180-32X S9180-32X Switch. https://www.ufispace.com/uploads/able/files/productfilemanager/000045467d1fc648d792c404372956a0.pdf.

[7]

Ryan Beckett and Aarti Gupta. 2022. Katra: Realtime Verification for Multilayer Networks. In NSDI'22. USENIX, 617--634.

[8]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A General Approach to Network Configuration Verification. In SIGCOMM'17. ACM, 155--168.

Digital Library

[9]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2018. Control Plane Compression. In SIGCOMM'18. ACM, 476--489.

[10]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2019. Abstract Interpretation of Distributed Network Control Planes. PACMPL'19, 1--27.

[11]

Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, and David Walker. 2016. Don't Mind the Gap: Bridging Network-Wide Objectives and Device-Level Configurations. In SIGCOMM'16. ACM, 328--341.

Digital Library

[12]

Nikolaj Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A Seshia, and George Varghese. 2016. Ddnf: An Efficient Data Structure for Header Spaces. In HVC'16. Springer, 49--64.

[13]

Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, et al. 2014. P4: Programming Protocol-Independent Packet Processors. In SIGCOMM'14. ACM, 87--95.

[14]

Randal E Bryant. 1986. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Comput. 100, 8 (1986), 677--691.

Digital Library

[15]

Shenghui Chen, Zhiming Fan, Haiying Shen, and Lu Feng. 2019. Performance Modeling and Verification of Load Balancing in Cloud Systems Using Formal Methods. In MASSW'19. IEEE, 146--151.

[16]

Sean Choi, Boris Burkov, Alex Eckert, Tian Fang, Saman Kazemkhani, Rob Sherwood, Ying Zhang, and Hongyi Zeng. 2018. Fboss: Building Switch Software at Scale. In SIGCOMM'18. ACM, 342--356.

Digital Library

[17]

Amogh Dhamdhere, David D Clark, Alexander Gamero-Garrido, Matthew Luckie, Ricky KP Mok, Gautam Akiwate, Kabir Gogia, Vaibhav Bajpai, Alex C Snoeren, and Kc Claffy. 2018. Inferring Persistent Interdomain Congestion. In SIGCOMM'18. ACM, 1--15.

[18]

Dragos Dumitrescu, Radu Stoenescu, Lorina Negreanu, and Costin Raiciu. 2020. Bf4: Towards Bug-Free P4 Programs. In SIGCOMM'20. ACM, 571--585.

Digital Library

[19]

Edgecore. 2021. Edgecore Wedge32-100X Switch. https://www.edge-core.com/productsInfo.php?cls=1&cls2=5&cls3=181&id=335.

[20]

Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2018. NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. In NSDI'18. USENIX, 579--594.

[21]

Seyed K Fayaz, Tushar Sharma, Ari Fogel, Ratul Mahajan, Todd Millstein, Vyas Sekar, and George Varghese. 2016. Efficient Network Reachability Analysis Using a Succinct Control Plane Representation. In OSDI'16. USENIX, 217--232.

[22]

fb 10-2021. 2021. Facebook Employees Were Unable to Access Critical Work Tools During Six-Hour Outage. https://www.cnbc.com/2021/10/04/facebook-workers-lose-access-to-internal-tools-following-outage.html.

[23]

Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP Configuration Faults with Static Analysis. In NSDI'05. USENIX, 43--56.

[24]

Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. 2015. A General Approach to Network Configuration Analysis. In NSDI'15. USENIX, 469--483.

[25]

Open Networking Foundation. 2015. Open Networking Foundation. https://www.opennetworking.org/images/stories/downloads/sdn-resources/onf-specifications/openflow/openflow-spec-v1.5.1.pdf.

[26]

Aaron Gember-Jacobson, Aditya Akella, Ratul Mahajan, and Hongqiang Harry Liu. 2017. Automatically Repairing Network Control Planes Using an Abstract Representation. In SOSP'17. ACM, 359--373.

Digital Library

[27]

Aaron Gember-Jacobson, Costin Raiciu, and Laurent Vanbever. 2017. Integrating verification and repair into the control plane. In HotNets'17. ACM, 129--135.

[28]

Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. In SIGCOMM'16. ACM, 300--313.

Digital Library

[29]

Nick Giannarakis, Devon Loehr, Ryan Beckett, and David Walker. 2020. NV: An Intermediate Language for Verification of Network Control Planes. In PLDI'20. ACM, 958--973.

Digital Library

[30]

Google. 2020. A Language-Neutral, Platform-Neutral Extensible Mechanism for Serializing Structured Data. urlhttps://developers.google.com/protocol-buffers.

[31]

Facebook Group. 2016. Facebook Open/R. https://github.com/facebook/openr.

[32]

Network Working Group. 1998. OSPF Version 2. https://www.rfc-editor.org/rfc/rfc2328.html.

[33]

Dong Guo. 2022. Flash Artifact for SIGCOMM22. https://github.com/snlab/flash.

[34]

Dong Guo, Shenshen Chen, Kai Gao, Qiao Xiang, Ying Zhang, and Y. Richard Yang. 2022. Flash: Fast, Consistent Data Plane Verification for Large-Scale Network Settings. In SIGCOMM'22 (Amsterdam, Netherlands). ACM, 314--335.

[35]

Chi-Yao Hong, Subhasree Mandal, Mohammad Al-Fares, Min Zhu, Richard Alimi, Chandan Bhagat, Sourabh Jain, Jay Kaimal, Shiyu Liang, Kirill Mendelev, et al. 2018. B4 and After: Managing Hierarchy, Partitioning, and Asymmetry for Availability and Scale in Google's Software-Defined WAN. In SIGCOMM'18. ACM, 74--87.

Digital Library

[36]

John Hopcroft. 1971. An n log n algorithm for minimizing states in a finite automaton. In Theory of machines and computations. Elsevier, 189--196.

[37]

Alex Horn, Ali Kheradmand, and Mukul Prasad. 2017. Delta-Net: Real-Time Network Verification Using Atoms. In NSDI'17. USENIX, 735--749.

[38]

Alex Horn, Ali Kheradmand, and Mukul R Prasad. 2019. A Precise and Expressive Lattice-Theoretical Framework for Efficient Network Verification. In ICNP'19. IEEE, 1--12.

[39]

Kuo-Feng Hsu, Ryan Beckett, Ang Chen, Jennifer Rexford, Praveen Tammana, and David Walker. 2020. Contra: A Programmable System for Performance-Aware Routing. In NSDI'20. USENIX, 701--721.

[40]

Sushant Jain, Alok Kumar, Subhasree Mandal, Joon Ong, Leon Poutievski, Arjun Singh, Subbaiah Venkata, Jim Wanderer, Junlan Zhou, Min Zhu, et al. 2013. B4: Experience with a Globally-Deployed Software Defined WAN. In SIGCOMM'13. ACM, 3--14.

Digital Library

[41]

Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, et al. 2019. Validating Datacenters at Scale. In SIGCOMM'19. ACM, 200--213.

Digital Library

[42]

Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd Millstein, and George Varghese. 2020. GRooT: Proactive Verification of DNS Configurations. In SIGCOMM'20. ACM, 310--328.

[43]

Peyman Kazemian, Michael Chan, Hongyi Zeng, George Varghese, Nick McKeown, and Scott Whyte. 2013. Real Time Network Policy Checking Using Header Space Analysis. In NSDI'13. USENIX, 99--111.

[44]

Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI'12. USENIX, 113--126.

Digital Library

[45]

Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P Brighten Godfrey. 2013. Veriflow: Verifying Network-Wide Invariants in Real Time. In NSDI'13. USENIX, 15--27.

[46]

Timo Kiravuo, Mikko Sarela, and Jukka Manner. 2013. A survey of Ethernet LAN security. IEEE Communications Surveys & Tutorials 15, 3 (2013), 1477--1491.

[47]

Simon Knight, Hung X Nguyen, Nickolas Falkner, Rhys Bowden, and Matthew Roughan. 2011. The Internet Topology Zoo. IEEE Journal on Selected Areas in Communications 29, 9 (2011), 1765--1775.

[48]

Karthik Lakshminarayanan, Matthew Caesar, Murali Rangan, Tom Anderson, Scott Shenker, and Ion Stoica. 2007. Achieving convergence-free routing using failure-carrying packets. In SIGCOMM'07. ACM, 241--252.

Digital Library

[49]

Franck Le, Geoffrey G Xie, and Hui Zhang. 2010. Theory and New Primitives for Safely Connecting Routing Protocol Instances. In SIGCOMM'10. ACM, 219--230.

[50]

Harry R Lewis and Christos H Papadimitriou. 1998. Elements of the Theory of Computation. In SIGACT'98. ACM, 62--78.

Digital Library

[51]

Hongqiang Harry Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno P Lopes, Andrey Rybalchenko, Guohan Lu, and Lihua Yuan. 2017. Crystalnet: Faithfully Emulating Large Production Networks. In SOSP'17. ACM, 599--613.

Digital Library

[52]

Jed Liu, William Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soulé, Han Wang, Călin Caşcaval, Nick McKeown, and Nate Foster. 2018. P4v: Practical Verification for Programmable Data Planes. In SIGCOMM'18. ACM, 490--503.

Digital Library

[53]

Nuno P Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. 2015. Checking Beliefs in Dynamic Networks. In NSDI'15. USENIX, 499--512.

[54]

Nuno P Lopes and Andrey Rybalchenko. 2019. Fast BGP Simulation of Large Datacenters. In VMCAI'19. Springer, 386--408.

[55]

Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P Brighten Godfrey, and Samuel Talmadge King. 2011. Debugging the Data Plane with Anteater. SIGCOMM'11, 290--301.

[56]

Gary S. Malkin. 1998. RIP Version 2. https://rfc-editor.org/rfc/rfc2453.txt.

[57]

Mellanox. 2015. Mellanox SN2700 Switch. https://www.mellanox.com/related-docs/prod_eth_switches/PB_SN2700.pdf.

[58]

Microsoft. 2021. SONiC: The Networking Switch Software That Powers the Microsoft Global Cloud. https://azure.github.io/SONiC/.

[59]

The Internet2 Observatory. 2021. The Internet2 Dataset. http://www.internet2.edu/research-solutions/research-support/observatory.

[60]

Aurojit Panda, Ori Lahav, Katerina Argyraki, Mooly Sagiv, and Scott Shenker. 2017. Verifying Reachability in Networks with Mutable Datapaths. In NSDI'17. USENIX, 699--718.

[61]

Gordon D Plotkin, Nikolaj Bjørner, Nuno P Lopes, Andrey Rybalchenko, and George Varghese. 2016. Scaling Network Verification Using Symmetry and Surgery. In SIGPLAN'16. ACM, 69--83.

[62]

Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. 2020. Plankton: Scalable Network Configuration Verification Through Model Checking. In NSDI'20. USENIX, 953--967.

[63]

Open Compute Project. 2021. Open Network Linux. http://opennetlinux.org/.

[64]

Yakov Rekhter, Susan Hares, and Dr. Tony Li. 2006. A Border Gateway Protocol 4 (BGP-4). https://rfc-editor.org/rfc/rfc4271.txt.

[65]

sonic 10-2021. 2022. SONiC High Level Design. https://github.com/sonic-net/SONiC/pull/948.

[66]

R. Soulé, S. Basu, P. J. Marandi, F. Pedone, R. Kleinberg, E. G. Sirer, and N. Foster. 2018. Merlin: A Language for Managing Network Resources. IEEE/ACM Transactions on Networking 26, 5 (2018), 2188--2201.

Digital Library

[67]

Neil Spring, Ratul Mahajan, and David Wetherall. 2002. Measuring ISP Topologies with Rocketfuel. In SIGCOMM'02. ACM, 133--145.

[68]

Samuel Steffen, Timon Gehr, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2020. Probabilistic Verification of Network Configurations. In SIGCOMM'20. ACM, 750--764.

[69]

Kausik Subramanian, Anubhavnidhi Abhashkumar, Loris D'Antoni, and Aditya Akella. 2021. D2R: Policy-Compliant Fast Reroute. In SOSR'21. ACM, 148--161.

Digital Library

[70]

Bingchuan Tian, Xinyi Zhang, Ennan Zhai, Hongqiang Harry Liu, Qiaobo Ye, Chunsheng Wang, Xin Wu, Zhiming Ji, Yihong Sang, Ming Zhang, et al. 2019. Safely and Automatically Updating In-Network ACL Configurations with Intent Language. In SIGCOMM'19. ACM, 214--226.

[71]

A. Vahidi. 2020. A BDD and Z-BDD Library Written in Java. https://bitbucket.org/vahidi/jdd.

[72]

Stefano Vissicchio, Luca Cittadini, Olivier Bonaventure, Geoffrey G Xie, and Laurent Vanbever. 2015. On the Co-Existence of Distributed and Centralized Routing Control-Planes. In INFOCOM'15. IEEE, 469--477.

[73]

Anduo Wang, Limin Jia, Wenchao Zhou, Yiqing Ren, Boon Thau Loo, Jennifer Rexford, Vivek Nigam, Andre Scedrov, and Carolyn Talcott. 2012. FSR: Formal Analysis and Implementation Toolkit for Safe Interdomain Routing. IEEE/ACM Transactions on Networking 20, 6 (2012), 1814--1827.

Digital Library

[74]

HuazheWang, Chen Qian, Ye Yu, Hongkun Yang, and Simon S Lam. 2015. Practical Network-Wide Packet Behavior Identification by AP Classifier. In CoNEXT'15. ACM, 1--13.

[75]

Huazhe Wang, Chen Qian, Ye Yu, Hongkun Yang, and Simon S Lam. 2017. Practical Network-Wide Packet Behavior Identification by AP Classifier. IEEE/ACM Transactions on Networking 25, 5 (2017), 2886--2899.

Digital Library

[76]

Konstantin Weitz, Doug Woos, Emina Torlak, Michael D Ernst, Arvind Krishnamurthy, and Zachary Tatlock. 2016. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. In OOPSLA'16. ACM, 765--780.

Digital Library

[77]

WonderNetwork. 2021. Global Ping Statistics. https://wondernetwork.com/pings.

[78]

SNGroup, Xiamen University. 2022. Tulkun Demos. http://distributeddpvdemo.tech/.

[79]

SNGroup, Xiamen University. 2023. Tulkun Prototype. https://github.com/sngroup-xmu/ddpv-pubilc.git.

[80]

Qiao Xiang, Chenyang Haung, Ridi Wen, Yuxin Wang, Xiwen Fan, Zaoxing Liu, Linghe Kong, Dennis Duan, Frank Le, and Wei Sun. 2023. Beyond a Centralized Verifier: Scaling Data Plane Checking via Distributed, On-Device Verification, Technical Report, Xiamen University. http://sngroup.org.cn/publication.html.

[81]

Qiao Xiang, Ridi Wen, Chenyang Huang, Yuxin Wang, and Franck Le. 2022. Network can check itself: scaling data plane checking via distributed, on-device verification. In HotNets'22. ACM, 85--92.

[82]

Geoffrey G Xie, Jibin Zhan, David A Maltz, Hui Zhang, Albert Greenberg, Gisli Hjalmtysson, and Jennifer Rexford. 2005. On Static Reachability Analysis of IP Networks. In INFOCOM'05. IEEE, 2170--2183.

[83]

Hongkun Yang and Simon S Lam. 2013. Real-Time Verification of Network Properties Using Atomic Predicates. In ICNP'13. IEEE, 1--11.

[84]

Hongkun Yang and Simon S Lam. 2014. Collaborative Verification of Forward and Reverse Reachability in the Internet Data Plane. In ICNP'14. IEEE, 320--331.

[85]

Hongkun Yang and Simon S Lam. 2016. Real-Time Verification of Network Properties Using Atomic Predicates. IEEE/ACM Transactions on Networking 24, 2 (2016), 887--900.

Digital Library

[86]

Hongkun Yang and Simon S Lam. 2017. Scalable Verification of Networks with Packet Transformers Using Atomic Predicates. IEEE/ACM Transactions on Networking 25, 5 (2017), 2900--2915.

Digital Library

[87]

Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, et al. 2020. Accuracy, Scalability, Coverage-A Practical Configuration Verifier on a Global WAN. In SIGCOMM'20. ACM, 599--614.

Digital Library

[88]

Yifei Yuan, Soo-Jin Moon, Sahil Uppal, Limin Jia, and Vyas Sekar. 2020. NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification. In NSDI'20. USENIX, 181--200.

[89]

Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina Argyraki, and George Candea. 2017. A Formally Verified NAT. In SIGCOMM'17. ACM, 141--154.

Digital Library

[90]

Hongyi Zeng, Shidong Zhang, Fei Ye, Vimalkumar Jeyakumar, Mickey Ju, Junda Liu, Nick McKeown, and Amin Vahdat. 2014. Libra: Divide and Conquer To Verify Forwarding Tables in Huge Networks. In NSDI'14. USENIX, 87--99.

[91]

Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang. 2020. Automated Verification of Customizable Middlebox Properties with Gravel. In NSDI'20. USENIX, 221--239.

[92]

Peng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang, Xu Liu, and Hao Li. 2022. Differential Network Analysis. In NSDI'22. USENIX, 601--615.

[93]

Peng Zhang, Xu Liu, Hongkun Yang, Ning Kang, Zhengchang Gu, and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. In NSDI'20. USENIX, 241--255.

[94]

Mingchen Zhao, Wenchao Zhou, Alexander JT Gurney, Andreas Haeberlen, Micah Sherr, and Boon Thau Loo. 2012. Private and Verifiable Interdomain Routing Decisions. In SIGCOMM'12. ACM, 383--394.

[95]

Jiaqi Zheng, Hong Xu, Xiaojun Zhu, Guihai Chen, and Yanhui Geng. 2016. We've got you covered: Failure recovery with backup tunnels in traffic engineering. In ICNP'16. IEEE, 1--10.

Cited By

Shen LWang YYou LLi HSong WYao ZYuan ZDong FSun R(2024)A Lightweight and Fast Network Verification Platform for Cloud Data Center NetworksProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673891(20-26)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673891
Hu KDu HWang Y(2024)Heracles: A Novel State-based Distributed Verification Framework for DNS ConfigurationsProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673890(27-32)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673890
Wen SAbhashkumar AZhao CJiang W(2024)Scaling Data Plane Verification via ParallelizationProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663420(81-87)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663420
Show More Cited By

Index Terms

Beyond a Centralized Verifier: Scaling Data Plane Checking via Distributed, On-Device Verification
1. Networks
  1. Network properties
    1. Network reliability
  2. Network protocols
    1. Protocol correctness
      1. Protocol testing and verification

Recommendations

Lightyear: Using Modularity to Scale BGP Control Plane Verification
ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference

Current network control plane verification tools cannot scale to large networks because of the complexity of jointly reasoning about the behaviors of all network nodes. We present a modular approach to control plane verification, where end-to-end network ...
Poster: Scaling Data Plane Verification with Throughput-Optimized Atomic Predicates
ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference

Atomic predicate is a key enabler to the rapid development of data plane verification, a technique to monitor and verify correctness of forwarding rules. Binary Decision Diagram (BDD) is widely used as the representation of atomic predicates for its ...
Large-scale Distributed Verification Using CADP: Beyond Clusters to Grids

Distributed verification uses the resources of several computers to speed up the verification and, even more importantly, to access large amounts of memory beyond the capabilities of a single computer. In this paper, we describe the distributed ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference

September 2023

1217 pages

ISBN:9798400702365

DOI:10.1145/3603269

Chairs:
Henning Schulzrinne,
Vishal Misra,
Program Chairs:
Eddie Kohler,
David Maltz

Copyright © 2023 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Key R&D Program of China
NSFC
Open Research Projects of Zhejiang Lab
Ministry of Education of China
NSF-Fujian-China

Conference

ACM SIGCOMM '23

Sponsor:

SIGCOMM

ACM SIGCOMM '23: ACM SIGCOMM 2023 Conference

September 10, 2023

NY, New York, USA

Acceptance Rates

Overall Acceptance Rate 462 of 3,389 submissions, 14%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
807
Total Downloads

Downloads (Last 12 months)490
Downloads (Last 6 weeks)52

Reflects downloads up to 05 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shen LWang YYou LLi HSong WYao ZYuan ZDong FSun R(2024)A Lightweight and Fast Network Verification Platform for Cloud Data Center NetworksProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673891(20-26)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673891
Hu KDu HWang Y(2024)Heracles: A Novel State-based Distributed Verification Framework for DNS ConfigurationsProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673890(27-32)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673890
Wen SAbhashkumar AZhao CJiang W(2024)Scaling Data Plane Verification via ParallelizationProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663420(81-87)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663420
Wang YYu KWang ZHu KDu HXiang QFang XLi GZhou RKong LShu J(2024)Rethinking DNS Configuration Verification with a Distributed ArchitectureProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663412(23-30)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663412

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents