Certifying a file system using crash hoare logic: correctness in the presence of crashes

Abstract

FSCQ is the first file system with a machine-checkable proof that its implementation meets a specification, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover its state correctly without losing data.

To state FSCQ's theorems, this paper introduces the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers.<!-- END_PAGE_1 -->

References

1. Amani, S., Hixon, A., Chen, Z., Rizkallah, C., Chubb, P., O'Connor, L., Beeren, J., Nagashima, Y., Lim, J., Sewell, T., Tuong, J., Keller, G., Murray, T., Klein, G., Heiser, G. Cogent: Verifying high-assurance file system implementations. In Proceedings of the 21th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (Atlanta, GA, Apr. 2016), 175--188.
2. Bobbio, J. et al. Haskell bindings for the FUSE library, 2014. https://github.com/m15k/hfuse.
3. Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N. Using Crash Hoare Logic for certifying the FSCQ file system. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP) (Monterey, CA, Oct. 2015).
4. Chinner, D. xfs: Fix double free in xlog_recover_commit_trans, Sept. 2014. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=88b863db97a18a04c90ebd57d84e1b7863114dcb.
5. Chinner, D. xfs: xfs_dir_fsync() returns positive errno, May 2014. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=43ec1460a2189fbee87980dd3d3e64cba2f11e1f.
6. Chlipala, A. Mostly-automated verification of low-level programs in computational separation logic. In Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (San Jose, CA, June 2011), 234--245.
7. Clements, A.T., Kaashoek, M.F., Zeldovich, N., Morris, R.T., Kohler, E. The scalable commutativity rule: Designing scalable software for multicore processors. In Proceedings of the 24th ACM Symposium on Operating Systems Principles (SOSP) (Farmington, PA, Nov. 2013), 1--17.
8. Coq development team. The Coq Proof Assistant Reference Manual, Version 8.5pl1. INRIA, Apr. 2016. http://coq.inria.fr/distrib/current/refman/.
9. Cox, R., Kaashoek, M.F., Morris, R.T. Xv6, a simple Unix-like teaching operating system, 2014. http://pdos.csail.mit.edu/6.828/2014/xv6.html.
10. Ernst, G., Pfahler, J., Schellhorn, G., Reif, W. Inside a verified flash file system: Transactions & garbage collection. In Proceedings of the 7th Working Conference on Verified Software: Theories, Tools and Experiments (San Francisco, CA, July 2015).
11. Freitas, L., Woodcock, J., Butterfield, A. POSIX and the verification grand challenge: A roadmap. In Proceedings of 13th IEEE International Conference on Engineering of Complex Computer Systems (Belfast, Northern Ireland, Mar.-Apr. 2008), 153--162.
12. FUSE: Filesystem in userspace, 2013. http://fuse.sourceforge.net/.
13. Goldstein, A. ext4: Handle errors in ext4_rename, Mar. 2011. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=ef6078930263bfcdcfe4dddb2cd85254b4cf4f5c.
14. Gray, J. Notes on data base operating systems. In Operating Systems: An Advanced Course, R. Bayer, R.M. Graham, and G. Seegmuller, eds. Springer-Verlag, London, UK, 1978, 393--481.
15. Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B. Ironclad Apps: End-to-end security via automated full-system verification. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) (Broomfield, CO, Oct. 2014), 165--181.
16. Hoare, C.A.R. An axiomatic basis for computer programming. Commun. ACM 12 10 (Oct. 1959), 576--580.
17. IEEE (The Institute of Electrical and Electronics Engineers) and The Open Group. The Open Group base specifications issue 7, 2013 edition (POSIX.1-2008/Cor 1-2013), Apr. 2013.
18. Joshi, R., Holzmann, G.J. A mini challenge: Build a verifiable filesystem. Formal Aspects Comput. 19, 2 (June 2007), 269--272.
19. Kara, J. ext3: Avoid filesystem corruption after a crash under heavy delete load, July 2010. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=f25f624263445785b94f39739a6339ba9ed3275d.
20. Kara, J. jbd2: Issue cache flush after checkpointing even with internal journal, Mar. 2012. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=79feb521a44705262d15cc819a4117a447b11ea7.
21. Kara, J. ext4: Fix overflow when updating superblock backups after resize, Oct. 2014. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=9378c6768e4fca48971e7b6a9075bc006eda981d.
22. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Norrish, M., Kolanski, R., Sewell, T., Tuch, H., Winwood, S. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP) (Big Sky, MT, Oct. 2009), 207--220.
23. Leroy, X. Formal verification of a realistic compiler. Commun. ACM 52, 7 (July 2009), 107--115.
24. Lu, L., Arpaci-Dusseau, A.C., Arpaci-Dusseau, R.H., Lu, S. A study of Linux file system evolution. In Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST) (San Jose, CA, Feb 2013), 31--44.
25. Manana, F. Btrfs: Fix race between writing free space cache and trimming, Dec. 2014. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=55507ce3612365a5173dfb080a4baf45d1ef8cd1.
26. Mason, C. Btrfs: Prevent loops in the directory tree when creating snapshots, Nov. 2008. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=ea9e8b11bd1252dcbc23afefcf1a52ec6aa3c113.
27. Morton, A. {PATCH} ext2/ext3-ENOSPC bug, Mar. 2004. https://git.kernel.org/cgit/linux/kernel/git/tglx/history.git/commit/?id=5e9087ad3928c9d80cc62b583c3034f864b6d315.
28. Ntzik, G., da Rocha Pinto, P., Gardner, P. Fault-tolerant resource reasoning. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS) (Pohang, South Korea, Nov.-Dec. 2015).
29. Pillai, T.S., Chidambaram, V., Alagappan, R., Al-Kiswany, S., Arpaci-Dusseau, A.C., Arpaci-Dusseau, R.H. All file systems are not created equal: On the complexity of crafting crash-consistent applications. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) (Broomfield, CO, Oct. 2014), 433--448.
30. Reynolds, J.C. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (Copenhagen, Denmark, July 2002), 55--74.
31. Rosenblum, M., Ousterhout, J. The design and implementation of a log-structured file system. In Proceedings of the 13th ACM Symposium on Operating Systems Principles (SOSP) (Pacific Grove, CA, Oct. 1991), 1--15.
32. Schellhorn, G., Ernst, G., Pfahler, J., Haneberg, D., Reif, W. Development of a verified flash file system. In Proceedings of the ABZ Conference (Toulouse, France, June 2014).
33. Schlichting, R.D., Schneider, F.B. Fail-stop processors: An approach to designing fault-tolerant computing systems. ACM Trans. Comput. Syst. 1, 3 (1983), 222--238.
34. Tweedie, S.C. Journaling the Linux ext2fs filesystem. In Proceedings of the 4th Annual LinuxExpo (Durham, NC, May 1998).
35. Wang, X., Lazar, D., Zeldovich, N., Chlipala, A., Tatlock, Z. Jitk: A trustworthy in-kernel interpreter infrastructure. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) (Broomfield, CO, Oct. 2014), 33--47.
36. Wong, D.J. ext4: Fix same-dir rename when inline data directory overflows, Aug. 2014. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=d80d448c6c5bdd32605b78a60fe8081d82d4da0f.
37. Xie, M. Btrfs: Fix broken free space cache after the system crashed, June 2014. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=e570fd27f2c5d7eac3876bccf99e9838d7f911a3.
38. Yang, J., Twohey, P., Engler, D., Musuvathi, M. eXplode: A lightweight, general system for finding serious storage system errors. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI) (Seattle, WA, Nov. 2006), 131--146.
39. Zheng, M., Tucek, J., Huang, D., Qin, F., Lillibridge, M., Yang, E.S., Zhao, B.W., Singh, S. Torturing databases for fun and profit. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) (Broomfield, CO, Oct. 2014), 449--464.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification