Reachability Analysis of the Domain Name System
Dhruv Nevatia, Si Liu, David Basin

TL;DR
This paper introduces a decision procedure for DNS verification, establishing its 2-ExpTime complexity, and models DNS attacks like amplification and blackholing within this formal framework.
Contribution
It formalizes DNS semantics as recursive communicating processes, introduces a novel bisimulation, and reduces DNS verification to pushdown system verification.
Findings
Decides DNS verification with 2-ExpTime complexity
Models DNS attacks such as amplification and blackholing
Provides a sound and complete abstraction for DNS analysis
Abstract
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 , 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
