Authors
Zhong Shao
Bryan Ford
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.