从高级类型到低级监控：为 MAVLink 合成验证运行时检查器
密码学与安全
2026-04-07 v1 形式语言与自动机理论
摘要
无人机标准通信协议如 MAVLink 缺乏对消息序列情境有效性的 enforcement 能力。因此，autopilot 仍然 vulnerable to 隐蔽攻击，这类攻击会产生语法正确但时机不当的语义错误命令，导致不安全状态而不会触发物理异常检测器。先前工作 (DATUM) 证明了全局 Refined Multiparty Session Types (RMPSTs) 是集中式 MAVLink 协议 enforcement 的有效规范语言，但受制于两个工程故障：手动 proof 术语交织在协议定义中，以及 OCaml 提取后端的受控运行时与资源受限的 UAV 硬件不兼容。我们提出了 Platum 框架，通过最小 DSL 解决上述两个问题，仅需五个语义组件（发送方、接收方、标签、负载变量、细化谓词），其结构良构性条件通过 Meta-F* 中的反射 decision 程序确认。确认的规范直接编译为平坦、无分配的 C 有限状态机 (FSM)，部署在 GCS/UAV 通信边界作为集中式代理监控器。我们的评估表明，与 DATUM 相比，Platum 在总体监控延迟和内存开销方面分别降低了 4 倍，测量通过 ArduPilot SITL 模拟仿真。
引用
@article{arxiv.2604.03886,
title = {From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink},
author = {Arthur Amorim and Paul Gazzillo and Max Taylor and Lance Joneckis},
journal= {arXiv preprint arXiv:2604.03886},
year = {2026}
}
备注
To appear in NASA Formal Methods Symposium 2026 (NFM'26)