TY - JOUR
T1 - Abstraction and subsumption in modular verification of C programs
AU - Beringer, Lennart
AU - Appel, Andrew W.
N1 - Funding Information:
This work was funded by the National Science Foundation under the awards 1005849 (Verified High Performance Data Structure Implementations, Beringer) and 1521602 Expedition in Computing: The Science of Deep Specification, Appel).
Publisher Copyright:
© 2021, Springer Science+Business Media, LLC, part of Springer Nature.
PY - 2021/10
Y1 - 2021/10
N2 - The type-theoretic notions of existential abstraction, subtyping, subsumption, and intersection have useful analogues in separation-logic proofs of imperative programs. We have implemented these as an enhancement of the verified software toolchain (VST). VST is an impredicative concurrent separation logic for the C language, implemented in the Coq proof assistant, and proved sound in Coq. For machine-checked functional-correctness verification of software at scale, VST embeds its expressive program logic in dependently typed higher-order logic (CiC). Specifications and proofs in the program logic can leverage the expressiveness of CiC—so users can overcome the abstraction gaps that stand in the way of top-to-bottom verification: gaps between source code verification, compilation, and domain-specific reasoning, and between different analysis techniques or formalisms. Until now, VST has supported the specification of a program as a flat collection of function specifications (in higher-order separation logic)—one proves that each function correctly implements its specification, assuming the specifications of the functions it calls. But what if a function has more than one specification? In this work, we exploit type-theoretic concepts to structure specification interfaces for C code. This brings modularity principles of modern software engineering to concrete program verification. Previous work used representation predicates to enable data abstraction in separation logic. We go further, introducing function-specification subsumption and intersection specifications to organize the multiple specifications that a function is typically associated with. As in type theory, if ϕ is a [InlineMediaObject not available: see fulltext.] of ψ, that is ϕ< : ψ, then x: ϕ implies x: ψ, meaning that any function satisfying specification ϕ can be used wherever a function satisfying ψ is demanded. Subsumption incorporates separation-logic framing and parameter adaptation, as well as step-indexing and specifications constructed via mixed-variance functors (needed for C’s function pointers).
AB - The type-theoretic notions of existential abstraction, subtyping, subsumption, and intersection have useful analogues in separation-logic proofs of imperative programs. We have implemented these as an enhancement of the verified software toolchain (VST). VST is an impredicative concurrent separation logic for the C language, implemented in the Coq proof assistant, and proved sound in Coq. For machine-checked functional-correctness verification of software at scale, VST embeds its expressive program logic in dependently typed higher-order logic (CiC). Specifications and proofs in the program logic can leverage the expressiveness of CiC—so users can overcome the abstraction gaps that stand in the way of top-to-bottom verification: gaps between source code verification, compilation, and domain-specific reasoning, and between different analysis techniques or formalisms. Until now, VST has supported the specification of a program as a flat collection of function specifications (in higher-order separation logic)—one proves that each function correctly implements its specification, assuming the specifications of the functions it calls. But what if a function has more than one specification? In this work, we exploit type-theoretic concepts to structure specification interfaces for C code. This brings modularity principles of modern software engineering to concrete program verification. Previous work used representation predicates to enable data abstraction in separation logic. We go further, introducing function-specification subsumption and intersection specifications to organize the multiple specifications that a function is typically associated with. As in type theory, if ϕ is a [InlineMediaObject not available: see fulltext.] of ψ, that is ϕ< : ψ, then x: ϕ implies x: ψ, meaning that any function satisfying specification ϕ can be used wherever a function satisfying ψ is demanded. Subsumption incorporates separation-logic framing and parameter adaptation, as well as step-indexing and specifications constructed via mixed-variance functors (needed for C’s function pointers).
KW - Foundational program verification
KW - Intersection specifications
KW - Separation logics
KW - Specification subsumption
UR - http://www.scopus.com/inward/record.url?scp=85103184385&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85103184385&partnerID=8YFLogxK
U2 - 10.1007/s10703-020-00353-1
DO - 10.1007/s10703-020-00353-1
M3 - Article
AN - SCOPUS:85103184385
SN - 0925-9856
VL - 58
SP - 322
EP - 345
JO - Formal Methods in System Design
JF - Formal Methods in System Design
IS - 1-2
ER -