Authors
Ronghui Gu
Zhong Shao
Hao Chen
Newman Wu
Jieung Kim
Vilhelm Sjöberg
David Costanzo
Abstract
Complete formal verification of a non-trivial concurrent OS kernel is
widely considered a grand challenge. We present a novel compositional
approach for building certified concurrent OS kernels. Concurrency
allows interleaved execution of kernel/user modules across different
layers of abstraction. Each such layer can have a different set of
observable events. We insist on formally specifying these layers and
their observable events, and then verifying each kernel module at its
proper abstraction level. To support certified linking with other CPUs
or threads, we prove a strong contextual refinement property for every
kernel function, which states that the implementation of each such
function will behave like its specification under any kernel/user
context with any valid interleaving. We have successfully developed a
practical concurrent OS kernel and verified its (contextual)
functional correctness in Coq. Our certified kernel is written in
6500 lines of C and x86 assembly and runs on stock x86 multicore
machines. To our knowledge, this is the first proof of functional
correctness of a complete, general-purpose concurrent OS kernel with
fine-grained locking.
Published
In
Proc. 2016 USENIX Symposium on Operating Systems
Design and Implementation (OSDI'16), Savannah, GA,
pages 653-669, November 2016.