論文の概要: Bridging Threat Models and Detections: Formal Verification via CADP

• arxiv url: http://arxiv.org/abs/2509.13035v1
• Date: Tue, 16 Sep 2025 12:53:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-17 17:50:53.0876
• Title: Bridging Threat Models and Detections: Formal Verification via CADP
• Title（参考訳）: ブリジング脅威モデルと検出:CADPによる形式的検証
• Authors: Dumitru-Bogdan Prelipcean, Cătălin Dima,
• Abstract要約: 検出ロジックとアタックツリーの両方をラベル付き遷移システム(LTS)としてモデル化する形式的検証フレームワークを提案する。 LokiBotやEmotetといった実世界のマルウェアシナリオに対するアプローチを評価した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Threat detection systems rely on rule-based logic to identify adversarial behaviors, yet the conformance of these rules to high-level threat models is rarely verified formally. We present a formal verification framework that models both detection logic and attack trees as labeled transition systems (LTSs), enabling automated conformance checking via bisimulation and weak trace inclusion. Detection rules specified in the Generic Threat Detection Language (GTDL, a general-purpose detection language we formalize in this work) are assigned a compositional operational semantics, and threat models expressed as attack trees are interpreted as LTSs through a structural trace semantics. Both representations are translated to LNT, a modeling language supported by the CADP toolbox. This common semantic domain enables systematic and automated verification of detection coverage. We evaluate our approach on real-world malware scenarios such as LokiBot and Emotet and provide scalability analysis through parametric synthetic models. Results confirm that our methodology identifies semantic mismatches between threat models and detection rules, supports iterative refinement, and scales to realistic threat landscapes.
• Abstract（参考訳）: 脅威検出システムは、敵の行動を特定するためにルールベースの論理に依存するが、高レベルの脅威モデルに対するこれらのルールの適合性は、形式的に検証されることは滅多にない。 本稿では,検出ロジックと攻撃木の両方をラベル付き遷移システム (LTS) としてモデル化し,バイシミュレーションと弱いトレースインクルージョンによる自動適合性チェックを可能にする形式的検証フレームワークを提案する。 ジェネリック・脅威検出言語(GTDL:Generic Threat Detection Language)で規定される検出ルールを構成的操作意味論に割り当て、攻撃木として表現された脅威モデルを構造的トレース意味論を通じてLTSとして解釈する。 どちらの表現も、CADPツールボックスでサポートされているモデリング言語であるLNTに変換される。 この共通セマンティックドメインは、検出カバレッジの体系的および自動検証を可能にする。 LokiBotやEmotetといった現実世界のマルウェアシナリオに対するアプローチを評価し,パラメトリック合成モデルによるスケーラビリティ解析を行った。 提案手法は,脅威モデルと検出規則のセマンティックミスマッチを識別し,反復的改善をサポートし,現実的な脅威景観にスケールする。

関連論文リスト

• See No Evil: Adversarial Attacks Against Linguistic-Visual Association in Referring Multi-Object Tracking Systems [21.34084466103555]
  本稿では,RMOTモデルの参照マッチング機構の統一化を阻止する新しい逆向きフレームワークVEILを提案する。 デジタル・物理的摂動は追跡ロジックの信頼性を損なう可能性を示し、トラックIDスイッチや用語を誘導する。
  論文  参考訳（メタデータ） (2025-09-02T07:17:32Z)
• Securing Agentic AI: Threat Modeling and Risk Analysis for Network Monitoring Agentic AI System [2.5145802129902664]
  MAESTROフレームワークはエージェントAIの脆弱性を公開、評価、排除するために使用された。 プロトタイプエージェントシステムはPython、LangChain、WebSocketでテレメトリを使用して構築、実装された。
  論文  参考訳（メタデータ） (2025-08-12T00:14:12Z)
• CLIProv: A Contrastive Log-to-Intelligence Multimodal Approach for Threat Detection and Provenance Analysis [6.680853786327484]
  本稿では,ホストシステムにおける脅威行動を検出する新しいアプローチであるCLIProvを紹介する。 脅威インテリジェンスに攻撃パターン情報を活用することで、CLIProvはTTPを特定し、完全かつ簡潔な攻撃シナリオを生成する。 最先端の手法と比較して、CLIProvは精度が高く、検出効率が大幅に向上している。
  論文  参考訳（メタデータ） (2025-07-12T04:20:00Z)
• SentinelAgent: Graph-based Anomaly Detection in Multi-Agent Systems [11.497269773189254]
  大規模言語モデル(LLM)に基づくマルチエージェントシステム(MAS)に適したシステムレベルの異常検出フレームワークを提案する。 本稿では,エージェント間相互作用を動的実行グラフとしてモデル化し,ノード,エッジ,パスレベルでの意味的異常検出を可能にするグラフベースのフレームワークを提案する。 第2に,セキュリティポリシとコンテキスト推論に基づくMAS実行の監視,解析,介入を行うLLMによる監視エージェントである,プラグイン可能なSentinelAgentを導入する。
  論文  参考訳（メタデータ） (2025-05-30T04:25:19Z)
• Benchmarking Unified Face Attack Detection via Hierarchical Prompt Tuning [58.16354555208417]
  PADとFFDはそれぞれ物理メディアベースのプレゼンテーションアタックとデジタル編集ベースのDeepFakeから顔データを保護するために提案されている。 これら2つのカテゴリの攻撃を同時に処理する統一顔攻撃検出モデルがないことは、主に2つの要因に起因する。 本稿では,異なる意味空間から複数の分類基準を適応的に探索する,視覚言語モデルに基づく階層型プロンプトチューニングフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-05-19T16:35:45Z)
• 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)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。 モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
  論文  参考訳（メタデータ） (2023-08-25T15:25:57Z)
• Red Teaming Language Model Detectors with Language Models [114.36392560711022]
  大規模言語モデル(LLM)は、悪意のあるユーザによって悪用された場合、重大な安全性と倫理的リスクをもたらす。 近年,LLM生成テキストを検出し,LLMを保護するアルゴリズムが提案されている。 1) LLMの出力中の特定の単語を, 文脈が与えられたシノニムに置き換えること, 2) 生成者の書き方を変更するための指示プロンプトを自動で検索すること,である。
  論文  参考訳（メタデータ） (2023-05-31T10:08:37Z)
• Logically Consistent Adversarial Attacks for Soft Theorem Provers [110.17147570572939]
  本稿では,言語モデルの推論能力の探索と改善のための生成的逆説フレームワークを提案する。 我々のフレームワークは、敵の攻撃をうまく発生させ、グローバルな弱点を識別する。 有効探索に加えて, 生成したサンプルのトレーニングにより, 対象モデルの性能が向上することを示す。
  論文  参考訳（メタデータ） (2022-04-29T19:10:12Z)
• Exploiting Multi-Object Relationships for Detecting Adversarial Attacks in Complex Scenes [51.65308857232767]
  ディープニューラルネットワーク(DNN)をデプロイするビジョンシステムは、敵の例に弱いことが知られている。 近年の研究では、入力データの固有成分のチェックは、敵攻撃を検出するための有望な方法であることが示された。 言語モデルを用いてコンテキスト整合性チェックを行う新しい手法を開発した。
  論文  参考訳（メタデータ） (2021-08-19T00:52:10Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。