論文の概要: SMT-Boosted Security Types and Correctness for Low-Level MPC
- arxiv url: http://arxiv.org/abs/2610.22047v1
- Date: Thu, 15 Oct 2026 15:16:32 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-17 06:09:33.144252
- Title: SMT-Boosted Security Types and Correctness for Low-Level MPC
- Title(参考訳): SMT-Boosted Security Types and correctness for Low-Level MPC
- Abstract要約: 我々は、Prelude/Overture言語フレームワークで記述されたプロトコルの正当性、機密性、整合性を自動的に適用する新しいHoare論理と型理論を開発した。
我々のアプローチは構成的、スケーラブルで、任意の素体と秘密共有スキームに一般化される。
- 参考スコア(独自算出の注目度): 1.8051006704301766
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. We develop a new Hoare logic and type theory to automatically enforce correctness, confidentiality, and integrity properties of protocols written in the Prelude/Overture language framework. Both definition and automation of our analyses leverages SMT verification, supporting precision and efficiency. Our approach is compositional, scalable, and generalizes to arbitrary prime fields and secret sharing schemes.
- Abstract(参考訳): Secure Multi-Party Computation (MPC)は、現代の分散アプリケーションにおけるデータプライバシを実現する重要な技術である。
我々は、Prelude/Overture言語フレームワークで記述されたプロトコルの正当性、機密性、整合性を自動的に適用する新しいHoare論理と型理論を開発した。
分析手法の定義と自動化は、SMT検証を活用し、精度と効率を向上する。
我々のアプローチは構成的、スケーラブルで、任意の素体と秘密共有スキームに一般化される。
関連論文リスト
- Provably Secure Steganography Based on List Decoding [5.421129051557276]
ステガノグラフィーは、監視下の秘密通信のために、一見無害なキャリアに秘密のメッセージを埋め込む。
現在のセキュアなステガノグラフィースキームは、表紙と表紙の区別が難しいことを保証できる。
理論的に証明された高容量な確実なステガノグラフィー手法を提案する。
論文 参考訳(メタデータ) (2026-04-23T08:02:21Z) - Federated Attention: A Distributed Paradigm for Collaborative LLM Inference over Edge Networks [63.541114376141735]
大規模言語モデル(LLM)は、さまざまなアプリケーションシナリオにまたがってインテリジェントな機能を提供しながら、急速に普及しています。
しかし、彼らの共同シナリオにおける実践的なデプロイは、プライバシの脆弱性、通信オーバーヘッド、計算ボトルネックといった根本的な課題に直面します。
我々はフェデレート・アテンション(FedAttn)を提案し、フェデレーション・パラダイムを自己注意機構に統合する。
論文 参考訳(メタデータ) (2025-11-04T15:14:58Z) - Optimizing Privacy-Preserving Primitives to Support LLM-Scale Applications [13.665746704069837]
本稿では,プライバシー保護学習システムにおける,このオーバーヘッドと実践性のギャップを埋めるための取り組みの概要を紹介する。
プライバシー保護設定におけるLLMスケールアプリケーションの実現に向けた進展を示す。
論文 参考訳(メタデータ) (2025-09-29T17:16:51Z) - Information-Theoretic Decentralized Secure Aggregation with Collusion Resilience [95.33295072401832]
情報理論の観点から分散型セキュアアグリゲーション(DSA)の問題点を考察する。
DSAの最小到達可能な通信量と秘密鍵率を指定する最適レート領域を特徴付ける。
本研究は,DSAの基本性能限界を確立し,信頼性の高い通信効率の高いプロトコルの設計に関する知見を提供する。
論文 参考訳(メタデータ) (2025-08-01T12:51:37Z) - Graft: Integrating the Domain Knowledge via Efficient Parameter Synergy for MLLMs [56.76586846269894]
MLLM(Multimodal Large Language Models)は、様々な領域で成功している。
その重要性にもかかわらず、ドメイン固有のMLLM間の知識共有の研究はほとんど未調査のままである。
専門家機能のモジュール構成を可能にする統一パラメータ統合フレームワークを提案する。
論文 参考訳(メタデータ) (2025-06-30T15:07:41Z) - SMT-Boosted Security Types for Low-Level MPC [2.798211113992669]
我々は,emphPrelude/Overture言語フレームワークで記述されたプロトコルの正当性,機密性,整合性を自動的に適用する新しい型理論を開発した。
我々のアプローチは、データとキーサイズに対する任意の素体に自動化され、構成され、拡張され、一般化されます。
論文 参考訳(メタデータ) (2025-01-29T18:16:20Z) - The Communication-Friendly Privacy-Preserving Machine Learning against Malicious Adversaries [14.232901861974819]
プライバシー保護機械学習(PPML)は、機密情報を保護しながらセキュアなデータ分析を可能にする革新的なアプローチである。
セキュアな線形関数評価のための効率的なプロトコルを導入する。
我々は、このプロトコルを拡張して、線形層と非線形層を扱い、幅広い機械学習モデルとの互換性を確保する。
論文 参考訳(メタデータ) (2024-11-14T08:55:14Z) - Language-Based Security for Low-Level MPC [2.798211113992669]
マルチパーティ計算は、現代の分散アプリケーションにおけるデータプライバシを実現する重要な技術である。
現在、低レベルのMPCプロトコルの証明方法は、主に手作業であり、退屈でエラーを起こしやすい。
我々は、様々な低レベルの確率的MPCプロトコルを定義するための新しい段階的なPLを開発した。
論文 参考訳(メタデータ) (2024-07-23T14:21:27Z) - Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive
Privacy Analysis and Beyond [57.10914865054868]
垂直ロジスティック回帰(VLR)をミニバッチ降下勾配で訓練した。
我々は、オープンソースのフェデレーション学習フレームワークのクラスにおいて、VLRの包括的で厳密なプライバシー分析を提供する。
論文 参考訳(メタデータ) (2022-07-19T05:47:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。