FMitF: Track I: Injecting Formal Methods into Internet Standardization

点击翻译按钮获取中文摘要

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.