論文の概要: CryptoBap: A Binary Analysis Platform for Cryptographic Protocols

• arxiv url: http://arxiv.org/abs/2308.14450v2
• Date: Mon, 18 Sep 2023 06:16:02 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-19 07:22:30.510881
• Title: CryptoBap: A Binary Analysis Platform for Cryptographic Protocols
• Title（参考訳）: CryptoBap: 暗号化プロトコルのバイナリ分析プラットフォーム
• Authors: Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati,
• Abstract要約: 暗号プロトコルの弱い秘密と認証を検証するプラットフォームであるCryptoBapを紹介する。 まずプロトコルのバイナリを中間表現に変換し、次に暗号対応のシンボル実行を実行する。 提案手法の健全性を実証し,CryptoBapを用いて,おもちゃの例から実世界のプロトコルまで,複数のケーススタディを検証した。
• 参考スコア（独自算出の注目度）: 6.514727189942011
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic execution resolves indirect jumps and supports bounded loops using the loop-summarization technique, which we fully automate. The extracted model is then translated into models amenable to automated verification via ProVerif and CryptoVerif using a third-party toolchain. We prove the soundness of the proposed approach and used CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols, TinySSH, an implementation of SSH, and WireGuard, a modern VPN protocol.
• Abstract（参考訳）: 暗号プロトコルの(ARMv8およびRISC-V)マシンコードに対する弱い秘密と認証を検証するためのプラットフォームであるCryptoBapを紹介する。 まずプロトコルのバイナリを中間表現にトランスパイルし、次に暗号対応のシンボル実行を実行して、すべての実行パスを表すプロトコルのモデルを自動的に抽出する。 我々のシンボリックな実行は間接ジャンプを解消し、完全に自動化されたループ要約技術を用いて有界ループをサポートする。 抽出されたモデルは、サードパーティのツールチェーンを使用して、ProVerifとCryptoVerifを介して自動検証が可能なモデルに変換される。 提案手法の健全さを実証し,CryptoBapを用いて,おもちゃの例から実世界のプロトコルまで,TinySSH,SSHの実装,最新のVPNプロトコルであるWireGuardの複数のケーススタディを検証する。

関連論文リスト

• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  本稿では,Byzantine-fault Tolerant(BFT)コンセンサスプロトコルを用いた,しきい値暗号とブロックチェーンのクラス間の相互作用について検討する。 しきい値暗号システムに対する既存のアプローチは、しきい値暗号プロトコルを実行するための少なくとも1つのメッセージ遅延の遅延オーバーヘッドを導入している。 しきい値が狭いブロックチェーンネイティブのしきい値暗号システムに対して,このオーバーヘッドを取り除く機構を提案する。
  論文  参考訳（メタデータ） (2024-07-16T20:53:04Z)
• Point Intervention: Improving ACVP Test Vector Generation Through Human Assisted Fuzzing [1.6651146574124565]
  本稿では,暗号ライブラリのACVPフォーマットで良好なテストを生成するための方法とツールを提供する。 本システムは,暗号プリミティブをファジリングするためのハイブリッドアプローチを用いて,既存のファジリング手法よりも優れたカバレッジを実現する。
  論文  参考訳（メタデータ） (2024-07-11T14:21:48Z)
• Parallel Decoding via Hidden Transfer for Lossless Large Language Model Acceleration [54.897493351694195]
  本稿では,複数連続するトークンを1つのフォワードパスで同時に復号する,新しい並列復号法,すなわちthithidden Transferを提案する。 加速度測定では,Medusa や Self-Speculative decoding など,単モデル加速技術よりも優れています。
  論文  参考訳（メタデータ） (2024-04-18T09:17:06Z)
• CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
  この文書はセキュリティプロトコル検証器CryptoVerifを示す。 これはシンボリックなドレフ・ヤオモデルではなく、計算モデルに依存している。 自動で動作させることもできるし、手動による証明表示でガイドすることもできる。
  論文  参考訳（メタデータ） (2023-10-23T07:53:38Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。 主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。 理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
  論文  参考訳（メタデータ） (2023-05-20T11:26:51Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。 ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。 提案手法を実用的な暗号プロトコルの検証に適用して評価する。
  論文  参考訳（メタデータ） (2023-04-26T02:37:43Z)
• Publicly-Verifiable Deletion via Target-Collapsing Functions [81.13800728941818]
  ターゲットの折り畳みは、公開可能な削除(PVD)を可能にすることを示す。 我々は、弱い暗号的仮定から公開可能な削除を支援する様々なプリミティブを得るために、このフレームワークを構築している。
  論文  参考訳（メタデータ） (2023-03-15T15:00:20Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。 ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。 これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
  論文  参考訳（メタデータ） (2022-05-20T12:37:09Z)
• Composably secure data processing for Gaussian-modulated continuous variable quantum key distribution [58.720142291102135]
  連続可変量子鍵分布(QKD)は、ボソニックモードの二次構造を用いて、2つのリモートパーティ間の秘密鍵を確立する。 構成可能な有限サイズセキュリティの一般的な設定におけるホモダイン検出プロトコルについて検討する。 特に、ハイレート(非バイナリ)の低密度パリティチェックコードを使用する必要のあるハイシグネチャ・ツー・ノイズ・システマを解析する。
  論文  参考訳（メタデータ） (2021-03-30T18:02:55Z)
• Deep Reinforcement Learning with Label Embedding Reward for Supervised Image Hashing [85.84690941656528]
  深層型ハッシュのための新しい意思決定手法を提案する。 我々はBose-Chaudhuri-Hocquenghem符号で定義された新しいラベル埋め込み報酬を用いて、深いQ-ネットワークを学ぶ。 我々の手法は、様々なコード長で最先端の教師付きハッシュ法より優れています。
  論文  参考訳（メタデータ） (2020-08-10T09:17:20Z)

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

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