Yggdrasil is a toolkit for verifying file system with push-button verification via crash refinement. As for push-button verification, it means that Yggdrasil needs no manual annotations or proofs. As for crash refinement, it is amenable to fully automated SMT reasoning. The whole verification is something like the State-Machine Specification in the project “Hyperkernel”.
The whole system architecture is shown as follows.
From this picture, we know that Yggdrasil needs three inputs: a specification of the expected behavior, an implementation and consistency invariants which indicate whether a file system image is in a consistent state or not. For better run-time performance, Yggdrasil optionally performs optimizations. If there is a bug, Yggdrasil produces a counterexample to help identify and fix the cause. It requires no manual annotations or proofs about the implementation code. Once the verification passes, Yggdrasil emits C code, which is then compiled and linked using a C compiler to produce an executable file system, as well as a “fsck” checker.
The above is the entire overall content of this project. The authors also introduced every part of this project. I will analyze it by following the paper.
Single-level File System (YminLFS)
In this project, every file system must contain three parts: an abstract data structure, a set of operations and a state equivalence predicate which defines whether a given implementation satisfies the specification. So the authors first defines a file system which contains these features.
Then it runs the verification. Yggdrasil uses the Z3 solver to prove a two-part crash refinement.
The first part deals with crash-free executions which requires the implementation and specification are similar in the absence of crashes, which means if both YminLFS and FSSpec start in equivalent and consistent states, they end up in equivalent and consistent states (just like state-machine). This project defines equivalence using the equivalent predicate and defines consistency using the consistency invariants as the above pictures show.
The second part deals with crash executions which requires the implementation to exist no more crash states than the specification, which means each possible state of the YminLFS implementation must be equivalent to some crash state of FSSpec. What’s more, Yggdrasil provides a greedy optimizer that tries to remove every disk flush and re-verify the code.
Multi-level File System (Yxv6)
We could directly prove crash refinement between the entire file system specification and implementation in a single-level file system, however, we couldn’t use the same method in a complex multi-level file system. First, let’s look at the structure of Yxv6 journaling file system.
This is the 5 layers of abstraction and every layer contains a specification and a implementation. The authors use this project to prove crash refinement for each layer and upper layers then use the specifications of lower layers. The lowest layer of the stack is a specification of an asynchronous disk. This specification comprises the asynchronous disk model which is to implement YminLFS.
Ycp has a formal specification which means if the copy operation succeeds, the result is the same as “cp”, however, if it fails, the file system is unchanged. To achieve this propose, the implementation of Ycp is something similar to Yxv6 file system specification. There are 3 atomicity patterns which are “create a temporary file”, “write the source data to it” and “rename it to atomically create the target file”. After doing such an analogy, verifying this operation is similar to verify the single-level file system.
本文链接： http://home.meng.uno/articles/5ed9f695/ 欢迎转载！