Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reachability Analysis of the Domain Name System

Dhruv Nevatia, Si Liu, David Basin

TL;DR

This paper provides the first decision procedure for the DNS verification problem, establishing its complexity as 2ExpTime, which was previously unknown.

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.

Reachability Analysis of the Domain Name System

TL;DR

This paper provides the first decision procedure for the DNS verification problem, establishing its complexity as 2ExpTime, which was previously unknown.

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 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.

Paper Structure

This paper contains 64 sections, 15 theorems, 19 equations, 15 figures.

Table of Contents

  1. Introduction
  2. DNS is Eager
  3. Congruence
  4. Kernel Bisimulation
  5. Reduction to Reachability
  6. Preliminaries
  7. DNS in a Nutshell
  8. Namespace
  9. Resource Records
  10. Name Resolution
  11. Subqueries
  12. Labelled Transition Systems
  13. A Formal Model for DNS
  14. Definitions and Notations
  15. Domain names and IP addresses
  16. ...and 49 more sections

Key Result

lemma 1

The sets $\scrsf{domain}\subsub{\monoid},\scrsf{record}\subsub{\monoid},\scrsf{zone}\subsub{\monoid}, \scrsf{zfc}\subsub{\monoid}, \scrsf{query}\subsub{\monoid}$, $\scrsf{answer}\subsub{\monoid}$, and $\scrsf{slist}\subsub{\monoid}$ are all functorialGiven an expression $A$ that contains $B$, we say

Figures (15)

  • Figure 1: A small portion of the DNS namespace. Dashed lines mark the zone cuts.
  • Figure 2: Name resolution for the type a query www.sigplan.org, with an empty cache at the DNS resolver.
  • Figure 3: Some DNS notation.
  • Figure 4: A pointed topology. The red process is the only tPDS in the network.
  • Figure 5: Some auxiliary operations.
  • ...and 10 more figures

Theorems & Definitions (32)

  • definition 1
  • lemma 1
  • definition 2
  • definition 3
  • definition 4
  • lemma 2
  • Remark 1
  • lemma 3
  • proof : Proof Sketch.
  • definition 5: Syntactic Congruence
  • ...and 22 more