{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T00:24:36Z","timestamp":1718929476144},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"name":"Office of Naval Research","award":["N68335-22-C-0411"]},{"name":"Defense Advanced Research Projects Agency","award":["W912CG23C0032"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT's potential as a practical, declarative language for network specification and verification.<\/jats:p>","DOI":"10.1145\/3656454","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1905-1928","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["KATch: A Fast Symbolic Verifier for NetKAT"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"http:\/\/orcid.org\/0009-0002-9512-565X","authenticated-orcid":false,"given":"Mark","family":"Moeller","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"http:\/\/orcid.org\/0009-0008-2809-6047","authenticated-orcid":false,"given":"Olivier Savary","family":"Belanger","sequence":"additional","affiliation":[{"name":"Galois, Portland, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0003-2314-0287","authenticated-orcid":false,"given":"David","family":"Darais","sequence":"additional","affiliation":[{"name":"Galois, Portland, USA"}]},{"ORCID":"http:\/\/orcid.org\/0009-0004-9350-3041","authenticated-orcid":false,"given":"Cole","family":"Schlesinger","sequence":"additional","affiliation":[{"name":"Galois, Portland, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-8625-5490","authenticated-orcid":false,"given":"Steffen","family":"Smolka","sequence":"additional","affiliation":[{"name":"Google, Mountain View, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Carolyn Jane Anderson Nate Foster Arjun Guha Jean-Baptiste Jeannin Dexter Kozen Cole Schlesinger and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In POPL. 10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2017. A General Approach to Network Configuration Verification. In SIGCOMM. 10.1145\/3098822.3098834","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2018. Control Plane Compression. In SIGCOMM. 10.1145\/3230543.3230583","DOI":"10.1145\/3230543.3230583"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2020. Abstract Interpretation of Distributed Network Control Planes. In POPL. 10.1145\/3371110","DOI":"10.1145\/3371110"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Ryan Beckett Ratul Mahajan Todd Millstein Jitendra Padhye and David Walker. 2016. Don\u2019t Mind the Gap: Bridging Network-Wide Objectives and Device-Level Configurations. In SIGCOMM. 10.1145\/2934872.2934909","DOI":"10.1145\/2934872.2934909"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Filippo Bonchi and Damien Pous. 2013. Checking NFA Equivalence with Bisimulations up to Congruence. In POPL. 10.1145\/2429069.2429124","DOI":"10.1145\/2429069.2429124"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604866"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the Symposium of Mathematical Theory of Automata.","author":"Brzozowski Janusz A.","year":"1962","unstructured":"Janusz A. Brzozowski. 1962. Canonical regular expressions and minimal state graphs for definite events. In Proceedings of the Symposium of Mathematical Theory of Automata."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Jerry R. Burch Edmund M. Clarke Kenneth L. McMillan David L. Dill and L. J. Hwang. 1990. Symbolic Model Checking: 10^20 States and Beyond. In LICS. 10.1109\/LICS.1990.113767","DOI":"10.1109\/LICS.1990.113767"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Loris D\u2019Antoni and Margus Veanes. 2014. Minimization of Symbolic Automata. In POPL. 10.1145\/2535838.2535849","DOI":"10.1145\/2535838.2535849"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Loris D\u2019Antoni and Margus Veanes. 2017. Forward Bisimulations for Nondeterministic Symbolic Finite Automata. In TACAS. 10.1007\/978-3-662-54577-5_30","DOI":"10.1007\/978-3-662-54577-5_30"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523715"},{"key":"e_1_2_1_19_1","unstructured":"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."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034812"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Nate Foster Dexter Kozen Konstantinos Mamouras Mark Reitblatt and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP. 10.1007\/978-3-662-49498-1_12","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Nate Foster Dexter Kozen Mae Milano Alexandra Silva and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT. In POPL. 10.1145\/2676726.2677011","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Michael Greenberg Ryan Beckett and Eric Campbell. 2022. Kleene Algebra Modulo Theories: A Framework for Concrete KATs. In PLDI. 10.1145\/3519939.3523722","DOI":"10.1145\/3519939.3523722"},{"key":"e_1_2_1_24_1","volume-title":"Fast and Precise Sanitizer Analysis with BEK. In USENIX Conference on Security.","author":"Hooimeijer Pieter","year":"2011","unstructured":"Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes. 2011. Fast and Precise Sanitizer Analysis with BEK. In USENIX Conference on Security."},{"key":"e_1_2_1_25_1","volume-title":"Karp","author":"Hopcroft John E.","year":"1971","unstructured":"John E. Hopcroft and Richard M. Karp. 1971. A Linear Algorithm for Testing Equivalence of Finite Automata."},{"key":"e_1_2_1_26_1","unstructured":"Peyman Kazemian George Varghese and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377677.2377766"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1996. Kleene Algebra with Tests and Commutativity Conditions. In TACAS. 10.1007\/3-540-61042-1_35","DOI":"10.1007\/3-540-61042-1_35"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1959.tb01585.x"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.149.2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018470"},{"key":"e_1_2_1_33_1","volume-title":"David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, and Alexandra Silva.","author":"Moeller Mark","year":"2024","unstructured":"Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, and Alexandra Silva. 2024. KATch: A Fast Symbolic Verifier for NetKAT. arxiv:2404.04760 [cs.PL] https:\/\/arxiv.org\/pdf\/2404.04760.pdf"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10961123"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1515\/9781400882618-006"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Damien Pous. 2015. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. In POPL. 10.1145\/2775051.2677007","DOI":"10.1145\/2775051.2677007"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Spiridon Eliopoulos Nate Foster and Arjun Guha. 2015. A Fast Compiler for NetKAT. In ICFP. 10.1145\/2784731.2784761","DOI":"10.1145\/2784731.2784761"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Nate Foster Justin Hsu Tobias Kapp\u00e9 Dexter Kozen and Alexandra Silva. 2019. Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time. In POPL. 10.1145\/3371129","DOI":"10.1145\/3371129"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar Nate Foster Justin Hsu Dexter Kozen and Alexandra Silva. 2019. Scalable Verification of Probabilistic Networks. In PLDI. 10.1145\/3314221.3314639","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar Nate Foster Dexter Kozen and Alexandra Silva. 2017. Cantor Meets Scott: Semantic Foundations for Probabilistic Networks. In POPL. 10.1145\/3093333.3009843","DOI":"10.1145\/3093333.3009843"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604842"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","unstructured":"Timothy Alberdingk Thijm Ryan Beckett Aarti Gupta and David Walker. 2023. Modular Control Plane Verification via Temporal Invariants. In PLDI. 10.1145\/3591222","DOI":"10.1145\/3591222"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bod\u00edk. 2013. Growing Solver-aided Languages with Rosette. In Onward! (SPLASH). 10.1145\/2509578.2509586","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_1_44_1","volume-title":"Vardi and Pierre Wolper","author":"Moshe","year":"1986","unstructured":"Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). In LICS."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Geoffry 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 INFOCOMM. 10.1109\/INFCOM.2005.1498492","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"e_1_2_1_47_1","unstructured":"Peng Zhang Xu Liu Hongkun Yang Ning Kang Zhengchang Gu and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. In NSDI."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656454","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:41:13Z","timestamp":1718901673000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656454"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":47,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656454"],"URL":"https:\/\/doi.org\/10.1145\/3656454","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}