| Autor: |
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 |
| Zdroj: |
ACM SIGOPS Operating Systems Review; January 2017, Vol. 50 Issue: 2 p175-188, 14p |
| Abstrakt: |
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. |
| Databáze: |
Supplemental Index |
| Externí odkaz: |
|
