Trustworthy Systems

Refinement through restraint: Bringing down the cost of verification

Authors

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

UNSW

Data61
CSIRO

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.

BibTeX Entry

  @inproceedings{OConnor_CRALMNSK_16,
    address          = {Nara, Japan},
    author           = {O'Connor, Liam and Chen, Zilin and Rizkallah, Christine and Amani, Sidney and Lim, Japheth and
                        Murray, Toby and Nagashima, Yutaka and Sewell, Thomas and Klein, Gerwin},
    booktitle        = {International Conference on Functional Programming},
    keywords         = {verification; semantics; linear types; programming languages; file systems; isabelle/hol},
    month            = sep,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9425.pdf},
    title            = {Refinement Through Restraint: Bringing Down the Cost of Verification},
    year             = {2016}
  }

Download