Verifiable TCP

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.

The goal of this project is to design and develop a new CCAI design and implementation methodology, called verifiable CCAI, which systematically enables CCAI developers to design and implement CCAIs with not only efficient performance but also verifiable correctness. The proposed verifiable CCAI methodology is inspired by the scalability of the flow modeling methods currently used by the networking community for performance evaluation but is tailored to the software verification methods proposed by the software engineering community.

Documents

• Ming Vu, “Network Protocol Implementation Testing and Verification under Packet Dynamics”, PhD Dissertation, University of Nebraska-Lincoln, November 2021
• Mingrui Zhang, “Experimental Study of Linux Flight Size Estimation”, Master Thesis, University of Nebraska-Lincoln, July 2023

Contributors

Prof. Lisong Xu

Prof. Hamid Bagheri

PhD Students

• Mingrui Zhang
• Minh Vu
• Clay Stevens
• Fahmida Afrin
• Md Rashedul Hasan

MS Students

• Mingrui Zhang

Undergraduate Students

• Uyen Tran
• Jessica Chen
• Patrick Murphy
• Khoa Tran
• Robert Sears
• Saicharith Vaitla

Acknowledgement

This project is supported in part by NSF FMitF