| 研究課題/領域番号 |
18KT0098
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 特設分野 |
|---|
| 研究分野 |
情報社会におけるトラスト
|
|---|
| 研究機関 | 大阪大学 |
|---|
研究代表者 |
土屋 達弘 大阪大学, 情報科学研究科, 教授 (30283740)
|
|---|
| 研究期間 (年度) |
2018-07-18 – 2022-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2021年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2020年度: 2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
2019年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2018年度: 130千円 (直接経費: 100千円、間接経費: 30千円)
|
|---|
| キーワード | コンセンサス / 形式検証 / ブロックチェーン / モデル検査 / スマートコントラクト |
|---|
| 研究成果の概要 |
本研究では，モデル検査を中心とした検証手法を，スマートコントラクト，および，その実行基盤であるブロックチェーンに適用することによって，これらの応用におけるトラスタビリティを実現することを目標とした．研究では，特にこれらの基礎となるコンセンサスアルゴリズムに注目し，不具合を検証する新しい手法を開発した．提案手法では，通常の逐次的なプログラムによって，メッセージ遅延や故障を含めたアルゴリズムの動作を模倣し，逐次プログラムに対するモデル検査手法を適用する．実際のアルゴリズムを対象に，安全性の違反を検出できることを示すことができた．
|
| 研究成果の学術的意義や社会的意義 |
スマートコントラクトやブロックチェーンを利用するアプリケーションは，それらが高い信頼性を提供できること前提としている．分散環境上での信頼性の実現の中核を担うのがコンセンサスであり，そのアルゴリズムには欠陥がないことが強く求められる．本研究で開発した手法では，分散アルゴリズムであるコンセンサスアルゴリズムを通常の逐次プログラムとして模倣するというアイデアにより，逐次プログラムに対する強力な形式手法を適用することを可能とした．
|
