| 研究課題/領域番号 |
18KT0098
|
|---|
| 研究機関 | 大阪大学 |
|---|
研究代表者 |
土屋 達弘 大阪大学, 情報科学研究科, 教授 (30283740)
|
|---|
| 研究期間 (年度) |
2018-07-18 – 2022-03-31
|
| キーワード | スマートコントラクト / モデル検査 / コンセンサス / ブロックチェーン |
|---|
| 研究実績の概要 |
本研究では，モデル検査を中心とした形式検証を，スマートコントラクト，および，その実行基盤であるブロックチェーンに適用することによって，これらの応用におけるトラスタビリティを実現することを目標としている．2年目である2019年度は，初年度における関連研究に関する情報収集と，形式検証手法についての適用可能性の検討結果をもとに，モデル検査手法の適用を進めた．
まず，スマートコントラクトにおける問題を，共有オブジェクトに対する並行処理の問題として取り扱うことができるという知見をもとに，並行処理の取り扱いに優れたモデル検査ツールであるSPINを用いて，コントラクト上の問題をSPINにおいて再現することを試みた．具体的には，実際の不具合であるDAOバグを例として，SPINの入力言語であるPromelaによって対象となるスマートコントラクトを記述している．このPromela記述に対して，適切に検査項目を定めることができれば，モデル検査器によってその検査項目が成り立たない状況を機械的に導出できるため，コントラクトが有する不具合の自動的な検出が可能となる．
本課題のもう一つのテーマである，ブロックチェーンへの形式手法の適用については，その基盤となるコンセンサスプロトコルの検証について，モデル検査の適用を進めている．特に，検証のコスト（特に，状態爆発による検証時間の増加）の軽減に関して，プロトコル中のカウンタの値の抽象化を中心に研究を進めている．カウンタは0以上の任意の整数値を取り得るため，これをそのまま状態の要素として扱うと状態数が爆発的に増加するため，開発している方法では，ノード間のカウンタの大小関係をもとにプロトコルの動作が依存する情報のみを状態に反映させることで，状態爆発を回避することができる．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
スマートコントラクト，および，分散コンセンサスプロトコルについて，モデル検査器SPINを用いて，その入力言語PROMELAによる記述を進めているが，成果発表にいたっていないため．部分的にでも性能評価が実施でき次第，成果公表を行う．
|
| 今後の研究の推進方策 |
2020年度においては，実際の不具合であるDAOバグに加えて，他の例についてもモデル化，および，不具合の検出が可能なことを示す．具体的な対象となるコントラクトの例としては，BlockKingコントラクトを検討している．
分散コンセンサスプロトコルについては，ノード数が少ない場合についての検証を実現する．開発中の状態削減技術を用いて，ブロックチェーンの応用で問題となるビザンチン故障（ノードの悪意ある動作）のモデル化に伴う状態増加を低減することで，これを実現する．また，クォーラム（プロトコルにおける論理的なノード集合）の動的最適化を伴うプロトコルに対する検証についても検討する．
また，モデル検査を十分な時間，並行的に実施できる計算機環境を構築する．
|
| 次年度使用額が生じた理由 |
3月チェコで開催予定だった国際会議ACM-SAC 2020参加のための旅費としての支出を予定していたが，コロナウィルスの影響で会議がオンライン開催となり，未使用分が生じたため．
|
