論文の概要: CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection

• arxiv url: http://arxiv.org/abs/2411.13627v1
• Date: Wed, 20 Nov 2024 14:16:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-22 15:19:42.354578
• Title: CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection
• Title（参考訳）: CryptoFormalEval: 自動暗号プロトコル脆弱性検出のためのLCMと形式検証の統合
• Authors: Cristian Curaba, Denis D'Ambrosi, Alessandro Minisini, Natalia Pérez-Campanero Antolín,
• Abstract要約: 我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
• 参考スコア（独自算出の注目度）: 41.94295877935867
• License:
• Abstract: Cryptographic protocols play a fundamental role in securing modern digital infrastructure, but they are often deployed without prior formal verification. This could lead to the adoption of distributed systems vulnerable to attack vectors. Formal verification methods, on the other hand, require complex and time-consuming techniques that lack automatization. In this paper, we introduce a benchmark to assess the ability of Large Language Models (LLMs) to autonomously identify vulnerabilities in new cryptographic protocols through interaction with Tamarin: a theorem prover for protocol verification. We created a manually validated dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents. Our results about the performances of the current frontier models on the benchmark provides insights about the possibility of cybersecurity applications by integrating LLMs with symbolic reasoning systems.
• Abstract（参考訳）: 暗号プロトコルは現代のデジタルインフラの確保において基本的な役割を担っているが、しばしば事前の正式な検証なしに展開される。 これにより、攻撃ベクトルに弱い分散システムが採用される可能性がある。 一方、形式的検証手法では、自動化に欠ける複雑で時間を要する。 本稿では,玉林との対話を通じて,新たな暗号プロトコルの脆弱性を自律的に識別するLarge Language Models (LLM) の能力を評価するためのベンチマークを提案する。 我々は、新しい、欠陥のある通信プロトコルを手動で検証したデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計した。 ベンチマークにおける現在のフロンティアモデルの性能に関する我々の結果は、LLMと象徴的推論システムを統合することで、サイバーセキュリティアプリケーションの可能性についての洞察を提供する。

関連論文リスト

• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach [3.9155346446573502]
  本稿では,5GおよびNextGプロトコル(AVRE)のための実世界プロンプトを用いた形式検証の自動モデリングを提案する。 AVREは次世代通信プロトコル(NextG)の正式な検証のために設計された新しいシステムである。
  論文  参考訳（メタデータ） (2023-12-28T20:41:24Z)
• Securing Graph Neural Networks in MLaaS: A Comprehensive Realization of Query-based Integrity Verification [68.86863899919358]
  我々は機械学習におけるGNNモデルをモデル中心の攻撃から保護するための画期的なアプローチを導入する。 提案手法は,GNNの完全性に対する包括的検証スキーマを含み,トランスダクティブとインダクティブGNNの両方を考慮している。 本稿では,革新的なノード指紋生成アルゴリズムを組み込んだクエリベースの検証手法を提案する。
  論文  参考訳（メタデータ） (2023-12-13T03:17:05Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。 モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
  論文  参考訳（メタデータ） (2023-08-25T15:25:57Z)
• SoK: Realistic Adversarial Attacks and Defenses for Intelligent Network Intrusion Detection [0.0]
  本稿では,現実的な実例を生み出すことのできる,最先端の対人学習アプローチの統合と要約を行う。 これは、逆例が現実的であるために必要な基本的性質を定義する。 研究者が将来の実験が実際の通信ネットワークに適切であることを確実にするためのガイドラインを提供する。
  論文  参考訳（メタデータ） (2023-08-13T17:23:36Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。 ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。 提案手法を実用的な暗号プロトコルの検証に適用して評価する。
  論文  参考訳（メタデータ） (2023-04-26T02:37:43Z)
• Auto.gov: Learning-based On-chain Governance for Decentralized Finance (DeFi) [18.849149890999687]
  分散型金融(DeFi)プロトコルはオフチェーンガバナンスを採用しており、トークン保有者がパラメータの変更に投票する。 しかしながら、プロトコルのコアチームがしばしば行う手動パラメータ調整は、システムの完全性とセキュリティを損なうことなく、衝突に対して脆弱である。 我々は、DeFiのための学習ベースのオンチェーンガバナンスフレームワークであるAuto.govを紹介し、セキュリティを強化し、攻撃に対する感受性を低減する。
  論文  参考訳（メタデータ） (2023-02-19T12:11:41Z)
• CC-Cert: A Probabilistic Approach to Certify General Robustness of Neural Networks [58.29502185344086]
  安全クリティカルな機械学習アプリケーションでは、モデルを敵の攻撃から守ることが不可欠である。 意味的に意味のある入力変換に対して、ディープラーニングモデルの証明可能な保証を提供することが重要である。 我々はChernoff-Cramer境界に基づく新しい普遍確率的証明手法を提案する。
  論文  参考訳（メタデータ） (2021-09-22T12:46:04Z)

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

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