Authors
Liang Gu
Alexander Vaynberg
Bryan Ford
Zhong Shao
David Costanzo
Abstract
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.
Published
In
Proc. 2nd ACM SIGOPS Asia-Pacific Workshop on Systems
(APSys'11), Shanghai, China,
July 2011. ©2011 ACM.