Avis: In-Situ Model Checking for Unmanned Aerial Vehicles

TL;DR

Avis is an in-situ model checking tool that efficiently detects sensor failure scenarios leading to unsafe UAV conditions by injecting failures during mode transitions, uncovering new bugs faster than existing methods.

Contribution

The paper introduces Avis, a novel in-situ model checker for UAV control firmware that operates during mode transitions to identify unsafe sensor failure scenarios more efficiently.

Findings

Avis found unsafe conditions 2.4 times faster than Bayesian Fault Injection.

Discovered 10 new software bugs causing unsafe UAV states.

Reinserted and verified 5 known critical bugs.

Abstract

Control firmware in unmanned aerial vehicles (UAVs) uses sensors to model and manage flight operations, from takeoff to landing to flying between waypoints. However, sensors can fail at any time during a flight. If control firmware mishandles sensor failures, UAVs can crash, fly away, or suffer other unsafe conditions. In-situ model checking finds sensor failures that could lead to unsafe conditions by systematically failing sensors. However, the type of sensor failure and its timing within a flight affect its manifestation, creating a large search space. We propose Avis, an in-situ model checker to quickly uncover UAV sensor failures that lead to unsafe conditions. Widely used control firmware already support operating modes. Avis injects sensor failures as the control firmware transitions between modes - a key execution point where mishandled software exceptions can trigger unsafe conditions. We implemented Avis and applied it to ArduPilot and PX4. Avis found unsafe conditions 2.4X faster than Bayesian Fault Injection, the leading, state-of-the-art approach. Within the current code base of ArduPilot and PX4, Avis discovered 10 previously unknown software bugs that lead to unsafe conditions. Additionally, we reinserted 5 known bugs that caused serious, unsafe conditions and Avis correctly reported all of them.