Reachability Analysis of the Domain Name System

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 $\mathsf{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.