"Columbia Engineering Team Builds First Hacker-Resistant Cloud Software System"
Columbia Engineering researchers have developed SeKVM, the first formally verified system that guarantees the security of virtual machines in the cloud. Formal verification is a process that proves the mathematical correctness of software, correct functionality of the program's code, and the absence of hidden security bugs. According to Jason Nieh, a Professor of Computer Science and Co-Director of the Software Systems Laboratory at Columbia University, this is the first time that a real-world multiprocessor software system has been proven to be mathematically correct. This will ensure that the software running in the cloud manages user data correctly, and that the data is protected from security bugs and hackers. The significant advancement of cloud computing has allowed companies and users to move their data and computation off-site into virtual machines in the cloud. Cloud computing providers use hypervisors to support these virtual machines. Hypervisors make cloud computing possible. The security of data stored on a virtual machine depends on the correctness and trustworthiness of the hypervisor. Even if a hypervisor is written 99 percent correctly, just one weak link can allow a hacker to take over a system. The researchers' work is the first to verify a commodity system, specifically the KVM hypervisor used by cloud providers such as Amazon to run virtual machines. They proved that SeKVM could guarantee that virtual computers are isolated. MicroV is a new framework for verifying the security properties of large systems, which was used to verify SeKVM. This hacker-resistant cloud software system is expected to change how cloud services are designed, developed, deployed, and trusted. This article continues to discuss the development and applications of SeKVM.