Thu 16 Jun 2016 16:00 - 16:30 at Grand Ballroom Santa Ynez - Verifying Systems Chair(s): Santosh Nagarakatte

Operating system kernel forms the lowest level of the system software stack. 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 interrupible OS kernel 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.

Thu 16 Jun

pldi-2016-papers
15:30 - 17:00: Research Papers - Verifying Systems at Grand Ballroom Santa Ynez
Chair(s): Santosh NagarakatteRutgers University
pldi-2016-papers15:30 - 16:00
Talk
Rian ShambaughUniversity of Massachusetts Amherst, Aaron WeissUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts, Amherst
Pre-print Media Attached
pldi-2016-papers16:00 - 16:30
Talk
Hao ChenYale University, Xiongnan (Newman) WuYale University, Zhong ShaoYale University, Joshua LockermanYale University, Ronghui GuYale University
Pre-print Media Attached
pldi-2016-papers16:30 - 17:00
Talk
Eric MullenUniversity of Washington, Daryl ZunigaUniversity of Washington, Zachary TatlockUniversity of Washington, Dan GrossmanUniversity of Washington, USA
Pre-print Media Attached