UCLA

The Domain Name System (DNS), one of the foundations of the modern-day Internet, primarily translates domain names into IP addresses, enabling easy access to online services. DNS name resolution appears simple at a high level but has evolved into a complex and intricate protocol over time. Errors in either DNS configurations or DNS implementations have far-reaching disruptive consequences. This is evident from past DNS issues that have rendered popular services such as GitHub, Twitter, HBO, LinkedIn, Yelp, and Azure inaccessible for extended periods. In this dissertation, I describe my work toward making the DNS as robust as possible by combining formal methods with DNS-specific insights to provide strong guarantees. This dissertation presents the first formalization of DNS semantics, which I developed from multiple RFCs; this serves as the foundation for the rest of my work. Second, I detail a new technique, SCALE, for finding RFC compliance errors in DNS nameserver implementations via automatic test generation. SCALE symbolically executes the developed DNS formal model to jointly generate both the test queries and configurations (zone files). Using SCALE, I identified 30 new bugs in 8 popular open-source DNS implementations such as Bind, PowerDNS, Knot, and NSD, including 3 previously unknown critical security vulnerabilities. Third, I describe GRoot, the first verification tool for DNS configurations. Given the DNS zone files of an organization and a property of interest, GRoot automatically verifies that the property holds for all possible DNS queries or provides all counterexamples. GRoot performs exhaustive and proactive static analysis of DNS configuration files using an efficient algorithm for finding the equivalence classes of all possible queries to guarantee key correctness properties. I conclude with a theoretical analysis of the DNS to categorize its complexity and expressive power.