Avis: In-Situ Model Checking for Unmanned Aerial Vehicles
This addresses safety-critical issues in UAV control firmware, offering a faster method for detecting sensor failure vulnerabilities, though it appears incremental as it builds on existing in-situ model checking techniques.
The paper tackles the problem of sensor failures in unmanned aerial vehicles (UAVs) that can lead to crashes or unsafe conditions, proposing Avis, an in-situ model checker that injects sensor failures during mode transitions to quickly uncover these issues. Avis found unsafe conditions 2.4 times faster than the leading approach and discovered 10 previously unknown bugs in ArduPilot and PX4 firmware.
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.