Secure System Virtualization: End-to-End Verification of Memory Isolation
This work addresses security for embedded devices by providing strong isolation guarantees, though it is incremental in applying existing virtualization techniques with formal methods.
The thesis tackled the problem of ensuring memory isolation in secure system virtualization by building a provably secure separation kernel, resulting in a reduced trusted computing base and enabling formal verification of security guarantees.
Over the last years, security kernels have played a promising role in reshaping the landscape of platform security on today's ubiquitous embedded devices. Security kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms. They reduce the software portion of the system's trusted computing base to a thin layer, which enforces isolation between low- and high-criticality components. The reduced trusted computing base minimizes the system attack surface and facilitates the use of formal methods to ensure functional correctness and security of the kernel. In this thesis, we explore various aspects of building a provably secure separation kernel using virtualization technology. In particular, we examine techniques related to the appropriate management of the memory subsystem. Once these techniques were implemented and functionally verified, they provide reliable a foundation for application scenarios that require strong guarantees of isolation and facilitate formal reasoning about the system's overall security.