论文标题
安全系统虚拟化：内存隔离的端到端验证
Secure System Virtualization: End-to-End Verification of Memory Isolation
论文作者
论文摘要
在过去的几年中，安全核在重塑当今无处不在的嵌入式设备上的平台安全景观方面发挥了有希望的作用。安全内核，例如分离内核，可以构建高保证混合批判性执行平台。他们将系统可信度计算基础的软件部分减少到薄层，从而在低临界和高临界成分之间进行隔离。减少的可信计算基础最小化了系统攻击表面，并促进了使用正式方法来确保内核的功能正确性和安全性。 在本文中，我们探索了使用虚拟化技术构建可证明安全的分离内核的各个方面。特别是，我们检查了与内存子系统的适当管理有关的技术。一旦实施了这些技术并在功能上进行了验证，它们就为需要大力隔离的应用程序方案提供了可靠的基础，并促进了有关系统整体安全性的正式推理。
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.
