seL4微内核架构的嵌入式虚拟化技术研究

Research on Embedded Virtualization Technology Based on seL4 Micro Kernel Architecture

随着嵌入式硬件技术水平的提升以及嵌入式应用的普及,用户对嵌入式系统可以提供的服务能力与质量水平提出了更高的要求。出于对成本和可靠性方面的考虑,开发者希望可以在同一硬件平台上同时运行多个互不影响的执行环境。本文提出了一种基于seL4微内核架构的嵌入式虚拟化技术,以Chcore微内核为基础,充分利用ARM硬件辅助虚拟化支持,设计并实现了基于能力调用机制的嵌入式虚拟机管理器。测试结果表明,该虚拟机管理器在处理器利用率、虚拟机调度、中断异常处理等方面性能良好,可以满足用户的常用应用需求。

With the improvement of embedded hardware technology and the popularity of embedded applications,users have higher requirements for the ability of service and quality level that embedded systems can provide.For the consideration of cost and reliability,developers hope to run multiple application environments,which do not affect each other on the same hardware platform.This paper proposes an embedded virtualization technology based on seL4 micro kernel architecture.Based on the Chcore micro kernel and making full use of ARM hardware assisted virtualization support.This embedded hypervisor based on capability mechanism is designed and implemented.The test results show that the hypervisor has good performance in processor utilization,virtual machine scheduling,interrupt exception handling and so on.And this hypervisor can meet the general application requirements of users.