論文の概要: Verifying Graceful Degradation in a Distributed Malware-Detection System with SPIN
- arxiv url: http://arxiv.org/abs/2609.34873v1
- Date: Mon, 28 Sep 2026 10:56:10 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-03 02:01:03.685121
- Title: Verifying Graceful Degradation in a Distributed Malware-Detection System with SPIN
- Title（参考訳）: SPINを用いた分散マルウェア検出システムにおけるグレースフル劣化の検証
- Abstract要約: 本稿では,現代のマルウェア検出システムのエンドポイント決定パイプラインの形式モデルであるPromelaについて述べる。
私たちは、フォールバックマシンが偽陽性を引き起こすことは決してなく、スキャン毎に正確に1つの評決にコミットし、常に強制的な決定で終了するということを証明しています。
この研究は、製品セキュリティシステムの障害処理ロジックに対して、モデルチェックが強い正当性を保証する方法を示している。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Modern endpoint malware detection is distributed: a lightweight agent on each endpoint collects features from a scanned file or process, sends them to a remote server for analysis, and then enforces the returned verdict locally by blocking, quarantining, or disinfecting. Because the endpoint acts on the verdict, the distributed machinery surrounding detection must never turn a transient server failure into a wrong action. We present a formal model, in Promela, of the endpoint decision pipeline of such a system, abstracted from a production architecture at Bitdefender. The model captures the system's graceful-degradation fallback chain: when the primary analysis server times out, the endpoint falls back to an older legacy-protocol server, and failing that to a reduced-signature local scan, before enforcing a verdict. Assuming detection signatures are sound, we specify six safety and liveness properties in linear temporal logic (LTL) and verify them exhaustively with the SPIN model checker. We prove that the fallback machinery never causes a false positive (an enforcement action against a benign file), commits to exactly one verdict per scan even when timed-out responses arrive late, weakens detection strength only in an explicit and ordered way, and always terminates in an enforcement decision, so the pipeline is deadlock-free. Each property is checked to hold non-vacuously, and we report how the state space grows with concurrent scans and endpoints. The work shows how model checking can give strong correctness guarantees for the failure-handling logic of a production security system, a layer that has received little direct formal attention.
- Abstract（参考訳）: 各エンドポイントの軽量エージェントがスキャンされたファイルやプロセスから機能を収集し、分析のためにリモートサーバに送信し、ブロック、隔離、消毒によって返却されたバリデーションをローカルに強制する。
エンドポイントが判定に作用するため、検出を取り巻く分散マシンは、過渡的なサーバの障害を間違ったアクションにしてはいけない。
本稿では,Bitdefenderのプロダクションアーキテクチャから抽象化された,そのようなシステムのエンドポイント決定パイプラインの形式モデルであるPromelaを提案する。
プライマリ分析サーバがタイムアウトすると、エンドポイントは古いレガシプロトコールサーバにフォールバックし、判断を下す前に、それをローカライズしたローカルスキャンに失敗する。
検出シグネチャが音であると仮定し、線形時間論理(LTL)において6つの安全性と生存性を規定し、SPINモデルチェッカーで徹底的に検証する。
我々は、フォールバック機構が偽陽性(良心的ファイルに対する強制行動)を起こさないことを証明し、タイムアウト応答が遅れた場合でも、スキャン毎に正確に1つの判定をコミットし、明示的かつ順序的な方法でのみ検出強度を弱め、常に強制決定で終了するので、パイプラインはデッドロックフリーである。
各プロパティは非空き保持のためにチェックされ、コンカレントスキャンとエンドポイントによって状態空間がどのように成長するかを報告します。
この研究は、モデルチェックが製品セキュリティシステムの障害処理ロジックに対して強力な正当性を保証する方法を示している。
関連論文リスト
- ROPE: Routed Origin Policy Enforcement against Indirect Prompt Injection [61.4148196085256]
本稿では,信頼という構造概念に根ざしたROPE(Routed Origin Policy Enforcement)について述べる。
提案手法では,(1)軌道の各段階において,攻撃可能コンテンツのみを起点とする値が,原点保護パラメータに到達しない,(2)注入のリワードがない,という2つの保証が認められている。
論文 参考訳（メタデータ） (2026-08-27T01:22:14Z) - SCOUT: Symmetric Consensus Outlier Detection for Failure Localization in LLM Pre-Training [7.018753691717986]
事前トレーニングでは、同期は、ランクローカルなストール、スローダウン、数値的なエラーをジョブワイドな症状へと伝播し、その起源を隠蔽する。
SCOUTは1つの設計原則に基づいて構築された統一型ランタイム障害局所化フレームワークである。
SCOUTはトレーニングループやフレームワークソースの変更なしに、PyTorch、TorchTitan、Megatron-Core、DeepSpeedと統合されている。
論文 参考訳（メタデータ） (2026-08-11T15:12:14Z) - Early Detection of Distributed Backdoors in Multi-Agent LLM Systems: A Characterization Study [3.799596277597438]
マルチエージェントLLMシステムは、単一のエージェントが完全に保持しないペイロードによって攻撃される。
ランがまだ展開されている間、そのような攻撃がどれほど早く検出できるかを示す。
次に、その警告のどれ程が、その分散構造ではなく、取り外し可能な表面のキューにかかっているかを測定する。
論文 参考訳（メタデータ） (2026-07-27T15:18:06Z) - PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。
セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。
SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。
ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
論文 参考訳（メタデータ） (2026-07-18T04:46:53Z) - Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。
敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。
最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
論文 参考訳（メタデータ） (2026-04-14T06:48:33Z) - Towards Verifiable AI with Lightweight Cryptographic Proofs of Inference [3.3323431541048385]
完全証明を軽量なサンプリングベースアプローチで置き換える検証フレームワークとプロトコルを提案する。
我々は,機能的に異なるモデル間のトレース分離を活用可能な条件を定式化し,検証可能な推論プロトコルの安全性について議論する。
我々の手法は、最先端の暗号証明システムと比較して、証明時間を桁違いに削減する。
論文 参考訳（メタデータ） (2026-03-19T15:24:27Z) - Detecting Object Tracking Failure via Sequential Hypothesis Testing [80.7891291021747]
ビデオにおけるリアルタイムのオンラインオブジェクト追跡は、コンピュータビジョンにおける中核的なタスクである。
本稿では,物体追跡を逐次的仮説テストとして解釈することを提案する。
本研究では,地中追跡情報と内部追跡情報の両方を活用することにより,教師なしと教師なしの両方の変種を提案する。
論文 参考訳（メタデータ） (2026-02-13T14:57:15Z) - interwhen: A Generalizable Framework for Verifiable Reasoning with Test-time Monitors [47.363850513075356]
実験時間検証フレームワークであるInterwhenを提案し, 与えられた検証結果に対して, 推論モデルの出力が有効であることを保証する。
検証された推論は、物理的な世界にエージェントを配置するといった高度なシナリオにおいて重要な目標である。
論文 参考訳（メタデータ） (2026-02-05T08:35:01Z) - SHIELD: Secure Host-Independent Extensible Logging for Tamper-Proof Detection and Real-Time Mitigation of Ransomware Threats [17.861324495723487]
低レベルのモニタリングとネットワークブロックデバイス(NBD)技術を活用して,ディスクアクティビティの連続観察のためのオフホスト,タンパー保護計測を行うメトリクス取得フレームワークShiELDを紹介した。
私たちは、ディスクアクションの頻度に基づいて集約された単純なメトリクスとともに、深い機能を採用しています。
コンセプションのデプロイでは、ランサムウェア検出後の悪質なディスク操作を最小限のファイル損失とメモリ破損で停止させることにより、これらのメトリクスでトレーニングされたモデルを用いてリアルタイムな緩和を実演する。
論文 参考訳（メタデータ） (2025-01-28T01:33:03Z) - Detection as Regression: Certified Object Detection by Median Smoothing [50.89591634725045]
この研究は、ランダム化平滑化による認定分類の最近の進歩によって動機付けられている。
我々は、$ell$-bounded攻撃に対するオブジェクト検出のための、最初のモデル非依存、トレーニング不要、認定された防御条件を得る。
論文 参考訳（メタデータ） (2020-07-07T18:40:19Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。