无人机、无人车和机器人等基于人工智能的复杂无人系统,深度融合了环境感知、数据分析、反馈控制和异构网络互联等技术,受到了军事、工业和民用等诸多领域的广泛关注。近年来军队信息化建设快速发展,此类无人系统及软件控制平台正日渐普及并装备部队,已经成为部队武器装备现代化发展的关键。随着无人系统的蓬勃发展,其面临的安全威胁随之增多,实施攻击的成本和门槛也越来越低,已无法满足人们对软件安全性的需求。由于外部不确定环境的行为难以预测、软件系统本身逻辑复杂和数据信息交互频繁等因素,无人系统安全问题涉及软件安全、硬件安全与信息安全等领域,传统被动的脆弱性检测及防护技术已不足以完全防范复杂多变的外部攻击。反应式程序综合方法能够自动生成针对无人系统的逻辑控制器,但在根据无人系统外部攻击威胁场景生成安全可靠的控制器方面,目前仍无具体的理论研究与实际应用。本文首先深入研究了无人系统尤其是无人飞行系统的各类安全威胁,分析总结并综述了13类无人系统典型的硬件、软件和数据传输安全威胁。在此基础上,本文提出了关于安全控制规约的模式框架,并基于线性时序逻辑总结了通用的安全防护规约模式,提高了形式化规约描述的效率和准确性。基于安全控制规约,本文提出了基于博弈的安全控制器自动生成方法,通过对无人系统进行多模块建模、求解博弈结构提取获胜策略和综合自动机模型结构,得到针对特定攻击威胁场景的安全控制器。最后,本文设计并实现了安全控制程序的生成与仿真平台,基于LTLMo P软件模拟平台和实际无人飞行系统Ardupilot平台,生成相应安全控制程序并开展仿真实验,针对GPS干扰诱骗、恶意注入和反常指令等典型攻击场景进行了有效监控检测和防护控制。实验结果表明,本文提出的方法能够有效自动生成针对特定外部攻击威胁场景的安全控制程序,确保系统始终运行在安全行为集内,提高软件运行的安全性,验证了本文该方法的实用性和可靠性。