Janus: Leveraging Incremental Computation for Efficient DNS Verification

TL;DR

Janus is a novel DNS verification tool that leverages incremental computation and symbolic execution to significantly improve efficiency and support scalable, real-time DNS configuration verification.

Contribution

It introduces a new approach transforming DNS query handling into a match-action process, enabling efficient incremental verification and large-scale applicability.

Findings

Achieves up to 255.7x speedup in verification tasks.

Reduces the number of LECs by up to 6046x.

Successfully verified over 6 million resource records.

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.