ReFX: 型に基づくスマートコントラクト自動検証器
ReFX: A type-based automated verifier for smart contracts
概要
最近のブロックチェーンにはスマートコントラクトというプログラムを動かす仕組みがあり、取引の自動化などに使われている。しかし、スマートコントラクトにバグがあると 莫大な金銭的損失が生まれてしまうことがあり、実際にEthereumというブロックチェーンではスマートコントラクトのバグにより50億円相当の暗号通貨が盗まれる事件が発生している。 本発表では、Tezosというブロックチェーン上で動くスマートコントラクト言語Michelsonに対して、 データについての様々な性質を型で表現できる篩型という仕組みを導入し、型システムによってスマートコントラクトの安全性を検証する手法を提案する。
産業界への展開例・適用分野
我々の提案する、篩型の導入された型システムを用いてプログラムを書くことで、より安全なスマートコントラクトが作成できるようになる。 これによりブロックチェーンとその取引に対する信頼の向上が期待でき、取引の促進や通貨価値の向上が見込めるだろう。 また、他の暗号通貨フレームワークへのプログラム検証技術の普及も期待できる。 本研究はダイラムダ株式会社の古瀬淳氏と共同で行っている。
研究者
| 氏名 | 専攻 | 研究室 | 役職/学年 |
|---|---|---|---|
| 陳 然 | 通信情報システム専攻 | コンピュータソフトウェア分野 | 修士2回生 |
| 齋藤 大聖 | 通信情報システム専攻 | コンピュータソフトウェア分野 | 修士1回生 |
| 河田 旺 | 通信情報システム専攻 | コンピュータソフトウェア分野 | 修士2回生 |
| 西田 雄気 | 通信情報システム専攻 | コンピュータソフトウェア分野 | 博士3回生 |
| 五十嵐 淳 | 通信情報システム専攻 | コンピュータソフトウェア分野 | 教授 |
| 末永 幸平 | 通信情報システム専攻 | コンピュータソフトウェア分野 | 准教授 |