# [2021-10-01] Prof. Shih-Wei Li, National Taiwan University, "A Secure and Formally Verified Commodity Multiprocessor Hypervisor"(English Speech) “Instead of building new fully verified system from scratch, modest changes to the existing commodity systems like the KVM hypervisor can make it possible to verify their security properties.” Using micro-verification, we made small changes to KVM and verify that the KVM implementation protects the confidentiality and integrity of VM data. To verify se-KVM, we introduced a novel layered hardware model that is simple enough to use for verify real software while accounting for realistic multiprocessor hardware features. We made modest changes to KVM such that the implementation can retains KVM’s overall commodity features and performance. Our work is the first machine-checked security and correctness proof for a commodity multiprocessor hypervisor. As cloud computing is becoming essential, there are future research opportunities for virtualization and security. There’s opportunities to apply micro-verification for proving various other security guarantees such as protecting against DoS Attack. Furthermore, there’s a trend of hardware-based security extension including Intel SGX, SCV and the confidential compute architecture CCA introduce by ARM this year in the Spring. There’s also opportunity to revisit software design to incorporate hardware-based protection. In addition, it currently still required substantial effort to formally verified commodity system like se-KVM. This effort can be reduced if there’s future programming language support that enables programming formally verified security software at the beginning. For the existing system like the X-Kernel, Raton, and Insecure language, there’s a change to use scalable approach to replace and rewrite components of existing software with formally verified or secure code. ## Note ### The note I write is totally summarized version of speaker with minor my opinion. The citation is described below. ## Citation ### Topic: A Secure and Formally Verified Commodity Multiprocessor Hypervisor ### Speaker: Prof. Shih-Wei Li