The December 2022 issue of IEEE Spectrum is here!

Close bar

SeKVM Makes Cloud Computing Provably Secure

Columbia University researchers have created a secure Linux-based hypervisor

3 min read
cloud computing code
ISTOCKPHOTO

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.

The Conversation (0)

Why Functional Programming Should Be the Future of Software Development

It’s hard to learn, but your code will produce fewer nasty surprises

11 min read
Vertical
A plate of spaghetti made from code
Shira Inbar
DarkBlue1

You’d expectthe longest and most costly phase in the lifecycle of a software product to be the initial development of the system, when all those great features are first imagined and then created. In fact, the hardest part comes later, during the maintenance phase. That’s when programmers pay the price for the shortcuts they took during development.

So why did they take shortcuts? Maybe they didn’t realize that they were cutting any corners. Only when their code was deployed and exercised by a lot of users did its hidden flaws come to light. And maybe the developers were rushed. Time-to-market pressures would almost guarantee that their software will contain more bugs than it would otherwise.

Keep Reading ↓Show less
{"imageShortcodeIds":["31996907"]}