自主电动垂直起降（eVTOL）系统的MAVLink协议的符号化与以安全性为中心的形式化验证

《IEEE Networking Letters》：Symbolic and Safety-Centric Formal Verification of MAVLink for Autonomous eVTOL Systems

自主电动垂直起降飞行器（A-eVTOL）需安全可靠的指挥控制通信，但广泛使用的MAVLink协议缺乏标准化加密认证机制，易受欺骗和篡改威胁。本文构建形式验证框架，揭示MAVLink在实时性、自主性和安全关键约束下的脆弱性，首次提出形式指导的定制加密策略，为下一代空中交通系统轻量级协议认证提供新方法。

　　

摘要：

随着自主电动垂直起降（A-eVTOL）车辆使用的日益增多，安全可靠的指挥与控制（C2）通信变得至关重要，以满足严格的安全性和监管要求。MAVLink（微型飞行器链接）是一种在无人机系统中广泛采用的轻量级协议，但缺乏标准化的加密和认证机制，这使其容易受到欺骗和消息篡改等严重威胁。本文提出了一个形式化验证框架，用于模拟MAVLink在A-eVTOL操作环境中的行为。我们发现，虽然在传统无人机应用中这些漏洞尚可容忍，但在A-eVTOL特有的约束条件下（如实时响应性、自主性和故障安全保障），这些漏洞会被放大。据我们所知，这是首次在安全关键的A-eVTOL环境中对MAVLink进行形式化分析的工作，揭示了攻击路径，并提出了针对自主飞行的形式化指导的加密缓解策略。我们的研究结果为下一代空中移动系统的轻量级协议认证提供了新的见解。