文献

J-GLOBAL ID：202202238574867742   整理番号：22A0446556

スマートACEにおける通信抽象化による充実性スマート契約の検証【JST・京大機械翻訳】

Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE

著者 (6件)： Wesley Scott (University of Waterloo, Waterloo, Canada) ,  Christakis Maria (MPI-SWS, Kaiserslautern and Saarbruecken, Germany) ,  Navas Jorge A. (SRI International, Menlo Park, USA) ,  Trefler Richard (University of Waterloo, Waterloo, Canada) ,  Wuestholz Valentin (ConsenSys, Kaiserslautern, Germany) ,  Gurfinkel Arie (University of Waterloo, Waterloo, Canada)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13182  ページ： 425-449  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 堅固な契約は開発者がユーザ間の財政的合意を定式化することを可能にする。それらの金銭的性質のため,スマート契約は多くの高プロファイル攻撃の目標である。[数式:原文を参照]ユーザまでのデータを維持するスマート契約のブリュート力検証は難治性である。本論文では,スマート契約検証のための自動化フレームワークであるスマートACEを提案した。大量のユーザによって誘発された状態爆発を改善するために,スマートACEは,任意に多くのユーザから少数の代表的ユーザへの検証を減らすローカルバンドル抽象化を実行する。多重トランザクションにわたる深いバグを明確化するために,スマートACEは,モデル検査,ファジィ化,および記号実行のような様々な技術を採用する。スマートACEの有効性を例証するために,一般的なOpenZeppelinライブラリからのいくつかの契約を検証した:アクセス制御ポリシーと e列サービス。各契約に対して,Scribble言語における仕様を提供し,故障注入を適用して各仕様を検証した。SmartACEとScribbleを統合する経験を報告し,各仕様に対するスマートACEの性能について述べた。Copyright Springer Nature Switzerland AG 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 自動化 ,  言語 ,  多重化 ,  *通信 ,  ソフトウェア障害 ,  有効性 ,  定式化 ,  ロバスト性 ,  アクセス制御 ,  モデル検査 ,  サイバー攻撃
準シソーラス用語： 故障注入 , 【Automatic Indexing@JST】

分類 (1件)： 計算機網  (JC03000K)

タイトルに関連する用語 (4件)： ACE ,  抽象化 ,  契約 ,  検証