{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,2]],"date-time":"2025-12-02T19:37:01Z","timestamp":1764704221195,"version":"3.46.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"CoNEXT4","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62394322"],"award-info":[{"award-number":["62394322"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2024YFB2906800"],"award-info":[{"award-number":["2024YFB2906800"]}],"id":[{"id":"10.13039\/501100012166","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":[[2025,11,24]]},"abstract":"<jats:p>\n                    Overlay\/underlay architecture is increasingly prevalent in modern networks but also introduces greater complexity and error-proneness. Existing control plane verifiers for underlay networks face scalability and interpretability challenges when extended to overlay\/underlay networks due to methodological limitations. This paper presents MEV, the first control plane verifier designed for overlay\/underlay networks. MEV introduces ensemble verification, a novel verification paradigm enabling independent reasoning for behaviors within each routing instance or protocol and forwarding behaviors within each virtual network. We implement and deploy MEV on a real nationwide overlay\/underlay network, FITI, where it successfully identifies 22 misconfigurations that could cause isolation and reachability issues. Furthermore, we evaluate MEV against Batfish\n                    <jats:sup>+<\/jats:sup>\n                    on FITI and a range of synthetic networks with diverse scales, and find that it achieves up to a 10\n                    <jats:sup>2<\/jats:sup>\n                    \u00d7 speedup over Batfish\n                    <jats:sup>+<\/jats:sup>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3768974","type":"journal-article","created":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T17:09:56Z","timestamp":1764090596000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Scalable and Interpretable Overlay Network Checking via Ensemble Verification"],"prefix":"10.1145","volume":"3","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-3895-8475","authenticated-orcid":false,"given":"XinZhe","family":"Liu","sequence":"first","affiliation":[{"name":"Tsinghua University, Beijing, China and Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0148-5965","authenticated-orcid":false,"given":"Yahui","family":"Li","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4429-9959","authenticated-orcid":false,"given":"Han","family":"Zhang","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China and Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0037-2777","authenticated-orcid":false,"given":"Xia","family":"Yin","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China and Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6487-9526","authenticated-orcid":false,"given":"Xingang","family":"Shi","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China and Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6587-820X","authenticated-orcid":false,"given":"Zhiliang","family":"Wang","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China and Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3560-6435","authenticated-orcid":false,"given":"Gang","family":"Ren","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China and Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4493-5145","authenticated-orcid":false,"given":"Jilong","family":"Wang","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China and Zhongguancun Laboratory, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6337-0728","authenticated-orcid":false,"given":"Jiangyuan","family":"Yao","sequence":"additional","affiliation":[{"name":"Hainan University, HaiKou, China"}]}],"member":"320","published-online":{"date-parts":[[2025,11,25]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Rfc 7432: Bgp mpls-based ethernet vpn","author":"Aggarwal R","year":"2015","unstructured":"R Aggarwal, N Bitar, A Isaac, J Uttaro, J Drake, and W Henderickx. Rfc 7432: Bgp mpls-based ethernet vpn, 2015."},{"key":"e_1_2_1_2_1","volume-title":"Rfc 4659: Bgp-mpls ip virtual private network (vpn) extension for ipv6 vpn","author":"Clercq J De","year":"2006","unstructured":"J De Clercq, D Ooms, M Carugi, and F Le Faucheur. Rfc 4659: Bgp-mpls ip virtual private network (vpn) extension for ipv6 vpn, 2006."},{"key":"e_1_2_1_3_1","unstructured":"Ghulam Bahoo and Hafiz Mati Ur Rahman. Segment routing over ipv6 (srv6)."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC7637"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC2784"},{"key":"e_1_2_1_6_1","unstructured":"Google. Google cloud: Cloud computing services. https:\/\/cloud.google.com\/."},{"key":"e_1_2_1_7_1","unstructured":"Microsoft. Microsoft azure: Cloud computing services. https:\/\/azure.microsoft.com\/en-us\/."},{"key":"e_1_2_1_8_1","unstructured":"AT&T. At&t virtual private network. https:\/\/www.attgtadirect.com\/att-virtual-private-network\/."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_2_1_10_1","volume-title":"12th USENIX Symposium on Networked Systems Design and Implementation (NSDI'15)","author":"Fogel Ari","year":"2015","unstructured":"Ari Fogel, Stanley Fung, Lu\u00eds Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. A General Approach to Network Configuration Analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI'15). USENIX Association, May 2015."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_2_1_12_1","first-page":"201","volume-title":"Proceedings of the 17th Usenix Conference on Networked Systems Design and Implementation, NSDI'20","author":"Abhashkumar Anubhavnidhi","year":"2020","unstructured":"Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. Tiramisu: fast multilayer network verification. In Proceedings of the 17th Usenix Conference on Networked Systems Design and Implementation, NSDI'20, page 201-220, USA, 2020. USENIX Association."},{"key":"e_1_2_1_13_1","first-page":"599","volume-title":"Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM '20","author":"Ye Fangdan","year":"2020","unstructured":"Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca. Accuracy, scalability, coverage: A practical configuration verifier on a global wan. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM '20, page 599-614, New York, NY, USA, 2020. Association for Computing Machinery."},{"key":"e_1_2_1_14_1","first-page":"953","volume-title":"Proceedings of the 17th Usenix Conference on Networked Systems Design and Implementation, NSDI'20","author":"Prabhu Santhosh","year":"2020","unstructured":"Santhosh Prabhu, Kuan-Yen Chou, Ali Kheradmand, P. Brighten Godfrey, and Matthew Caesar. Plankton: scalable network configuration verification through model checking. In Proceedings of the 17th Usenix Conference on Networked Systems Design and Implementation, NSDI'20, page 953-968, USA, 2020. USENIX Association."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026895"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544264"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/3691825.3691884"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3651890.3672220"},{"key":"e_1_2_1_19_1","volume-title":"the verifiable art of network cutting","author":"Thijm Timothy Alberdingk","year":"2024","unstructured":"Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Kirigami, the verifiable art of network cutting. IEEE\/ACM Transactions on Networking, 2024."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the ACM on Programming Languages, 7(PLDI):50-75","author":"Thijm Timothy Alberdingk","year":"2023","unstructured":"Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Modular control plane verification via temporal invariants. Proceedings of the ACM on Programming Languages, 7(PLDI):50-75, 2023."},{"key":"e_1_2_1_21_1","first-page":"94","volume-title":"Proceedings of the ACM SIGCOMM 2023 Conference, ACM SIGCOMM 2023","author":"Tang Alan","year":"2023","unstructured":"Alan Tang, Ryan Beckett, Steven Benaloh, Karthick Jayaraman, Tejas Patil, Todd D. Millstein, and George Varghese. Lightyear: Using modularity to scale BGP control plane verification. In Henning Schulzrinne, Vishal Misra, Eddie Kohler, and David A. Maltz, editors, Proceedings of the ACM SIGCOMM 2023 Conference, ACM SIGCOMM 2023, New York, NY, USA, 10-14 September 2023, pages 94-107. ACM, 2023."},{"key":"e_1_2_1_22_1","volume-title":"World's first 1.2tb ultra-high-speed backbone network opens in china. https:\/\/www.globaltimes.cn\/page\/202311\/1301765.shtml","author":"Times Global","year":"2023","unstructured":"Global Times. World's first 1.2tb ultra-high-speed backbone network opens in china. https:\/\/www.globaltimes.cn\/page\/202311\/1301765.shtml, 2023."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386019"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3651890.3672238"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984012"},{"key":"e_1_2_1_26_1","first-page":"601","volume-title":"19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Zhang Peng","year":"2022","unstructured":"Peng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang, Xu Liu, and Hao Li. Differential network analysis. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22), pages 601-615, 2022."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3422604.3425936"},{"key":"e_1_2_1_28_1","unstructured":"Differential datalog (ddlog). https:\/\/github.com\/ vmware\/differential-datalog."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192400"},{"key":"e_1_2_1_30_1","first-page":"113","volume-title":"Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2012","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In Steven D. Gribble and Dina Katabi, editors, Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2012, San Jose, CA, USA, April 25-27, 2012, pages 113-126. USENIX Association, 2012."},{"key":"e_1_2_1_31_1","first-page":"113","volume-title":"Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14","author":"Anderson Carolyn Jane","year":"2014","unstructured":"Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. Netkat: semantic foundations for networks. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, page 113-126, New York, NY, USA, 2014. Association for Computing Machinery."},{"key":"e_1_2_1_32_1","first-page":"499","volume-title":"12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15","author":"Lopes Nuno P.","year":"2015","unstructured":"Nuno P. Lopes, Nikolaj S. Bj\u00f8rner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. Checking beliefs in dynamic networks. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4-6, 2015, pages 499-512. USENIX Association, 2015."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604843"},{"key":"e_1_2_1_34_1","first-page":"15","volume-title":"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. VeriFlow: Verifying Network-Wide invariants in real time. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13), pages 15-27, Lombard, IL, April 2013. USENIX Association."},{"key":"e_1_2_1_35_1","first-page":"617","volume-title":"19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Beckett Ryan","year":"2022","unstructured":"Ryan Beckett and Aarti Gupta. Katra: Realtime verification for multilayer networks. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22), pages 617-634, 2022."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3629145"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472925"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the ACM on Programming Languages, 8(PLDI):199-222","author":"Reddy Kakarla Siva Kesava","year":"2024","unstructured":"Siva Kesava Reddy Kakarla, Francis Y Yan, and Ryan Beckett. Diffy: Data-driven bug finding for configurations. Proceedings of the ACM on Programming Languages, 8(PLDI):199-222, 2024."},{"key":"e_1_2_1_39_1","first-page":"999","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Reddy Kakarla Siva Kesava","year":"2020","unstructured":"Siva Kesava Reddy Kakarla, Alan Tang, Ryan Beckett, Karthick Jayaraman, Todd Millstein, Yuval Tamir, and George Varghese. Finding network misconfigurations by automatic template inference. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 999-1013, 2020."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3626111.3628194"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the ACM on Networking, 2(CoNEXT2):1-25","author":"Wang Changjie","year":"2024","unstructured":"Changjie Wang, Mariano Scazzariello, Alireza Farshin, Simone Ferlin, Dejan Kosti\u0107, and Marco Chiesa. Netconfeval: Can llms facilitate network configuration? Proceedings of the ACM on Networking, 2(CoNEXT2):1-25, 2024."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3411029.3411031"},{"key":"e_1_2_1_43_1","unstructured":"IPWITHEASE. What is clos architecture or clos network? https:\/\/ipwithease.com\/clos-architecture\/."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_2_1_45_1","unstructured":"Huawei. https:\/\/www.huawei.com\/en\/."},{"key":"e_1_2_1_46_1","unstructured":"Z3. https:\/\/github.com\/Z3Prover\/z3."},{"key":"e_1_2_1_47_1","unstructured":"MEV source code. https:\/\/github.com\/LXZ230901\/MEV."},{"key":"e_1_2_1_48_1","unstructured":"H3C. Evpn vxlan technology white paper-6w100. https:\/\/www.h3c.com\/en\/Support\/Resource_Center\/EN\/Home\/Switches\/00-Public\/Trending\/Technology_White_Papers\/EVPN_VXLAN_Technology_WP-6W100\/."},{"key":"e_1_2_1_49_1","unstructured":"Cisco. White papers. https:\/\/www.cisco.com\/c\/en\/us\/products\/switches\/nexus-9000-series-switches\/white-paper-listing.html."},{"key":"e_1_2_1_50_1","unstructured":"Huawei. Ip new technologies. https:\/\/support.huawei.com\/enterprise\/en\/doc\/EDOC1000173015."}],"container-title":["Proceedings of the ACM on Networking"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3768974","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,2]],"date-time":"2025-12-02T19:33:14Z","timestamp":1764703994000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3768974"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,24]]},"references-count":50,"journal-issue":{"issue":"CoNEXT4","published-print":{"date-parts":[[2025,11,24]]}},"alternative-id":["10.1145\/3768974"],"URL":"https:\/\/doi.org\/10.1145\/3768974","relation":{},"ISSN":["2834-5509"],"issn-type":[{"type":"electronic","value":"2834-5509"}],"subject":[],"published":{"date-parts":[[2025,11,24]]},"assertion":[{"value":"2025-11-25","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}