Whenever we buy something from Aliexpress or Amazon, their customer data tends to be automatically updated and stored in thousands of virtual machines in the cloud. Due to its importance, for this type of company, guaranteeing the security and protection of the data of its millions of clients is characterized by being something as fundamental as it is essential. And the same goes for smaller companies and organizations.
However, until now there has been no way to guarantee that a certain software system is safe from vulnerabilities, computer attacks or, most simply, errors. But this could change in a short time, as Columbia Engineering researchers may have solved the safety-related problem.
Under the name of SeKVM , they have developed the first system that guarantees, through a mathematical proof, the security of virtual machines in the cloud . And the researchers are very optimistic in this regard, as they hope to lay the foundation for future innovations related to system software verification, leading to a new generation of cyber-resilient system software.
Formal verification is considered a critical step for cloud computing, since it consists of the process of proving that the software is mathematically correct, that there are no hidden security bugs to worry about, and that the program code it works as it should.
And SeKVM becomes the first verified system in this regard, since “it is the first time that a multiprocessor software system in the real world has been shown to be mathematically safe and correct”, so that “user data is managed correctly by software that runs in the cloud ”, and is safe from hackers and security bugs .
The exponential growth of cloud computing has offered the possibility that many companies (large and small) and users can move their data and computing off-site, to virtual machines that, originally, run on hosts present in the cloud. And in the case of Amazon, as a cloud computing provider, it implements hypervisors to support these types of virtual machines.
To verify the system, the scientists used MicroV, seen as a new framework for verifying the safety properties of large and extensive systems. This framework is based on the hypothesis that small changes in the system can make it much easier and simpler to verify (which experts now know under the name of micro-verification).
What is and what does a hypervisor consist of?
Under the name of hypervisor we are faced with a key piece of software, essential for cloud computing , since the security of your data depends to a large extent on its accuracy and reliability. But, although fundamental, they are also complicated, being able to include a complete Linux operating system. So a single weak link in the code, impossible to detect through classical tests, can make the system vulnerable to hackers.
What’s more, as computer security specialists point out, even if a hypervisor was spelled 99 percent correctly, a hacker might be able to sneak into that particular 1 percent configuration, taking control of the entire system. .
The work carried out by the researchers is the first to verify the widely used KVM hypervisor, as major cloud providers, such as Amazon, use it to run their virtual machines.
Thus, they were able to show that their KVM modified with a few small changes (and named SeKVM), is really safe and guarantees that virtual computers are isolated from each other .
There is no doubt that SeKVM could be able to change the way cloud services should be designed, developed and implemented, especially at a time when cybersecurity has become a constant and growing concern.
Reference: A Secure and Formally Verified Linux KVM Hypervisor, DOI: 10.1109 / SP40001.2021.00049
