Reachability Analysis of the Domain Name System

Explore a groundbreaking 18-minute video presentation from POPL 2025 conference where researchers Dhruv Nevatia, Si Liu, and David Basin from ETH Zurich present the first decision procedure for DNS verification, establishing its complexity as 2ExpTime. The presentation formalizes DNS semantics as a system of recursive communicating processes with timers and an infinite message alphabet, introducing an algebraic abstraction with finite equivalence classes using semigroups that recognize positive prefix-testable languages. Learn about their novel generalization of bisimulation for labelled transition systems that proves their abstraction is sound and complete, and how they reduce the DNS verification problem to pushdown systems verification. The research addresses prominent DNS attack vectors including amplification attacks and rewrite blackholing, offering significant contributions to DNS security and reliability. The full article is available via DOI 10.1145/3704898 with supplementary materials on arXiv.