George Varghese

When Facebook/Twitter is down for several hours, it affects our social life.  But beyond interaction, the Internet matters greatly as more commerce is electronic (19 trillion per year). I will describe steps we have taken towards creating a new field, Network Design Automation (NDA). NDA seeks to create computer-aided design (CAD) tools for designing and managing networks to reduce design effort and increase reliability.  We were inspired by the Electronic Design Automation (EDA), a $7B industry that underpins the $100B chip industry and is also a vibrant intellectual discipline. While more work is required to complete the vision, at UCLA we have produced an initial set of tools to construct and manage networks that satisfy formal properties, while minimizing the frequency of failures and reducing recovery time.  

A common meme is “If the Internet is down it’s always DNS, except if it's BGP”. For context, DNS is the protocol used in the Internet to translate domain names like cnn.com to Internet addresses, and BGP is the protocol that spreads routes among ISPs.  In this talk, I will describe the new tools we have developed to help proactively find and avoid bugs in DNS and BGP implementations and configurations.

After briefly surveying our earlier techniques to verify correctness of DNS and BGP configurations, I will describe in detail a new technique, SCALE (NSDI 2022), for finding protocol 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. I will also describe a generalization of the SCALE methods to handle structure and state and its application to finding bugs in BGP implementations using a tool called MESSI (NSDI 2024).

In the second part, I will describe some new ideas we have worked on for synthesizing network configurations using LLMs (HotNets 2023) like GPT-4.  LLMs in isolation work very badly, producing promising draft configurations but with egregious errors in topology, syntax, and semantics. Our strategy, that we call Verified Prompt Programming, is to combine LLMs with verifiers, and use localized feedback from the verifier to automatically correct errors. While human input is still required, if we define the leverage as the number of automated prompts to the number of human prompts, our experiments show a leverage of 10X for Juniper translation, and 6X for implementing the no-transit policy, ending with verified configurations.

 I will end by describing what remains to complete the NDA vision.

This talk is based on joint work with Behnaz Arzani and Ryan Beckett at MSR, and Alan Tang, Rajdeep Mondal, Siva Karkarla and Todd Millstein at UCLA.