論文の概要: Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis
- arxiv url: http://arxiv.org/abs/2607.08417v1
- Date: Thu, 09 Jul 2026 12:42:20 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-10 14:45:27.530238
- Title: Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis
- Title（参考訳）: ESBMC-PLC+を用いたIEC 61131-3 PLCプログラムにおけるラダー論理爆弾の検出:トリガー合成による形式的検証手法
- Abstract要約: Ladder Logic Bomb (LLB) はProgrammable Logic Controller (PLC) プログラムの悪意のある制御ロジックで、トリガーがペイロードを起動してアクチュエータの操作、センサの読み取り、オペレータの制御を無効にする。
本稿では,ESBMC-PLC+を検証エンジンとして使用するESBMC-LLBについて述べる。
パブリックなIacobelli 2024データセットでは、ESBMC-LLBは30発すべての爆弾を検出し、すべてのトリガーを回収する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: A Ladder Logic Bomb (LLB) is malicious control logic in a Programmable Logic Controller (PLC) program that lies dormant until a trigger activates a payload to manipulate actuators, forge sensor readings, or deny operator control. We observe that real malicious logic hides inside function-block bodies, which existing ladder-diagram verifiers drop from their intermediate representation (IR), making bombs invisible to provers. We present ESBMC-LLB, which uses ESBMC-PLC+ as its verification engine and adds a modeling layer that exposes function-block logic and recasts bomb detection as a formal verification problem: a scan-watchdog exposes non-termination payloads, and output wiring exposes actuator-forgery payloads as safety violations. k-induction gives an unbounded proof of bomb-absence across all scans, and the bounded model checker returns a counterexample that is the trigger - guarantees that signature, anomaly, and CFG-triage detectors lack. On the public Iacobelli 2024 dataset, ESBMC-LLB detects all 30 bombs and recovers every trigger; it also detects adaptive triggers (computed, opaque-arithmetic, multi-scan) that evade CFG-triage. We also report the first semantic model-checker evaluation on PLC-Defuser's SWaT corpus: our analog extension makes the full corpus parseable; on v1.0.0, it detects 149/150 bombs (99%) with zero false positives, recovering each trigger; on a later version with nonlinear non-termination bombs, detection drops to 49% as the SMT solver times out. We conclude that semantic model checking and CFG-triage are complementary - the former gives unbounded proofs, adaptive-trigger robustness, and handles Boolean/integer and linear analog logic; the latter leads to nonlinear analog non-termination, and we delineate where each wins.
- Abstract（参考訳）: Ladder Logic Bomb (LLB) はProgrammable Logic Controller (PLC) プログラムの悪意のある制御ロジックで、トリガーがペイロードを起動してアクチュエータの操作、センサの読み取り、オペレータの制御を無効にする。
我々は,既存のラダーダイアグラム検証器が中間表現(IR)から落とされた関数ブロック本体の中に,本当の悪意のある論理が隠されていることを観察した。
本稿では,ESBMC-PLC+を検証エンジンとして使用するESBMC-LLBについて,機能ブロックロジックを公開し,爆弾検出を形式的検証問題として再キャストするモデリングレイヤを付加する。
k-inductionは、すべてのスキャンに無拘束の爆弾の存在の証明を与え、バウンドモデルチェッカーは、トリガーである反例を返す。
パブリックなIacobelli 2024データセットでは、ESBMC-LLBは30発すべての爆弾を検出し、すべてのトリガーを回収する。
また,PLC-Defuser の SWaT コーパスに対する最初のセマンティック・モデル・チェッカー評価を報告する。私たちのアナログ拡張は全コーパスを解析可能とし,v1.0.0では149/150爆弾(99%)を検出,各トリガを回収し,非線形非終端爆弾を用いた後のバージョンでは,SMTソルバがタイムアウトすると49%まで低下する。
セマンティックモデルチェックとCFG-トリアージは相補的であり、前者は非有界証明、適応・トリガーの堅牢性を与え、ブール/整数および線形アナログ論理を扱う。
関連論文リスト
- CyberLLM: A Multi-Agent LLM Framework for Autonomous Detection and Guarded Response in Automotive Cybersecurity [22.68559728326395]
CyberLLMは、脆弱性を自律的に検出し、正式なランタイム安全ガードの下で修正を実行するフレームワークである。
決定エージェントは発見を集約し、人間中心のアセット分類でタグ付けし、タイレッド応答を選択する。
対称攻撃パイプラインはエクスプロイトを生成し再生し、両方のサイドを同じシナリオで実行することができる。
論文 参考訳（メタデータ） (2026-08-06T23:39:13Z) - Cybersecurity Detection Classification with Reasoning-enabled Language Models [50.72675435043546]
セキュリティオペレーションセンター(SOC)の大きな問題は、警告疲労である。
以前の作業では、大きな言語モデル(LLM)がトリアージラベルを直接出力するように促すか、あるいは微調整するが、検出が真の脅威であるかどうかを判断するよう訓練することはない。
我々は、実際の人間ラベルのWindowsエンドポイント検出に対して、推論可能なトリアージ分類器(CoT)を訓練する。
論文 参考訳（メタデータ） (2026-07-30T16:22:13Z) - From Detection to Action: Using LLM Agents for Fault-Tolerant Control [0.21313236831585222]
我々は,耐故障性制御のためのエージェント型大規模言語モデル(LLM)フレームワークを提案する。
故障検出出力を、植物固有の知識に基づく制約対応回復行動に変換する。
我々は,各プロセスのダイナミックスと互換性のある遅延予算内で,意味的基盤を持つエージェントが有効なリカバリ決定を導出できることを示す。
論文 参考訳（メタデータ） (2026-06-26T12:13:58Z) - CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
我々は、フロンティアモデル全体でのtextbfcontrol textbfintervention (CI) の認識を測定するベンチマークである textbfCIAware-Bench を紹介する。
CIAware-Benchは、モデルが自身の軌跡を制御介入によって修正されたものと区別できるかどうかをテストする。
論文 参考訳（メタデータ） (2026-06-09T16:24:16Z) - From Attack Simulation to SIEM Rule: Deterministic Detection-as-Code Synthesis with Probe-Level Traceability [51.56484100374058]
セキュリティチームは、自身のシステムに対する攻撃をシミュレートして、監視が真の侵入者を捕まえるかどうかをチェックする。
人間はそのギャップを手でブリッジし、それぞれの発見を読み、対応するシグマルールを書きます。
ロックされたコーパスからプローブが引き出されると,この変換が部分的に自動化されることを示す。
論文 参考訳（メタデータ） (2026-06-03T14:26:25Z) - Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。
敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。
最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
論文 参考訳（メタデータ） (2026-04-14T06:48:33Z) - Explainability-Guided Adversarial Attacks on Transformer-Based Malware Detectors Using Control Flow Graphs [0.19116784879310025]
本稿では,制御フローグラフを関数呼び出しのシーケンスに線形化するRoBERTaベースのマルウェア検出器の脆弱性について検討する。
このグラフ・ツー・シーケンス・フレームワーク内での回避戦略を評価することにより、トランスフォーマー・ベースのマルウェア検知器の実用的堅牢性について、集約的検出精度以上の知見を提供する。
論文 参考訳（メタデータ） (2026-04-04T19:50:04Z) - From Passive Monitoring to Active Defence: Resilient Control of Manipulators Under Cyberattacks [42.72791770760975]
FDIA(False Data Injection attack)は、アラームを発生させることなく、実質的なエンドエフェクタ偏差を発生させる。
本稿では、冗長マニピュレータのステルス型FDIAに対するレジリエンスについて検討し、パッシブモニタリングからアクティブディフェンスへアーキテクチャを進化させる。
論文 参考訳（メタデータ） (2026-03-13T14:08:41Z) - Beyond Reward Suppression: Reshaping Steganographic Communication Protocols in MARL via Dynamic Representational Circuit Breaking [0.0]
監視を回避するためのプライベートプロトコルを開発するエージェントによるステガノグラフィーの共謀は、AIの安全性に重大な脅威をもたらす。
既存の防御は行動層や報酬層に限られており、潜伏する通信路での調整を検知できない。
本稿では,動的表現回路ブレーカ(DRCB)について紹介する。
論文 参考訳（メタデータ） (2026-03-07T04:14:38Z) - A multi-layered embedded intrusion detection framework for programmable logic controllers [0.0]
本研究は,コントローラ内で動作し,ヘッダレベルのテレメトリを用いてネットワーク攻撃を検出し,応答する組込み侵入検知システムを提案する。
提案アーキテクチャは,産業システムのリアルタイム要件を満たす多層組込みセキュリティを提供する。
論文 参考訳（メタデータ） (2025-10-08T16:12:02Z) - Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
生成のための教師なし共形推論フレームワークを提案する。
我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。
その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
論文 参考訳（メタデータ） (2025-09-26T23:40: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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。