GRoot: Proactive Verification of DNS Configurations
ACM SIGCOMM Conference (SIGCOMM 2020), August 10-14, 2020.
Best Student Paper Award
Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd Millstein, George Varghese
The Domain Name System (DNS) plays a vital role in
today's Internet but relies on complex distributed management of
records. DNS misconfiguration related outages have rendered
popular services like GitHub, HBO, LinkedIn, and Azure inaccessible
for extended periods. 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. To prove the correctness of our approach, we
develop a formal semantic model of DNS resolution. Applied to the
configuration files from a campus network with over a hundred
thousand records, GRoot revealed 109 bugs within 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, initiating a cleanup.
Finally, on a synthetic dataset with over 65 million real records,
we find GRoot can scale to networks with tens of millions of records.
[PDF | Implementation]