@inproceedings{536eecda71a5461ea0679713d17e045f,
title = "PAVE++ Demo: Cross-Layer Formal Verification and OTA Validation for UAV Communications",
abstract = "This demonstration presents an interactive showcase of the Prompt Aided Formal Verification (PAVE) framework applied to MAVLink 2, emphasizing practical and visual verification processes. Attendees will experience real-time demonstrations including: automatic translation of natural language protocol specifications into symbolic verification models using Large Language Models (LLMs); visual state-machine verification via nuXmv and ProVerif; simulated cyber-attacks on the Damn Vulnerable Drone (DVD) platform; and over-the-air (OTA) security validation using a physical PX4-based drone. Participants will directly observe MAVLink 2 vulnerabilities being exploited and immediately mitigated through ChaCha20 encryption. The demonstration underscores the effectiveness of combining symbolic verification with practical cryptographic protections, providing a clear and compelling methodology for ensuring secure UAV communication in contested operational scenarios.",
keywords = "5G, Formal Verification, MAVLink, Prompt Engineering, Security",
author = "Tom Wray and Ying Wang",
note = "Publisher Copyright: {\textcopyright} 2025 IEEE.; 2025 IEEE Military Communications Conference, MILCOM 2025 ; Conference date: 06-10-2025 Through 10-10-2025",
year = "2025",
doi = "10.1109/MILCOM64451.2025.11310334",
language = "English",
series = "Proceedings - IEEE Military Communications Conference MILCOM",
pages = "915--916",
booktitle = "2025 IEEE Military Communications Conference, MILCOM 2025",
}