Advanced Development of Certified OS Kernels
Last modified: Fri Nov 5 18:41:12 2010 GMT.
AbstractIn 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.
Copyright © 1996-2023 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science