Unified Monitor and Controller Synthesis for Securing Complex Unmanned Aircraft Systems

Unmanned Aircraft Systems (UASs) have undergone rapid development over recent years, but have also became vulnerable to security attacks and the volatile external environment. Ensuring that the performance of UASs is safe and secure no matter how the environment changes is challenging. Runtime Verification (RV) is a lightweight formal verification technique that could be used to monitor UAS performance to guarantee safety and security, while reactive synthesis is a methodology for automatically synthesizing a correct-by-construction controller. This paper addresses the problem of the generation and design of a secure UAS controller by introducing a unified monitor and controller synthesis method based on RV and reactive synthesis. First, we introduce a novel methodological framework, in which RV monitors is applied to guarantee various UAS properties, with the reactive controller mainly focusing on the handling of tasks. Then, we propose a specification pattern to represent different UAS properties and generate RV monitors. In addition, a detailed priority-based scheduling method to schedule monitor and controller events is proposed. Furthermore, we design two methods based on specification generation and re-synthesis to solve the problem of task generation using metrics for reactive synthesis. Then, to facilitate users using our method to design secure UAS controllers more efficiently, we develop a domain-specific language (UAS-DL) for modeling UASs. Finally, we use F Prime to implement our method and conduct experiments on a joint simulation platform. The experimental results show that our method can generate secure UAS controllers, guarantee greater UAS safety and security, and require less synthesis time.