ABSTRACT
We present a framework aimed at significantly reducing the cost of verifying certain classes of systems software, such as file systems. Our framework allows for equational reasoning about systems code written in our new language, Cogent. Cogent is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. Linear types allow us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. As Cogent is a restricted language, it is designed to easily interoperate with existing C functions and to connect to existing C verification frameworks. Our framework is based on certifying compilation: For a well-typed Cogent program, our compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.
- Amal Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. In Proceedings of the 10th International Conference on Functional Programming, pages 78–91, 2005. Google ScholarDigital Library
- Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. Cogent: Verifying high-assurance file system implementations. In International Conference on Architectural Support for Programming Languages and Operating Systems, pages 175–188, Atlanta, GA, USA, April 2016. Google ScholarDigital Library
- Erik Barendsen and Sjaak Smetsers. Conventional and uniqueness typing in graph rewrite systems. In Foundations of Software Technology and Theoretical Computer Science, volume 761 of Lecture Notes in Computer Science, pages 41–51, 1993. Google ScholarDigital Library
- Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. Verified correctness and security of OpenSSL HMAC. In Proceedings of the 24th USENIX Security Symposium, pages 207–221, Washington, DC, US, August 2015. Google ScholarDigital Library
- Arthur Charguéraud. Program verification through characteristic formulae. In Proceedings of the 15th International Conference on Functional Programming, ICFP ’10, pages 321–332, New York, NY, USA, 2010. Google ScholarDigital Library
- Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In Proceedings of the 16th International Conference on Functional Programming, ICFP ’11, pages 418–430, New York, NY, USA, 2011. Google ScholarDigital Library
- 2034828.Google Scholar
- Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using Crash Hoare logic for certifying the FSCQ file system. In ACM Symposium on Operating Systems Principles, pages 18–37, Monterey, CA, October 2015. Google ScholarDigital Library
- Adam Chlipala. An optimizing compiler for a purely functional webapplication language. In Proceedings of the 20th International Conference on Functional Programming, ICFP 2015, pages 10–21, New York, NY, USA, 2015. Google ScholarDigital Library
- 2784741.Google Scholar
- David Cock, Gerwin Klein, and Thomas Sewell. Secure microkernels, state monads and scalable refinement. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, pages 167–182, Montreal, Canada, August 2008. Google ScholarDigital Library
- Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’01, pages 59–69, New York, NY, USA, 2001. Google ScholarDigital Library
- Edsger Wybe Dijkstra. A Discipline of Programming. Upper Saddle River, NJ, USA, 1st edition, 1997. Google ScholarDigital Library
- Rob Ennals, Richard Sharp, and Alan Mycroft. Linear types for packet processing. In Proceedings of the 13th European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, pages 204–218, 2004.Google ScholarCross Ref
- Manuel Fahndrich and Robert DeLine. Adoption and focus: Practical linear types for imperative programming. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’02, pages 13–24, New York, NY, USA, 2002. Google ScholarDigital Library
- Filebench Project. Filebench file system benchmark. http:// sourceforge.net/projects/filebench. Accessed Nov 2015.Google Scholar
- Go. The Go programming language. https://go.googlesource.com/ go, 2015. Accessed Nov 2015.Google Scholar
- David Greenaway, June Andronick, and Gerwin Klein. Bridging the gap: Automatic verified abstraction of C. In International Conference on Interactive Theorem Proving, pages 99–115, Princeton, New Jersey, USA, August 2012.Google ScholarCross Ref
- David Greenaway, Japheth Lim, June Andronick, and Gerwin Klein. Don’t sweat the small stu ff: Formal verification of C code without the pain. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 429–439, Edinburgh, UK, June 2014. Google ScholarDigital Library
- Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 595–608, 2015. Google ScholarDigital Library
- HASP project. The Habit programming language: The revised preliminary report. Technical Report http://hasp.cs.pdx.edu/habitreport-Nov2010.pdf, Department of Computer Science, Portland State University, Portland, OR, USA, November 2010.Google Scholar
- Martin Hofmann. A type system for bounded space and functional in-place update–extended abstract. In ESOP, volume 1782 of Lecture Notes in Computer Science, pages 165–179, 2000. Google ScholarDigital Library
- IOZone. IOzone filesystem benchmark. http://www.iozone.org/. Accessed Mar 2015.Google Scholar
- Gabriele Keller, Toby Murray, Sidney Amani, Liam O’Connor-Davis, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, and Gernot Heiser. File systems deserve verification too! In Workshop on Programming Languages and Operating Systems (PLOS), pages 1–7, Farmington, Pennsylvania, USA, November 2013. Google ScholarDigital Library
- Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In ACM Symposium on Operating Systems Principles, pages 207–220, Big Sky, MT, USA, October 2009. Google ScholarDigital Library
- Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):2:1–2:70, February 2014. Google ScholarDigital Library
- Ramana Kumar, Magnus Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179–191, San Diego, January 2014. Google ScholarDigital Library
- Xavier Leroy. 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, pages 42–54, Charleston, SC, USA, 2006. Google ScholarDigital Library
- Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009. Google ScholarDigital Library
- LLVM. The Low-Level Virtual Machine Compiler. Accessed Feb 2016.Google Scholar
- Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. Lightweight Linear Types in System F ◦. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI ’10, pages 77–88, New York, NY, USA, 2010. Google ScholarDigital Library
- Andrew McCreight, Tim Chevalier, and Andrew Tolmach. A certified framework for compiling and executing garbage-collected languages. In Proceedings of the 15th International Conference on Functional Programming, pages 273–284, 2010. Google ScholarDigital Library
- Mirabox. MiraBox development kit. https://www. globalscaletechnologies.com/p-58-mirabox-developmentkit.aspx, 2015. Accessed Nov 2015.Google Scholar
- Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. Pilsner: A compositionally verified compiler for a higher-order imperative language. In Proceedings of the 20th International Conference on Functional Programming, ICFP ’15, pages 166–178, New York, NY, USA, 2015. Google ScholarDigital Library
- Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle /HOL. 2014. Google ScholarDigital Library
- Martin Odersky. Observers for linear types. In ESOP ’92: 4th European Symposium on Programming, Rennes, France, Proceedings, pages 390– 407, February 1992. Lecture Notes in Computer Science 582. Nicolas Palix, Ga¨el Thomas, Suman Saha, Christophe Calvès, Julia Lawall, and Gilles Muller. Faults in Linux: ten years later. In Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 305–318, Newport Beach, CA, US, 2011. Google ScholarDigital Library
- Benjamin C. Pierce. Types and Programming Languages. 2002. Google ScholarDigital Library
- Lee Pike, Patrick Hickey, James Bielman, Trevor Elliott, Thomas DuBuisson, and John Launchbury. Programming languages for high-assurance autonomous vehicles: Extended abstract. In Proceedings of the 2014ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, pages 1–2, San Diego, California, USA, 2014. Google ScholarDigital Library
- Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O’Connor, Toby Murray, Gabriele Keller, and Gerwin Klein. A framework for the automatic formal verification of refinement from cogent to c. In International Conference on Interactive Theorem Proving, Nancy, France, August 2016.Google ScholarCross Ref
- Rust. The Rust programming language. http://rustlang.org, 2014.Google Scholar
- Accessed March 2015.Google Scholar
- Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. SIGPLAN Lisp Pointers, V(1):288–298, January 1992. Google ScholarDigital Library
- Norbert Schirmer. Verification of Sequential Imperative Programs in Isabelle /HOL. PhD thesis, Technische Universität München, 2006.Google Scholar
- Thomas Sewell, Magnus Myreen, and Gerwin Klein. Translation validation for a verified OS kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 471–481, Seattle, Washington, USA, June 2013. Google ScholarDigital Library
- Harvey Tuch, Gerwin Klein, and Michael Norrish. Types, bytes, and separation logic. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 97–108, Nice, France, January 2007. Google ScholarDigital Library
- Philip Wadler. Linear types can change the world! In Programming Concepts and Methods, 1990.Google Scholar
Index Terms
- Refinement through restraint: bringing down the cost of verification
Recommendations
Cogent: Verifying High-Assurance File System Implementations
ASPLOS '16: Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating SystemsWe 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 ...
Refinement through restraint: bringing down the cost of verification
ICFP '16We present a framework aimed at significantly reducing the cost of verifying certain classes of systems software, such as file systems. Our framework allows for equational reasoning about systems code written in our new language, Cogent. Cogent is a ...
Cogent: Verifying High-Assurance File System Implementations
ASPLOS '16We 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 ...
Comments