Seminar Series Archive

Network verification, applying formal methods to verify properties of router configurations, is already mainstream with startups like Forward and Veriflow Networks, and divisions in established companies such as Amazon’s ARG and Cisco’s Candid. In this talk, I will survey what remains to be done including: extending formal methods to implementations, and to other parts of the network ecosystem besides routing. I will illustrate these points with recent work we have done on improving the robustness of the Domain Name Service (DNS). Notable errors in DNS have rendered popular services such as GitHub, Twitter, and HBO inaccessible for extended periods.
First, I will present GRoot (SIGCOMM 2020, Best Student Paper), a new verification tool that performs exhaustive and proactive static analysis of DNS configuration files (zone files) based on an efficient algorithm to determine the equivalence class of all possible queries to guarantee key correctness properties. Next, I will describe a new technique, SCALE (NSDI 2022), for finding RFC compliance errors in DNS nameserver implementations via symbolic execution of a DNS formal model to jointly generate test queries and zone files. Using SCALE, we 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.
This talk is based on Siva Kakarla’s Ph.D. work at UCLA and is joint work with Ryan Beckett, Behnaz Armani at MSR , and Todd Millstein at UCLA.

George Varghese is Chancellor’s Professor of Computer Science at UCLA. He was elected to the National Academy of Engineering in 2017, to the National Academy of Inventors in 2020, and to the Internet Hall of Fame in 2021.