論文の概要: DT-SIM: Property-Based Testing for MPC Security

• arxiv url: http://arxiv.org/abs/2403.04991v2
• Date: Tue, 12 Mar 2024 01:07:49 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-17 13:47:35.118812
• Title: DT-SIM: Property-Based Testing for MPC Security
• Title（参考訳）: DT-SIM: MPCセキュリティのためのプロパティベースのテスト
• Authors: Mako Bates, Joseph P. Near,
• Abstract要約: プロパティベースのテストはセキュアプロトコルのセキュリティバグの検出に有効である。 セキュアマルチパーティ計算(MPC)を特に対象とする。 MPCプロトコルのビットレベル実装において,様々な欠陥を検出するテストを作成する。
• 参考スコア（独自算出の注目度）: 2.0308771704846245
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal methods for guaranteeing that a protocol satisfies a cryptographic security definition have advanced substantially, but such methods are still labor intensive and the need remains for an automated tool that can positively identify an insecure protocol. In this work, we demonstrate that property-based testing, "run it a bunch of times and see if it breaks", is effective for detecting security bugs in secure protocols. We specifically target Secure Multi-Party Computation (MPC), because formal methods targeting this security definition for bit-model implementations are particularly difficult. Using results from the literature for Probabilistic Programming Languages and statistical inference, we devise a test that can detect various flaws in a bit-level implementation of an MPC protocol. The test is grey-box; it requires only transcripts of randomness consumed by the protocol and of the inputs, outputs, and messages. It successfully detects several different mistakes and biases introduced into two different implementations of the classic GMW protocol. Applied to hundreds of randomly generated protocols, it identifies nearly all of them as insecure. We also include an analysis of the parameters of the test, and discussion of what makes detection of MPC (in)security difficult.
• Abstract（参考訳）: プロトコルが暗号化のセキュリティ定義を満たすことを保証するための形式的手法は大幅に進歩しているが、そのような手法は依然として労働集約的であり、安全でないプロトコルを肯定的に識別できる自動化ツールの必要性が残っている。 この研究では、プロパティベースのテストである“何度も実行して、それが壊れているかどうかを確認する”ことが、セキュアなプロトコルのセキュリティバグの検出に有効であることを実証しています。 ビットモデル実装に対するこのセキュリティ定義を対象とする形式的手法は特に難しいため,特にMPC(Secure Multi-Party Computation)を対象とする。 MPCプロトコルのビットレベル実装において,確率型プログラミング言語の文献と統計的推論の結果を用いて,様々な欠陥を検出するテストを開発した。 テストはグレーボックスで、プロトコルと入力、出力、メッセージによって消費されるランダム性の書き起こしのみを必要とする。 古典的なGMWプロトコルの2つの異なる実装に導入されたいくつかの異なる誤りとバイアスを検出することに成功した。 何百ものランダムに生成されたプロトコルに適用すると、ほとんどすべてのプロトコルが安全でないと識別される。 また、テストのパラメータの分析や、MPC(in)セキュリティの検出を困難にしているのは何かという議論も含んでいる。

関連論文リスト

• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• Pretraining Data Detection for Large Language Models: A Divergence-based Calibration Method [108.56493934296687]
  本研究では,乱数から発散する概念に触発された偏差に基づくキャリブレーション手法を導入し,プリトレーニングデータ検出のためのトークン確率のキャリブレーションを行う。 我々は,中国語テキスト上でのLLMの検出手法の性能を評価するために,中国語のベンチマークであるPatentMIAを開発した。
  論文  参考訳（メタデータ） (2024-09-23T07:55:35Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。 ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。 提案手法を実用的な暗号プロトコルの検証に適用して評価する。
  論文  参考訳（メタデータ） (2023-04-26T02:37:43Z)
• Single-photon-memory measurement-device-independent quantum secure direct communication [63.75763893884079]
  量子セキュアダイレクト通信(QSDC)は、量子チャネルを使用して情報を確実かつ安全に送信する。 実用検出器によるセキュリティの抜け穴を取り除くため,測定デバイス非依存(MDI)QSDCプロトコルが提案されている。 高速な量子メモリを不要とする単一光子メモリ MDI QSDC プロトコル (SPMQC) を提案する。
  論文  参考訳（メタデータ） (2022-12-12T02:23:57Z)
• Towards Semantic Communication Protocols: A Probabilistic Logic Perspective [69.68769942563812]
  我々は,NPMを確率論理型言語ProbLogで記述された解釈可能なシンボルグラフに変換することによって構築された意味プロトコルモデル(SPM)を提案する。 その解釈性とメモリ効率を利用して、衝突回避のためのSPM再構成などのいくつかの応用を実演する。
  論文  参考訳（メタデータ） (2022-07-08T14:19:36Z)
• Unifying Quantum Verification and Error-Detection: Theory and Tools for Optimisations [0.5825410941577593]
  クラウドベースの量子コンピューティングは、クライアントによって量子サービスプロバイダに委譲された計算が忠実に実行されるという強力な保証を提供するために不可欠である。 現在のプロトコルには、コンポーザビリティ、ノイズ・ロバスト性、モジュール性という3つの要素の少なくとも1つが欠落している。 本稿では,SDQCプロトコルの基本構造,すなわちクライアントがサーバの実行を希望する暗号化と,サーバの悪意のある動作を検出するように設計されたテストの2つのコンポーネントを混合する。 テストの種類を変えたり、クライアントの計算と混同したりすると、セキュリティとノイズの異なる新しいSDQCプロトコルが自動的に生成される。
  論文  参考訳（メタデータ） (2022-06-01T17:03:07Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。 ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。 これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
  論文  参考訳（メタデータ） (2022-05-20T12:37:09Z)
• Unbalanced-basis-misalignment tolerant measurement-device-independent quantum key distribution [22.419105320267523]
  測定デバイスに依存しない量子鍵分布(MDIQKD)は、検出側の全ての攻撃に対して物理的に免疫があるため、革命的なプロトコルである。 一部のプロトコルは、実際のセキュリティを維持するためにエンコードシステムの前提の一部を解放するが、性能は劇的に低下する。 本稿では,不都合な変調エラーやゆらぎに対処するために,符号化システムの知識を少なくするMDIQKDプロトコルを提案する。
  論文  参考訳（メタデータ） (2021-08-27T02:16:20Z)
• Composably secure data processing for Gaussian-modulated continuous variable quantum key distribution [58.720142291102135]
  連続可変量子鍵分布(QKD)は、ボソニックモードの二次構造を用いて、2つのリモートパーティ間の秘密鍵を確立する。 構成可能な有限サイズセキュリティの一般的な設定におけるホモダイン検出プロトコルについて検討する。 特に、ハイレート(非バイナリ)の低密度パリティチェックコードを使用する必要のあるハイシグネチャ・ツー・ノイズ・システマを解析する。
  論文  参考訳（メタデータ） (2021-03-30T18:02:55Z)
• Twin-field quantum digital signatures [4.503555294002338]
  デジタルシグネチャ(Digital signature)は、情報セキュリティ、特にID認証において重要な技術である。 量子デジタルシグネチャ(QDS)は、情報理論のセキュリティなど、より高度なセキュリティを提供する。
  論文  参考訳（メタデータ） (2020-03-25T08:04:59Z)

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

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