Trustworthy Systems

Program verification in the presence of I/O: semantics, verified library routines, and verified applications

Authors

Hugo Feree, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus Myreen and Son Ho

University of Kent

DATA61

École Polytechnique

Chalmers University of Technology

UNSW Sydney

Abstract

Software verification tools that build machine-checked proofs of functional correctness usually focus on the algorithmic content of the code. Their proofs are not grounded in a formal semantic model of the environment that the program runs in, or the program’s interaction with that environment. As a result, several layers of translation and wrapper code must be trusted. In contrast, the CakeML project focuses on end-to-end verification to replace this trusted code with verified code in a cost-effective manner. In this paper, we present infrastructure for developing and verifying impure functional programs with I/O and imperative file handling. Specifically, we extend CakeML with a low-level model of file I/O, and verify a high-level file I/O library in terms of the model. We use this library to develop and verify several Unix-style command-line utilities: cat, sort, grep, diff and patch. The workflow we present is built around the HOL4 theorem prover, and therefore all our results have machine-checked proofs.

BibTeX Entry

  @inproceedings{Feree_AKOMH_18,
    address          = {Oxford, UK},
    author           = {Feree, Hugo and {\AA}man Pohjola, Johannes and Kumar, Ramana and Owens, Scott and Myreen, Magnus and
                        Ho, Son},
    booktitle        = {Verified Software: Theories, Tools and Experiments},
    date             = {2018-11-24},
    month            = nov,
    pages            = {88-111},
    paperurl         = {https://trustworthy.systems/publications/full_text/Feree_AKOMH_18.pdf},
    publisher        = {Springer},
    title            = {Program Verification in the Presence of {I}/{O}: Semantics, verified library routines, and verified
                        applications},
    volume           = {11294},
    year             = {2018}
  }

Download