Cogent: Verifying High-Assurance File System Implementations

Select |




Print


Amani, Sidney; Hixon, Alex; Chen, Zilin; Rizkallah, Christine; Chubb, Peter; O'Connor, Liam; Beeren, Joel; Nagashima, Yutaka; Lim, Japheth; Sewell, Thomas; Tuong, Joseph; Keller, Gabriele; Murray, Toby; Klein, Gerwin; Heiser, Gernot

Amani, Sidney; Hixon, Alex; Chen, Zilin; Rizkallah, Christine; Chubb, Peter; O'Connor, Liam; Beeren, Joel; Nagashima, Yutaka; Lim, Japheth; Sewell, Thomas; Tuong, Joseph; Keller, Gabriele; Murray, Toby; Klein, Gerwin; Heiser, Gernot


2016-04-02


Conference Material


Architectural Support for Programming Languages and Operating Systems


Atlanta, GA, USA


175-188


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.


Data61


English


nicta:8956


Amani, Sidney; Hixon, Alex; Chen, Zilin; Rizkallah, Christine; Chubb, Peter; O'Connor, Liam; Beeren, Joel; Nagashima, Yutaka; Lim, Japheth; Sewell, Thomas; Tuong, Joseph; Keller, Gabriele; Murray, Toby; Klein, Gerwin; Heiser, Gernot. Cogent: Verifying High-Assurance File System Implementations. In: Architectural Support for Programming Languages and Operating Systems; Atlanta, GA, USA. 2016-04-02. 175-188.



Loading citation data...

Citation counts
(Requires subscription to view)