FMitF: Track I: Flow Modeling Meets Software Verification: Redesign Internet Congestion Control for Performance and Verifiability

University Of Nebraska-Lincoln, Lincoln NE

Investigators

Abstract

The Transmission Control Protocol (TCP) is a fundamental Internet protocol responsible for transmitting data in daily Internet activities, such as checking emails, reading news, watching videos, messaging friends, making online orders, and many others. An essential component of TCP is the congestion-control algorithm implementations (CCAIs) that determine how fast TCP transmits data on the Internet. Therefore, CCAIs are imperative for the performance and stability of the Internet. However, many bugs have been detected and reported in the CCAIs. These bugs are mistakes made by CCAI developers, and some of them have potentially severe impacts on the performance and stability of the Internet. This project develops and studies a methodology to help CCAI developers avoid such mistakes and thus make the Internet not only more efficient but also more reliable. This project will provide the students with a unique opportunity to explore and study interdisciplinary topics in computer networks, software engineering, and operating system. In addition to graduate students, this project will also involve undergraduate, female, underrepresented minority, and high-school students. Congestion-control algorithm implementations (CCAIs) are essential for the performance and stability of the Internet. The goal of this project is to propose verifiable CCAIs as a new CCAI design and implementation methodology, which systematically enables CCAI developers to design and implement CCAIs with not only efficient performance but also verifiable correctness. Specifically, the proposed research work falls into three research thrusts: 1) a methodology to guide CCAI developers to design and implement verifiable CCAIs; 2) symbolic network environments to represent the aggregate information of packets in various network environments; 3) easy-to-adopt and scalable CCAI verification methods. The proposed work is inspired by the scalability of the flow-modeling methods proposed by the networking community for performance evaluation but tailored to the software-verification methods proposed by the software-engineering community. 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.