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

传输控制协议(TCP)是一种基本的互联网协议，负责在日常互联网活动中传输数据，例如查看电子邮件、阅读新闻、观看视频、向朋友发送消息、在线订购等。Tcp的一个重要组件是拥塞控制算法实现(CCAI)，它决定了tcp在互联网上传输数据的速度。因此，CCAI对于互联网的性能和稳定性是必不可少的。然而，在CCAI中检测到并报告了许多错误。这些错误是CCAI开发人员犯下的错误，其中一些错误可能会对互联网的性能和稳定性造成严重影响。这个项目开发和研究了一种方法来帮助CCAI开发人员避免这样的错误，从而使互联网不仅更高效，而且更可靠。这个项目将为学生提供一个独特的机会来探索和学习计算机网络、软件工程和操作系统的跨学科主题。除了研究生，这个项目还将涉及本科生、女性、代表性不足的少数族裔和高中生。本项目的目标是提出一种新的CCAI设计和实现方法--可验证CCAI，它系统地使CCAI开发人员能够设计和实现不仅具有高效性能而且具有可验证正确性的CCAI。具体地说，本文的研究工作分为三个方面：1)指导CCAI开发人员设计和实现可验证的CCAI的方法学；2)表示各种网络环境中的报文聚集信息的符号网络环境；3)易于采用和可扩展的CCAI验证方法。拟议工作的灵感来自于网络社区为性能评估提出的流建模方法的可扩展性，但根据软件工程社区提出的软件验证方法量身定做。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.