Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink

Arthur Amorim, Paul Gazzillo, Max Taylor, Lance Joneckis

Abstract

Standard communication protocols for Unmanned Aerial Vehicles (UAVs), such as MAVLink, lack the capability to enforce the contextual validity of message sequences. Autopilots therefore remain vulnerable to stealthy attacks, where syntactically correct but semantically ill-timed commands induce unsafe states without triggering physical anomaly detectors. Prior work (DATUM) demonstrated that global Refined Multiparty Session Types (RMPSTs) are an effective specification language for centralized MAVLink protocol enforcement, but suffered from two engineering failures: manual proof terms interleaved with protocol definitions, and an OCaml extraction backend whose managed runtime is incompatible with resource-constrained UAV hardware. We present Platum, a framework that addresses both failures with a minimal DSL requiring only the five semantic components of a global session type (sender, receiver, label, payload variable, refinement predicate), whose structural well-formedness conditions are confirmed via reflective decision procedures in Meta-F*. Confirmed specifications are compiled directly into flat, allocation-free C Finite State Machines (FSMs), deployed as centralized proxy monitors at the GCS/UAV communication boundary. Our evaluation demonstrates a 4x reduction in total monitor latency and lower memory overhead compared to DATUM, measured via ArduPilot SITL simulation.

From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink

Abstract

Standard communication protocols for Unmanned Aerial Vehicles (UAVs), such as MAVLink, lack the capability to enforce the contextual validity of message sequences. Autopilots therefore remain vulnerable to stealthy attacks, where syntactically correct but semantically ill-timed commands induce unsafe states without triggering physical anomaly detectors. Prior work (DATUM) demonstrated that global Refined Multiparty Session Types (RMPSTs) are an effective specification language for centralized MAVLink protocol enforcement, but suffered from two engineering failures: manual proof terms interleaved with protocol definitions, and an OCaml extraction backend whose managed runtime is incompatible with resource-constrained UAV hardware. We present Platum, a framework that addresses both failures with a minimal DSL requiring only the five semantic components of a global session type (sender, receiver, label, payload variable, refinement predicate), whose structural well-formedness conditions are confirmed via reflective decision procedures in Meta-F*. Confirmed specifications are compiled directly into flat, allocation-free C Finite State Machines (FSMs), deployed as centralized proxy monitors at the GCS/UAV communication boundary. Our evaluation demonstrates a 4x reduction in total monitor latency and lower memory overhead compared to DATUM, measured via ArduPilot SITL simulation.

Paper Structure

This paper contains 28 sections, 9 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Overview
  3. A Birds-Eye View of Platum
  4. Refined Multiparty Session Types (RMPSTs)
  5. The DATUM Approach and its Limitations
  6. The Burden of Intrinsic Verification
  7. The Deployment Gap: OCaml vs. Embedded Systems
  8. Methodology
  9. Formalization of Protocol Logic
  10. Integrating MAVLink Specifications
  11. Algorithmic Well-Formedness Checking via Meta-F*
  12. Synthesis of Performant Protocol Monitors
  13. Extraction Semantics
  14. Direct Translation Semantics
  15. Scalability and Correctness Rationale
  16. ...and 13 more sections

Figures (4)

  • Figure 1: The Platum Workflow. The compile-time pipeline (above the dotted line) proceeds from F* specification, through AST decomposition and Meta-F* well-formedness checking, to C monitor synthesis. The runtime deployment (below the dotted line) shows the synthesized monitor operating as a centralized proxy: the GCS transmits MAVLink traffic to Platum, which enforces the global session type at the network boundary before relaying conformant messages to the UAV autopilot.
  • Figure 2: RMPST Formalization of the MAVLink Mission Protocol
  • Figure 3: The reification pipeline. The meta-program inspects the F* AST (top), mapping logical operators like op_Logical_And to C's &&, and resolving the variable x to its runtime location payload.x.
  • Figure : Performance comparison: Platum (Optimized C) vs. DATUM (OCaml). Platum achieves a significant reduction in system latency and lower memory pressure.