Whenever you buy something on Amazon, your customer data is automatically updated and stored on thousands of virtual machines in the cloud. For businesses like Amazon, ensuring the safety and security of the data of its millions of customers is essential. This is true for large and small organizations alike. But up to now, there has been no way to guarantee that a software system is secure from bugs, hackers, and vulnerabilities.

Columbia Engineering researchers may have solved this security issue. They have developed SeKVM, the first system that guarantees—through a mathematical proof—the security of virtual machines in the cloud. In a new paper to be presented on May 26, 2021, at the 42nd IEEE Symposium on Security & Privacy, the researchers hope to lay the foundation for future innovations in system software verification, leading to a new generation of cyber-resilient system software.

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.

“This is the first time that a real-world multiprocessor software system has been shown to be mathematically correct and secure,” said Jason Nieh, professor of computer science and co-director of the Software Systems Laboratory. “This means that users’ data are correctly managed by software running in the cloud and are safe from security bugs and hackers.”

The construction of correct and secure system software has been one of the grand challenges of computing. |Nieh has worked on different aspects of software systems since joining Columbia Engineering in 1999. When Ronghui Gu, the Tang Family Assistant Professor of Computer Science and an expert in formal verification, joined the computer science department in 2018, he and Nieh decided to…