論文の概要: SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols
- arxiv url: http://arxiv.org/abs/2409.02918v1
- Date: Wed, 4 Sep 2024 17:54:29 GMT
- ステータス: 処理完了
- システム内更新日: 2024-09-05 16:37:56.144782
- Title: SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols
- Title(参考訳): SpecMon: セキュリティプロトコルのモジュールブラックボックスランタイム監視
- Authors: Kevin Morio, Robert Künnemann,
- Abstract要約: 我々は、アプリケーションがイベントストリームを取得するのに使用するネットワークと暗号化ライブラリを実装します。
次に、これらの観測結果を仕様モデルで有効なトレースにマッチングするために、効率的なアルゴリズムを使用します。
- 参考スコア(独自算出の注目度): 5.202524136984542
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: There exists a verification gap between formal protocol specifications and their actual implementations, which this work aims to bridge via monitoring for compliance to the formal specification. We instrument the networking and cryptographic library the application uses to obtain a stream of events. This is possible even without source code access. We then use an efficient algorithm to match these observations to traces that are valid in the specification model. In contrast to prior work, our algorithm can handle non-determinism and thus, multiple sessions. It also achieves a low overhead, which we demonstrate on the WireGuard reference implementation and a case study from prior work. We find that the reference Tamarin model for WireGuard can be used with little change: We only need to specify wire formats and correct some small inaccuracies that we discovered while conducting the case study. We also provide a soundness result for our algorithm that ensures it accepts only event streams that are valid according to the specification model.
- Abstract(参考訳): 正式なプロトコル仕様と実際の実装の間には検証のギャップがあり、この作業は、正式な仕様への準拠の監視を通じてブリッジすることを目的としています。
我々は、アプリケーションがイベントストリームを取得するのに使用するネットワークと暗号化ライブラリを実装します。
これはソースコードアクセスなしでも可能である。
次に、これらの観測結果を仕様モデルで有効なトレースにマッチングするために、効率的なアルゴリズムを使用します。
従来の作業とは対照的に,アルゴリズムは非決定性を扱うことができ,複数のセッションを処理できる。
また、WireGuard参照実装と先行作業のケーススタディで示すように、オーバーヘッドも低くなります。
WireGuardの参照Tamarinモデルは、ほとんど変更を加えることなく使用できることがわかった。
また,提案アルゴリズムは,仕様モデルに従って有効なイベントストリームのみを受け入れることを保証する。
関連論文リスト
- Are you still on track!? Catching LLM Task Drift with Activations [55.75645403965326]
大規模言語モデル(LLM)は、ユーザや他のソースからの入力を処理したり、タスクを編成したりするための検索拡張されたアプリケーションで日常的に使用される。
これにより、LDMがデータのみのソースからの命令を受け取り、作用するインジェクション攻撃を誘導する扉が開き、ユーザーの元の命令から逸脱する。
我々はこれをタスクドリフトと定義し、LCMのアクティベーションをスキャンして解析することでこれをキャッチすることを提案する。
このアプローチは、これらの攻撃に対してトレーニングを受けることなく、インジェクションやジェイルブレイク、悪意のある指示など、目に見えないタスクドメインに対して驚くほどうまく一般化することを示す。
論文 参考訳(メタデータ) (2024-06-02T16:53:21Z) - DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
プロパティベースのテストはセキュアプロトコルのセキュリティバグの検出に有効である。
セキュアマルチパーティ計算(MPC)を特に対象とする。
MPCプロトコルのビットレベル実装において,様々な欠陥を検出するテストを作成する。
論文 参考訳(メタデータ) (2024-03-08T02:02:24Z) - Model Pairing Using Embedding Translation for Backdoor Attack Detection
on Open-Set Classification Tasks [51.78558228584093]
バックドア検出のためのオープンセット分類タスクにモデルペアを用いることを提案する。
両モデルがバックドアされている場合でも,バックドアが検出可能であることを示す。
論文 参考訳(メタデータ) (2024-02-28T21:29:16Z) - Unsupervised Continual Anomaly Detection with Contrastively-learned
Prompt [80.43623986759691]
UCADと呼ばれる新しい非教師付き連続異常検出フレームワークを提案する。
このフレームワークは、対照的に学習したプロンプトを通じて、UDAに継続的な学習能力を持たせる。
我々は総合的な実験を行い、教師なし連続異常検出とセグメンテーションのベンチマークを設定した。
論文 参考訳(メタデータ) (2024-01-02T03:37:11Z) - Publicly-Detectable Watermarking for Language Models [45.32236917886154]
LLMの高精度かつ信頼性の高い透かし方式を提案する。
このアルゴリズムは秘密情報を含んでおらず、誰でも実行可能である。
提案手法は, 暗号的に正しい, 音響的, 歪みのないものであることを実証する。
論文 参考訳(メタデータ) (2023-10-27T21:08:51Z) - A Security Verification Framework of Cryptographic Protocols Using
Machine Learning [0.0]
機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。
ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。
提案手法を実用的な暗号プロトコルの検証に適用して評価する。
論文 参考訳(メタデータ) (2023-04-26T02:37:43Z) - Robustness of implemented device-independent protocols against
constrained leakage [0.0]
デバイス非依存(DI)プロトコルは近年大きな進歩を遂げている。
これらのデモのセキュリティ証明は、DI暗号の典型的な前提に依存しており、デバイスは互いに望ましくない情報を漏らさないし、敵にも漏らさない。
論文 参考訳(メタデータ) (2023-02-27T16:28:23Z) - Black-box Dataset Ownership Verification via Backdoor Watermarking [67.69308278379957]
我々は、リリースデータセットの保護を、(目立たしい)サードパーティモデルのトレーニングに採用されているかどうかの検証として定式化する。
バックドアの透かしを通じて外部パターンを埋め込んでオーナシップの検証を行い,保護することを提案する。
具体的には、有毒なバックドア攻撃(例えばBadNets)をデータセットのウォーターマーキングに利用し、データセット検証のための仮説テストガイダンスメソッドを設計する。
論文 参考訳(メタデータ) (2022-08-04T05:32:20Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。
AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文 参考訳(メタデータ) (2021-09-25T22:53:24Z) - On the Importance of Encrypting Deep Features [15.340540198612823]
ユーザデータの特徴ベクトルが知られ、推論のためのブラックボックスAPIが提供される。
個人再識別における最先端モデルの実験を行い,2つの攻撃シナリオ(補助属性の認識とユーザデータの再構築)について検討した。
その結果、厳しい制約下であっても、敵は機密情報を推測することに成功した。
論文 参考訳(メタデータ) (2021-08-16T15:22:33Z) - Pseudo-IoU: Improving Label Assignment in Anchor-Free Object Detection [60.522877583407904]
現在のアンカーフリー物体検出器は非常に単純で有効であるが、正確なラベル割り当て方法がない。
Pseudo-Intersection-over-Union(Pseudo-IoU): アンカーフリーなオブジェクト検出フレームワークに、より標準化され、正確な割り当てルールをもたらす単純なメトリックである。
本手法はベルやホイッスルを使わずに最新のアンカーフリー手法と同等の性能を実現する。
論文 参考訳(メタデータ) (2021-04-29T02:48:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。