論文の概要: From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink
- arxiv url: http://arxiv.org/abs/2604.03886v1
- Date: Sat, 04 Apr 2026 22:45:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-07 15:49:18.816053
- Title: From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink
- Title（参考訳）: 高レベルタイプから低レベルモニター:MAVLinkの検証実行チェッカーの合成
- Authors: Arthur Amorim, Paul Gazzillo, Max Taylor, Lance Joneckis,
- Abstract要約: Platumは、最小限のDSLで両方の障害に対処するフレームワークです。
DATUMと比較して,総モニタ遅延とメモリオーバーヘッドの4倍の低減効果を示した。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: MAVLinkのような無人航空機(UAV)の標準的な通信プロトコルは、メッセージシーケンスの文脈的妥当性を強制する能力が欠如している。
したがって、オートパイロットは、構文的に正しいが意味的に不適切なコマンドが物理的異常検知装置を起動することなく、安全でない状態を誘導するステルス攻撃に弱いままである。
以前の研究 (DATUM) では、グローバル精製マルチパーティセッションタイプ (RMPST) は、集中型のMAVLinkプロトコル実行のための効果的な仕様言語であるが、プロトコル定義と相互にインターリーブされた手動証明項と、リソース制約のあるUAVハードウェアと互換性のないマネージドランタイムを持つOCaml抽出バックエンドという2つのエンジニアリング上の障害に悩まされていた。
本稿では,グローバルセッション型の5つの意味的コンポーネント(セダ,レシーバ,ラベル,ペイロード変数,洗練述語)のみを必要とする最小限のDSLで,両方の障害に対処するフレームワークであるPlatumについて述べる。
確認された仕様は、GCS/UAV通信境界で集中的なプロキシモニターとしてデプロイされる、フラットでアロケーションフリーなC有限状態マシン(FSM)に直接コンパイルされる。
本評価は,ArduPilot SITLシミュレーションにより測定したDATUMと比較して,総モニタレイテンシとメモリオーバーヘッドの4倍の低減効果を示した。
関連論文リスト
- T-MAP: Red-Teaming LLM Agents with Trajectory-aware Evolutionary Search [49.99459363244884]
提案手法は, 対向的プロンプトの発見を導くために, 実行トラジェクトリを利用するトラジェクトリ対応の進化探索手法であるT-MAPを提案する。
本手法は,安全ガードレールをバイパスするだけでなく,実際のツールインタラクションによる有害な目標を確実に実現するための攻撃の自動生成を可能にする。
論文 参考訳（メタデータ） (2026-03-21T12:33:34Z) - AgenticCyOps: Securing Multi-Agentic AI Integration in Enterprise Cyber Operations [7.660803748903973]
マルチエージェントシステム(MAS)は適応的で推論駆動の企業を約束するが、ツール、メモリ、通信の自律的な制御をエージェントに与えることで、決定論的パイプラインが欠如する攻撃面を導入する。
AgenticCyOpsは、コンポーネント層、調整層、プロトコル層にまたがる攻撃面を体系的に分解するフレームワークである。
このフレームワークをSecurity Operations Center(SOC)ワークフローに適用し、モデルコンテキストプロトコル(MCP)を構造基盤として採用する。
論文 参考訳（メタデータ） (2026-03-10T03:15:36Z) - Beyond Input Guardrails: Reconstructing Cross-Agent Semantic Flows for Execution-Aware Attack Detection [32.301679396929536]
静的な入力フィルタリングから実行対応分析へ、防御パラダイムをシフトするフレームワークであるSysNameを提案する。
SysNameは断片化された操作プリミティブを連続した行動軌跡に合成し、システムアクティビティの全体像を可能にする。
実証的な評価により、SysNameは10以上の異なる複合攻撃ベクトルを効果的に検出し、それぞれノードレベルとパスレベルのエンドツーエンド攻撃検出に対して85.3%と66.7%のF1スコアを達成した。
論文 参考訳（メタデータ） (2026-03-04T01:59:16Z) - Verifier-Bound Communication for LLM Agents: Certified Bounds on Covert Signaling [0.0]
言語モデルエージェントを結合することで、ポリシーに準拠したメッセージの調整を表面レベルで隠蔽することができる。
生成と受け入れを分離するプロトコルであるCLBCを提案する。
このプロトコルは、遅延リークと明示的な残留チャネルの観点から、転写リークの上限をいかに高めるかを示す。
論文 参考訳（メタデータ） (2026-02-27T23:42:37Z) - Cross-Layer Detection of Wireless Misbehavior Using 5G RAN Telemetry and Operational Metadata [0.0]
本研究では,物理層計測,MACスケジューリング決定,構成メタデータのコヒーレンスに及ぼす操作の影響について検討する。
すべての操作は、単一のテレメトリソースから見えない、明瞭で再現可能なシグネチャを生成する。
クロス層コヒーレンス(英語版)は標準のgNBテレメトリのみを用いてアップリンク誤りを検出する実用的な信号を提供することを示す。
論文 参考訳（メタデータ） (2025-11-26T18:53:26Z) - Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
プロトコルとモニタモデルを知っている信頼できないモデルによるアダプティブアタックについて検討する。
我々は、攻撃者がモデル出力に公知またはゼロショットプロンプトインジェクションを埋め込む単純な適応攻撃ベクトルをインスタンス化する。
論文 参考訳（メタデータ） (2025-10-10T15:12:44Z) - Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
生成のための教師なし共形推論フレームワークを提案する。
我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。
その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
論文 参考訳（メタデータ） (2025-09-26T23:40:47Z) - DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
大規模言語モデル(LLM)は、強力な推論と計画能力のため、エージェントシステムの中心となってきています。
この相互作用は、外部ソースからの悪意のある入力がエージェントの振る舞いを誤解させる可能性がある、インジェクション攻撃のリスクも引き起こす。
本稿では,信頼に値するエージェントシステムのための動的ルールベースの分離フレームワークを提案する。
論文 参考訳（メタデータ） (2025-06-13T05:01:09Z) - ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
本稿では,広く使用されているSystemVerilogプロトコルを対象とした最初のベンチマークスイートであるProtocolLLMを紹介する。
我々は,ほとんどのモデルがタイミング制約に従う通信プロトコルのSystemVerilogコードを生成するのに失敗したことを観察する。
論文 参考訳（メタデータ） (2025-06-09T17:10:47Z) - CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
物理ECUアクティベーションに基づく最初の決定論的侵入検知・防止システムであるCANTXSecを提案する。
CANバスの古典的な攻撃を検知・防止し、文献では調査されていない高度な攻撃を検知する。
物理テストベッド上での解法の有効性を実証し,攻撃の両クラスにおいて100%検出精度を達成し,100%のFIAを防止した。
論文 参考訳（メタデータ） (2025-05-14T13:37:07Z) - A Novel Cipher for Enhancing MAVLink Security: Design, Security Analysis, and Performance Evaluation Using a Drone Testbed [0.0]
我々はMAVLinkプロトコルを用いて無人航空機(UAV)の通信をセキュアにするための軽量暗号MAVShieldを提案する。
我々は、AES-CTR、ChaCha20、Speck-CTR、Rabbitと共にMAVShieldを実装し、実際のドローンテストベッドでそれらを評価した。
論文 参考訳（メタデータ） (2025-04-29T10:53:17Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。