Janus: Leveraging Incremental Computation for Efficient DNS Verification

TL;DR

Janus tackles the high-cost problem of DNS configuration verification by reframing nameserver behavior as a match-action system and introducing Local Equivalence Classes (LECs) to compress query outcomes. It combines a symbolic query execution engine with an incremental verification mechanism to support rapid, localized updates, significantly reducing verification workload. Empirical results on real-world and university datasets show substantial improvements over prior approaches, including up to 255x end-to-end speedups and over 6000x reductions in the number of equivalence classes. The approach enables scalable, accurate DNS verification with practical incremental updates, with potential for further diagnosis and repair of misconfigurations.

Abstract

Existing DNS configuration verification tools face significant issues (e.g., inefficient and lacking support for incremental verification). Inspired by the advancements in recent work of distributed data plane verification and the resemblance be- tween the data plane and DNS configuration, we tackle the challenge of DNS misconfiguration by introducing Janus, a DNS verification tool. Our key insight is that the process of a nameserver handling queries can be transformed into a matching process on a match-action table. With this insight, Janus consists of (1) an efficient data structure for partition query space based on the behaviors, (2) a symbolic execution algorithm that specifies how a single nameserver can efficiently cover all possible queries and ensure the accuracy of verification, (3) a mechanism to support incremental verification with less computational effort. Extensive experiments on real-world datasets (with over 6 million resource records) show that Janus achieves significant speedups, with peak improvements of up to 255.7x and a maximum 6046x reduction in the number of LECs.

Figures (6)

• Figure 1: Example zonefiles for three nameservers and the result of query space partitioning for each nameserver. For simplicity, we merge the NXDOMAIN and REFUSE behaviors. $S_0$ denotes the entire query space.
• Figure 2: An illustration example in Figure \ref{['fig: workflow']} to demonstrate the workflow of Janus.
• Figure 3: Comparison of the LEC/EC in the example of Figure \ref{['fig: workflow']} in detail.
• Figure 4: An example with a large number of LEC.
• Figure 5: Burst update experiment result using Census dataset.

Theorems & Definitions (1)

• Definition 1: Action