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（Verified Concurrent File System）。研究人员的目标是使 VCFS 的性能足以支持要求苛刻的应用，同时保证碰撞安全。 VCFS 及其应用程序将提供数学证明，证明其实现在任何崩溃序列下都满足其规范。这项研究的主要成果如下： (1) 逻辑系统 CFSL（并发文件系统逻辑），允许推理关于并行性和崩溃。 (2)并发和崩溃情况下POSIX API的精确规范。 (3) VCFS 文件系统，我们将证明其实现在崩溃和并发情况下满足我们的 POSIX 规范。 VCFS 将包括复杂的性能优化。 (4) 一个经过认证的高性能邮件服务器，作为使用 VCFS 及其正式指定的 API 来证明应用程序级属性的测试用例（在这种情况下，服务器不会丢失已确认的消息）。CFSL 将使开发人员能够推理关于文件系统上下文中的并发和崩溃。 POSIX 规范与 VCFS 一起将帮助程序员开发在计算机崩溃时既高性能又安全的应用程序。 研究人员将利用他们对编写认证软件的理解来创建一个关于认证软件的新课程。

项目成果

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 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

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