Home - Topics - Publications - Blog - CV - Photos - Funny

Advanced Development of Certified OS Kernels

Zhong Shao and Bryan Ford
Department of Computer Science, Yale University

Yale University Technical Report TR1436
July 15, 2010


Operating System (OS) kernels form the bedrock of all system software—they can have the greatest impact on the resilience, extensibility, and security of today’s computing hosts. A single kernel bug can easily wreck the entire system’s integrity and protection. We propose to apply new advances in certified software to the development of a novel 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.

Our certified kernel builds on proof-carrying code concepts, where a binary executable includes a rigorous machine-checkable proof that the software is free of bugs with respect to specific requirements. Unlike traditional verification systems, our certified software approach uses an expressive general-purpose meta-logic and machine-checkable proofs to support modular reasoning about sophisticated invariants. The rich meta-logic enables us to verify all kinds of low-level assembly and C code and to establish dependability claims ranging from simple safety properties to advanced security, correctness, and liveness properties.

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. In place of the rigid safety conditions used in traditional extension mechanisms (e.g., that kernel extensions must be type-safe), our approach will assure both the safety and semantic correctness of extensions with respect to appropriate specifications (e.g., that a file system extension behaves like a file system). Our certified kernel will use this flexibility, for example, to provide accountability and recovery mechanisms, formally guaranteeing that whenever an application fails, the system can always be rolled back to an earlier, consistent state. Our certified kernel will also provide information flow control not only enforcing policies on user applications, but also guaranteeing that the security monitor itself and other kernel modules manipulate all security labels correctly.

Paper: PDF

Topics: Operating Systems Security Modularity Formal Verification Reliability and Robustness Bryan Ford