Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types

TL;DR

Stealthy attacks on UAV control channels can exploit legal MAVLink sequences to cause unsafe outcomes. The paper presents DATUM, a runtime verification framework using refined multiparty session types (RMPSTs) to express and enforce value-dependent protocol constraints for MAVLink, and it formalizes a substantial portion of MAVLink with automated F* implementations. Through three case studies and evaluations on ArduPilot and PX4, the authors demonstrate that dynamic attestation can mitigate real-world safety and security issues with manageable overhead. This approach enables safer, patch-robust UAV operation by preventing attacks that exploit protocol-level vulnerabilities while patches are developed and deployed.

Abstract

A compromised system component can issue message sequences that are legal while also leading the overall system into unsafe states. Such stealthy attacks are challenging to characterize, because message interfaces in standard languages specify each individual message separately but do not specify safe sequences of messages. We present initial results from ongoing work applying refined multiparty session types as a mechanism for expressing and enforcing proper message usage to exclude unsafe sequences. We illustrate our approach by using refined multiparty session types to mitigate safety and security issues in the MAVLink protocol commonly used in UAVs.

Figures (2)

• Figure 1: The RMPST from our case study, written in F* using DATUM.
• Figure 2: Engineers use RMPSTs from the DATUM MAVLink specification to create a protocol that mitigates safety and security issues. At runtime, DATUM checks on the UAV that messages conform to the protocol.