What good is body armor when you have feet of clay? Lots of effort is going into operating system (OS) security, but the OS is increasingly being virtualized, and the hypervisor (virtual machine manager) is more vulnerable than an OS. That’s the basic premise of this paper, which makes its point by detailing many vulnerabilities in current hypervisors.

To address these weaknesses, the authors propose rebuilding hypervisors in safe languages, instead of in C. They define “safe” as type-safe and object-oriented with built-in verification techniques. Their implementation of this idea is called SafeHype, and they review its goals and underlying architecture in the paper. However, it’s still in its preliminary stages, so the paper is more concerned with stating a position than with documenting research results.

At six pages (including an extensive reference section), the paper is a short read. There are some awkward English moments, but compared to my Chinese, the writing is excellent. It’s thought-provoking and should interest the security and programming language communities in addition to the hypervisor community.

I am curious as to why Ada (“the most advanced language for safe and secure software,” http://www.adacore.com/adaanswers/about/ada-2012/) wasn’t mentioned in the authors’ survey of language candidates, especially considering its 2012 revisions and the ease of adoption by C programmers, but that issue is not important for this review. What is important is that the authors have identified a very real and glaring software weakness and the principles that will fix it. Implementers can choose whatever tools they want.