Refinement through restraint: bringing down the cost of verification

Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein

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

Abstract

We present a framework aimed at significantly reducing the cost of verifying certain classes of systems software, such as file systems. Our framework allows for equational reasoning about systems code written in our new language, Cogent. Cogent is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. Linear types allow us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. As Cogent is a restricted language, it is designed to easily interoperate with existing C functions and to connect to existing C verification frameworks. Our framework is based on certifying compilation: For a well-typed Cogent program, our compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.
Original languageEnglish
Title of host publicationProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
EditorsMatthew Fluet
Place of PublicationNew York, NY, USA
PublisherACM Association for Computing Machinery
Pages89–102
Number of pages14
ISBN (Print)9781450342193
DOIs
Publication statusPublished - 4 Sep 2016
Event21st ACM SIGPLAN International Conference on Functional Programming - Nara, Japan
Duration: 18 Sep 201624 Sep 2016
https://conf.researchr.org/home/icfp-2016

Publication series

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

Conference

Conference21st ACM SIGPLAN International Conference on Functional Programming
Abbreviated titleICFP 2016
CountryJapan
CityNara
Period18/09/1624/09/16
Internet address

Keywords

  • linear types
  • Isabelle/HOL
  • programming languages
  • semantics
  • file systems
  • verification

Fingerprint Dive into the research topics of 'Refinement through restraint: bringing down the cost of verification'. Together they form a unique fingerprint.

Cite this