SeKVM Makes Cloud Computing Provably Secure
Complex hypervisor software helps run cloud computers, but verifying its security is often thought to be nigh impossible. Now computer scientists at Columbia University have developed what they say is the first hypervisor that can guarantee secure cloud computing.
Hypervisors organize cloud servers into virtual machines to supply data and computing power over the Internet. Hacks that successfully exploit hypervisor vulnerabilities could gain unfettered access to the data of millions of customers of cloud computing providers such as Amazon.
"All it takes is a single weak link in the code - one that is virtually impossible to detect via traditional testing - to leave a system vulnerable to hackers," says Ronghui Gu, a computer scientist at Columbia University's School of Engineering and Applied Science and co-author on the researchers' published study about the work.
In theory, scientists can formally verify software to mathematically prove that its code "protects data security under 100% of circumstances," Gu says. However, most verified hypervisors are often far simpler than their commercial counterparts, since they are specifically designed for verification instead of practical applications. In contrast, modern commercial hypervisors are huge pieces of software, often including an entire operating system kernel, which can make verifying them a seemingly insurmountable task.
For example, it took three person-years to verify 6,500 lines of code with the CertiKOS hypervisor and 10 person-years to verify 9,000 lines of code with the seL4 hypervisor, both of which were designed for verification. In comparison, the widely used KVM open-source hypervisor, a full-featured multi-processor system integrated with Linux, has more than 2 million lines of code.
Now the Columbia computer scientists have developed a way to verify commercial-grade hypervisors. They used their new technique to develop a secure version of KVM named SeKVM, which they suggest is the first machine-checked formally verified commercial-grade hypervisor.
The researchers dubbed their new technique microverification, which reduces the amount of work needed to verify a hypervisor. It breaks down a hypervisor into a small core and a set of untrusted services, and then goes on to prove the hypervisor secure by verifying the core alone. The core has no vulnerabilities for a hack to exploit, and this core mediates all the hypervisor's interactions with virtual machines, so even if a hack undermines one virtual machine, it does not compromise the others.
Based on microverification, the scientists developed software named MicroV to verify large commercial-grade multi-processor hypervisors. With the help of MicroV, they developed a secure core for SeKVM only 3,800 lines of code long, which they verified over the course of two person-years.
When it comes to real application workloads, SeKVM performed similarly to unmodified KVM, at most incurring less than 10% performance overhead on native hardware KVM was specifically designed to run on. At the same time, SeKVM supported KVM's wide range of features.
"SeKVM is just KVM with some minor changes," says study co-author Jason Nieh, a computer scientist at Columbia University's School of Engineering and Applied Science. "It performs like regular KVM, inherits the functionality of regular KVM, but on top of that, provides security guarantees that regular KVM does not have."
In the future, "we will keep exploring this concept of cyber-resilient systems software and build safeguards in various domains, from banking systems and Internet of Things devices to autonomous vehicles and cryptocurrencies," Gu says. "SeKVM will lay a foundation for future innovations in systems verification and lead to a new generation of cyber-resilient systems software. In a world where cybersecurity is a growing concern, this resiliency is in high demand."
The scientists detailed their findings May 26 at the IEEE Symposium on Security & Privacy.