Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, David Costanzo
Yale University

2nd ACM SIGOPS Asia-Pacific Workshop on Systems (APSys 2011),
July 11-12, 2011, Shanghai, China


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.

Paper: PDF

This research is sponsored in part by DARPA CRASH grant FA8750-10-2-0254 and NSF grants CNS-1017206, CNS-0915888, CNS-0910670, and CCF-0811665.