基于可信执行环境的机器人实时操作系统架构及形式化验证研究

The operating system is a critical component of the robot controller, which plays an important role in the implementation of collision detection, emergency braking or other real-time control functionalities and motion planning, image processing or other complex computation functionalities. The real-time operating system can not meet complex computation requirements of robot control. The existing dual operating system (dual-OS) architectures can not effectively guarantee the fault isolation between the real-time operating system and the general purpose operating system, and they do not undergo rigorously formal verification, which makes them not meet the reliability requirement of the robot controller. This project will build a dual-OS architecture by establishing a trusted execution environment (TEE) using hardware-based isolation mechanisms, and will carry out the formal verification of the architecture to analyze its reliability. We focus on the research of building the TEE-based robot real-time operating system architecture, and the formal verification method which is based on the labelled transition system to analyze the core mechanisms (isolation, schedule, and communication) of the operating system architecture. The goal of the project is to present a robot real-time operating system architecture, which meets requirements of real-time control, complex computation, and formal verification, and supports the modular development and distributed execution of robot software. This research will provide strong technical support for the design and application of robot operating systems, and will build theoretical basis for the formal verification of robot control software, so this research is important for the development and promotion of robot control technology.

操作系统是机器人控制器的关键组成部分，它对于碰撞检测、紧急制动等实时控制功能和运动规划、图像处理等复杂计算功能的实现具有重要作用。单一的实时操作系统不满足机器人控制对复杂计算功能的要求；现有双操作系统架构不能有效保证实时和通用操作系统故障隔离，且未经过严格的形式化验证，不满足机器人控制系统对可靠性的要求。本项目将采用基于硬件隔离机制建立可信执行环境的方式构建双操作系统架构，并利用形式化验证技术分析架构可靠性，重点研究基于可信执行环境的机器人实时操作系统架构，以及基于标记转换系统分析该操作系统架构隔离、调度和通信等核心机制的形式化验证方法，实现满足实时控制、复杂计算、形式化验证要求的机器人实时操作系统架构，支持机器人软件的模块化开发和分布式运行，为机器人操作系统设计和应用提供技术支撑，并为机器人控制软件形式化验证奠定理论基础，对机器人控制技术发展和推广具有重要意义。

为了满足机器人控制器对操作系统的实时性、通用性和可靠性需求，本项目采用基于硬件隔离机制建立可信执行环境的方式构建双操作系统架构，并利用形式化验证技术分析架构的可靠性，主要研究成果如下：.在机器人操作系统架构研究方面，针对实时性要求，提出基于可信执行环境的机器人实时操作系统架构和面向多核架构的实时操作系统任务迁移方案，在满足通用性要求的同时，为机器人控制系统提供更好的实时性支持；针对安全性要求，分别提出基于片内存储的可信执行环境抗物理攻击防护方法、基于软件方式的高安全Enclave构建方法和基于微内核架构的可信执行环境操作系统构建技术，以提高可信执行环境对板级物理攻击、内存侧信道攻击和软件攻击的防御能力。.在机器人应用软件框架研究方面，提出可信执行环境用户层可信计算服务构建技术，为节点的认证和通信提供基础服务；提出机器人应用软件远程证明服务框架构建技术，为节点间的远程证明和数据通信提供支持。.在机器人系统形式化验证研究方面，对实时操作系统任务调度算法、共享资源独占访问算法、认证密钥协商协议和机器人关节通信总线系统等机制进行了分析和验证，保证了机器人操作系统关键机制的可靠性；对与机器人运动学特性相关的雅可比矩阵、辛几何、几何代数和矩阵函数微分进行了形式化验证，为机器人运动学算法验证提供了理论支持。.综上所述，本项目按研究计划圆满完成了研究目标，并增加了一些新的研究内容，这些新的研究内容是申请书中研究内容的拓展和延伸。