ACM通信
研究突出了
使用Crash Hoare逻辑验证文件系统:存在崩溃时的正确性
来源:iStockPhoto.com
FSCQ是第一个可以通过机器检查证明其实现满足规范的文件系统，即使出现了故障停止崩溃。FSCQ可以避免困扰以前文件系统的bug，比如执行磁盘写入时没有足够的障碍，或者忘记清空目录块。如果崩溃发生在不合适的时间，这些错误会导致数据丢失。FSCQ的定理证明，在任何一系列崩溃之后重新启动的情况下，FSCQ将正确地恢复其状态而不会丢失数据。
为了阐明FSCQ的定理，本文引入了Crash Hoare逻辑(CHL)，它扩展了传统的Hoare逻辑，提供了一个崩溃条件、一个恢复过程和用于指定不同抽象级别上的磁盘状态的逻辑地址空间。CHL还通过证明自动化减少了开发人员的证明工作。使用CHL，我们开发、指定并证明了FSCQ文件系统的正确性。尽管FSCQ的设计相对简单，但将FSCQ作为用户级文件系统的实验表明，它足以运行具有可用性能的Unix应用程序。FSCQ的规范和证明需要比实现多得多的工作，但即使对于少数研究人员组成的小团队，这些工作也是可以管理的。
1.简介
本文描述了Crash Hoare逻辑(CHL)，它允许开发人员为崩溃安全存储系统编写规范并证明其正确性。“正确”是指，如果计算机由于电源故障或其他故障停止故障而崩溃，然后重新启动，存储系统将恢复到与其规范相符的状态(例如，POSIX17)．例如，在恢复之后，文件系统调用的所有磁盘写操作要么都在磁盘上，要么一个也没有。使用CHL，我们为POSIX的一个子集编写了一个简单的规范，并构建了FSCQ认证文件系统，它附带一个机器可检查的证明，证明其实现符合规范。
证明文件系统实现的正确性是很重要的，因为现有的文件系统在正常操作和处理崩溃方面都有很长的错误历史。24关于崩溃的推理尤其具有挑战性，因为对于文件系统开发人员来说，很难考虑所有可能发生崩溃的点，无论是在文件系统调用运行时还是在执行恢复代码期间。通常情况下，系统在许多情况下可以正常工作，但如果在两个特定磁盘写入之间的特定点发生崩溃，那么就会出现问题。29，39
构建崩溃安全文件系统的大多数方法大致可分为三类(参见SOSP论文)3.有关相关工作的更深入的讨论):测试、程序分析和模型检查。尽管它们在实际中可以有效地发现错误，但它们都不能保证在实际实现中不存在崩溃安全错误。本文主要关注这个问题:帮助开发人员使用机器可检查的证明来构建文件系统，以便在任何时候都能正确地从崩溃中恢复。
研究人员已经使用定理证明来证明现实世界的系统，比如编译器，23小的内核,22内核扩展,35以及简单的远程服务器。15部分认证项目1，10，11，18，28，32我们甚至已经瞄准了文件系统，但在每一种情况下，文件系统都不是完整的、可执行的，并准备好在真正的操作系统上运行;或者它的证明没有考虑碰撞。关于无崩溃执行的推理通常涉及考虑某些操作前后的状态。关于崩溃的推理更为复杂，因为崩溃可能暴露操作的中间状态。
构建一个用于推理文件系统崩溃的基础设施带来了几个挑战。这些挑战中最重要的是需要一个规范框架，允许文件系统开发人员形式化崩溃下的系统行为。其次，规范框架允许自动进行证明，这一点很重要，这样就可以对规范及其实现进行更改，而不必手动重做所有的证明。第三，规范框架必须能够捕获重要的性能优化，例如异步磁盘写，以便文件系统的实现具有可接受的性能。最后，规范框架必须允许模块化开发:开发人员应该能够独立地指定和验证每个组件，然后组合经过验证的组件。例如，一旦实现了日志层，文件系统开发人员应该能够证明inode层的端到端崩溃安全性，仅仅依靠日志确保原子性这一事实;他们不应该考虑inode代码中每一个可能的崩溃点。
CHL通过允许程序员指定在崩溃的情况下保留的不变量，并通过合并崩溃后运行的恢复过程的概念来解决这些挑战。CHL通过逻辑地址空间的概念支持模块化系统的构建。CHL还允许高程度的自动化证明。使用CHL，我们指定并证明了FSCQ文件系统是正确的，它包括一个简单的预写日志，并使用异步磁盘写入。
本文的下一部分概述了我们的系统体系结构，包括实现和证明。然后我们介绍CHL，我们用来验证可能崩溃的存储程序的方法。随后，我们讨论了用CHL验证的原型文件系统实现FSCQ，并从性能、正确性和其他可取的品质方面对其进行了评估。
2.系统概述
我们用广泛使用的Coq防助剂实现了CHL规范框架，8它为证明和实现提供了单一的编程语言。源代码可在以下网站获得https://github.com/mit-pdos/fscq．图1显示实现中涉及的组件。CHL是嵌入在Coq中的一种小型规范语言，它允许文件系统开发人员编写包括事故情况而且恢复过程，并证明实现满足这些规范。我们已经说明了CHL的语义，并证明它在Coq中是可靠的。
我们使用CHL实现并认证FSCQ。也就是说，我们使用CHL为POSIX系统调用的一个子集编写了规范，在Coq内部实现了这些调用，并证明每个调用的实现都满足其规范。我们投入了大量的精力为CHL构建可重用的证明自动化。但是，与编写实现相比，编写规范和证明仍然需要大量的时间。
作为FSCQ的完整性标准，我们的目标是实现与xv6文件系统相同的功能，9一种教学操作系统，它实现了带有预写日志的Unix v6文件系统。FSCQ支持的特性比今天的Unix文件系统少;例如，它缺乏对多处理器和延迟持久性的支持(即，fsync)．但是，它提供了核心POSIX文件系统调用，包括对使用间接块、嵌套目录和的大文件的支持重命名．
使用Coq的提取特性，我们将FSCQ的Coq代码自动转换为Haskell程序。我们将这个生成的实现与一个小型(未经认证的)Haskell驱动程序结合运行作为FUSE12用户级文件服务器。这种实现策略允许我们运行未经修改的Unix应用程序，但引入Haskell(我们的Haskell驱动程序)和Haskell FUSE库作为可信组件。
3.Crash Hoare逻辑
我们的目标是允许开发人员正式验证存储系统的正确性——也就是说，证明存储系统在正常运行时能够正常工作，并且能够从任何可能的崩溃中正常恢复。正如在摘要中提到的，文件系统可能忘记清空新分配的目录或间接块的内容，从而导致正常操作期间的损坏，或者它可能在没有足够的屏障的情况下执行磁盘写操作，从而导致磁盘内容可能无法恢复。先前的工作已经表明，即使是Linux内核中成熟的文件系统在正常运行过程中也有这样的错误24在崩溃恢复中。38
为了证明实现符合规范，我们必须有一种方法让开发人员声明在崩溃下允许哪些行为。为此，我们进行扩展Hoare逻辑，16其中规范的形式为{P｝过程｛问}。在这里,过程可能是一个磁盘操作序列(例如，读和写)，中间穿插着操作磁盘上的持久状态的计算，就像重命名系统调用或较低级别的操作，如分配磁盘块。P对应之前要坚持的前提过程是运行和问是后置条件。为了证明一个规范是正确的，我们必须证明它过程建立了问,假设P在调用之前保持过程．在我们的重命名系统调用示例，P可能要求文件系统用某种树表示t而且问可能承诺结果文件系统由修改过的树表示t，反映重命名操作。
Hoare逻辑不足以对崩溃进行推理，因为崩溃可能导致崩溃过程在执行过程中的任何一点停止，并可能使磁盘处于问不成立(如在重命名例如，新文件名已经创建，但旧文件名还没有删除)。此外，如果计算机重新启动，它通常运行一个恢复过程(如fsck)，方可恢复正常运作。霍尔逻辑没有提供一个概念，在任何时候过程的执行，则可能运行恢复过程。本节的其余部分描述CHL如何扩展Hoare逻辑来处理崩溃。
传统的Hoare逻辑区分了部分正确(我们证明终止程序给出正确答案)和完全正确(我们也证明终止程序)。我们使用Coq的内置终止检查器来确保我们的系统调用总是在没有崩溃发生的情况下完成。然而，我们建模的情况下，一个程序仍然永远运行，因为它不断崩溃，然后在恢复期间再次崩溃，直到无限。由于这个原因，我们的规范可以解释为无崩溃执行的完全正确和崩溃执行的部分正确，这是有道理的，因为底层硬件平台拒绝为程序员提供在出现崩溃时保证正常终止的方法。
3.1.例子
许多文件系统操作必须以原子方式更新两个或多个磁盘块。例如，在创建一个文件时，文件系统必须将一个inode标记为已分配，并更新创建该文件的目录(以记录带有已分配inode号的文件名)。为了确保在崩溃下的正确行为，一种常见的方法是使用预写日志。日志记录可以确保，如果文件系统操作在应用其更改到磁盘时崩溃，那么在崩溃之后，恢复过程可以通过应用日志内容完成任务。提前写日志可以避免不必要的中间状态，即分配了inode但没有记录到目录中，从而有效地丢失了一个inode。许多文件系统，包括广泛使用的Linux的ext4，34正是出于这个原因才使用日志记录。
所示的简单程序图2捕获必须更新两个或多个块的文件系统调用的本质。该过程使用预写日志执行两次磁盘写操作log_begin, log_commit,log_writeapi。这个过程log_write将磁盘块的内容追加到内存日志中，而不是原地更新磁盘块。这个过程log_commit将日志写入磁盘，写入提交记录，然后将日志中的块内容复制到磁盘上的块位置。如果此过程崩溃并重新引导系统，则运行恢复过程。恢复过程查找提交记录。如果存在提交记录，它将从日志中将块内容复制到适当的位置，然后清理日志，从而完成操作。
如果没有提交记录，则恢复过程只清理日志。如果在恢复期间出现崩溃，那么在重新启动之后，恢复过程将再次运行。原则上，这种情况可能会发生几次。但是，如果恢复完成，那么要么两个块都更新了，要么都没有更新。因此，在atomic_two_write程序从图2时，预写日志保证两个写都发生或都不发生，无论何时发生和发生了多少次崩溃。
CHL使编写诸如atomic_two_write以及预写日志系统，我们将在本节的其余部分中解释。
3.2.事故情况
CHL需要一种方法让开发人员写下关于磁盘状态的谓词，例如对可能发生崩溃的中间状态的描述。为此，CHL扩展了带有崩溃条件的Hoare逻辑，在精神上类似于先前在故障停止处理器上的工作33，第3节和并发工作的故障条件，28但是精确地形式化，允许可执行的实现和机器检查的证明。
对于模块化，CHL应该只允许对磁盘的一个部分进行推理，而不是必须始终指定整个磁盘的内容。例如，我们想要指定两个块发生了什么atomic_two_write更新，而不必说明磁盘的其他部分。为了做到这一点，CHL雇佣了逻辑分离，30.这是一种组合存储(在我们的例子中是磁盘)中不相连部分上的谓词的方法。分离逻辑中的基本谓词是一个点-指向关系，写为一个v，就是那个地址一个是有价值的v．给定两个谓词x而且y，分离逻辑允许CHL生成一个组合谓词x
没有找到条目