CSR: Medium: A High-Performance Certified File System and Applications

CSR：Medium：高性能认证文件系统和应用程序

• 批准号: 1563763
• 负责人: Marinus Kaashoek
• 金额: $ 90万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-06-01 至 2021-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1563763&HistoricalAwards=false
• 关键词: CSR; Medium; Performance; Certified; File

Applications rely on file systems to store their data, but even carefully written applications and file systems may have bugs that cause data loss, especially in the face of system crashes (e.g., due to power failure). Even in mature file systems such as ext4, bugs that can lead to data loss are not uncommon. Application developers also misuse file-system APIs in ways that lead to user data being lost after a crash.Formal verification is a good way to prove the absence of bugs in a file system. By considering all possible operations and crashes, verification can ensure that the file system is bug-free. The goal of this proposal is to develop a certified high-performance file system, VCFS (Verified Concurrent File System). The investigators aim to make VCFS's performance good enough to support demanding applications while guaranteeing crash safety. VCFS and its applications will come with mathematical proofs that their implementations meet their specifications under any sequences of crashes.The main outcomes of this research will be as follows: (1) A logic system, CFSL (Concurrent File System Logic), that allows reasoning about parallelism and crashes. (2) A precise specification of the POSIX API under concurrency and crashes. (3) The VCFS file system, for which we will prove that its implementation meets our POSIX specification under crashes and concurrency. VCFS will include sophisticated performance optimizations. (4) A certified high-performance mail server, as a test case of using VCFS and its formally specified APIs to prove application-level properties (in this case, that the server will not lose acknowledged messages).CFSL will enable developers to reason about concurrency and crashes in the context of file systems. The POSIX specification, along with VCFS, will help programmers develop applications that are both high-performance and safe under computer crashes. The investigators will use their understanding of writing certified software to create a new class on certified software.

应用程序依靠文件系统来存储其数据，但是即使是仔细编写的应用程序和文件系统也可能会导致数据丢失，尤其是在系统崩溃时（例如，由于电源故障）。 即使在诸如EXT4之类的成熟文件系统中，可能导致数据丢失的错误并不少见。 应用程序开发人员还以导致崩溃后用户数据丢失的方式滥用文件系统API。形式验证是证明文件系统中没有错误的好方法。通过考虑所有可能的操作和崩溃，验证可以确保文件系统不存在。 该建议的目的是开发经认证的高性能文件系统VCFS（已验证的并发文件系统）。调查人员的目的是使VCFS的性能足够出色，以支持苛刻的应用程序，同时保证碰撞安全性。 VCF及其应用程序将带有数学证明，即它们的实现在任何崩溃序列下都符合其规格。这项研究的主要结果将如下：（1）逻辑系统CFSL（并发文件系统逻辑），允许对并行性和崩溃进行推理。 （2）在并发和崩溃下的POSIX API的精确规范。 （3）VCFS文件系统，我们将证明其实现符合我们在崩溃和并发下的POSIX规范。 VCF将包括复杂的性能优化。 （4）使用VCFS及其正式指定的API来证明应用程序级属性的测试案例（在这种情况下，该服务器将不会丢失已确认的消息）.CFSL将使开发人员能够理解汇总并在文件系统的上下文中崩溃。 POSIX规范以及VCF将帮助程序员开发在计算机崩溃下既具有高性能又安全的应用程序。 调查人员将利用他们对书面认证软件的理解来创建有关认证软件的新类。

项目成果

Argosy: verifying layered storage systems with recovery refinement

• DOI: 10.1145/3314221.3314585
• 发表时间: 2019-06
• 期刊: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
• 作者: Tej Chajed;Joseph Tassarotti;M. Kaashoek;Nickolai Zeldovich

Proving confidentiality in a file system using DISKSEC

使用 DISKSEC 证明文件系统的机密性

• 发表时间: 2018
• 期刊: Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI
• 作者: Ileri, Atalay;Chajed, Tej;Chlipala, Adam;Kaashoek, Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai

GoJournal: a verified, concurrent, crash-safe journaling system

GoJournal：经过验证、并发、防崩溃的日志系统

• 发表时间: 2021
• 期刊: Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation
• 作者: Chajed, Tej;Tassarotti, Joseph;Theng, Mark;Jung, Ralf;Kaashoek, M. Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai

Verifying concurrent, crash-safe systems with Perennial

使用 Perennial 验证并发、防碰撞系统

• DOI: 10.1145/3341301.3359632
• 发表时间: 2019
• 期刊: Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP
• 作者: Chajed, Tej;Tassarotti, Joseph;Kaashoek, Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai

Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning

使用顺序推理验证 DaisyNFS 并发和崩溃安全文件系统

• 发表时间: 2022
• 期刊: Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022
• 作者: Chajed, Tej;Tassarotti, Joseph;Theng, Mark;Kaashoek, M. Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai