Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification
This addresses security concerns for UAV systems, which are critical for safety and reliability, but the approach is incremental as it builds on existing verification methods.
The paper tackled the problem of security vulnerabilities in Unmanned Aerial Vehicles (UAVs) by applying software verification techniques like fuzzing and bounded model checking, and demonstrated successful cyber-attacks through penetration testing, revealing real cyber-threats in UAV software.
The proliferation of Unmanned Aerial Vehicles (UAVs) embedded with vulnerable monolithic software has recently raised serious concerns about their security due to concurrency aspects and fragile communication links. However, verifying security in UAV software based on traditional testing remains an open challenge mainly due to scalability and deployment issues. Here we investigate software verification techniques to detect security vulnerabilities in typical UAVs. In particular, we investigate existing software analyzers and verifiers, which implement fuzzing and bounded model checking (BMC) techniques, to detect memory safety and concurrency errors. We also investigate fragility aspects related to the UAV communication link. All UAV components (e.g., position, velocity, and attitude control) heavily depend on the communication link. Our preliminary results show that fuzzing and BMC techniques can detect various software vulnerabilities, which are of particular interest to ensure security in UAVs. We were able to perform successful cyber-attacks via penetration testing against the UAV both connection and software system. As a result, we demonstrate real cyber-threats with the possibility of exploiting further security vulnerabilities in real-world UAV software in the foreseeable future.