Cogent: Verifying High-Assurance File System Implementations

ABSTRACT

We present an approach to writing and formally verifying high-assurance file-system code in a restricted language called Cogent, supported by a certifying compiler that produces C code, high-level specification of Cogent, and translation correctness proofs. The language is strongly typed and guarantees absence of a number of common file system implementation errors. We show how verification effort is drastically reduced for proving higher-level properties of the file system implementation by reasoning about the generated formal specification rather than its low-level C code. We use the framework to write two Linux file systems, and compare their performance with their native C implementations.

References

1. Alkassar, E., Hillebrand, M., Leinenbach, D., Schirmer, N., Starostin, A., and Tsyban, A. Balancing the load -- leveraging a semantics stack for systems verification. Journal of Automated Reasoning: Special Issue on Operating System Verification 42, Numbers 2--4 (2009), 389--454.
2. Alkassar, E., Paul, W., Starostin, A., and Tsyban, A. Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices. In Proceedings of Verified Software: Theories, Tools and Experiments 2010 (Edinburgh, UK, Aug. 2010), vol. 6217 of Lecture Notes in Computer Science, pp. 71--85.
3. Amani, S., and Murray, T. Specifying a realistic file system. In Workshop on Models for Formal Analysis of Real Systems (Suva, Fiji, Nov. 2015), pp. 1--9.
4. Andronick, J. Formally Proved Anti-tearing Properties of Embedded C Code. In Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Paphos, Cyprus, Nov. 2006), pp. 129--136. Invited Speaker.
5. Arkoudas, K., Zee, K., Kuncak, V., and Rinard, M. C. Verifying a file system implementation. In Proceedings of the 6th International Conference on Formal Engineering Methods (Seattle, WA, USA, Nov. 2004), vol. 3308 of Lecture Notes in Computer Science, pp. 373--390.
6. Bertot, Y., and Castéran, P. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. 2004.
7. Bevier, W., Cohen, R., and Turner, J. A specification for the Synergy file system. Tech. Rep. Technical Report 120, Computational Logic Inc., Austin, Texas, USA, Sept. 1995.
8. Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M. F., and Zeldovich, N. Using Crash Hoare logic for certifying the FSCQ file system. In Proceedings of the 25rd ACM Symposium on Operating Systems Principles (Monterey, CA, Oct. 2015), pp. 18--37.
9. Damchoom, K., Butler, M., and Abrial, J.-R. Modelling and proof of a tree-structured file system in Event-B and Rodin. In Proceedings of the 10th International Conference on Formal Engineering Methods (Kitakyushu-City, Japan, Oct. 2008), vol. 5256 of Lecture Notes in Computer Science, pp. 25--44.
10. Elphinstone, K., and Heiser, G. From L3 to seL4 -- what have we learnt in 20 years of L4 microkernels? In ACM Symposium on Operating Systems Principles (Farmington, PA, USA, Nov. 2013), pp. 133--150.
11. Ernst, G., Schellhorn, G., Haneberg, D., Pfahler, J., and Reif, W. Verification of a virtual filesystem switch. In Proceedings of Verified Software: Theories, Tools and Experiments 2013 (Menlo Park, CA, USA, May 2013), vol. 8164 of Lecture Notes in Computer Science, pp. 242--261.
12. Gu, L., Vaynberg, A., Ford, B., Shao, Z., and Costanzo, D. CertiKOS: A certified kernel for secure cloud computing. In Proceedings of the 2nd Asia-Pacific Workshop on Systems (APSys) (2011).
13. Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X. N., Weng, S., Zhang, H., and Guo, Y. Deep specifications and certified abstraction layers. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2015), pp. 595--608.
14. Gunawi, H. S., Rubio-González, C., Arpaci-Dusseau, A. C., Arpaci-Dussea, R. H., and Liblit, B. EIO: error handling is occasionally correct. In Proceedings of the 6th USENIX Conference on File and Storage Technologies (Feb. 2008), pp. 207--222.
15. Hawblitzel, C., Howell, J., Lorch, J. R., Narayan, A., Parno, B., Zhang, D., and Zill, B. Ironclad apps: End-to-end security via automated full-system verification. In USENIX Symposium on Operating Systems Design and Implementation (Broomfield, CO, US, Oct. 2014), pp. 165--181.
16. The Heartbleed bug. http://heartbleed.com, https://www.openssl.org/news/secadv_20140407.txt, Apr. 2014. Accessed March 2015.
17. Herder, J. N., Bos, H., Gras, B., Homburg, P., and Tanenbaum, A. S. MINIX 3: A highly reliable, self-repairing operating system. ACM Operating Systems Review 40, 3 (July 2006), 80--89.
18. Hesselink, W. H., and Lali, M. I. Formalizing a hierarchical file system. In Proceedings of the 14th BCS-FACS Refinement Workshop (Eindhoven, The Netherlands, Nov. 2009), vol. 259 of Electronic Notes in Theoretical Computer Science, pp. 67--85.
19. Hunter, A. A brief introduction to the design of UBIFS, 03 2008.
20. IOzone filesystem benchmark. http://www.iozone.org/.
21. Joshi, R., and Holzmann, G. J. A mini challenge: build a verifiable filesystem. Formal Aspects of Computing 19, 2 (2007), 269--272.
22. Katcher, J. PostMark: A new file system benchmark. Tech. Rep. TR-3022, NetApp, October 1997.
23. Keller, G., Murray, T., Amani, S., O'Connor-Davis, L., Chen, Z., Ryzhyk, L., Klein, G., and Heiser, G. File systems deserve verification too! In Workshop on Programming Languages and Operating Systems (PLOS) (Farmington, Pennsylvania, USA, Nov. 2013), pp. 1--7.
24. Klein, G. Operating system verification -- an overview. S\=adhan\=a 34, 1 (Feb. 2009), 27--69.
25. Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., and Heiser, G. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems 32, 1 (Feb. 2014), 2:1--2:70.
26. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., et al. seL4: Formal verification of an OS kernel. In ACM Symposium on Operating Systems Principles (Big Sky, MT, US, Oct. 2009), pp. 207--220.
27. Leroy, X. Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston, SC, USA, 2006), pp. 42--54.
28. Leroy, X. Formal verification of a realistic compiler. Communications of the ACM 52, 7 (2009), 107--115.
29. Liedtke, J. Improving IPC by kernel design. In Proceedings of the 14th ACM Symposium on Operating Systems Principles (Asheville, NC, US, Dec. 1993), pp. 175--188.
30. Memory leak in Android Lollipop's rendering engine. https://code.google.com/p/android/issues/detail?id=79729#c177, Dec. 2014. Accessed March 2015.
31. Maric, O., and Sprenger, C. Verification of a transactional memory manager under hardware failures and restarts. In Proceedings of the 19th International Symposium on Formal Methods (FM) (May 2014), vol. 8442 of Lecture Notes in Computer Science, pp. 449--464.
32. Matichuk, D., Murray, T., Andronick, J., Jeffery, R., Klein, G., and Staples, M. Empirical study towards a leading indicator for cost of formal software verification. In International Conference on Software Engineering (Firenze, Italy, Feb. 2015), p. 11.
33. Morgan, C., and Sufrin, B. Specification of the UNIX filing system. IEEE Transactions on Software Engineering 10, 2 (1984), 128--142.
34. Nipkow, T., Paulson, L., and Wenzel, M. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic, vol. 2283 of Lecture Notes in Computer Science. 2002.
35. POSIX filesystem test project. http://sourceforge.net/p/ntfs-3g/pjd-fstest/ci/master/tree/. Retrieved Jan., 2016.
36. O'Connor, L., Rizkallah, C., Chen, Z., Amani, S., Lim, J., Nagashima, Y., Sewell, T., Hixon, A., Keller, G., Murray, T., and Klein, G.textscCOGENT: Certified compilation for a functional systems language. CoRR abs/1601.05520 (2016).
37. Apple's SSL/TLS bug. https://www.imperialviolet.org/2014/02/22/applebug.html, Feb. 2014. Accessed March 2015.
38. Palix, N., Thomas, G., Saha, S., Calvès, C., Lawall, J., and Muller, G. Faults in Linux: ten years later. In Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (Newport Beach, CA, US, 2011), pp. 305--318.
39. Reif, W., Schellhorn, G., Stenzel, K., and Balser, M. Structured specifications and interactive proofs with KIV. In Automated Deduction -- A Basis for Applications, vol. 9 of Applied Logic Series. 1998, pp. 13--39.
40. Reynolds, J. C. Separation logic: A logic for mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (Copenhagen, Denmark, July 2002).
41. Rubio-González, C., and Liblit, B. Defective error/pointer interactions in the Linux kernel. In Proceedings of the 20th International Symposium on Software Testing and Analysis (Toronto, ON, Canada, July 2011), pp. 111--121.
42. Saha, S., Lawall, J., and Muller, G. An approach to improving the structure of error-handling code in the Linux kernel. In Conference on Language, Compiler and Tool Support for Embedded Systems (LCTES) (Chicago, IL, USA, Apr. 2011), pp. 41--50.
43. Saha, S., Lozi, J.-P., Thomas, G., Lawall, J. L., and Muller, G. Hector: Detecting resource-release omission faults in error-handling code for systems software. In Dependable Systems and Networks (DSN), 2013 43rd Annual IEEE/IFIP International Conference on (2013), IEEE, pp. 1--12.
44. Schellhorn, G., Ernst, G., Pfahler, J., Haneberg, D., and Reif, W. Development of a verified Flash file system. In Proceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (Toulouse, France, June 2014), vol. 8477 of Lecture Notes in Computer Science, pp. 9--24.
45. Schierl, A., Schellhorn, G., Haneberg, D., and Reif, W. Abstract specification of the UBIFS file system for flash memory. In Proceedings of the Second World Congress on Formal Methods (FM) (Nov. 2009), vol. 5850 of Lecture Notes in Computer Science, pp. 190--206.
46. Sewell, T., Myreen, M., and Klein, G. Translation validation for a verified OS kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle, Washington, USA, June 2013), pp. 471--481.
47. Singaravelu, L., Pu, C., H\"artig, H., and Helmuth, C. Reducing TCB complexity for security-sensitive applications: Three case studies. In Proceedings of the 1st EuroSys Conference (Leuven, BE, Apr. 2006), pp. 161--174.
48. Tseng, H.-W., Grupp, L., and Swanson, S. Understanding the impact of power loss on flash memory. In Proceedings of the 48th Design Automation Conference (2011), ACM, pp. 35--40.
49. Wadler, P. Linear types can change the world! In Programming Concepts and Methods (1990).
50. Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., and Norrish, M. Mind the gap: A verification framework for low-level C. In International Conference on Theorem Proving in Higher Order Logics (Munich, Germany, Aug. 2009), pp. 500--515.
51. Yang, J., and Hawblitzel, C. Safe to the last instruction: automated verification of a type-safe operating system. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (Toronto, Ont, CA, June 2010), pp. 99--110.
52. Yang, J., Sar, C., and Engler, D. EXPLODE: a lightweight, general system for finding serious storage system errors. In USENIX Symposium on Operating Systems Design and Implementation (Nov. 2006), pp. 131--146.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification