The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Advanced Development of Certified OS Kernels

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

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


Copyright © 1996-2017 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon