Advanced Development of Certified OS Kernels

Last modified: Fri Nov 5 18:41:12 2010 GMT.

Authors

Abstract

In this white paper, we propose a new synergistic effort that combines novel advances in programming languages, operating systems, and formal methods to develop a novel certified OS kernel. Our certified kernel will offer safe and application-specific extensibility, provable security properties with information flow control, and accountability and recovery from hardware or application failures. We advocate a modular certification framework for kernel components, which mirrors and enhances the modularity of the kernel itself. Using this framework, we aim to create not just a ``one-off'' lump of verified kernel code, but a statically and dynamically extensible kernel that can be incrementally built and extended with individual certified modules, each of which will provably preserve the kernel's overall safety and security properties. Our new kernel will provide certified guarantee about the soundness of its innate immunity mechanisms and solid support for new adaptive immunity mechanisms.

Published

Technical Report YALEU/DCS/TR-1436, Department of Computer Science, Yale University, July 15, 2010 [PDF]

An Overview Talk, November 2, 2010 [Powerpoint]

Supplementary Readings

Certified Software by Zhong Shao. To appear in CACM, December 2010.
Microkernels Meet Recursive Virtual Machines, by Bryan Ford, Mike Hibler, Jay Lepreau, Patrick Tullmann, Godmar Back, and Stephen Clawson. In OSDI'96, October 1996.
VeriML: Typed Computation of Logical Terms inside a Language with Effects by Antonis Stampoulis and Zhong Shao. In ICFP'10, September 2010.
Efficient System-Enforced Deterministic Paralllism, by Amittai Aviram, Shu-Chun Weng, Sen Hu, and Bryan Ford. In OSDI'10, October 2010.

colophon