GRoot: Proactive Verification of DNS Configurations

The Domain Name System (DNS) plays a vital role in today’s Internet but relies on complex distributed management of host records. DNS misconfigurations are responsible for many outages that have rendered popular services such as GitHub, Twitter, HBO, LinkedIn, Yelp, and Azure inaccessible for extended periods of time. This paper introduces GRoot, the first verifier that performs static analysis of DNS configuration files enabling proactive and exhaustive checking for common DNS bugs; by contrast, existing solutions are reactive and incomplete. GRoot uses a new, fast verification algorithm based on generating and enumerating DNS query equivalence classes. GRoot symbolically executes the set of queries in each equivalence class to efficiently find (or prove the absence of) any bugs such as rewrite loops or no response. To prove the correctness of our approach, we develop a formal semantic model of DNS resolution. Applied to a set of configuration files obtained from a large campus network with over a hundred thousand records, GRoot revealed 109 bugs, analyzing the network in seconds. When applied to internal zone files consisting of over 3.5 million records from a large infrastructure service provider, GRoot revealed around 160k issues of blackholing, which initiated a cleanup. Finally, on a synthetic dataset created from over 65 million real records, we find that GRoot can scale to networks with tens of millions of records.