Published papers, technical reports, and talks online.


Zhong Shao
Bryan Ford


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.


  • 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