基于运行时验证的无人飞行系统安全威胁检测方法

来源：软件学报杂志2018年第5期北京时间：

作者：杨栋,史浩,董威,刘宗林,周戈

单位：杨栋，国防科技大学 计算机学院, 湖南 长沙 41007311,史浩，国防科技大学 计算机学院, 湖南 长沙 41007302,董威，国防科技大学 计算机学院, 湖南 长沙 41007303,刘宗林，国防科技大学 计算机学院, 湖南 长沙 41007304,周戈，国防科技大学 计算机学院, 湖南 长沙 41007305

摘要：无人飞行系统（unmanned aerial system，简称UAS）的软、硬件存在缺陷以及遇到外部恶意攻击，会给UAS的安全性带来极大的威胁.由于UAS的运行环境复杂多变，很多因素在开发过程中难以准确预测，因此，研究有效的运行时安全保证机制具有重要意义.提出了一种基于运行时验证的UAS安全威胁检测方法.首先，对UAS可能遇到的多种安全威胁进行分析，并采用离散时间时序逻辑进行描述，提出相应的UAS-DL语言描述安全监控规约；然后，基于交错自动机提出了自动生成安全威胁监控器的算法，并利用参数化方法实现对多UAS的安全监控.为了提高检测的准确性，进一步研究了将运行时验证和贝叶斯网络推断相结合的方法.采用实际的UAS开发仿真平台Ardupilot进行了实验，并设计了将监控器独立部署在FPGA硬件上的方法，以避免对UAS计算资源的过多占用.实验结果表明，上述方法能够有效地检测UAS的安全威胁.

关键词：无人飞行系统;安全威胁检测;运行时验证

基金资助：国家重点研发计划（2017YFB1001802）；国家重点基础研究发展计划（973）（2014CB340703）；国家自然科学基金（61690203，61532007）