FMitF: Track I: NLP-Assisted Formal Verification of the NFS Distributed File System Protocol

互联网的成功和发展归功于确保计算机可以相互通信的标准。这些标准是人工编写的技术设计文档，需要数年时间来开发和实现。然而，这样的设计文档通常是不精确的，并且它们的软件实现并不总是符合它们的设计。本项目旨在加速互联网标准的设计和实施过程，采用：(1)人工智能（AI）技术自动处理设计文档，以便快速发现和报告设计文档中的缺陷；(2)对软件实现进行运行时分析，以检测其各自设计的偏差。项目工件——软件、源代码、经过验证和修复的rfc、数据集、跟踪和结果都将包含在我们称为“NFS验证器”的系统中。研究结果将通过同行评审的出版物和arxiv.org进行传播。所有文物将通过项目网站：https://www.filesystems.org/nfsval公开，并将在项目结束后至少十年可用。该项目将：(1)开展涉及复杂的分布式网络文件系统第4版（NFSv4）协议的主要案例研究；(2)利用自然语言处理（NLP）人工智能技术建立NFSv4预期行为的理论模型；(3)分析模型，发现不一致之处；(4)将模型与已知正确的另一个参考实现进行核对；(5)监控实际运行的NFS实现是否符合我们验证的理论模型。NFS是一种流行且不断发展的协议，它使用户能够跨任何网络访问他们的文件和数据。NFSv4设计文档相当复杂，长达500多页。该项目将(1)帮助加快NFSv4正在进行的设计、开发和采用；(2)推动NLP/AI技术的发展，以理解人类编写的设计文档；（三）提高设计的形式化建模和验证的技术水平；（四）培养和教育研究生和本科生；(5)产生适用于许多其他互联网标准的结果。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The Internet's success and growth is owed to standards that ensure computers can talk to each other. These standards are human-written, technical design documents that take years to develop and implement. However, such design documents are often imprecise, and their software implementations do not always conform to their designs. This project aims to speed up the process of designing and implementing Internet standards using: (1) Artificial Intelligence (AI) techniques to automatically process design documents so that flaws in them can be detected and reported quickly, and (2) runtime analysis of software implementations to detect deviations from their respective designs. The project artifacts - software, source code, verified and fixed RFCs, data sets, traces, and results will all be embodied in a system we call "NFS Validator". Results will be disseminated using peer-reviewed publications and arxiv.org. All artifacts will be made public through the project Website: https://www.filesystems.org/nfsval, and will be available for at least ten years following the end of the project.This project will: (1) conduct a major case study involving the complex, distributed Network File System version 4 (NFSv4) protocol; (2) develop a theoretical model of NFSv4's expected behavior using Natural Language Processing (NLP) AI techniques; (3) analyze the model to detect inconsistencies; (4) check the model against another reference implementation that is known to be correct; and (5) monitor an actual running NFS implementation for compliance with our verified theoretical model. The NFS is a popular and growing protocol that enables users to access their files and data across any network. The NFSv4 design documents are fairly complex and over 500 pages long. This project will (1) help accelerate NFSv4's ongoing design, development, and adoption; (2) advance the state of the art in NLP/AI techniques to understand human-written design documents; (3) advance the state of the art in formally modeling and verifying such designs; (4) train and educate graduate and undergraduate students; and (5) produce results that are applicable to many other Internet standards.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.