← 研踪 PaperTrailarXiv:2611.11689 · v1
Declarative DNS - Resolving Recursive Resolution
首次提交 2026-11-09 07:17
版本更新 2026-11-09 07:17
雷达观测 2026-11-10 13:19
摘要
DNS zone configuration errors are a frequent source of outages and frustration, particularly in combination with DNSSEC. Research has attempted to address the problem of zone configuration errors using formal methods, but existing proposals (i) only verify the absence of specific, known configuration errors, and (ii) do not consider DNSSEC. We present a new formal model of the DNS that covers most of DNSSEC, making it one of the most complete DNS models to date. In addition, we present a new tool, DecDNS, that performs a resolvability change-impact analysis of zone configuration updates using our model. We show that such a change-impact analysis can identify configuration errors without explicitly searching for them. We evaluate DecDNS both formally and empirically. We prove that DecDNS is sound and complete and show that its results agree with widely used DNS software. Finally, we explain how our approach can be integrated into operational practice, helping guide zone management in the real world.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-09 07:17 · 最新观测版本
Declarative DNS - Resolving Recursive Resolution
DNS zone configuration errors are a frequent source of outages and frustration, particularly in combination with DNSSEC. Research has attempted to address the problem of zone configuration errors using formal methods, but existing proposals (i) only verify the absence of specific, known configuration errors, and (ii) do not consider DNSSEC. We present a new formal model of the DNS that covers most of DNSSEC, making it one of the most complete DNS models to date. In addition, we present a new tool, DecDNS, that performs a resolvability change-impact analysis of zone configuration updates using our model. We show that such a change-impact analysis can identify configuration errors without explicitly searching for them. We evaluate DecDNS both formally and empirically. We prove that DecDNS is sound and complete and show that its results agree with widely used DNS software. Finally, we explain how our approach can be integrated into operational practice, helping guide zone management in the real world.
查看此版本解读 →查看此版本原文 ↗