Cogent: Verifying High-Assurance File System Implementations

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, Gernot Heiser

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationProceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems
Place of PublicationNew York, NY, USA
PublisherACM Association for Computing Machinery
Pages175–188
Number of pages14
ISBN (Print)9781450340915
DOIs
Publication statusPublished - 25 Mar 2016
Event21st International Conference on Architectural Support for Programming Languages and Operating Systems - Atlanta, United States
Duration: 2 Apr 20166 Apr 2016
http://www.ece.cmu.edu/calcm/asplos2016

Publication series

NameACM SIGPLAN Notices
PublisherACM
Number4
Volume51
ISSN (Print)0362-1340
ISSN (Electronic)1558-1160

Conference

Conference21st International Conference on Architectural Support for Programming Languages and Operating Systems
Abbreviated titleASPLOS 2016
Country/TerritoryUnited States
CityAtlanta
Period2/04/166/04/16
Internet address

Keywords

  • file systems
  • verification
  • domain-specific languages
  • isabelle/hol
  • co-generation

Fingerprint

Dive into the research topics of 'Cogent: Verifying High-Assurance File System Implementations'. Together they form a unique fingerprint.

Cite this