域名系统的可达性分析

DNS 的高复杂性给确保其安全性和可靠性带来独特挑战。尽管 DNS 测试、监控和验证持续进步，协议层面的缺陷仍导致大量漏洞和攻击。本文为 DNS 验证问题提供首个判定过程，确立其复杂度为 $\mathsf{2ExpTime}$，此前未知。我们首先将 DNS 语义形式化为带定时器和无限消息字母表的递归通信进程系统。利用识别正前缀可测试语言的半群子类，给出字母表的代数抽象，具有有限个等价类。随后引入标记迁移系统的一种新型模拟推广，比强模拟更弱，以证明该抽象的可靠性和完备性。最后，利用该抽象将 DNS 验证问题归约为下推系统验证问题。为展示框架的表达能力，我们建模了 DNS 最突出的两个攻击向量：放大攻击和重写黑洞攻击。