An Open Framework for Foundational Proof-Carrying Code

Today's software systems often use many different computation features and span different abstraction levels (e.g., user code and runtime-system code). To build foundational certified systems, it is hard to have a single verification system supporting all computation features. In this paper we present an open framework for foundational proof-carrying code (FPCC). It allows program modules to be specified and certified separately using different type systems or program logics. Certified modules (i.e., code and proof) can be linked together to build fully certified systems. The framework supports modular verification and proof reuse. It is also expressive enough so that invariants established in specific verification systems are preserved even when they are embedded into our framework. Our work presents the first FPCC framework that systematically supports interoperation between different verification systems. It is fully mechanized in the Coq proof assistant with machine-checkable Soundness proof.