NeTS: Medium: Provable Guarantees for Network Protocol Implementations

When one uses a social media site or accesses services on a phone (e.g., to make an online purchase) one relies on the Internet to be available. The Internet works using software running on multiple servers and routers called protocol implementations. It includes implementations of famous protocols like Transmission Control Protocol/Internet Protocol (TCP/IP) and Domain Name System (DNS). The Internet is sometimes down because of hardware failures; however, many major outages have been caused by bugs in protocol implementations. This project uses mathematical methods and AI to create protocol implementations provably free of errors. This research uses three different approaches. First, the project plans to develop techniques to generate tests for protocol implementations that provably cover all the features/behaviors that the protocol claims to support. This is done by first building simple models of Internet protocols from their specifications and analyzing the models mathematically to identify behavior classes. Second, the project plans to build provably correct network protocol implementations by breaking up complex protocols into pieces (sublayers), which are mini-protocols in themselves, to make proofs easier. Third, the project plans to exploit advances in large language models (LLMs) to lower the large human cost today to develop reliable protocol implementations. LLMs may hallucinate and (by themselves) can, in fact, make the Internet less reliable. The key insight is that combining LLMs with progress in computer aided proofs can provide the best of both worlds: provably correct protocol implementations with greatly reduced human effort. This project will create a more reliable Internet by making one important part (implementations of popular protocols like TCP, DNS, QUIC and Border Gateway Protocol) of the Internet provably reliable in a mathematically precise sense. When social media sites are down for several hours, it greatly affects our social life. But beyond interaction, the Internet matters greatly as more commerce is electronic (19 trillion USD per year) and the dollar cost of Internet outages can be hundreds of millions of dollars per day. In addition to the techniques that the project will develop, it will also produce concrete artifacts for use by others, including new protocol implementations with provable guarantees. This project is part of a broader vision to build an industry for Network Design Automation (NDA), a set of tools for networks akin to those that led to the billion dollar chip industry in Electronic Design Automation (EDA). Publications, tools, data, and coursework related to this project will be stored at the NDA website and maintained indefinitely: https://www.georgevargheseucla.com/nda This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.