研究課題/領域番号 |
18KT0098
|
研究機関 | 大阪大学 |
研究代表者 |
土屋 達弘 大阪大学, 情報科学研究科, 教授 (30283740)
|
研究期間 (年度) |
2018-07-18 – 2022-03-31
|
キーワード | スマートコントラクト / コンセンサス / ブロックチェーン / 形式検証 / モデル検査 |
研究実績の概要 |
本研究ではスマートコントラクト,および,その実行基盤であるブロックチェーンを対象として,形式検証を適用することで,トラスタビリティを保証することを目標としている.初年度である2018年度は,関連研究についての情報収集と,適用可能な形式検証手法についての検討を主に行った. 本研究で実施する形式検証では,トラストの基盤となる正しさを機械的に検証可能な形で定義した上で,自動検証を実現することが必要となる.研究計画時では自動検証の手法としてモデル検査技術の利用を想定していたが,2018年度における検討により,この方針が妥当である点について確信を深めた.特に,Maurice Herlihy による"Blockchains from a distributed computing perspective" (Communications of the ACM: Volume 62 Issue 2, February 2019)という論考では,ブロックチェーン,および,スマートコントラクトに関連する諸問題が,計算機科学における並行性の問題として扱うことができることが示唆されており,この考えを援用することで,元々並行システムの検証を目的として開発されたモデル検査を,本課題の新しい対象に適用する方針について道筋が得られた. また,ブロックチェーンの基盤である分散コンセンサスプロトコルの検証についても,本研究では対象としている.この検証問題に関しては,メッセージの偽造を含むノードの悪意ある動作のモデル化と,その上での現実的なコスト(時間)での検証の実現を図る必要がある.2018年度では,特に後者に関して,状態の抽象化による状態削減を検討した.
|
現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
初年度である2018年度は,情報収集と基本方針の検討を主に予定しており,研究実績の概要で述べたように,これらは順調に進展している.
|
今後の研究の推進方策 |
2019年度は本課題の2年目に当たる.初年度における研究期間は1年に満たなかったので,本年度においては,基本方針だけでなく具体的な適用技術の選択を早期に行い,課題が対象とする具体的な問題に対して選択した技術を適用し問題解決に入る段階とする. スマートコントラクトに関しては,Herlihyによる並行性の問題としてのとらえ方を採用し,その考え方を元に,スマートコントラクトにおける問題を形式的にモデル化する.これにより,モデル検査手法の適用が可能になる. ブロックチェーンに関しては,その基盤である分散コンセンサスプロトコルに注目し,ノードの悪意ある動作のモデル化と,モデル検査に必要な検証コストの両面から研究を継続する.
|
次年度使用額が生じた理由 |
2019年度は全直接経費が100千円のみであり,必要資料の購入の結果,当初想定していた国内出張ができなくなったため,50千円弱の余りが生じた.
|