インタビュー：Etherem Dev 平井 洋一氏「イーサリアムの可能性と、形式検証」

9月19日から21日まで上海で開催されたイーサリアム デベコン2では、イーサリアムの技術開発状況のアップデートと共に、現状のいくつかの課題にいかに取り組むか解決策が話し合われた。大きな焦点のひとつは、まだ新技術であるスマートコントラクトにおいてセキュリティーをどう向上させるかという点だ。

このセキュリティー向上の解決策のひとつとしてEthereum Devが提供するものに、スマートコントラクトにバグがないかを確かめる作業（形式検証、Formal Verification）がある。デべコン2では現在Ethereum Devに所属して形式検証に従事する平井 洋一氏が、形式検証を利用してなにができるのかプレゼンを行った。

今回編集部は平井氏に、イーサリアムに感じる可能性と、形式検証の観点から見る特長とについてわかりやすくお話していただいた。

平井 洋一氏は東京大学情報理工学研究科博士課程修了、産業技術総合研究所で形式検証に従事。その後アメリカの企業でも同様に形式検証に携わった後、2016年9月よりEthereum Devでスマートコントラクトの形式検証に着手している。平井氏はイーサリアムを、「計算機が単純で形式検証がしやすく、ソフトウェアを“正しく”作ることを可能にするポテンシャルを持つのでは」と評価している。

「非同期の通信で共有知識は得られない」という知識論理の定理の裏をかくビットコインに興味

平井氏が最初にブロックチェーン技術の概念に触れたのは7，8年前のビットコインの論文だった。当時は一読した後、「これでは動かないだろう」と思い忘れてしまっていたが、その後3年ほどたってもビットコインがまだ動いており、価格が上がってユーザーも増加していることに驚いた。その頃から「どうして動くのかわからない」と気になり始めた。

平井氏が当初ビットコインは動かないと思った理由は、大学在籍時に知識論理という論理学の一分野を学んでいたためだった。この知識論理の定理に「非同期の通信で共有知識は得られない」というものがある。ビットコインの場合も参加者同士はこの定理でいうところの非同期通信しかできていないため、「お互いを確認できないのに動いている」点が気になったものの、当時はまだブロックチェーン関連の仕事をしようとまでは思っていなかった。

「今の計算機は複雑になりすぎている」

転換点は、仕事上で論理学を使って正しく動くソフトウェアの検証を行い始めた頃。「今の計算機は複雑になりすぎている」と気づいた。40～50年前のSFでは、「コンピューターは正しいはずだ」という前提で描かれる高度に発展した近未来都市がよく題材となっていたが、実際にコンピューターが普及する現在ではまだ「あまり信用できないもの」として人が大部分を管理する状況だ。形式検証もしにくく、「どうやって“正しいソフトウェア”を作るか」と悩んでいた。

ちょうどその頃イーサリアムを知った。「イーサリアムは簡単に説明すると、とても単純なしくみの想像上のコンピューター１台を皆で動かし、誰か1人が止めたいと思っても止めることはできないという仕組みです。これの上でなら“正しいソフトウェア”を作ることができるかもと思いました」

それから休日にコードを書いてredditに載せてみたところ、イーサリアムの開発者からコンタクトを受けて同組織で働き始めることになった。

「実際にイーサリアムで働き始めてみた今も、複雑さが普通の計算機の100分の１くらいだと感じています。扱いやすいものを見つけた、ちょうどよい砂場を発見したという気持ちです」と平井氏は語る。

管理人なしで動き続ける計算機を

イーサリアムは「管理人はいらない」という理念があるため、正しいコードを作る必要がある。また管理人なしで動き続ける計算機を作るためには、バーチャルマシーン自体も単純にした方がやりやすい。両方とも、形式検証のやりやすさと動機につながっている。

「計算機は、良かれと思って機能をどんどん足したことで複雑化して今があります。例えばノートパソコンに入っているCPUなど、複雑になったものを単純にすることは難しいものです。プログラマーとしては、大きなものを作っているとひっくり返して１から作りたくなることがよくあります。小さな砂場で遊んでみたい、という感覚です」

コードのミスを防ぐ証明士という職業を確立したい

「イーサリアムは形式検証の対象として筋が悪くはないし、やる理由もあります。今後は、プログラマーや企業など他の協力者とどのように協力していくかが課題となっていくと思います。またこれから検証者が増えてゆけば、コードのミスの減少も期待できます」と平井氏は語る。

現在Ethereum Devでは平井氏ともう１人が形式検証に携わっているが、これからさらに多くの形式検証の人員がスマートコントラクトの研究領域に入ってくれば、開発者にとってブロックチェーンは一種の「楽園」になるかもしれない。

インタビュー：Etherem Dev 平井 洋一氏「イーサリアムの可能性と、形式検証」はCoinPortalで公開された投稿です。

Source: Coin Portal