FMitF: Track I: Injecting Formal Methods into Internet Standardization

该项目的目标是开发一种由工具支持的方法，该方法使用正式的方法来获得网络协议标准的清晰度，并测试实现与这些标准的一致性。这项工作将在QUIC上进行演示，QUIC是一种新的复杂协议，目前承载着大约10%的互联网流量，在不久的将来可能会承载更多的流量。QUIC的标准化工作正在IETF下进行。本项目开发的软件和实验结果将存储在GitHub中。方法本身将通过通常的手段（出版物、演讲等）广泛传播。实验结果将与QUIC实现的开发人员和IETF共享。该项目将用于培养研究生，他们将接触到最先进的技术以及学术界（UIC）和工业界（微软）之间的合作。本课程的内容将整合到UIC的课程中。UIC是一个少数民族服务机构（MSI），亚裔美国人和美洲原住民太平洋岛民服务机构（AANAPISI）和西班牙裔服务机构（HSI）。网络协议标准由rfc描述：rfc是一种英文文档，为协议的实现提供了广泛的指导，但仍然是模糊的，并且有广泛的解释余地。解决这些歧义和验证协议设计的主要机制是产生多个独立的实现，并测试这些实现的互操作性，这通常会使rfc过时，而实现成为事实上的标准。该项目的目标是在标准化过程中注入正式的方法。该方法基于一种新的基于规范的测试方法，该方法允许严格指定和测试复杂的互联网协议。一个主要的目标是在标准化过程中演示正式规范的实用价值，特别是显示正式规范具有实用价值，而不仅仅是以更严格的方式简单地表达标准。这为形式化方法在Internet协议开发过程中获得一席之地提供了良好的机会，从而最终提高Internet服务的可靠性、安全性和可维护性。该项目将开发新的方法和工具，在互联网协议领域应用轻量级的形式化方法。这项工作还将为一项重要的新兴互联网标准——QUIC安全传输协议——制定正式规范。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The goal of the project is to develop a methodology, supported by tools, that uses formal methods to gain clarity into the standards of network protocols and test the conformance of implementations to these standards. The work will be demonstrated on QUIC, a new complex protocol that is currently carrying about 10% of the internet traffic and is likely to carry much more of it in the near future. The standardization of QUIC is ongoing under the IETF. The software and the experimental results developed under this project will be stored in GitHub. The methodology itself will be widely disseminated by the usual means (publications, talks, etc.). The experimental results will be shared with the developers of QUIC implementations and the IETF. The project will be used to train graduate students who will be exposed to state-of-the-art techniques as well as collaboration between academia (UIC) and industry (Microsoft). The material of the course will be integrated in UIC classes. UIC is a Minority Serving Institution (MSI), Asian American and Native American Pacific Islander-Serving Institution (AANAPISI) and an Hispanic Serving Institution (HSI).Network protocol standards are described by RFCs: English-language documents that provide extensive guidance for those implementing the protocol, but are nonetheless ambiguous and broadly open to interpretation. The primary mechanism for resolving these ambiguities and validating the protocol design is to produce multiple independent implementations, and to test these implementations for interoperability which often renders the RFCs obsolete and the implementations the de-facto standard. The goal of the project is to inject formal methods into the standardization process. The approach is based on a new methodology for specification-based testing that allows to rigorously specify and test complex Internet protocols. A primary objective is to demonstrate the practical value of formal specifications in the standardization process, and in particular to show that formal specifications have practical value beyond simply expressing the standard in a more rigorous way. This has a good chance to gain entry for formal methods in the Internet protocol development process, and thus ultimately to improve the reliability, security and maintainability of Internet services. The project will develop new methodologies, accompanied by tools, to apply lightweight formal methods in the Internet protocol domain. The work will also develop a formal specification of an emerging Internet standard of significant importance --- the QUIC secure transport protocol.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.