Skip to main content

TS

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,
    doi              = {10.1145/2872362.2872404},
    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},
    month            = apr,
    year             = {2016},
    title            = {{Cogent}: Verifying High-Assurance File System Implementations},
    booktitle        = {International Conference on Architectural Support for Programming Languages and Operating Systems},
    pages            = {175-188},
    address          = {Atlanta, GA, USA}
  }

Download

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.