一句话：首次给出 DNS 验证问题的判定过程，证明其复杂度为 2ExpTime，并将其归约到下推系统验证。
DNS 协议高度复杂，尽管测试、监控与验证不断进步，协议层缺陷仍导致大量缺陷和攻击。本文研究 DNS 验证问题，首次给出判定过程，并确定其复杂度为 2ExpTime。作者将 DNS 语义形式化为带定时器和无限消息字母表的递归通信进程系统；对字母表进行代数抽象，使用识别正前缀可测试语言的半群子类得到有限多个等价类；提出一种弱于强互模拟的标记迁移系统互模拟泛化，证明该抽象既可靠又完备。基于该抽象，将 DNS 验证归约为下推系统验证，并通过建模放大攻击和重写黑洞攻击展示框架表达力。
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 2ExpTime , 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2411-10188,
title = {Reachability Analysis of the Domain Name System},
author = {Dhruv Nevatia and Si Liu and David Basin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704898}
}