自主无人系统高完整性理论及关键技术研究

Networked autonomous unmanned systems are confronted with the threats of malwares, false data injection, configuration tampering, and generalized signal spoofing. In order to ensure the integrity of system software, data and signals of autonomous unmanned systems, in this project, we will investigate the highly precise swarm remote attestation for system software with traceability on abnormality. We will propose new security property of information flow integrity with uncertainty constraints of faults and false data, as well as the probabilistic automated verification on this property. We will give the quantitative specification on the integrity of control data and GPS signal payloads based on entropy, and propose a quantitative measurement which is further used to intervene the flight control of autonomous unmanned systems. We expect to discuss the compositional remote attestation for multiple task software and the compositional verification on probabilistic noninterference based on the probabilistic assume-guarantee reasoning. Finally, our project will offer demo system for the remote attestation of autonomous unmanned systems, and the approaches on modeling, measurement, analysis and verification for the enforcement of data and signal integrity. The evaluation results will show the precision of attestation, verification and quantitative measurement, as well as the performance of swarm attestation and compositional approaches. The outcome of this project will provide theoretical and technical supports for the construction of secure network of autonomous unmanned systems.

针对网络化自主无人系统面临的恶意软件、错误数据注入、配置篡改和广义信号欺骗等典型安全威胁，以保证自主无人系统的软件、数据和信号的完整性为基本安全目标，本项目研究网络化自主无人系统软件的高精确性且异常可追溯的群集可信远程证明；研究支持故障和错误数据不确定性约束的信息流完整性定义及概率自动化验证；研究基于信息熵的系统控制信息和定位信号载荷定量信息流完整性度量及依据度量结果的飞行控制干预方法；研究多任务软件的组合可信证明及基于概率化假设-保证推理的概率无干扰性可组合验证。最终提供适用于自主无人系统的可信远程证明演示验证系统及针对数据和信号完整性的建模、度量、分析与验证方法，并从证明及验证精度、度量准确性、群集证明及可组合方案效率等方面对本项目方法进行评价。项目成果将为安全的自主无人系统网络构建提供理论和技术支撑。

网络化自主无人系统在软件、数据、配置、信号等多个层面均存在典型安全威胁。本项目以保证自主无人系统的软件、数据和信号的完整性为基本安全目标，具体研究了自主无人系统软件行为的高精确性可信远程证明、基于边缘计算的异常可追溯的无人系统群集可信远程证明、破坏性网络环境下的无人机群集分角色聚合可信远程证明、基于安全迁移系统的无人机任务软件的可组合数据流安全验证、二进制软件的高效动态污点分析、程序二进制的信息流安全分析和控制流完整性分析、采用完整性威胁树的飞控系统定量信息流完整性度量，针对无人机飞行模式切换模型的多时间无干扰性验证。.本项目实现并开源了控制流可信远程证明工具(ReCFA)和程序二进制本地代码信息流分析工具(μDep)，实现了基于PDG函数摘要的高效动态污点分析工具(Sdft)和基于安全迁移系统的软件可组合数据流安全验证工具等工具系统，实现了对无人机软件行为、数据和控制操作的完整性进行建模、分析、验证、度量和运行时保护。从可信证明及验证精度、群集证明及安全可组合验证方案效率、动态污点跟踪效率等方面评价说明了本项目方法的有效性。本项目成果可以为自主无人系统及其网络的安全构建提供理论和技术支撑。