随着越来越多的功能要求由计算机实现,对机载操作系统的功能要求越来越多,内核形式化验证变成一个重要方向。结合对多核处理器的支持,与虚拟化相结合的微内核是当前机载操作系统研究热点。它具有支持多级安全等众多机载要求的特性。
系统综合化以后,原来运行在不同计算机的软件被合并到一个平台中,需要机载操作系统提供分区隔离机制,同时综合化后更多的系统功能由软件来承担,机载软件复杂度显著增加,软件存在潜在缺陷的几率也相应增加,软件复杂性与安全性(Safety)之间的矛盾越来越突出。”分而治之”是应对软件复杂,提高系统安全性的有效途径。采用微内核架构设计机载分区操作系统,可以将机载软件部署在不同的分区以实现隔离,同时也可以使用形式化方法对操作系统的微内核进行验证。只有微小的内核才具备形式化验证的可行性。
随着网络中心战在现代战争中越来越得到重视,信息安全成为机载软件新的关注焦点。由于网络化战争需要在作战实体间传递信息,共享战场资源,带来了信息安全问题,使其成为机载软件设计所必须关注的焦点。对于较高级别的信息安全系统,要求软件进行形式化验证,采用微核架构成为机载操作系统设计的方向。
在综合化系统中,更多的功能由软件实现,机载软件的规模急剧膨胀,新型飞行器机载软件代码行数已达到千万行的规模。由于机载设备有适航要求,按照DO-178B A级要求进行机载软件开发,成本可达到100美元/行,研制费用极为昂贵。如何有效地控制全机软件成本,成为亟待解决的问题。虚拟化成为复用成熟软件、降低软件成本的有效方法。
图1微内核机载操作系统结构示意图
因此,下一代的机载操作系统应以微内核、虚拟化和信息安全为特征,其概念架构见图1。在该结构中,机载操作系统由虚拟机管理器、应用运行环境和客户服务适配层组成。虚拟机管理器用于建立安全(Safety)的分区环境,应用运行环境则负责在分区内为应用程序提供传统操作系统的服务,如运行时库和其他方便用户编程的公共函数库等。为了支持客户服务OS在分区内运行,需要客户服务OS适配层的支持。
虚拟机管理器采用微内核技术构建,这样可以使用形式化验证的方法对该系统进行验证。微内核的架构也进一步提高了系统的安全性和可靠性。微内核机制的本质思想就是运行于特权模式的内核仅提供最基本的服务,建立软件实现的虚拟硬件执行环境,所有其他应用所依赖的操作系统服务均由运行于用户模式的软件组件实现。
基于微内核的设计思想,整个系统中只有虚拟机管理器运行在特权级,以确保其对系统物理资源的管理和控制。其他操作系统功能组件,包括客户操作系统、应用运行环境、驱动运行环境等全部运行在非特权级,以防止其异常行为对整个系统的运行状态产生影响。由于运行级别的不同,可以保证虚拟机管理器不会遭到客户操作系统及应用的破坏,虚拟机管理器所构建的高安全分区也可以按照预期的那样在不同分区间提供安全保护,从而确保了系统分区特性得以满足。
微内核的虚拟机管理器应该只提供最基本的服务,从系统信息安全支持的角度,虚拟机管理器还应该提供基本的信息安全能力,从而构建完整的信息安全支撑体系。
图2微内核机载操作系统功能分布示意图
在图2所示的微内核机载操作系统体系结构中,微内核的虚拟机管理器应提供分区管理、分区间通信、内存管理单元(MemoryManagement Unit,MMU)管理、中断处理、线程调度以及基本安全访问控制功能,将代码行数有效控制在可形式化验证的范围内。
***—点击二维码深度关注—**
领取专属 10元无门槛券
私享最新 技术干货