DeepSpec Summer School, July 13-28, 2017
CertiKOS: Certified kit operating systems Zhong Shao
The CertiKOS project at Yale takes compositionality (especially "semantic compositionality") as the most important structuring principle for building large-scale certified system software. One key technology (pioneered by CertiKOS) is to decompose the specifications, the semantics, and the proofs of any large complex (software and hardware) system using the new language construct known as certified abstraction layers. These layers correspond to traditional notions of components, but they are certified, meaning that they come with formal deep specifications and certified implementation. They can be composed horizontally and vertically; and they can be compiled from one implementation language (e.g., C) into another (e.g., assembly). We use contextual refinement as a unifying mechanism to support certified linking and prove end-to-end functional correctness properties. We also use fully abstract deep specifications so security properties proved at higher abstraction levels can be propagated to the actual low-level implementation. In these lectures, we will show how to design and implement certified abstration layers in Coq and how to use them to build certified OS kernels.
Preparation
- Install Coq 8.6.
- Check out the github dsss17 files for dsss17/CAL . Follow the installation instruction in the CAL/tutorial/Tutorial.md file to make sure that all files compile and you can step through them in the IDE of your choice.
- Skim through the following research papers (and slides) on CertiKOS: