文献

J-GLOBAL ID：202002271542909698   整理番号：20A2471950

Isabelle/HOLを用いたエーテルeumスマート契約の形式的検証【JST・京大機械翻訳】

Formal Verification of Ethereum Smart Contracts Using Isabelle/HOL

著者 (5件)： Ribeiro Maria (Instituto Superior Tecnico, Universidade de Lisboa, Lisbon, Portugal) ,  Adao Pedro (Instituto Superior Tecnico, Universidade de Lisboa, Lisbon, Portugal) ,  Adao Pedro (Instituto de Telecomunicacoees, Lisbon, Portugal) ,  Mateus Paulo (Instituto Superior Tecnico, Universidade de Lisboa, Lisbon, Portugal) ,  Mateus Paulo (Instituto de Telecomunicacoees, Lisbon, Portugal)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 12300  ページ： 71-97  発行年： 2020年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： ブロックチェーンの概念は,資産の取引を分散する目的で開発し,また,このプロセスの間の仲介者の必要性を抑制し,また,関係者間のディジタル信用を達成した。ブロックチェーンは,各ブロックが有限数のトランザクションの記録を含むように,年代的に順序付けされたブロックによって構成される,公共の可換なレッダーに構成される。Ethereumプラットフォームは,ブロックチェーンアーキテクチャを用いて実装し,Turing完全プログラムを保存する可能性を導入した。また,スマート契約として知られているこれらのプログラムは,Ethereum仮想マシンを用いて実行することができる。そのコア言語がEVMバイトコードであるにもかかわらず,それらはさらにEVMにコンパイルされた高レベル言語を用いて実装でき,最も使用された固体である。そのアプリケーションの中で,分散情報ストレージ,資産のトークン化,およびディジタルアイデンティティ検証が行われる。本論文では,Isabelle/HOLにおける固体スマート契約の形式的検証法を提案した。著者らは,Schirmer[23]によって提案された必須言語および大ステップ意味論から始め,それを,Isabelle/HOL証明支援を用いてそれを実行する,充実性の豊富な部分集合を記述するためにそれを適応させた。次に,Hoare論理を用いたプログラムに関する特性を記述し,音性と(相対)完全性に関する結果を得る言語のための証明システムを提示した。最後に,電子投票スマート契約の検証を記述し,この方法を用いて達成できる証明複雑性の程度を説明した。オーバフローと反復脆弱性を含むスマート契約の例も示した。Copyright Springer Nature Switzerland AG 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 意味論 ,  言語 ,  音響 ,  *エーテル ,  情報蓄積 ,  高水準言語 ,  応用プログラム ,  ディジタル方式 ,  仮想機械システム ,  オーバフロー ,  完全性 ,  計算機アーキテクチャ ,  トークン
準シソーラス用語： 脆弱性 ,  ブロックチェーン , 【Automatic Indexing@JST】

著者キーワード (6件)： 形式的検証 ,  Isabelle/HOL ,  Hoare論理 ,  スマート契約 ,  固体性 ,  エーテル

分類 (3件)： 符号理論  (ND02030R) ,  電話・データ通信・交換一般  (ND11010T) ,  データ保護  (JD01020V)

タイトルに関連する用語 (3件)： エーテル ,  契約 ,  形式的検証