Extensible specifications for automatic re-use of specifications and proofs

One way to reduce the cost of formally verifying a large 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. This simplifies reasoning and increases the property's robustness against later tweaks to the program's implementation. We introduce extensible specifications, a lightweight technique for constructing a specification that can be instantiated and reasoned about at multiple levels of abstraction. This avoids having to write and maintain a different specification for each property being proved whilst still allowing properties to be proved at the highest levels of abstraction. Importantly, properties proved of an extensible specification hold automatically for all instantiations of it, avoiding unnecessary proof duplication. We explain how we applied this idea in the context of verifying confidentiality enforcement for the seL4 microkernel, saving us significant proof and code duplication.