Abstraction and subsumption in modular verification of C programs

Abstract

The type-theoretic notions of existential abstraction, subtyping, subsumption, and intersec-tion have useful analogues in separation-logic proofs of imperative programs. We haveimplemented these as an enhancement of the verified software toolchain (VST). VST isan impredicative concurrent separation logic for the C language, implemented in the Coqproof assistant, and proved sound in Coq. For machine-checked functional-correctness veri-fication of software at scale, VST embeds its expressive program logic in dependently typedhigher-order logic (CiC). Specifications and proofs in the program logic can leverage theexpressiveness of CiC—so users can overcome the abstraction gaps that stand in the way oftop-to-bottom verification: gaps between source code verification, compilation, and domain-specific reasoning, and between different analysis techniques or formalisms. Until now, VSThas supported the specification of a program as a flat collection of function specifications (inhigher-order separation logic)—one proves that each function correctly implements its spec-ification, assuming the specifications of the functions it calls. But what if a function has morethan one specification? In this work, we exploit type-theoretic concepts to structure specifica-tion interfaces for C code. This brings modularity principles of modern software engineeringto concrete program verification. Previous work used representation predicates to enabledataabstractionin separation logic. We go further, introducingfunction-specification subsump-tionandintersection specificationsto organize the multiple specifications that a function istypically associated with. As in type theory, ifφis afunspec-subofψ,thatisφ<:ψ,thenx:φimpliesx:ψ, meaning that any function satisfying specificationφcan be usedwherever a function satisfyingψis demanded. Subsumption incorporates separation-logicframing and parameter adaptation, as well as step-indexing and specifications constructedvia mixed-variance functors (needed for C’s function pointers).