文献

J-GLOBAL ID：202202264425581722   整理番号：22A1104995

エーテルeum2.0ビーコンチェーンの形式的検証【JST・京大機械翻訳】

Formal Verification of the Ethereum 2.0 Beacon Chain

著者 (3件)： Cassez Franck (ConsenSys, New York, USA) ,  Fuller Joanne (ConsenSys, New York, USA) ,  Asgaonkar Aditya (Ethereum Foundation, Zug, Switzerland)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13243  ページ： 167-182  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： Beacon連鎖の参照実装の形式的検証における経験を報告する。Beaconチェーンは,新しいProof-Sake Ethereum2.0ネットワークのバックボーン成分であり,それは,検証者,それらの考慮,それらの証明(投票)に関する追跡情報の電荷であり,そして,いくつかの検証者が,それら(それらの考慮の幾つかを失う)を slすのに,何人かの正当なものが見つかるかどうかである。Beaconチェーンはミッションクリティカルであり,その中のバグは全体のネットワークを妥協できる。Ethereum Foundationによって開発されたBeacon連鎖参照実装はPythonで書かれ,各Beaconチェーンネットワーク参加者(ノード)の,状態機械の詳細な操作記述を提供する。正式に指定し,検証フレンドリーな言語Dafnyを用いたBeacon連鎖参照実装の(大きな部分と重要な部分)の実行時間誤差の欠如を検証した。本研究の経過中に,著者らは,いくつかの問題を明らかにし,提案した固定具を提案した。また,ランタイムエラーを超える保証を提供できる機能的正当性仕様も合成した。Dafnyのコードと証明とのソフトウェアアーチファクトは,利用可能である。Copyright The Author(s) 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 言語 ,  情報 ,  *ネットワーク ,  ソフトウェア ,  投票 ,  ソフトウェア障害 ,  固定具 ,  アーチファクト
準シソーラス用語： 形式的検証 ,  実行時間 ,  Python , 【Automatic Indexing@JST】

分類 (3件)： 計算機網  (JC03000K) ,  無線通信一般  (ND08010L) ,  移動通信  (ND08030H)

タイトルに関連する用語 (4件)： エーテル ,  ビーコン ,  チェーン ,  形式的検証