{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T04:13:56Z","timestamp":1777349636874,"version":"3.51.4"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"CoNEXT3","license":[{"start":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T00:00:00Z","timestamp":1701043200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["62272382?62272382"],"award-info":[{"award-number":["62272382?62272382"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Netw."],"published-print":{"date-parts":[[2023,11,27]]},"abstract":"<jats:p>Modern networks are increasingly using layering and bridging to form a compositional architecture. Layering protocols like VXLAN create multiple overlay networks on top of a single underlay network infrastructure. This makes network configurations even more complex, and error-prone. To check the correctness of such compositional networks, one needs to model the dependency across multiple layers (underlay and overlay) and multiple domains (different VPNs\/VPCs). Existing verifiers, which are optimized to scale in single-layer single-domain networks, exhibit scalability limitations when applied to compositional networks. This paper proposes MNV, a modular network verifier that scales to large compositional networks. At its core is a new verification method termed decompose-merge reasoning, which decomposes the network into self-contained modules, verifies each module independently, and merges the verification results. Our experiments show that for a typical data center network virtualized with VXLAN, to check reachability for more than 100 million pairs of subnets, MNV is at least 100x faster than state-of-the-art tools.<\/jats:p>","DOI":"10.1145\/3629145","type":"journal-article","created":{"date-parts":[[2023,11,28]],"date-time":"2023-11-28T15:40:05Z","timestamp":1701186005000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Modular Data Plane Verification for Compositional Networks"],"prefix":"10.1145","volume":"1","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-1190-9829","authenticated-orcid":false,"given":"Xu","family":"Liu","sequence":"first","affiliation":[{"name":"Xi'an Jiaotong University, Xi'an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7721-2675","authenticated-orcid":false,"given":"Peng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong University, Xi'an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8776-6911","authenticated-orcid":false,"given":"Hao","family":"Li","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong Universifty, Xi'an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2471-191X","authenticated-orcid":false,"given":"Wenbing","family":"Sun","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong Universifty, Xi'an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,11,28]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the ACM on Programming Languages 7, PLDI","author":"Thijm Timothy Alberdingk","year":"2023","unstructured":"Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. 2023. Modular Control Plane Verification via Temporal Invariants. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 50--75."},{"key":"e_1_2_1_2_1","unstructured":"Amazon. [n. d.]. Amazon EC2 secure and resizable compute capacity for virtually any workload. https:\/\/aws.amazon.com\/ec2\/."},{"key":"e_1_2_1_3_1","volume-title":"An introduction to binary decision diagrams. Lecture notes, available online","author":"Andersen Henrik Reif","year":"1997","unstructured":"Henrik Reif Andersen. 1997. An introduction to binary decision diagrams. Lecture notes, available online, IT University of Copenhagen (1997), 5."},{"key":"e_1_2_1_4_1","volume-title":"Katra: Realtime Verification for Multilayer Networks. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Beckett Ryan","year":"2022","unstructured":"Ryan Beckett and Aarti Gupta. 2022. Katra: Realtime Verification for Multilayer Networks. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22). 617--634."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3422604.3425930"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"D Black Jon Hudson Larry Kreeger Marc Lasserre and T Narten. 2016. An Architecture for Data-Center Network Virtualization over Layer 3 (NVO3). Technical Report.","DOI":"10.17487\/RFC8014"},{"key":"e_1_2_1_7_1","unstructured":"Cisco. [n. d.]. BGP EVPN VXLAN Configuration Guide Cisco IOS XE Bengaluru 17.6.x (Catalyst 9400 Switches). https:\/\/www.cisco.com\/c\/en\/us\/td\/docs\/switches\/lan\/catalyst9400\/software\/release\/17--6\/configuration_guide\/vxlan\/b_176_bgp_evpn_vxlan_9400_cg\/bgp_evpn_vxlan_overview.html?dtid=osscdc000283."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Clarence Filsfils Pablo Camarillo John Leddy Daniel Voyer Satoru Matsushima and Zhenbin Li. 2021. Segment Routing over IPv6 (SRv6) Network Programming. RFC 8986. https:\/\/doi.org\/10.17487\/RFC8986","DOI":"10.17487\/RFC8986"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808753"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC7637"},{"key":"e_1_2_1_11_1","volume-title":"Compositional reasoning. Handbook of Model Checking","author":"Giannakopoulou Dimitra","year":"2018","unstructured":"Dimitra Giannakopoulou, Kedar S Namjoshi, and Corina S P\u0103s\u0103reanu. 2018. Compositional reasoning. Handbook of Model Checking (2018), 345--383."},{"key":"e_1_2_1_12_1","unstructured":"Google. [n. d.]. Google cloud: Cloud computing services. https:\/\/cloud.google.com\/."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592568.1592576"},{"key":"e_1_2_1_14_1","volume-title":"Geneve: Generic network virtualization encapsulation. IETF draft.","author":"Gross J","year":"2016","unstructured":"J Gross, T Sridhar, P Garg, C Wright, and I Ganga. 2016. Geneve: Generic network virtualization encapsulation. IETF draft."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028765"},{"key":"e_1_2_1_16_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Horn Alex","year":"2017","unstructured":"Alex Horn, Ali Kheradmand, and Mukul Prasad. 2017. Delta-net: Real-time network verification using atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). 735--749."},{"key":"e_1_2_1_17_1","unstructured":"Huawei. [n. d.]. Understanding Microsegmentation. https:\/\/support.huawei.com\/enterprise\/en\/doc\/EDOC1100198635\/8f515dd\/understanding-microsegmentation."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"e_1_2_1_19_1","volume-title":"9th IFIP World Computer Congress (Information Processing 83)","author":"Jones Cliff B","year":"1983","unstructured":"Cliff B Jones. 1983. Specification and design of (parallel) programs. In 9th IFIP World Computer Congress (Information Processing 83). Newcastle University."},{"key":"e_1_2_1_20_1","volume-title":"9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12)","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header space analysis: Static checking for networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12). 113--126."},{"key":"e_1_2_1_21_1","volume-title":"VeriFlow: Verifying Network-Wide Invariants in Real Time. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13)","author":"Khurshid Ahmed","year":"2013","unstructured":"Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13). 15--27."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC7938"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Mallik Mahalingam Dinesh Dutt Kenneth Duda Puneet Agarwal Lawrence Kreeger T Sridhar Mike Bursell and Chris Wright. 2014. Virtual extensible local area network (VXLAN): A framework for overlaying virtualized layer 2 networks over layer 3 networks. Technical Report.","DOI":"10.17487\/rfc7348"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018470"},{"key":"e_1_2_1_25_1","unstructured":"Microsoft. [n. d.]. Microsoft azure: Cloud computing services. https:\/\/azure.microsoft.com\/en-us\/."},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Charles Perkins. 1996. IP encapsulation within IP. Technical Report.","DOI":"10.17487\/rfc2003"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. 1985. In transition from global to modular temporal reasoning about programs. Springer.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_2_1_28_1","unstructured":"E. Rosen and Y. Rekhter. [n. d.]. RFC 4364: BGP\/MPLS IP Virtual Private Networks (VPNs). https:\/\/datatracker.ietf.org\/doc\/html\/rfc4364."},{"key":"e_1_2_1_29_1","unstructured":"Ali Sajassi J Drake N Bitar R Shekhar J Uttaro and W Henderickx. 2018. A network virtualization overlay solution using ethernet VPN (eVPN). Technical Report."},{"key":"e_1_2_1_30_1","volume-title":"d.]. Advanced Computer Architectures, a design space approach","author":"Sima Deszo","year":"1997","unstructured":"Deszo Sima, Terence Fountain, and Peter Kacsuk. [n. d.]. Advanced Computer Architectures, a design space approach, 1997."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604842"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP55882.2022.9940333"},{"key":"e_1_2_1_33_1","unstructured":"Arash Vahidi. [n. d.]. JDD a pure Java BDD and Z-BDD library. https:\/\/bitbucket.org\/vahidi\/jdd."},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Yushun Wang. 2017. Tenantguard: Scalable runtime verification of cloud-wide vm-level network isolation. Ph.D. Dissertation. Concordia University.","DOI":"10.14722\/ndss.2017.23365"},{"key":"e_1_2_1_35_1","unstructured":"Hongkun Yang and Simon S Lam. [n. d.]. Scalable Network Verification Using Atomic Predicates. https:\/\/www.cs.utexas.edu\/users\/lam\/NRL\/Atomic_Predicates_Verifiers.html."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2017.2720172"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2021.3114448"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3226588"},{"key":"e_1_2_1_40_1","volume-title":"The Remaining Improbable: Toward Verifiable Network Services. arXiv preprint arXiv:2009.12861","author":"Zave Pamela","year":"2020","unstructured":"Pamela Zave, Jennifer Rexford, and John Sonchack. 2020. The Remaining Improbable: Toward Verifiable Network Services. arXiv preprint arXiv:2009.12861 (2020)."},{"key":"e_1_2_1_41_1","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Zhang Peng","year":"2020","unstructured":"Peng Zhang, Xu Liu, Hongkun Yang, Ning Kang, Zhengchang Gu, and Hao Li. 2020. {APKeep}: Realtime Verification for Real Networks. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). 241--255."}],"container-title":["Proceedings of the ACM on Networking"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3629145","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3629145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:03:31Z","timestamp":1755907411000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3629145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,27]]},"references-count":41,"journal-issue":{"issue":"CoNEXT3","published-print":{"date-parts":[[2023,11,27]]}},"alternative-id":["10.1145\/3629145"],"URL":"https:\/\/doi.org\/10.1145\/3629145","relation":{},"ISSN":["2834-5509"],"issn-type":[{"value":"2834-5509","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,11,27]]},"assertion":[{"value":"2023-11-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}