Vulnerabilities Analysis and Secure Controlling for Unmanned Aerial System Based on Reactive Synthesis

TL;DR

The paper addresses vulnerabilities in Unmanned Aerial Systems (UAS), particularly GPS spoofing and related cyber-physical risks, by introducing a pattern-based framework to express security properties via Linear Temporal Logic (LTL). It then applies GR(1) reactive synthesis to automatically generate secure UAS controllers, modeling the UAV as an actuator and a monitor in a two-player game against the environment, with the winning condition described by $\,\phi=\varphi^e_g\Rightarrow\varphi^s_g$ and synthesis running in $O(n^3)$ time. The authors enumerate 13 specification patterns across hardware, software, cyber-physical threats, plus safety and task properties, translating them into automata that guide secure behavior during flight. Validation on the ArduPilot platform demonstrates the approach can detect and counter attacks (e.g., waypoint modifications) by forcing safe maneuvers like RTL, indicating practical promise for automatic secure UAV control in real-world deployments, and outlining avenues for future integration with tools like Spectra and additional platforms.

Abstract

Complex Cyber-Physical System (CPS) such as Unmanned Aerial System (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 introducing a pattern-based framework to describe the security properties of UAS, and 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-level model consisting of actuator and monitor. Besides, we analyze the security threats of UAS from the perspective of hardware, software and cyber physics, and then summarize the corresponding specification patterns of security properties with LTL formulas. With the UAS model and security specification patterns, automatons for controller can be constructed by General Reactivity of Rank 1 (GR(1)) synthesis algorithm, which is a two-player game process between Unmanned Aerial Vehicle (UAV) and its environment. Finally, we experimented under the Ardupilot simulation platform to test the effectiveness of our method.

Figures (5)

• Figure 1: System Structure of UAS
• Figure 2: UAS Security Vulnerabilities
• Figure 3: The workspace of UAS model
• Figure 4: No-fly zone and simulation of UAS
• Figure 5: The simulation of secured UAS model