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

TL;DR

This paper introduces a pattern-based framework and reactive synthesis approach to automatically generate secure controllers for Unmanned Aerial Systems, enhancing their resilience against cyber-physical threats.

Contribution

It presents a novel method combining security specification patterns with reactive synthesis to automatically produce secure UAS controllers based on high-level models.

Findings

Successfully modeled UAS operating mechanisms and security threats.

Generated secure controllers using GR(1) synthesis in simulation.

Validated the approach on the Ardupilot platform.

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.