論文の概要: Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking

• arxiv url: http://arxiv.org/abs/2509.22215v1
• Date: Fri, 26 Sep 2025 11:29:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-29 20:57:54.388268
• Title: Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking
• Title（参考訳）: 自動学習とモデルチェックによるセキュリティテストの学習、チェック、テスト
• Authors: Stefan Marksteiner, Mikael Sjödin, Marjan Sirjani,
• Abstract要約: 外部通信インタフェースを用いたブラックボックスとしてのサイバー物理システムについて検討する。 まず、各プロトコルからモデルにコンテキスト情報をマッピングすることで、命題付きモデルにアノテートする。 基本的なセキュリティ要件に基づいて、一般的なセキュリティ特性を定義します。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Cyber-physical systems are part of industrial systems and critical infrastructure. Therefore, they should be examined in a comprehensive manner to verify their correctness and security. At the same time, the complexity of such systems demands such examinations to be systematic and, if possible, automated for efficiency and accuracy. A method that can be useful in this context is model checking. However, this requires a model that faithfully represents the behavior of the examined system. Obtaining such a model is not trivial, as many of these systems can be examined only in black box settings due to, e.g., long supply chains or secrecy. We therefore utilize active black box learning techniques to infer behavioral models in the form of Mealy machines of such systems and translate them into a form that can be evaluated using a model checker. To this end, we will investigate a cyber-physical systems as a black box using its external communication interface. We first annotate the model with propositions by mapping context information from the respective protocol to the model using Context-based Proposition Maps (CPMs). We gain annotated Mealy machines that resemble Kripke structures. We then formally define a template, to transfer the structures model checker-compatible format. We further define generic security properties based on basic security requirements. Due to the used CPMs, we can instantiate these properties with a meaningful context to check a specific protocol, which makes the approach flexible and scalable. The gained model can be easily altered to introduce non-deterministic behavior (like timeouts) or faults and examined if the properties still. Lastly, we demonstrate the versatility of the approach by providing case studies of different communication protocols (NFC and UDS), checked with the same tool chain and the same security properties.
• Abstract（参考訳）: サイバー物理システムは産業システムと重要なインフラの一部である。 したがって、それらの正しさと安全性を総合的に検証すべきである。 同時に、そのようなシステムの複雑さは、このような検査を体系的かつ可能であれば、効率と正確性のために自動化することを要求している。 この文脈で有用であるメソッドは、モデルチェックである。 しかし、これは検査されたシステムの振舞いを忠実に表現するモデルを必要とする。 このようなモデルを持つことは簡単ではない。例えば、長いサプライチェーンや機密性のために、ブラックボックス設定でのみ検査できるシステムが多いからだ。 そこで我々は,アクティブなブラックボックス学習技術を用いて,そのようなシステムのメアリーマシンの形で行動モデルを推論し,それらをモデルチェッカーを用いて評価可能な形式に変換する。 この目的のために,外部通信インタフェースを用いたブラックボックスとしてのサイバー物理システムについて検討する。 まず、各プロトコルのコンテキスト情報をコンテキストベースのプロポーズマップ(CPM)を用いてモデルにマッピングすることで、命題付きモデルにアノテートする。 我々はKripke構造に似た注釈付きMealyマシンを得る。 次に、正式にテンプレートを定義し、構造モデルチェッカー互換フォーマットを転送します。 さらに、基本的なセキュリティ要件に基づいて、一般的なセキュリティ特性を定義します。 使用されるCPMによって、特定のプロトコルをチェックするために意味のあるコンテキストでこれらのプロパティをインスタンス化できます。 得られたモデルは容易に変更でき、非決定論的動作(タイムアウトなど)や障害を導入し、その特性がまだ残っているかどうかを調べることができる。 最後に、異なる通信プロトコル(NFCとUDS)のケーススタディを提供し、同じツールチェーンと同じセキュリティプロパティでチェックすることで、このアプローチの汎用性を実証する。

関連論文リスト

• Interpretable Anomaly Detection in Encrypted Traffic Using SHAP with Machine Learning Models [0.0]
  本研究の目的は,暗号化されたネットワークトラフィックにおける異常検出のための解釈可能な機械学習ベースのフレームワークを開発することである。 モデルはトレーニングされ、3つのベンチマークで暗号化されたトラフィックデータセットで評価される。 SHAPビジュアライゼーションは、異常予測に寄与する最も影響力のあるトラフィック特徴を明らかにした。
  論文  参考訳（メタデータ） (2025-05-22T05:50:39Z)
• Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes [1.6078581568133972]
  ノイズの多いデータから直接システムの安全性を検証するための,データ駆動型安全性検証フレームワークを提案する。 1つの信頼できないモデルを信頼するのではなく、観測されたデータと整合する一連のモデルを構築します。 このモデル集合は行列ゾノトープを用いてコンパクトに表現され、効率的な計算と不確実性の伝播を可能にする。
  論文  参考訳（メタデータ） (2025-04-01T17:46:42Z)
• Predicting the Performance of Black-box LLMs through Self-Queries [60.87193950962585]
  大規模言語モデル(LLM)は、AIシステムにおいてますます頼りになってきている。 本稿では、フォローアッププロンプトを使用し、異なる応答の確率を表現として捉え、ブラックボックス方式でLCMの特徴を抽出する。 これらの低次元表現上で線形モデルをトレーニングすると、インスタンスレベルでのモデル性能の信頼性を予測できることを示す。
  論文  参考訳（メタデータ） (2025-01-02T22:26:54Z)
• Type-level Property Based Testing [0.0]
  本稿では,ソフトウェア仕様と依存型付けモデル,コンパイル時の実装の結合を統一する自動フレームワークを提案する。 いくつかの興味深いシステムやネットワークプロトコルをモデル化し、型チェッカーで実装が指定された動作であることを検証し、モデルが仕様のセマンティクスにマッチしていることをテストすることができます。
  論文  参考訳（メタデータ） (2024-07-17T16:43:41Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)
• Explaining RADAR features for detecting spoofing attacks in Connected Autonomous Vehicles [2.8153045998456188]
  コネクテッド・自動運転車(CAV)は、サイバー攻撃から守るためのAIシステムが組み込まれていると期待されている。 機械学習(ML)モデルは、このようなAIシステムの基盤となる。 本稿では,センサ入力におけるテキストの不確かさとテキスト不確かさを説明するモデルを提案する。
  論文  参考訳（メタデータ） (2022-03-01T00:11:46Z)

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

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