随着嵌入式系统的应用越来越广泛,运用场景和需求时刻在变化,但是由于原有系统需要继续运行和维护,如果系统功能的增强继续沿用原有框架,就会导致平台的功能无法满足日益复杂的需求,且造成开发模式必须兼容原有平台而导致生产力低下的问题。在需求推动下,引入了嵌入式虚拟化平台,该平台的特点就是能够满足原有系统和功能稳定的前提下,引入新的硬件和系统,达到功能上的更新迭代。嵌入式虚拟化技术的特点是在同一个硬件平台上多个执行环境的并行执行,通常是嵌入式实时系统、裸机代码和Linux等复杂操作系统的混合。通过分区技术将执行环境进行隔离,使得系统之间独立运行,其中一个系统的崩溃不会导致其他系统发生故障。此外将微内核技术作为虚拟化平台底层,可以在完成虚拟化分区的前提下,减少内核组件的复杂度,提高内核的可信性。本论文围绕基于微内核的嵌入式虚拟化平台展开,对L4微内核技术和体系框架进行了介绍,提及了通过形式化验证的微内核seL4,针对选定的Fiasco微内核虚拟化平台进行了分析,涵盖了Fiasco内核的安全框架Capability和虚拟化系统环境L4Android及L4Linux,L4Android是为适配L4微内核虚拟化平台而对Android系统修改后的版本。然后引入了L4微内核的安全机制,解释了Capability机制的安全控制逻辑,并结合L4微内核的特点介绍了L4安全标准L4.sec。接着对系统的虚拟化移植进行了拓展,移植逻辑集中在如何适配微内核系统接口,达到与虚拟化管理器的协调,并使分区系统完成系统调用到IPC通信的转变。最后在现有安全机制的基础上进行了增强,针对L4当前Capability机制存在管理粒度较粗,且安全性和效率低下的问题,提出了自己的安全加固方案:分布式安全策略监视器和类型增强,该框架将安全判定节点从核心组件init拓展到所有子节点的父节点,达到了功能分解的目的,使得系统不存在热点问题,然后类型增强完成了能力的属性改造,使得在进行安全通信申请时,资源可以被进一步划分和定位,从而可以指定更加细粒度的访问规则。