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

应用程序依赖于文件系统来存储其数据，但即使是精心编写的应用程序和文件系统也可能存在导致数据丢失的错误，特别是在面临系统崩溃时（例如，由于停电）。 即使在ext4这样的成熟文件系统中，可能导致数据丢失的错误也并不罕见。 应用程序开发人员还滥用文件系统API，导致用户数据在崩溃后丢失。形式化验证是证明文件系统中没有错误的好方法。通过考虑所有可能的操作和崩溃，验证可以确保文件系统没有错误。 该提案的目标是开发一个经过认证的高性能文件系统，VCFS（验证并发文件系统）。研究人员的目标是使VCFS的性能足够好，以支持要求苛刻的应用，同时保证碰撞安全。 本文的主要研究成果如下：（1）提出了一个并行文件系统逻辑系统CFSL（ConcurrentFileSystemLogic），它支持并行性和崩溃的推理。(2)并发和崩溃下POSIX API的精确规范。(3)VCFS文件系统，我们将证明其实现在崩溃和并发情况下符合我们的POSIX规范。VCFS将包括复杂的性能优化。(4)一个经过认证的高性能邮件服务器，作为使用VCFS及其正式指定的API来证明应用程序级属性（在这种情况下，服务器不会丢失已确认的消息）的测试用例。CFSL将使开发人员能够在文件系统的上下文中推理并发和崩溃。 POSIX规范，沿着VCFS，将帮助程序员开发高性能和在计算机崩溃下安全的应用程序。 研究人员将利用他们对编写认证软件的理解来创建一个关于认证软件的新课程。

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.