The main contribution of this thesis is a methodology for designing, implementing and verifying realistic file systems with evidence of its effectiveness by application to a non-trivial flash file system. The goal of this research is to demonstrate that an implementation level machine-checked proof of correctness of a file system can be done at reasonable cost.Our approach leverages Cogent, a purely functional, memory- and type-safe language we helped design, that bridges the gap between verifiable formal model and low-level code. Cogent takes a modular file system implementation as input and generates a C implementation and a formal proof that links it to its corresponding generated Cogent specification. Cogent specifications inherit the purely functional aspect of the input source code, and thus they proved much easier to reason about than the C code directly.In order to prove the correctness of complex file system components at reasonable cost, we decompose the functionality into a set of components such that the correctness of each can be proven in isolation. The component proofs are mechanically composed into a theorem that holds on the C implementation by refinement.To validate our approach, we designed and implemented BilbyFs, a modular flash file system. We formally specified BilbyFs' file system operations in Isabelle/HOL, and proved the functional correctness of two key operations: sync() and iget().BilbyFs' design demonstrates the practicality of aggressive modular decomposition, and its Cogent implementation highlights the benefits and feasibility of using a linearly-typed language to implement a realistic file system. Our verification results show that we can exploit our modular design to reason about implementation components in isolation, and that overall our methodology drastically reduces the effort of verifying file system code.
展开▼
