The FLINT Project








CertiKOS: A Certified Kernel for Secure Cloud Computing

Last modified: Tue Oct 11 03:51:43 2011 GMT.


Liang Gu
Alexander Vaynberg
Bryan Ford
Zhong Shao
David Costanzo


Though attractive as a model for elastic on-demand service, cloud computing solutions based on existing hypervisors cannot guarantee that the provider will service a user's requests correctly, and will not leak sensitive information to unauthorized parties. We introduce CertiKOS (Certified Kit Operating System), a hypervisor architecture that leverages formal certification to ensure correctness and counter information leakage in cloud computing. CertiKOS isolates guest applications not only from each other but from provider-controlled resource management mechanisms. The kernel's API gives untrusted, provider-supplied management software control over allocation and delegation of resources such as memory and I/O devices, but prohibits management code from accessing a guest's memory or other resources while in use, or from interfering with a guest's execution except through clean resource revocation. CertiKOS represents an effort to apply recent advances in certified software design to a ground-up design of a modular and evolvable certified kernel. Through machine-checkable proof certificates and runtime monitoring, CertiKOS aims to offer users the assurance of correct and leak-free execution of their cloud services.


In Proc. 2nd ACM SIGOPS Asia-Pacific Workshop on Systems (APSys'11), Shanghai, China, July 2011. ©2011 ACM.

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