Synthesizing Secure Reactive Controller for Unmanned Aerial System

摘要

Complex CPS such as UAS got rapid development these years, but also became vulnerable to GPS spoofing, packets injection, buffer-overflow and other malicious attacks. Ensuring the behaviors of UAS always keeping secure no matter how the environment changes, would be a prospective direction for UAS security. This paper aims at presenting a reactive synthesis-based approach to implement the automatic generation of secure UAS controller. First, we study the operating mechanism of UAS and construct a high-Ievel model consisting of actuator and monitor. Besides, we analyze the security threats of UAS from the perspective of hardware, software and data transmission, and then extract the corresponding specifications of security properties with LTL formulas. Based on the UAS model and security specifications, the controller can be constructed by GR(1) synthesis algorithm, which is a two-player game process between UAV and Environment. Finally, we expand the function of LTLMoP platform to construct the automatons for controller in multi-robots system, which provides secure behavior strategies under several typical UAS attack scenarios.