スマートコントラクトはブロックチェーン上で動作するプログラムであり，取引の自動化等に用いられている．ブロックチェーン技術が広く利用されるにつれ，扱うデータの重要性やプログラムの運用形態から，静的な形式検証の需要が高まっている．本発表で紹介する Helmholtz はブロックチェーンプラットホームの一つである Tezos で用いられているスマートコントラクト用言語 Michelson に対する静的な検証器である．本研究では検証器の実装の他に理論的基礎付けとして，データの性質について言及できる篩型と呼ばれる型を利用できる型システムを Michelson のサブセットについて与えている．
本検証器は実際に運用されるようなスマートコントラクトに適用可能な検証器を目的として開発されている．本検証器を既存もしくは新規のスマートコントラクトに適用することで，その動作に一定の保証を与えることができるであろう．これはスマートコントラクトの信頼性向上に繋がり，ひいては当該暗号通貨の価値向上に繋ると期待される．本研究はダイラムダ株式会社の古瀬淳氏と共同で行っている．
| 氏名 | 専攻 | 研究室 | 役職/学年 |
|---|---|---|---|
| 西田 雄気 | 通信情報システム専攻 | 五十嵐研究室 | 研究員 |
| 齋藤 大聖 | 通信情報システム専攻 | 五十嵐研究室 | 修士2回生 |
| 陳 然 | 通信情報システム専攻 | 五十嵐研究室 | その他学生 |
| 河田 旺 | 通信情報システム専攻 | 五十嵐研究室 | その他学生 |
| 末永 幸平 | 通信情報システム専攻 | 五十嵐研究室 | 准教授 |
| 五十嵐 淳 | 通信情報システム専攻 | 五十嵐研究室 | 教授 |