| Project/Area Number |
18KT0098
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 特設分野 |
|---|
| Research Field |
The Information Society and Trust
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2018-07-18 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2021: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2020: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Fiscal Year 2019: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2018: ¥130,000 (Direct Cost: ¥100,000、Indirect Cost: ¥30,000)
|
|---|
| Keywords | コンセンサス / 形式検証 / ブロックチェーン / モデル検査 / スマートコントラクト |
|---|
| Outline of Final Research Achievements |
The goal of this research was to achieve trustability by applying formal verification methods, such as model checking, to smart contracts and blockchains. During the course of the research, a focus was placed on the correctness of consensus, which is at the heart of the applications above mentioned. As a result, a new verification method has been developed. The unique feature of this method is that it can make full use of verification techniques for sequential programs by simulating distributed consensus algorithms using sequential, ordinary programs. Using existing consensus algorithms, the research showed that the proposed approach is capable of finding safety defects.
|
| Academic Significance and Societal Importance of the Research Achievements |
スマートコントラクトやブロックチェーンを利用するアプリケーションは，それらが高い信頼性を提供できること前提としている．分散環境上での信頼性の実現の中核を担うのがコンセンサスであり，そのアルゴリズムには欠陥がないことが強く求められる．本研究で開発した手法では，分散アルゴリズムであるコンセンサスアルゴリズムを通常の逐次プログラムとして模倣するというアイデアにより，逐次プログラムに対する強力な形式手法を適用することを可能とした．
|
