Towards a Robust DNS
The Domain Name System (DNS) is the "phonebook" of the Internet, efficiently connecting users to online services. Yet despite its importance, the DNS is also extraordinarily complex and, as a result, fraught with misconfigurations, software implementation bugs, and attack vectors for malicious actors, all of which can impact millions of users. In the past, issues in the DNS have rendered popular services such as GitHub, Twitter, HBO, LinkedIn, Yelp, and Azure inaccessible for extended periods of time. In this talk I will describe our work towards making the DNS as robust as possible. In the first part of the talk I will present GRoot, a new verification tool that we have built that performs exhaustive and proactive static analysis of DNS configuration files to eliminate logical misconfigurations that can lead to services becoming unavailable. Then, in the second part of the talk, I will describe our experience building a tool called Ferret, which uses a formal model of the DNS to automatically generate high-coverage test suites for DNS software nameservers implementations that stress test many corner cases of the DNS RFCs. Using Ferret we have identified 25 new bugs in 8 popular open-source DNS implementations, including 3 previously unknown critical security vulnerabilities.
Ryan Beckett is a researcher at Microsoft working in the area of network reliability. He graduated with his PhD from Princeton in 2018 after working with his advisor David Walker. While a graduate student, Ryan was a recipient of the Google Fellowship and his PhD thesis won the ACM dissertation honorable mention award as well as the SIGCOMM 2018 dissertation award in networking and the Paul Reynolds dissertation award in Programming Languages. His research interests lie primarily at the intersection of programming languages and networks, and he is broadly interested in topics spanning compilers, verification, static analysis, distributed systems, and networks. He has recently focused on improving network reliability by both designing higher-level language abstractions for network automation as well as by applying ideas from formal methods to statically verify the correctness of network configurations.