Trustworthy Systems

Extensible specifications for automatic re-use of specifications and proofs

Authors

Daniel Matichuk and Toby Murray

NICTA

UNSW

Abstract

One way to reduce the cost of formally verifying a program is to perform proofs over a specification of its behaviour, which its implementation refines. However, interesting programs must often satisfy multiple properties. Ideally, each property should be proved against the most abstract specification for which it holds, to simplify reasoning and increase its robustness against later tweaks to the program's implementation.

In this short paper we introduce extensible specifications, a technique for writing specifications that allows properties to be proved at the highest levels of abstraction, while avoiding having to write and maintain a different specification for each property being proved. We explain how we applied this idea in the context of verifying confidentiality enforcement for the seL4 microkernel, saving us significant code and proof duplication.

BibTeX Entry

  @inproceedings{Matichuk_Murray_12,
    address          = {Thessaloniki, Greece},
    author           = {Matichuk, Daniel and Murray, Toby},
    booktitle        = {10th International Conference on Software Engineering and Formal Methods},
    keywords         = {formal verification re-use refinement sel4 extensible specifications},
    month            = dec,
    pages            = {8},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/5872.pdf},
    title            = {Extensible Specifications for Automatic Re-Use of Specifications and Proofs},
    year             = {2012}
  }

Download