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过时，实现成为事实上的标准。该项目的目标是将形式化方法注入标准化过程。该方法基于一种新的基于规范的测试方法，允许严格指定和测试复杂的互联网协议。一个主要的目标是证明形式规格在标准化过程中的实用价值，特别是要表明，形式规格有实用价值，而不仅仅是简单地表达标准，在一个更严格的方式。这是一个很好的机会，在互联网协议开发过程中获得正式的方法，从而最终提高互联网服务的可靠性，安全性和可维护性。该项目将开发新的方法，并配以工具，在因特网协议领域应用轻量级正式方法。 这项工作还将为一个重要的新兴互联网标准--QUIC安全传输协议制定正式规范。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.