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

应用程序依赖于文件系统来存储它们的数据，但是即使是精心编写的应用程序和文件系统也可能存在导致数据丢失的错误，特别是在面对系统崩溃时（例如，由于电源故障）。即使在成熟的文件系统（如ext4）中，导致数据丢失的错误也并不少见。应用程序开发人员还会滥用文件系统api，导致用户数据在崩溃后丢失。形式化验证是证明文件系统中不存在错误的好方法。通过考虑所有可能的操作和崩溃，验证可以确保文件系统没有错误。本提案的目标是开发一个经过认证的高性能文件系统，VCFS（验证并发文件系统）。研究人员的目标是使VCFS的性能足够好，以支持苛刻的应用，同时保证碰撞安全。VCFS及其应用程序将提供数学证明，证明它们的实现在任何崩溃序列下都符合其规范。本研究的主要成果将如下：(1)一个逻辑系统，CFSL（并发文件系统逻辑），允许对并行性和崩溃进行推理。(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.