Trustworthy Systems

Cogent: verifying high-assurance file system implementations

Authors

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

NICTA

UNSW

Abstract

We present an approach to writing and formally verifying high-assurance file-system code in a restricted language called COGENT, supported y 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.

BibTeX Entry

  @inproceedings{Amani_HCRCOBNLSTKMKH_16,
    address          = {Atlanta, GA, USA},
    author           = {Amani, Sidney and Hixon, Alex and Chen, Zilin and Rizkallah, Christine and Chubb, Peter and
                        O'Connor, Liam and Beeren, Joel and Nagashima, Yutaka and Lim, Japheth and Sewell, Thomas and Tuong,
                        Joseph and Keller, Gabriele and Murray, Toby and Klein, Gerwin and Heiser, Gernot},
    booktitle        = {International Conference on Architectural Support for Programming Languages and Operating Systems},
    doi              = {10.1145/2872362.2872404},
    month            = apr,
    pages            = {175--188},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8956.pdf},
    title            = {{Cogent}: Verifying High-Assurance File System Implementations},
    year             = {2016}
  }

Download