随着无人机在军事领域及民用领域中的广泛应用,其面临的安全问题也日益受到研究人员的重视。经过形式化验证的操作系统内核虽然能够保证无人机系统的安全性,但是其缺乏扩展性,无法提供一个丰富的软件开发环境用以开发第三方应用。如何在保证操作系统内核正确性的同时,提高整个无人机系统的扩展性是一个值得深入研究的问题。本论文提出了一种层级式的软件架构,这种架构在保证无人机安全性的同时,利用虚拟化技术来提高整个系统的扩展性。该软件架构主要包括三个部分:系统内核、用户空间以及虚拟机。在系统内核部分采用了可信操作系统内核CertiKOSARM,在用户空间部分运行了多个实时用户进程用于飞行姿态控制,虚拟机部分负责驱动Linux系统内核来运行第三方应用。论文为经过形式化验证的操作系统内核CertiKOS-ARM添加了内核中断功能以及多核并发处理功能。内核中断功能有效降低了时钟中断延迟,而多核并发处理功能则保证了核心之间的安全隔离。为实现创建与管理虚拟机,论文设计了一个轻量化的虚拟机管理软件Hypervisor,称为CertiKOS-ARM Hypervisor。CertiKOS-ARM Hypervisor采用了新型的mixed-type架构,能够利用硬件辅助的方式减少虚拟化技术带来的额外花销。CertiKOS-ARM Hypervisor具有轻量化与层级式的特点。轻量化设计使得其代码行数比其他商业化的Hypervisor少一个量级,有效减少了系统的可信计算基。层级式设计使得其代码被划分成多个软件层,这种软件层的划分方式能够适用于ARM与x86两种平台。论文实验部分包括Hypervisor的性能测试实验与无人机飞行测试实验。论文利用了微型测试工具集LMbench对CertiKOS-ARM Hyperviosr进行了性能测试,实验结果表明CertiKOS-ARM Hpervisor创建的虚拟机性能与实际机器性能相当。无人机飞行测试实验则表明了这种软件架构具有较强的扩展性。论文提出的这种软件架构除了能够应用到无人飞行器上,还能够推广到其它智能系统中。