Finding Software Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification

Abstract

Unmanned Aerial Vehicles (UAVs) usage in various tasks has increased exponentially in the recent past, which enable users to complete vital missions efficiently and without risking human lives. However, and like any other systems, it poses a cybersecurity threat if not handled correctly. Therefore, it is essential to know the risk and understand the impact of various possible attacks on the overall UAVs. For this purpose, model checking and fuzzing techniques have been applied to improve the UAV approach's security. Nevertheless, there is little effort focused on using those methods in the software domain, especially when investigating low-level implementation vulnerabilities related to UAV software. In this dissertation, UAV risks and the impact of cyberattacks investigated by applying bounded model checking and fuzzing techniques. As a result, a new verification algorithm was developed in a tool named DepthK to verify UAV software correctness. The work's primary research objectives examined through two scientific papers centred on these key research disciplines. These studies undertaken described in Chapter 4 and 5. Paper 1 (Verification and refutation of C programs based on k-induction and invariant inference) outlines a new verification algorithm for detecting UAV software vulnerabilities (e.g., concurrency and buffer overflow bugs). The approach's effectiveness was evaluated and showed better results compared to the state-of-the-art testing tools. The new framework also formed the basis for UAVs software verification development. Paper 2 (Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification) demonstrated the risks from exploiting UAV software vulnerabilities and the effectiveness of the proposed approach. The experiment results show UAV software failures that hardly detected by other verifiers and was quickly and efficiently detected by the proposed verification algorithm.

Date of Award	1 Aug 2021
Original language	English
Awarding Institution	The University of Manchester
Supervisor	Lucas Cordeiro (Supervisor) & Mustafa Mustafa (Supervisor)