Whenever you buy something online, your customer data is automatically updated and stored on thousands of virtual machines in the cloud. But up to now, there has been no way to guarantee that a software system is secure from bugs, hackers, and vulnerabilities. Now, researchers have developed SeKVM, the first system that guarantees — through a mathematical proof — the security of virtual machines in the cloud.
SeKVM is the first formally verified system for cloud computing. Formal verification is a critical step as it is the process of proving that software is mathematically correct, that the program's code works as it should, and there are no hidden security bugs to worry about.
The SeKVM real-world multiprocessor software system has been shown to be mathematically correct and secure, meaning that users’ data are correctly managed by software running in the cloud and are safe from security bugs and hackers.
Over the past dozen years, there has been a good deal of attention paid to formal verification including work on verifying multiprocessor operating systems. Verifying a multiprocessor commodity system — a system in wide use such as Linux — has been thought to be more or less impossible.
The exponential growth of cloud computing has enabled companies and users to move their data and computation off-site into virtual machines running on hosts in the cloud. Cloud computing providers deploy hypervisors to support these virtual machines. A hypervisor is the key piece of software that makes cloud computing possible. The security of the virtual machine's data hinges on the correctness and trustworthiness of the hypervisor.
Despite their importance, hypervisors are complicated — they can include an entire Linux operating system. Just a single weak link in the code — one that is virtually impossible to detect via traditional testing — can make a system vulnerable to hackers. Even if a hypervisor is written 99 percent correctly, a hacker can still sneak into that 1 percent setup and take control of the system.
SeKVM, which is the KVM hypervisor with some small changes, is secure and guarantees that virtual computers are isolated from one another. SeKVM was verified using MicroV, a new framework for verifying the security properties of large systems. It is based on the hypothesis that small changes to the system can make it significantly easier to verify — a new technique called microverification. This novel layering technique retrofits an existing system and extracts the components that enforce security into a small core that is verified and guarantees the security of the entire system.
The changes needed to retrofit a large system are quite modest — the researchers demonstrated that if the small core of the larger system is intact, then the system is secure and no private data will be leaked.