Séminaire des équipes de recherche
CompCertX: verified separate compilation for compositional verification of layered systems
- Date : 24/08/2015
- Place : Paris-Rocquencourt - Amphi Turing du bâtiment 1 - 10h30
- Guest(s) : Tahina Ramananandro
Joint work with Pr. Zhong Shao, Yale University, New Haven, CT, USA, and his valiant army of PhD students and postdocs.
Modern computer systems consist of a multitude of abstraction layers (e.g., OS kernels, hypervisors, device drivers, network protocols), each of which defines an interface that hides the implementation details of a particular set of functionality. Client programs built on top of each layer can be understood solely based on the interface, independent of the layer implementation. Despite their obvious importance, abstraction layers have mostly been treated as a system concept; they have almost never been formally specified or verified. This makes it difficult to establish strong correctness properties, and to scale program verification across multiple layers.
We have developed a new layer calculus showing how to formally specify, program, verify, and compose abstraction layers. Our layer calculus allows the compositional verification of layered systems based on contextual refinement of abstraction layers. We show how modules can be proven to be correct implementations of their corresponding abstraction layers. To carry on such correctness proofs, we present ClightX and AsmX, which we obtain by eXtending the formal semantics of CompCert Clight and x86 assembly languages with support for certified abstraction layers. Thanks to these languages, not only can we develop C or assembly layered systems, but we also handle separate compilation of certified ClightX modules and enable their linking with certified AsmX assembly modules; to this end, we present CompCertX, an adapted version of the CompCert verified whole-program compiler.
The work presented in this talk has allowed us to successfully develop and verify CertiKOS, a family of realistic operating systems and hypervisors, consisting of up to 37 abstraction layers, which took less than one person year to develop, and can boot a version of Linux as a guest.