OGST/Jeremie Koenig
Advisor: Zhong Shao
Title: A module system for certified low-level code
Abstract: One way to ensure the reliability of software is formal verification:
the use of mechanized reasoning tools to ensure that a program satisfies some specification. Certified software is a particular form of software verification where the code is accompanied by an independently checkable “certificate”, which encodes a mathematical proof of this fact.
The FLINT team has been working on the verification of our hypervisor CertiKOS. To make this task tractable, we decompose the hypervisor into a series of abstraction layers. Each layer is able to use the services provided by the layer below, in order to implement the services required by the layer above. We have successfully completed an initial verification effort which uses the very general paradigm of abstract machines as layer interfaces and simulations as proofs of layer correctness. However, this paradigm is insufficient to capture the common patterns occurring at each layer, and offers only limited means of composition.
My talk will present the architecture of the CertiKOS proof, and discuss our ongoing attempt at addressing these limitations.