論文の概要: Smart Casual Verification of CCF's Distributed Consensus and Consistency Protocols
- arxiv url: http://arxiv.org/abs/2406.17455v1
- Date: Tue, 25 Jun 2024 10:49:54 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-26 14:42:03.057712
- Title: Smart Casual Verification of CCF's Distributed Consensus and Consistency Protocols
- Title（参考訳）: CCFの分散コンセンサスと一貫性プロトコルのスマートカジュアル検証
- Authors: Heidi Howard, Markus A. Kuppe, Edward Ashton, Amaury Chamayou, Natacha Crooks,
- Abstract要約: Confidential Consortium Framework(CCF)は、信頼できる信頼性のあるクラウドアプリケーションを開発するためのオープンソースプラットフォームである。
CCFはMicrosoftのAzure Confidential Ledgerサービスを動かしている。
本稿では、CCFの新しい分散プロトコルの正当性を検証するために、スマートカジュアル検証を適用した経験を報告する。
- 参考スコア（独自算出の注目度）: 2.160395257762205
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The Confidential Consortium Framework (CCF) is an open-source platform for developing trustworthy and reliable cloud applications. CCF powers Microsoft's Azure Confidential Ledger service and as such it is vital to build confidence in the correctness of CCF's design and implementation. This paper reports our experiences applying smart casual verification to validate the correctness of CCF's novel distributed protocols, focusing on its unique distributed consensus protocol and its custom client consistency model. We use the term smart casual verification to describe our hybrid approach, which combines the rigor of formal specification and model checking with the pragmatism of automated testing, in our case binding the formal specification in TLA+ to the C++ implementation. While traditional formal methods approaches require substantial buy-in and are often one-off efforts by domain experts, we have integrated our smart casual verification approach into CCF's continuous integration pipeline, allowing contributors to continuously validate CCF as it evolves. We describe the challenges we faced in applying smart casual verification to a complex existing codebase and how we overcame them to find subtle bugs in the design and implementation before they could impact production.
- Abstract（参考訳）: Confidential Consortium Framework(CCF)は、信頼できる信頼性のあるクラウドアプリケーションを開発するためのオープンソースプラットフォームである。
CCFはMicrosoftのAzure Confidential Ledgerサービスを動かしているため、CCFの設計と実装の正確性に対する信頼性を構築することが不可欠である。
本稿では、CCFの新しい分散プロトコルの正当性を検証するために、スマートカジュアル検証を適用した経験を報告する。
我々はスマートカジュアル検証という用語を使って,形式仕様の厳密さと自動テストの実用性を備えたモデルチェックを組み合わせたハイブリッドアプローチを記述しています。
従来の形式的なアプローチでは、かなりの買い入れが必要で、ドメインの専門家によるワンオフの取り組みも少なくありませんが、私たちはスマートカジュアルな検証アプローチをCCFの継続的インテグレーションパイプラインに統合し、コントリビュータがCCFの進化を継続的に検証できるようにしています。
私たちは、複雑なコードベースにスマートカジュアルな検証を適用する上で直面した課題と、運用に影響を与える前に設計と実装の微妙なバグを見つけるためにそれらを克服する方法について説明します。
関連論文リスト
- Analogous Alignments: Digital "Formally" meets Analog [0.0]
本稿では,デジタルブロックとアナログブロックを組み合わせた混合信号知的特性(IP)の実用的形式検証に着目する。
Digital and Analog Mixed-Signal (AMS)設計は、本質的に異なるが、形式的な検証設定でシームレスに統合される。
論文 参考訳（メタデータ） (2024-09-23T13:38:31Z) - Collaborative CP-NIZKs: Modular, Composable Proofs for Distributed Secrets [3.3373764108905455]
構成性により、ユーザーは異なるNIZKを組み合わせられる。
我々は、NIZKのコラボレーティブ・コミット・アンド・プロブのための、最初の一般的な定義を示す。
論文 参考訳（メタデータ） (2024-07-27T08:45:34Z) - Formally Certified Approximate Model Counting [25.20597060311209]
本稿では、その出力近似の品質に関する保証を正式に保証した、近似モデルカウントのための最初の認証フレームワークを提案する。
i)Isabelle/HOL証明アシスタントにおけるアルゴリズムのPAC保証の静的かつ1回限りの公式な証明、(ii)証明証明書を用いた外部CNF-XORソルバに対するApproxMCの呼び出しの動的かつ1回実行による検証。
論文 参考訳（メタデータ） (2024-06-17T11:02:04Z) - 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) - Efficient Conformal Prediction under Data Heterogeneity [79.35418041861327]
コンフォーマル予測(CP)は不確実性定量化のための頑健な枠組みである。
非交換性に対処するための既存のアプローチは、最も単純な例を超えて計算不可能なメソッドにつながる。
この研究は、比較的一般的な非交換可能なデータ分布に対して証明可能な信頼セットを生成する、CPに新しい効率的なアプローチを導入する。
論文 参考訳（メタデータ） (2023-12-25T20:02:51Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - Provably Secure Commitment-based Protocols over Unauthenticated Channels [0.0]
我々は、認証された交換のための既存のモデルと必ずしも一致しない可能性のあるプロトコルをカバーするための理論的なセキュリティフレームワークを構築している。
本稿では,両当事者間の共通秘密を確立するためのコミットベースのプロトコルをいくつか提案し,その非認証チャネルに対する抵抗性について検討する。
これは、プロトコル自体のセキュリティの堅牢性、およびMan-in-the-Middle攻撃に対する堅牢性を分析することを意味する。
論文 参考訳（メタデータ） (2023-07-28T10:35:35Z) - Federated Conformal Predictors for Distributed Uncertainty
Quantification [83.50609351513886]
コンフォーマル予測は、機械学習において厳密な不確実性定量化を提供するための一般的なパラダイムとして現れつつある。
本稿では,共形予測を連邦学習環境に拡張する。
本稿では、FL設定に適した部分交換可能性の弱い概念を提案し、それをフェデレート・コンフォーマル予測フレームワークの開発に利用する。
論文 参考訳（メタデータ） (2023-05-27T19:57:27Z) - Joint Differentiable Optimization and Verification for Certified
Reinforcement Learning [91.93635157885055]
安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。
本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
論文 参考訳（メタデータ） (2022-01-28T16:53:56Z) - CRFL: Certifiably Robust Federated Learning against Backdoor Attacks [59.61565692464579]
本稿では,第1の汎用フレームワークであるCertifiably Robust Federated Learning (CRFL) を用いて,バックドアに対する堅牢なFLモデルをトレーニングする。
提案手法は, モデルパラメータのクリッピングと平滑化を利用して大域的モデル平滑化を制御する。
論文 参考訳（メタデータ） (2021-06-15T16:50:54Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。