{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T23:21:18Z","timestamp":1770247278275,"version":"3.49.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    The high complexity of DNS poses unique challenges for ensuring its security and reliability. Despite continuous advances in DNS testing, monitoring, and verification, protocol-level defects still give rise to numerous bugs and attacks. In this paper, we provide the first decision procedure for the DNS verification problem, establishing its complexity as\n                    <jats:monospace>2ExpTime<\/jats:monospace>\n                    , which was previously unknown.\n                  <\/jats:p>\n                  <jats:p>We begin by formalizing the semantics of DNS as a system of recursive communicating processes extended with timers and an infinite message alphabet. We provide an algebraic abstraction of the alphabet with finitely many equivalence classes, using the subclass of semigroups that recognize positive prefix-testable languages. We then introduce a novel generalization of bisimulation for labelled transition systems, weaker than strong bisimulation, to show that our abstraction is sound and complete. Finally, using this abstraction, we reduce the DNS verification problem to the verification problem for pushdown systems. To show the expressiveness of our framework, we model two of the most prominent attack vectors on DNS, namely amplification attacks and rewrite blackholing.<\/jats:p>","DOI":"10.1145\/3704898","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1840-1870","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Reachability Analysis of the Domain Name System"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-0845-6754","authenticated-orcid":false,"given":"Dhruv","family":"Nevatia","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3578-7432","authenticated-orcid":false,"given":"Si","family":"Liu","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2952-939X","authenticated-orcid":false,"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"1957. Fundamental Concepts in the Theory of Systems. Wright Air Development Center Air Research and Development Command United States Air Force"},{"key":"e_1_3_2_3_2","volume-title":"IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)","author":"Abdulla Parosh Aziz","year":"2012","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. 2012. Timed lossy channel systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.15"},{"key":"e_1_3_2_5_2","first-page":"160","article-title":"Verifying Programs with Unreliable Channels","author":"Abdulla Parosh Aziz","year":"1993","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. 1993. Verifying Programs with Unreliable Channels. In Proc. LICS '93-8th IEEE Int. Symp. on Logic in Computer Science. 160\u2013170.","journal-title":"Proc. LICS '93-8th IEEE Int. Symp. on Logic in Computer Science"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0053"},{"key":"e_1_3_2_7_2","first-page":"631","volume-title":"USENIX Security 2020","author":"Afek Yehuda","year":"2020","unstructured":"Yehuda Afek, Anat Bremler-Barr, and Lior Shafir. 2020. NXNSAttack: Recursive DNS Inefficiencies and Vulnerabilities. In USENIX Security 2020. USENIX Association, 631\u2013648."},{"key":"e_1_3_2_8_2","first-page":"3187","volume-title":"USENIX Security '23","author":"Afek Yehuda","year":"2023","unstructured":"Yehuda Afek, Anat Bremler-Barr, and Shani Stajnrod. 2023. NRDelegationAttack: Complexity DDoS attack on DNS Recursive Resolvers. In USENIX Security '23. USENIX Association, 3187\u20133204."},{"key":"e_1_3_2_9_2","first-page":"3","volume-title":"International Conference on Networked Systems","author":"Aiswarya C","year":"2020","unstructured":"C Aiswarya. 2020. On network topologies and the decidability of reachability problem. In International Conference on Networked Systems. Springer, 3\u201310."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1142\/2481"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_29"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_10"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-51476-0_4"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/GLOCOM.2012.6503217"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0003"},{"key":"e_1_3_2_18_2","volume-title":"All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic","author":"Clavel Manuel","year":"2007","unstructured":"Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet ,Jos\u00e9 Meseguer, and Carolyn L. Talcott (Eds.). 2007. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, Vol. 4350. Springer."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.73"},{"key":"e_1_3_2_20_2","first-page":"5769","volume-title":"USENIX Security '24","author":"Duan Huayi","year":"2024","unstructured":"Huayi Duan, Marco Bearzi, Jodok Vieli, David Basin, Adrian Perrig, Si Liu, and Bernhard Tellenbach. 2024. CAMP: Compositional Amplification Attacks against DNS. In USENIX Security '24. USENIX Association, 5769\u20135786."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Robert Elz and Randy Bush. 1997. Clarifications to the DNS Specification. RFC 2181 (1997) 1\u201314. https:\/\/doi.org\/10.17487\/RFC2181 10.17487\/RFC2181","DOI":"10.17487\/RFC2181"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_20"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1070\/RM1961v016n05ABEH004112"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_17"},{"key":"e_1_3_2_26_2","first-page":"267","volume-title":"FoSSaCS '10","author":"Heu\u00dfner Alexander","year":"2010","unstructured":"Alexander Heu\u00dfner, J\u00e9r\u00f4me Leroux, Anca Muscholl, and Gr\u00e9goire Sutre. 2010. Reachability analysis of communicating pushdown systems. In FoSSaCS '10. Springer, 267\u2013281."},{"issue":"2012","key":"e_1_3_2_27_2","article-title":"Reachability analysis of communicating pushdown systems","volume":"8","author":"Heu\u00dfner Alexander","year":"2012","unstructured":"Alexander Heu\u00dfner, J\u00e9r\u00f4me Leroux, Anca Muscholl, and Gr\u00e9goire Sutre. 2012. Reachability analysis of communicating pushdown systems. Logical Methods in Computer Science 8 (2012).","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_28_2","unstructured":"Check Host. Accessed in July 2024. DNS checking. https:\/\/check-host.net\/check-dns."},{"key":"e_1_3_2_29_2","unstructured":"IETF. Accessed 2024-10-15. Internet Engineering Task Force. https:\/\/www.hex-rays.com\/products\/ida."},{"key":"e_1_3_2_30_2","unstructured":"Siva Kesava Reddy Kakarla and Ryan Beckett. 2023. Oracle-based Protocol Testing with Eywa. arXiv:2312.06875 [cs.NI]"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405871"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3484266.3487369"},{"key":"e_1_3_2_33_2","first-page":"307","volume-title":"NSDI '22","author":"Kakarla Siva Kesava Reddy","year":"2022","unstructured":"Siva Kesava Reddy Kakarla, Ryan Beckett, Todd Millstein, and George Varghese. 2022. SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers. In NSDI '22. USENIX Association, 307\u2013323."},{"key":"e_1_3_2_34_2","volume-title":"Automata and computability","author":"Kozen Dexter C","year":"2012","unstructured":"Dexter C Kozen. 2012. Automata and computability. Springer Science \u2013 Business Media."},{"key":"e_1_3_2_35_2","volume-title":"Computer Networking: A Top-Down Approach","author":"Kurose James F.","year":"2016","unstructured":"James F. Kurose and Keith W. Ross. 2016. Computer Networking: A Top-Down Approach (7 ed.). Pearson, Boston, MA.","edition":"7"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00172"},{"key":"e_1_3_2_37_2","first-page":"932","article-title":"A Formal Framework for End-to-End DNS Resolution","author":"Liu Si","year":"2023","unstructured":"Si Liu, Huayi Duan, Lukas Heimes, Marco Bearzi, Jodok Vieli, David A. Basin, and Adrian Perrig. 2023. A Formal Framework for End-to-End DNS Resolution. In SIGCOMM '23. ACM, 932\u2013949.","journal-title":"SIGCOMM '23"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Mockapetris P.Mockapetris. 1987. DOMAIN NAMES - CONCEPTS AND FACILITIES. RFC 1034. RFC Editor. https:\/\/doi.org\/10.17487\/RFC103410.17487\/RFC1034","DOI":"10.17487\/RFC1034"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Mockapetris. P.Mockapetris. 1987. DOMAIN NAMES - IMPLEMENTATION AND SPECIFICATION. RFC 1035. RFC Editor. https:\/\/doi.org\/10.17487\/RFC103510.17487\/RFC1035","DOI":"10.17487\/RFC1035"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3487552.3487824"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","unstructured":"Nerode. A.Nerode. 1958. Linear Automaton Transformations. Proc. Amer. Math. Soc. 9 4 (1958) 541\u2013544.","DOI":"10.1090\/S0002-9939-1958-0135681-9"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Dhruv Nevatia Si Liu and David Basin. 2024. Reachability Analysis of the Domain Name System. Technical Report. https:\/\/doi.org\/10.48550\/arXiv.2411.1018810.48550\/arXiv.2411.10188","DOI":"10.48550\/arXiv.2411.10188"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Dr. Masataka Ohta. 1996. Incremental Zone Transfer in DNS. RFC 1995. https:\/\/doi.org\/10.17487\/RFC199510.17487\/RFC1995","DOI":"10.17487\/RFC1995"},{"key":"e_1_3_2_45_2","first-page":"80","article-title":"A variety theorem without complementation","volume":"39","author":"Pin Jean-\u2013ric","year":"1995","unstructured":"Jean-\u2013ric Pin. 1995. A variety theorem without complementation. Russian Mathematics (Izvestija vuzov.Matematika) 39 (1995), 80\u201390.","journal-title":"Russian Mathematics (Izvestija vuzov.Matematika)"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1147\/rd.32.0114"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","unstructured":"S. Rose and W. Wijngaards. 2012. DNAME Redirection in the DNS. RFC 6672. RFC Editor. https:\/\/doi.org\/10.17487\/RFC667210.17487\/RFC6672","DOI":"10.17487\/RFC6672"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_26"},{"key":"e_1_3_2_50_2","doi-asserted-by":"crossref","unstructured":"Sam Staton. 2011. Relating coalgebraic notions of bisimulation. Logical Methods in Computer Science 7 (2011).","DOI":"10.2168\/LMCS-7(1:13)2011"},{"key":"e_1_3_2_51_2","unstructured":"ThousandEyes. Accessed in July 2024. DNS Monitoring Across Your Entire Network. https:\/\/www.thousandeyes.com\/solutions\/dns-monitoring.."},{"key":"e_1_3_2_52_2","unstructured":"Liam Tung. Accessed in July 2024. Azure global outage: Our DNS update mangled domain records says Microsoft. https:\/\/www.zdnet.com\/article\/azureglobal-outage-our-dns-update-mangled-domain-records-says-microsoft."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2023.105013"},{"key":"e_1_3_2_54_2","unstructured":"Lorijn van Rooijen and Marc Zeitoun. 2013. The separation problem for regular languages by piecewise testable languages. arXiv preprint arXiv:1303.2143 (2013)."},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3663408.3663412"},{"key":"e_1_3_2_56_2","unstructured":"Zack Whittaker. Accessed 2023-02-07. A DNS outage just took down a large chunk of the internet. https:\/\/techcrunchcom\/2021\/07\/22\/a-dns-outage-just-took-down-a-good-chunk-of-the-internet\/."},{"key":"e_1_3_2_57_2","unstructured":"Wikipedia. Accessed in July 2024. 2021 Facebook outage. https:\/\/en.wikipedia.org\/wiki\/2021_Facebook_outage."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616668"},{"key":"e_1_3_2_59_2","volume-title":"USENIX Security '24","author":"Zhang Qifan","year":"2024","unstructured":"Qifan Zhang, Xuesong Bai, Xiang Li, Haixin Duan, Qi Li, and Zhou Li. 2024. ResolverFuzz: Automated Discovery of DNS Resolver Vulnerabilities with Query-Response Fuzzing. In USENIX Security '24. USENIX Association."},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613153"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704898","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704898","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:21Z","timestamp":1770200181000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704898"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704898"],"URL":"https:\/\/doi.org\/10.1145\/3704898","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}