Authors
Hao Chen
Newman Wu
Zhong Shao
Joshua Lockerman
Ronghui Gu
Abstract
An operating system (OS) kernel forms the lowest level of any system
software stack. The correctness of the OS kernel is the basis for the
correctness of the entire system. Recent efforts have demonstrated the
feasibility of building formally verified general-purpose kernels, but
it is unclear how to extend their work to verify the functional
correctness of device drivers, due to the non-local effects of
interrupts. In this paper, we present a novel compositional framework
for building certified interruptible OS kernels with device drivers.
We provide a general device model that can be instantiated with
various hardware devices, and a realistic formal model of interrupts,
which can be used to reason about interruptible code. We have realized
this framework in the Coq proof assistant. To demonstrate the
effectiveness of our new approach, we have successfully extended an
existing verified non-interruptible kernel with our framework and
turned it into an interruptible kernel with verified device drivers.
To the best of our knowledge, this is the first verified interruptible
operating system with device drivers.
Published
In
Proc. 2016
ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI'16), Santa Barbara, CA,
pages 431-447, June 2016.
An extended version of this paper appeared in
Journal of Automated Reasoning (JAR), volume 61, issue 1-4, pages 141-189, June 2018.