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

• URL: http://arxiv.org/abs/2604.03886v1
• Date: Sat, 04 Apr 2026 22:45:02 GMT
• Title: From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink
• Abstract summary: Platum is a framework that addresses both failures with a minimal DSL.<n>Our evaluation demonstrates a 4x reduction in total monitor latency and lower memory overhead compared to DATUM.
• Score: 2.4755749916288714
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• LMSM: LLM Security Framework Inspired by Linux Security Modules [56.93644694627783]
  Large language models (LLMs) are increasingly deployed with layered defenses, yet malicious prompts can still bypass them.<n>We present Language Model Security Modules (LMSM), a security framework that adapts the separation behind Linux Security Modules (LSM) to LLM serving.
  arXiv  Detail & Related papers  (2026-08-26T12:13:05Z)
• RT-SHCUA: Real-Time Self-Hosted Computer-Use Agent for UAV Control [29.46902986541309]
  Natural-language control offers a promising interface for unmanned aerial vehicles (UAVs)<n>But directly applying self-hosted computer-use agents (SHCUAs) to UAV control introduces a structural mismatch.<n>This paper proposes a real-time and security-oriented restructuring of SHCUA-based UAV control.
  arXiv  Detail & Related papers  (2026-07-20T13:52:24Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• Design and Performance Evaluation of Secure RF and WiFi-Based Communication in Drone Swarms via Testbed Implementation [0.5863360388454261]
  We present MAVShield, a lightweight encryption framework for MAVLink communications.<n>It is integrated into four custom-built UAVs to establish secure communication links over RF and WiFi channels.<n>Their performance is evaluated through flight experiments using a UAV swarm testbed.
  arXiv  Detail & Related papers  (2026-06-25T13:36:12Z)
• A Source Domain is All You Need: Source-Only Cross-OS Transfer Learning for APT Anomaly Detection via Semantic Alignment and Optimal Transport [3.005222044503286]
  We study a source-only cross-OS APT detection problem using system-level provenance traces.<n>We propose a transport-based framework for ranking anomalous target processes under zero target supervision.<n>The proposed framework improves ROC-AUC and nDCG over source-only anomaly-detection baselines.
  arXiv  Detail & Related papers  (2026-06-08T22:13:42Z)
• WISV: Wireless-Informed Semantic Verification for Distributed Speculative Decoding in Device-Edge LLM Inference [56.297697169678095]
  WISV (Wireless-Informed Semantic Verification) is a novel distributed speculative decoding framework.<n>We show that WISV achieves up to a 60.8% increase in accepted length, a 37.3% reduction in interaction rounds, and a 31.4% improvement in end-to-end latency.<n>We validate WISV on a hardware testbed comprising an NVIDIA Jetson AGX Orin and an A40-equipped server.
  arXiv  Detail & Related papers  (2026-04-20T01:29:56Z)
• T-MAP: Red-Teaming LLM Agents with Trajectory-aware Evolutionary Search [49.99459363244884]
  We propose a trajectory-aware evolutionary search method, T-MAP, which leverages execution trajectories to guide the discovery of adversarial prompts.<n>Our approach enables the automatic generation of attacks that not only bypass safety guardrails but also reliably realize harmful objectives through actual tool interactions.
  arXiv  Detail & Related papers  (2026-03-21T12:33:34Z)
• AgenticCyOps: Securing Multi-Agentic AI Integration in Enterprise Cyber Operations [7.660803748903973]
  Multi-agent systems (MAS) promise adaptive, reasoning-driven enterprise, yet granting agents autonomous control over tools, memory, and communication introduces attack surfaces absent from deterministic pipelines.<n>We introduce AgenticCyOps, a framework built on a systematic decomposition of attack surfaces across component, coordination, and protocol layers.<n>We apply the framework to a Security Operations Center (SOC) workflow, adopting the Model Context Protocol (MCP) as the structural basis.
  arXiv  Detail & Related papers  (2026-03-10T03:15:36Z)
• Beyond Input Guardrails: Reconstructing Cross-Agent Semantic Flows for Execution-Aware Attack Detection [32.301679396929536]
  We propose SysName, a framework that shifts the defensive paradigm from static input filtering to execution-aware analysis.<n>SysName synthesizes fragmented operational primitives into contiguous behavioral trajectories, enabling a holistic view of system activity.<n> Empirical evaluations demonstrate that SysName effectively detects over ten distinct compound attack vectors, achieving F1-scores of 85.3% and 66.7% for node-level and path-level end-to-end attack detection, respectively.
  arXiv  Detail & Related papers  (2026-03-04T01:59:16Z)
• Verifier-Bound Communication for LLM Agents: Certified Bounds on Covert Signaling [0.0]
  Colluding language-model agents can hide coordination in messages that remain policy-compliant at the surface level.<n>We present CLBC, a protocol where generation and admission are separated.<n>We show how this protocol yields an upper bound on transcript leakage in terms of latent leakage plus explicit residual channels.
  arXiv  Detail & Related papers  (2026-02-27T23:42:37Z)
• Cross-Layer Detection of Wireless Misbehavior Using 5G RAN Telemetry and Operational Metadata [0.0]
  We study how manipulation affects the coherence among physical layer measurements, MAC scheduling decisions, and configuration metadata.<n>Every manipulation produces a distinct and reproducible signature that is not visible from any single telemetry source.<n>Findings indicate that cross layer coherence provides a practical signal for detecting uplink misbehavior using only standard gNB telemetry.
  arXiv  Detail & Related papers  (2025-11-26T18:53:26Z)
• Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
  We study adaptive attacks by an untrusted model that knows the protocol and the monitor model.<n>We instantiate a simple adaptive attack vector by which the attacker embeds publicly known or zero-shot prompt injections in the model outputs.
  arXiv  Detail & Related papers  (2025-10-10T15:12:44Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  We propose an unsupervised conformal inference framework for generation.<n>Our gates achieve close-to-nominal coverage and provide tighter, more stable thresholds than split UCP.<n>The result is a label-free, API-compatible gate for test-time filtering.
  arXiv  Detail & Related papers  (2025-09-26T23:40:47Z)
• DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
  Large Language Models (LLMs) are increasingly central to agentic systems due to their strong reasoning and planning capabilities.<n>This interaction also introduces the risk of prompt injection attacks, where malicious inputs from external sources can mislead the agent's behavior.<n>We propose a Dynamic Rule-based Isolation Framework for Trustworthy agentic systems, which enforces both control and data-level constraints.
  arXiv  Detail & Related papers  (2025-06-13T05:01:09Z)
• ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
  We introduce ProtocolLLM, the first benchmark suite specifically targeting widely used SystemVerilog protocols.<n>We observe that most of the models fail to generate SystemVerilog code for communication protocols that follow timing constrains.
  arXiv  Detail & Related papers  (2025-06-09T17:10:47Z)
• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  We propose CANTXSec, the first deterministic Intrusion Detection and Prevention system based on physical ECU activations.<n>It detects and prevents classical attacks in the CAN bus, while detecting advanced attacks that have been less investigated in the literature.<n>We prove the effectiveness of our solution on a physical testbed, where we achieve 100% detection accuracy in both classes of attacks while preventing 100% of FIAs.
  arXiv  Detail & Related papers  (2025-05-14T13:37:07Z)
• A Novel Cipher for Enhancing MAVLink Security: Design, Security Analysis, and Performance Evaluation Using a Drone Testbed [0.0]
  We present MAVShield, a lightweight cipher designed to secure communications in Unmanned Aerial Vehicles (UAVs) using the MAVLink protocol.<n>We implement MAVShield alongside AES-CTR, ChaCha20, Speck-CTR, and Rabbit, and evaluate them on a real drone testbed.
  arXiv  Detail & Related papers  (2025-04-29T10:53:17Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.