New hacker-resistant system could change how cloud services are designed, deployed

As the first formally verified system for cloud computing, SeKVM could transform the way cloud services are designed, developed, deployed, and trusted.

A team of researchers at Columbia Engineering have developed SeKVM, the first system to guarantee the security of virtual machines (VMs) in the cloud, that the researchers hope will lead to a new generation of the cyber-resilient system software in a world where cybersecurity is a growing concern.

As the first formally verified system for cloud computing, SeKVM could transform the way cloud services are designed, developed, deployed, and trusted. Formal verification is the process of proving that:

• the software is mathematically correct
• the program's code works as it should
• there are no hidden security bugs to worry about

Major cloud providers like Amazon deploy hypervisor(s), a crucial piece of software that makes cloud computing possible, to support the virtual machines in the cloud and the security of a VM's data hinges on the correctness and trustworthiness of the hypervisor.

Modern hypervisors are complex and just a single weak link in the code can make a system vulnerable to hackers. Bad actors can exploit these vulnerabilities to take control of the VMs and compromise their confidentiality and integrity.

Jason Nieh, professor of computer science and co-director of the Software Systems Laboratory, and Ronghui Gu, the Tang Family Assistant Professor of Computer Science and an expert in formal verification, proved that SeKVM - KVM with some small change - is secure and guarantees that virtual machines are isolated from one another.

"Verifying a multiprocessor commodity system, a system in wide use like Linux, has been thought to be more or less impossible," said Gu.

The researchers used MicroV, a novel framework to verify the security properties of large systems, to verify SeKVM. They demonstrated that if the small core of the larger system is intact, then the system is secure and no private data will be leaked.

"We've shown that our system can protect and secure private data and computing uploaded to the cloud with mathematical guarantees. This has never been done before," said Xupeng Li, Gu's PhD student and co-lead author of the paper.

The study will be presented at the 42nd IEEE Symposium on Security & Privacy on May 26, 2021. For more details, read Columbia Engineering's official news release.