Advanced Development of Certified OS Kernels

Abstract:

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