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.
翻译:虚拟化在通过隔离执行环境为计算系统提供安全方面发挥着至关重要的作用。 许多软件解决方案,称为超视仪,被提议提供虚拟化能力。 然而,只有少数软件被设计为在网络边缘部署,与云中服务器相比,计算资源较少。在能够发挥超光速作用的为数不多的轻量软件中,SEL4通过提供一个小的受信任的计算机基地和正式核查的部件而显出突出的作用,加强了它的安全。尽管今天拥有SEL4微内核技术已有十多年,但现有的用户用地和工具仍然稀缺,而且并不十分成熟。在过去几年里,主要工作是提高内核本身的成熟度,而不是增加顶部可以容纳的工具和应用程序。因此,它目前缺乏适当的支持,能够发挥超高光速作用的用户域虚拟机监测器,而现有的监测器则十分支离破碎。这篇文章讨论了标准VMMM的潜在方向,展示了我们所需要的设计原则和特征。这篇文章不打算界定标准VMMM,我们打算通过SEL4社区推动这一讨论这一讨论。