AgdaにおけるHotStuffベースByzantineフォールトトレラントコンセンサスの形式的検証に向けて:拡張バージョン【JST・京大機械翻訳】

Carr Harold; Jenkins Christopher; Moir Mark; Miraldo Victor Cacciari; Silva Lisandra

プレプリント

J-GLOBAL ID：202202216369981762 整理番号：22P0311361

AgdaにおけるHotStuffベースByzantineフォールトトレラントコンセンサスの形式的検証に向けて:拡張バージョン【JST・京大機械翻訳】

Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (5件)： , , , ,
資料名：
発行年： 2022年03月25日プレプリントサーバーでの情報更新日： 2022年03月28日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

LibraBFTは,HotStuffに基づくビザンチン故障トレラント(BFT)コンセンサスプロトコルである。著者らは,HotStuff/LibraBFTの根底にあるプロトコルの抽象モデル,および,それらのコア正しさ(安全性)特性の形式的,機械検査証明,および,非参加型関係者がコミット結果の検証を可能にする拡張条件を提示した。(ここで提示した抽象モデルではなく,特定の実装に対して),重要な貢献は,特定の実装に無関係に,抽象的な方法で,ホネストピアの挙動に関する仮定を正確に定義する。したがって,本研究は,基本的なプロトコルの正当性を証明する困難な作業を繰り返すことなく,コンクリート実装の全クラスの正当性を証明するための重要なステップである。抽象証明は単一構成(epoch);構成変化にわたるこれらの証明の拡張は将来の研究である。著者らのモデルと証明はAgdaで表され,オープンソースで利用可能である。【JST・京大機械翻訳】

, , , ,
, , , , 【Automatic Indexing@JST】

計算理論 , その他のディジタル計算機方式

, , ,

前のページに戻る