2020 Fiscal Year Research-status Report
形式検証によるスマートコントラクトとその実行基盤に対するトラスタビリティの実現
| Project/Area Number |
18KT0098
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
土屋 達弘 大阪大学, 情報科学研究科, 教授 (30283740)
|
|---|
| Project Period (FY) |
2018-07-18 – 2022-03-31
|
| Keywords | ブロックチェーン / 形式検証 / コンセンサス / スマートコントラクト |
|---|
| Outline of Annual Research Achievements |
本研究では，モデル検査を中心とした形式検証を，スマートコントラクト，および，その実行基盤であるブロックチェーンに適用することによって，これらの応用におけるトラスタビリティを実現することを目標としている．以下，2020年度の研究実績について，スマートコントラクトの形式検証と，ブロックチェーンの形式検証に分けて説明する．
前者については，重要な関連研究の発表が相次いだことから，形式検証分野だけではなく，ソフトウェア工学分野からの知見を取り入れる必要性が生じたため，現在の最新研究の再整理を行った．その結果，モデル検査などの純粋な形式検証手法に加え，ソフトウェアテスティング技術である記号実行やミューテーションテスティングなどの適用についても研究が進められていること，現在検討している並行性の問題としてスマートコントラクトの正しさを捉える方法は，それらを補完する位置づけとなることがが分かった．
一方，後者については，ブロックチェーンの中心技術であるコンセンサスアルゴリズムの検証について，新たな方法論の提案を行った．提案手法では，逐次プログラムで分散アルゴリズムであるコンセンサスアルゴリズムの一定の長さの動作をシミュレートし，そのプログラムを検証することでアルゴリズム中の不具合を検出する．これは，小スコープ仮説と呼ばれる，不具合による異常は小さい動作範囲中でも顕在化するという考えに基づく．提案法では，小スコープ仮説に基づき，アルゴリズムの全状態を探索するのではなく，プログラムの一定の長さの動作を出来る限り網羅的に探索することで，アルゴリズムの誤りの検出を行う．実際にCBMCというC言語に対する有界モデル検査ツールを用いて，既存のアルゴリズムで安全性が違反される例を検出できた．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
スマートコントラクトの検証について，成果発表に至っていないため，2021年度は部分的にでも論文として公表を進める．コンセンサスアルゴリズムの検証については提案手法の発表を行ったが，検証を実施したアルゴリズムが少数のため，この数を増やしてより一般的な結果を導く必要がある．
|
| Strategy for Future Research Activity |
スマートコントラクトの検証については，手法の提案だけでなく，これまで行った関連研究のサーベイに基づいて，トラスタビリティについての多面的な特徴付けを行う．
コンセンサスアルゴリズムの検証については，提案手法をより多くのアルゴリズムへ適用する．特に，まだ，ビザンチン故障（悪意ある振る舞い）耐性を持つアルゴリズムへの適用を行っていないので，これを進める．また，提案手法は，動的記号実行等など，2020年度で用いたモデル検査以外のテスト・検証手法と組み合わせることが可能である．このような手法を利用した場合についても評価を行い，成果発表を実施する．
|
| Causes of Carryover |
コロナ禍によって予定していた国内出張，国外出張が，すべてキャンセルとなったことなどから未使用額が生じたため．次年度においては，博士後期課程の学生をRAとして雇用し，RAとの連携とのもと研究の総括を図る．
|
