Reachability Analysis of the Domain Name System Article Swipe
YOU?
·
· 2025
· Open Access
·
· DOI: https://doi.org/10.1145/3704898
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 2 ExpTime , which was previously unknown. 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.
Related Topics
- Type
- article
- Language
- en
- Landing Page
- https://doi.org/10.1145/3704898
- OA Status
- diamond
- References
- 35
- Related Works
- 10
- OpenAlex ID
- https://openalex.org/W4404648185
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W4404648185Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.1145/3704898Digital Object Identifier
- Title
-
Reachability Analysis of the Domain Name SystemWork title
- Type
-
articleOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2025Year of publication
- Publication date
-
2025-01-07Full publication date if available
- Authors
-
Dhruv Nevatia, Si Liu, David BasinList of authors in order
- Landing page
-
https://doi.org/10.1145/3704898Publisher landing page
- Open access
-
YesWhether a free full text is available
- OA status
-
diamondOpen access status per OpenAlex
- OA URL
-
https://doi.org/10.1145/3704898Direct OA link when available
- Concepts
-
Reachability, Computer science, Domain (mathematical analysis), Programming language, Theoretical computer science, Mathematics, Mathematical analysisTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
0Total citation count in OpenAlex
- References (count)
-
35Number of works referenced by this work
- Related works (count)
-
10Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W4404648185 |
|---|---|
| doi | https://doi.org/10.1145/3704898 |
| ids.doi | https://doi.org/10.1145/3704898 |
| ids.openalex | https://openalex.org/W4404648185 |
| fwci | 0.0 |
| type | article |
| title | Reachability Analysis of the Domain Name System |
| biblio.issue | POPL |
| biblio.volume | 9 |
| biblio.last_page | 1870 |
| biblio.first_page | 1840 |
| topics[0].id | https://openalex.org/T12029 |
| topics[0].field.id | https://openalex.org/fields/13 |
| topics[0].field.display_name | Biochemistry, Genetics and Molecular Biology |
| topics[0].score | 0.9943000078201294 |
| topics[0].domain.id | https://openalex.org/domains/1 |
| topics[0].domain.display_name | Life Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1312 |
| topics[0].subfield.display_name | Molecular Biology |
| topics[0].display_name | DNA and Biological Computing |
| topics[1].id | https://openalex.org/T13999 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.9927999973297119 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1710 |
| topics[1].subfield.display_name | Information Systems |
| topics[1].display_name | Digital Rights Management and Security |
| topics[2].id | https://openalex.org/T11567 |
| topics[2].field.id | https://openalex.org/fields/17 |
| topics[2].field.display_name | Computer Science |
| topics[2].score | 0.9842000007629395 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/1703 |
| topics[2].subfield.display_name | Computational Theory and Mathematics |
| topics[2].display_name | semigroups and automata theory |
| is_xpac | False |
| apc_list | |
| apc_paid | |
| concepts[0].id | https://openalex.org/C136643341 |
| concepts[0].level | 2 |
| concepts[0].score | 0.8805264234542847 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q1361526 |
| concepts[0].display_name | Reachability |
| concepts[1].id | https://openalex.org/C41008148 |
| concepts[1].level | 0 |
| concepts[1].score | 0.6221809387207031 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[1].display_name | Computer science |
| concepts[2].id | https://openalex.org/C36503486 |
| concepts[2].level | 2 |
| concepts[2].score | 0.49604782462120056 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q11235244 |
| concepts[2].display_name | Domain (mathematical analysis) |
| concepts[3].id | https://openalex.org/C199360897 |
| concepts[3].level | 1 |
| concepts[3].score | 0.33884841203689575 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q9143 |
| concepts[3].display_name | Programming language |
| concepts[4].id | https://openalex.org/C80444323 |
| concepts[4].level | 1 |
| concepts[4].score | 0.2652030885219574 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q2878974 |
| concepts[4].display_name | Theoretical computer science |
| concepts[5].id | https://openalex.org/C33923547 |
| concepts[5].level | 0 |
| concepts[5].score | 0.18713656067848206 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q395 |
| concepts[5].display_name | Mathematics |
| concepts[6].id | https://openalex.org/C134306372 |
| concepts[6].level | 1 |
| concepts[6].score | 0.0 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q7754 |
| concepts[6].display_name | Mathematical analysis |
| keywords[0].id | https://openalex.org/keywords/reachability |
| keywords[0].score | 0.8805264234542847 |
| keywords[0].display_name | Reachability |
| keywords[1].id | https://openalex.org/keywords/computer-science |
| keywords[1].score | 0.6221809387207031 |
| keywords[1].display_name | Computer science |
| keywords[2].id | https://openalex.org/keywords/domain |
| keywords[2].score | 0.49604782462120056 |
| keywords[2].display_name | Domain (mathematical analysis) |
| keywords[3].id | https://openalex.org/keywords/programming-language |
| keywords[3].score | 0.33884841203689575 |
| keywords[3].display_name | Programming language |
| keywords[4].id | https://openalex.org/keywords/theoretical-computer-science |
| keywords[4].score | 0.2652030885219574 |
| keywords[4].display_name | Theoretical computer science |
| keywords[5].id | https://openalex.org/keywords/mathematics |
| keywords[5].score | 0.18713656067848206 |
| keywords[5].display_name | Mathematics |
| language | en |
| locations[0].id | doi:10.1145/3704898 |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S4210216081 |
| locations[0].source.issn | 2475-1421 |
| locations[0].source.type | journal |
| locations[0].source.is_oa | True |
| locations[0].source.issn_l | 2475-1421 |
| locations[0].source.is_core | True |
| locations[0].source.is_in_doaj | False |
| locations[0].source.display_name | Proceedings of the ACM on Programming Languages |
| locations[0].source.host_organization | https://openalex.org/P4310319798 |
| locations[0].source.host_organization_name | Association for Computing Machinery |
| locations[0].source.host_organization_lineage | https://openalex.org/P4310319798 |
| locations[0].source.host_organization_lineage_names | Association for Computing Machinery |
| locations[0].license | cc-by |
| locations[0].pdf_url | |
| locations[0].version | publishedVersion |
| locations[0].raw_type | journal-article |
| locations[0].license_id | https://openalex.org/licenses/cc-by |
| locations[0].is_accepted | True |
| locations[0].is_published | True |
| locations[0].raw_source_name | Proceedings of the ACM on Programming Languages |
| locations[0].landing_page_url | https://doi.org/10.1145/3704898 |
| locations[1].id | pmh:oai:arXiv.org:2411.10188 |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306400194 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | True |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | arXiv (Cornell University) |
| locations[1].source.host_organization | https://openalex.org/I205783295 |
| locations[1].source.host_organization_name | Cornell University |
| locations[1].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[1].license | |
| locations[1].pdf_url | https://arxiv.org/pdf/2411.10188 |
| locations[1].version | submittedVersion |
| locations[1].raw_type | text |
| locations[1].license_id | |
| locations[1].is_accepted | False |
| locations[1].is_published | False |
| locations[1].raw_source_name | |
| locations[1].landing_page_url | http://arxiv.org/abs/2411.10188 |
| indexed_in | arxiv, crossref |
| authorships[0].author.id | https://openalex.org/A5067969358 |
| authorships[0].author.orcid | https://orcid.org/0009-0008-0845-6754 |
| authorships[0].author.display_name | Dhruv Nevatia |
| authorships[0].countries | CH |
| authorships[0].affiliations[0].institution_ids | https://openalex.org/I35440088 |
| authorships[0].affiliations[0].raw_affiliation_string | ETH Zurich, Zurich, Switzerland |
| authorships[0].institutions[0].id | https://openalex.org/I35440088 |
| authorships[0].institutions[0].ror | https://ror.org/05a28rw58 |
| authorships[0].institutions[0].type | education |
| authorships[0].institutions[0].lineage | https://openalex.org/I2799323385, https://openalex.org/I35440088 |
| authorships[0].institutions[0].country_code | CH |
| authorships[0].institutions[0].display_name | ETH Zurich |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Dhruv Nevatia |
| authorships[0].is_corresponding | False |
| authorships[0].raw_affiliation_strings | ETH Zurich, Zurich, Switzerland |
| authorships[1].author.id | https://openalex.org/A5100330142 |
| authorships[1].author.orcid | https://orcid.org/0000-0003-3578-7432 |
| authorships[1].author.display_name | Si Liu |
| authorships[1].countries | CH |
| authorships[1].affiliations[0].institution_ids | https://openalex.org/I35440088 |
| authorships[1].affiliations[0].raw_affiliation_string | ETH Zurich, Zurich, Switzerland |
| authorships[1].institutions[0].id | https://openalex.org/I35440088 |
| authorships[1].institutions[0].ror | https://ror.org/05a28rw58 |
| authorships[1].institutions[0].type | education |
| authorships[1].institutions[0].lineage | https://openalex.org/I2799323385, https://openalex.org/I35440088 |
| authorships[1].institutions[0].country_code | CH |
| authorships[1].institutions[0].display_name | ETH Zurich |
| authorships[1].author_position | middle |
| authorships[1].raw_author_name | Si Liu |
| authorships[1].is_corresponding | False |
| authorships[1].raw_affiliation_strings | ETH Zurich, Zurich, Switzerland |
| authorships[2].author.id | https://openalex.org/A5025344654 |
| authorships[2].author.orcid | https://orcid.org/0000-0003-2952-939X |
| authorships[2].author.display_name | David Basin |
| authorships[2].countries | CH |
| authorships[2].affiliations[0].institution_ids | https://openalex.org/I35440088 |
| authorships[2].affiliations[0].raw_affiliation_string | ETH Zurich, Zurich, Switzerland |
| authorships[2].institutions[0].id | https://openalex.org/I35440088 |
| authorships[2].institutions[0].ror | https://ror.org/05a28rw58 |
| authorships[2].institutions[0].type | education |
| authorships[2].institutions[0].lineage | https://openalex.org/I2799323385, https://openalex.org/I35440088 |
| authorships[2].institutions[0].country_code | CH |
| authorships[2].institutions[0].display_name | ETH Zurich |
| authorships[2].author_position | last |
| authorships[2].raw_author_name | David Basin |
| authorships[2].is_corresponding | False |
| authorships[2].raw_affiliation_strings | ETH Zurich, Zurich, Switzerland |
| has_content.pdf | False |
| has_content.grobid_xml | False |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://doi.org/10.1145/3704898 |
| open_access.oa_status | diamond |
| open_access.any_repository_has_fulltext | False |
| created_date | 2025-10-10T00:00:00 |
| display_name | Reachability Analysis of the Domain Name System |
| has_fulltext | False |
| is_retracted | False |
| updated_date | 2025-11-06T03:46:38.306776 |
| primary_topic.id | https://openalex.org/T12029 |
| primary_topic.field.id | https://openalex.org/fields/13 |
| primary_topic.field.display_name | Biochemistry, Genetics and Molecular Biology |
| primary_topic.score | 0.9943000078201294 |
| primary_topic.domain.id | https://openalex.org/domains/1 |
| primary_topic.domain.display_name | Life Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1312 |
| primary_topic.subfield.display_name | Molecular Biology |
| primary_topic.display_name | DNA and Biological Computing |
| related_works | https://openalex.org/W4391375266, https://openalex.org/W2899084033, https://openalex.org/W2748952813, https://openalex.org/W2127267268, https://openalex.org/W2136512912, https://openalex.org/W2067910792, https://openalex.org/W2156446763, https://openalex.org/W2143461633, https://openalex.org/W2150194458, https://openalex.org/W4321471459 |
| cited_by_count | 0 |
| locations_count | 2 |
| best_oa_location.id | doi:10.1145/3704898 |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S4210216081 |
| best_oa_location.source.issn | 2475-1421 |
| best_oa_location.source.type | journal |
| best_oa_location.source.is_oa | True |
| best_oa_location.source.issn_l | 2475-1421 |
| best_oa_location.source.is_core | True |
| best_oa_location.source.is_in_doaj | False |
| best_oa_location.source.display_name | Proceedings of the ACM on Programming Languages |
| best_oa_location.source.host_organization | https://openalex.org/P4310319798 |
| best_oa_location.source.host_organization_name | Association for Computing Machinery |
| best_oa_location.source.host_organization_lineage | https://openalex.org/P4310319798 |
| best_oa_location.source.host_organization_lineage_names | Association for Computing Machinery |
| best_oa_location.license | cc-by |
| best_oa_location.pdf_url | |
| best_oa_location.version | publishedVersion |
| best_oa_location.raw_type | journal-article |
| best_oa_location.license_id | https://openalex.org/licenses/cc-by |
| best_oa_location.is_accepted | True |
| best_oa_location.is_published | True |
| best_oa_location.raw_source_name | Proceedings of the ACM on Programming Languages |
| best_oa_location.landing_page_url | https://doi.org/10.1145/3704898 |
| primary_location.id | doi:10.1145/3704898 |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S4210216081 |
| primary_location.source.issn | 2475-1421 |
| primary_location.source.type | journal |
| primary_location.source.is_oa | True |
| primary_location.source.issn_l | 2475-1421 |
| primary_location.source.is_core | True |
| primary_location.source.is_in_doaj | False |
| primary_location.source.display_name | Proceedings of the ACM on Programming Languages |
| primary_location.source.host_organization | https://openalex.org/P4310319798 |
| primary_location.source.host_organization_name | Association for Computing Machinery |
| primary_location.source.host_organization_lineage | https://openalex.org/P4310319798 |
| primary_location.source.host_organization_lineage_names | Association for Computing Machinery |
| primary_location.license | cc-by |
| primary_location.pdf_url | |
| primary_location.version | publishedVersion |
| primary_location.raw_type | journal-article |
| primary_location.license_id | https://openalex.org/licenses/cc-by |
| primary_location.is_accepted | True |
| primary_location.is_published | True |
| primary_location.raw_source_name | Proceedings of the ACM on Programming Languages |
| primary_location.landing_page_url | https://doi.org/10.1145/3704898 |
| publication_date | 2025-01-07 |
| publication_year | 2025 |
| referenced_works | https://openalex.org/W1976426006, https://openalex.org/W4247648311, https://openalex.org/W2123160677, https://openalex.org/W4299651338, https://openalex.org/W1496958170, https://openalex.org/W1589224558, https://openalex.org/W2025970201, https://openalex.org/W1985925577, https://openalex.org/W1524026935, https://openalex.org/W1988922130, https://openalex.org/W1491036809, https://openalex.org/W1967174286, https://openalex.org/W2077450865, https://openalex.org/W1518679248, https://openalex.org/W1823865466, https://openalex.org/W3046558375, https://openalex.org/W3208094982, https://openalex.org/W4402265432, https://openalex.org/W4386385015, https://openalex.org/W1828150029, https://openalex.org/W4213362721, https://openalex.org/W3210579705, https://openalex.org/W2088432971, https://openalex.org/W6948217204, https://openalex.org/W1790119490, https://openalex.org/W2054801208, https://openalex.org/W4244831445, https://openalex.org/W2269418601, https://openalex.org/W4321368781, https://openalex.org/W4400236978, https://openalex.org/W4388858757, https://openalex.org/W4387321107, https://openalex.org/W4246777216, https://openalex.org/W4390742456, https://openalex.org/W2194869982 |
| referenced_works_count | 35 |
| abstract_inverted_index., | 53 |
| abstract_inverted_index.2 | 51 |
| abstract_inverted_index.a | 67, 107 |
| abstract_inverted_index.In | 33 |
| abstract_inverted_index.To | 146 |
| abstract_inverted_index.We | 58, 81, 104 |
| abstract_inverted_index.an | 77, 83 |
| abstract_inverted_index.as | 50, 66 |
| abstract_inverted_index.by | 60 |
| abstract_inverted_index.in | 17 |
| abstract_inverted_index.is | 125 |
| abstract_inverted_index.of | 3, 64, 69, 86, 97, 110, 150, 156 |
| abstract_inverted_index.on | 162 |
| abstract_inverted_index.to | 28, 120, 139 |
| abstract_inverted_index.we | 36, 133, 153 |
| abstract_inverted_index.DNS | 4, 18, 44, 65, 136 |
| abstract_inverted_index.The | 0 |
| abstract_inverted_index.and | 12, 21, 31, 76, 127, 167 |
| abstract_inverted_index.for | 8, 42, 112, 143 |
| abstract_inverted_index.its | 10, 48 |
| abstract_inverted_index.our | 123, 151 |
| abstract_inverted_index.the | 38, 43, 62, 87, 95, 135, 140, 148, 157 |
| abstract_inverted_index.two | 155 |
| abstract_inverted_index.was | 55 |
| abstract_inverted_index.DNS, | 163 |
| abstract_inverted_index.bugs | 30 |
| abstract_inverted_index.give | 26 |
| abstract_inverted_index.high | 1 |
| abstract_inverted_index.many | 91 |
| abstract_inverted_index.most | 158 |
| abstract_inverted_index.rise | 27 |
| abstract_inverted_index.show | 121, 147 |
| abstract_inverted_index.than | 117 |
| abstract_inverted_index.that | 99, 122 |
| abstract_inverted_index.then | 105 |
| abstract_inverted_index.this | 34, 131 |
| abstract_inverted_index.with | 74, 89 |
| abstract_inverted_index.begin | 59 |
| abstract_inverted_index.first | 39 |
| abstract_inverted_index.model | 154 |
| abstract_inverted_index.novel | 108 |
| abstract_inverted_index.poses | 5 |
| abstract_inverted_index.sound | 126 |
| abstract_inverted_index.still | 25 |
| abstract_inverted_index.using | 94, 130 |
| abstract_inverted_index.which | 54 |
| abstract_inverted_index.attack | 160 |
| abstract_inverted_index.namely | 164 |
| abstract_inverted_index.paper, | 35 |
| abstract_inverted_index.reduce | 134 |
| abstract_inverted_index.strong | 118 |
| abstract_inverted_index.system | 68 |
| abstract_inverted_index.timers | 75 |
| abstract_inverted_index.unique | 6 |
| abstract_inverted_index.weaker | 116 |
| abstract_inverted_index.Despite | 14 |
| abstract_inverted_index.ExpTime | 52 |
| abstract_inverted_index.attacks | 166 |
| abstract_inverted_index.defects | 24 |
| abstract_inverted_index.message | 79 |
| abstract_inverted_index.problem | 138, 142 |
| abstract_inverted_index.provide | 37, 82 |
| abstract_inverted_index.rewrite | 168 |
| abstract_inverted_index.vectors | 161 |
| abstract_inverted_index.Finally, | 129 |
| abstract_inverted_index.advances | 16 |
| abstract_inverted_index.alphabet | 88 |
| abstract_inverted_index.attacks. | 32 |
| abstract_inverted_index.classes, | 93 |
| abstract_inverted_index.decision | 40 |
| abstract_inverted_index.ensuring | 9 |
| abstract_inverted_index.extended | 73 |
| abstract_inverted_index.finitely | 90 |
| abstract_inverted_index.infinite | 78 |
| abstract_inverted_index.labelled | 113 |
| abstract_inverted_index.numerous | 29 |
| abstract_inverted_index.positive | 101 |
| abstract_inverted_index.problem, | 46 |
| abstract_inverted_index.pushdown | 144 |
| abstract_inverted_index.security | 11 |
| abstract_inverted_index.subclass | 96 |
| abstract_inverted_index.systems, | 115 |
| abstract_inverted_index.systems. | 145 |
| abstract_inverted_index.testing, | 19 |
| abstract_inverted_index.unknown. | 57 |
| abstract_inverted_index.algebraic | 84 |
| abstract_inverted_index.alphabet. | 80 |
| abstract_inverted_index.complete. | 128 |
| abstract_inverted_index.introduce | 106 |
| abstract_inverted_index.procedure | 41 |
| abstract_inverted_index.processes | 72 |
| abstract_inverted_index.prominent | 159 |
| abstract_inverted_index.recognize | 100 |
| abstract_inverted_index.recursive | 70 |
| abstract_inverted_index.semantics | 63 |
| abstract_inverted_index.challenges | 7 |
| abstract_inverted_index.complexity | 2, 49 |
| abstract_inverted_index.continuous | 15 |
| abstract_inverted_index.framework, | 152 |
| abstract_inverted_index.languages. | 103 |
| abstract_inverted_index.previously | 56 |
| abstract_inverted_index.semigroups | 98 |
| abstract_inverted_index.transition | 114 |
| abstract_inverted_index.abstraction | 85, 124 |
| abstract_inverted_index.equivalence | 92 |
| abstract_inverted_index.formalizing | 61 |
| abstract_inverted_index.monitoring, | 20 |
| abstract_inverted_index.abstraction, | 132 |
| abstract_inverted_index.bisimulation | 111 |
| abstract_inverted_index.blackholing. | 169 |
| abstract_inverted_index.establishing | 47 |
| abstract_inverted_index.reliability. | 13 |
| abstract_inverted_index.verification | 45, 137, 141 |
| abstract_inverted_index.amplification | 165 |
| abstract_inverted_index.bisimulation, | 119 |
| abstract_inverted_index.communicating | 71 |
| abstract_inverted_index.verification, | 22 |
| abstract_inverted_index.expressiveness | 149 |
| abstract_inverted_index.generalization | 109 |
| abstract_inverted_index.protocol-level | 23 |
| abstract_inverted_index.prefix-testable | 102 |
| cited_by_percentile_year | |
| countries_distinct_count | 1 |
| institutions_distinct_count | 3 |
| sustainable_development_goals[0].id | https://metadata.un.org/sdg/16 |
| sustainable_development_goals[0].score | 0.5 |
| sustainable_development_goals[0].display_name | Peace, Justice and strong institutions |
| citation_normalized_percentile.value | 0.00062333 |
| citation_normalized_percentile.is_in_top_1_percent | False |
| citation_normalized_percentile.is_in_top_10_percent | False |