The Science of Deep Specification

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

Day one: Overview and Certified Abstraction Layers

Material

Suggested homework

Homework: CAL dsss17 tutorial on Counter.v

Lecture recordings

Day two: Certified Layered Programming and mCertiKOS

Material

More examples & LayerLib (by Jeremie Koenig)
mCertiKOS

Suggested homework

Homework: CAL dsss17 tutorial on Stack.v and Container and Queue.

Lecture recordings

Day three: Information-Flow Security

Lecture recordings

Day four: Concurrent CertiKOS

Lecture recordings