论文标题
用于虚拟化用例的SEL4微粒：标准VMM的潜在方向
seL4 Microkernel for virtualization use-cases: Potential directions towards a standard VMM
论文作者
论文摘要
虚拟化在通过隔离执行环境为计算系统提供安全性方面起着至关重要的作用。已经提出了许多称为虚拟机程序的软件解决方案，以提供虚拟化功能。但是，与云中的服务器相比，只有少数用于部署在网络边缘，计算资源较少的设备中。在可以扮演Hybervisor角色的少数轻量级软件中，SEL4通过提供一个较小的值得信赖的计算基础和正式验证的组件来脱颖而出，从而提高了其安全性。尽管今天使用SEL4 Microkernel技术已经有十多年了，但其现有的Userland和工具仍然很少，而且不是很成熟。在过去的几年中，主要的努力是为了增加内核本身的成熟度，而不是可以托管的工具和应用程序的成熟度。因此，目前缺乏对全功能的Userland虚拟机监视器的适当支持，并且现有的机器非常分散。本文通过介绍我们所需的设计原理和功能集来讨论标准VMM的潜在方向。本文不打算定义标准VMM，我们打算通过SEL4社区来激发这一讨论。
Virtualization plays an essential role in providing security to computational systems by isolating execution environments. Many software solutions, called hypervisors, have been proposed to provide virtualization capabilities. However, only a few were designed for being deployed at the edge of the network, in devices with fewer computation resources when compared with servers in the Cloud. Among the few lightweight software that can play the hypervisor role, seL4 stands out by providing a small Trusted Computing Base and formally verified components, enhancing its security. Despite today being more than a decade with seL4 microkernel technology, its existing userland and tools are still scarce and not very mature. Over the last few years, the main effort has been put into increasing the maturity of the kernel itself and not the tools and applications that can be hosted on top. Therefore, it currently lacks proper support for a full-featured userland Virtual Machine Monitor, and the existing one is quite fragmented. This article discusses the potential directions to a standard VMM by presenting our view of design principles and feature set needed. This article does not intend to define a standard VMM, we intend to instigate this discussion through the seL4 community.
