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

Suny At Stony Brook, Stony Brook NY

Investigators

Abstract

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.