Synthesizing Secure Reactive Controller for Unmanned Aerial System

Complex CPS such as VAS got rapid development these years, but also became vulnerable to GPS spoofing, packets injection, buffer-overflow and other malicious attacks. Ensuring the behaviors of VAS always keeping secure no matter how the environment changes, would be a prospective direction for VAS security. This paper aims at presenting a reactive synthesisbased approach to implement the automatic generation of secure VAS controller. First, we study the operating mechanism of VAS and construct a high-Ievel model consisting of actuator and monitor. Besides, we analyze the security threats of VAS from the perspective of hardware, software and data transmission, and then extract the corresponding specifications of security properties with LTL formulas. Based on the VAS model and security specifications, the controller can be constructed by GR(l) synthesis algorithm, which is a two-player game process between VAV 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 VAS attack scenarios.