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

FMITF：第一轨：NLP 辅助 NFS 分布式文件系统协议的形式验证

• 批准号: 1918225
• 负责人: Erez Zadok
• 金额: $ 74.83万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1918225&HistoricalAwards=false
• 关键词: FMitF; Track; NLP; Assisted; Formal

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.

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

项目成果

Input and Output Coverage Needed in File System Testing

文件系统测试所需的输入和输出覆盖率

• DOI: 10.1145/3599691.3603405
• 发表时间: 2023
• 期刊: The 15th ACM Workshop on Hot Topics in Storage and File Systems (HotStorage '23
• 作者: Liu, Yifei;Ahuja, Gautam;Kuenning, Geoff;Smolka, Scott;Zadok, Erez
• 通讯作者: Zadok, Erez

A distributed simplex architecture for multi-agent systems

多智能体系统的分布式单纯形体系结构

• DOI: 10.1016/j.sysarc.2022.102784
• 发表时间: 2023
• 期刊: Journal of Systems Architecture
• 影响因子: 4.5
• 作者: Mehmood, Usama;Roy, Shouvik;Damare, Amol;Grosu, Radu;Smolka, Scott A.;Stoller, Scott D.
• 通讯作者: Stoller, Scott D.

SpecNFS: A Challenge Dataset Towards Extracting Formal Models from Natural Language Specifications

• 发表时间: 2022
• 作者: Sayontan Ghosh;Amanpreet Singh;Alex Merenstein;S. Smolka;E. Zadok;Niranjan Balasubramanian

Synthesizing Pareto-Optimal Signal-Injection Attacks on ICDs

综合 ICD 的帕累托最优信号注入攻击

• DOI: 10.1109/access.2022.3233010
• 发表时间: 2023
• 期刊: IEEE Access
• 影响因子: 3.9
• 作者: Krish, Veena;Paoletti, Nicola;Smolka, Scott A.;Rahmati, Amir
• 通讯作者: Rahmati, Amir

Swarm Model Checking on the {GPU}

{GPU} 上的群体模型检查

• DOI: 10.1007/978-3-030-30923-7_6
• 发表时间: 2020
• 期刊: International journal on software tools for technology transfer
• 影响因子: 1.5
• 作者: DeFrancisco, R.;Cho, S.;Ferdman, M.;Smolka, S. A.
• 通讯作者: Smolka, S. A.