本連載シリーズは新しいスマートコントラクトブロックチェーンであるテゾス（Tezos）を特集しています。Tezosについての基本的な概要はこちらのコラムで配信しました。
関連：・新しいスマートコントラクトブロックチェーンTezosとは?仕組みや特徴など
Tezosの特徴の一つとして、スマートコントラクトの形式検証が可能である点があげられますが、何なのかよく分からない読者の方も多いのではないでしょうか。今回はそんな形式検証についてと、なぜ重要なのかについて考えてみましょう。
スマートコントラクトの安全性は何故重要なのか？
Tezosのスマートコントラクトは形式検証が行えるように設計されています。これはスマートコントラクトの安全性の担保をプロトコルレベルで高めるための設計です。
イーサリアムではスマートコントラクトの脆弱性によって多額の資金が過去に失われていることは周知の通りです。スマートコントラクトの脆弱性を突かれる事例として、多くの人の記憶に残っているものは、2016年のThe DAOでしょう。The DAO事件では、分散管理をするファンドから当時のレートで80億円の資金がハッキングされた事件です。
The DAOのコンセプトは、DAOトークン保有者の投票により投資対象が決定するというファンドマネージャーが存在しないファンドでした。プロジェクトが始まるも、数日後にハックされてしまいますが、これはシステムのルールに乗っ取った犯行でした。
具体的には、スプリットという機能がもとから実装されており、それはDAOファンドの運営に賛同しない場合、自分がDAOに対してプールを行った資金をDAOから切り離して新しいDAOを別に作成できるというものです。この機能を悪用してハッカーは80億円の資金を盗みました。これはテストされていないコントラクトコードの危険性が明るみになった事件であると言えます。
その他の大きい事件として、パリティ・テクノロジーズ（Parity Technologies）社が提供するマルチシグウォレットの事例があります。マルチシグウォレットをスマートコントラクトで実装していましたが、そのコントラクトに脆弱性が見つかり、ある期間に作成されたマルチシグウォレットが凍結され、今にいたるまで300億円以上の資金が凍結されています。
重要な点として、Parity Technologies社は、ギャビン・ウッド（Gavin Wood）氏などによって設立された会社であり、業界のなかでもレベルが高い技術者が複数名在籍している企業です。そのようなParity Technologies社でもこのような事件が起きてしまったことは、スマートコントラクトのバグなどはいつ起きてもおかしくないということが分かります。
そして、コントラクトのバグにより資金が凍結されてしまった場合、それはブロックチェーンを書き換えないと取り戻すことができず、それは基本的には行われないので、過去の事件の資金は永久に凍結されたままになります。
Tezosの特徴である形式検証とは？
Tezosのスマートコントラクトは形式検証が行えるように設計されています。スマートコントラクトをマイケルソン（Michelson）という独自言語で書き、クライアント自体はオキャムル（OCaml）という関数型言語で実装されています。
形式検証という概念自体はブロックチェーン以前から存在するテーマでTezosで使用されるOCamlという言語は形式検証領域で最も支持されているプログラミング言語です。OCamlは歴史的には形式検証は原子力発電などバグがあった場合の被害が大きくなるようなシーンで利用されてきました。
イーサリアムなどではスマートコントラクトのバグについての問題を未然に解決するためスマートコントラクトの監査などが行われることは一般的ですが、監査会社による業務は人の手によって行われる部分が多く、時間と費用を消費します。
そのコストはそのブロックチェーン上で開発を行うプロジェクトや企業が負担しており、重荷になっています。また監査したとはいえ、それが確実に脆弱性がないコードなのかを保証することはできません。
スマートコントラクトのコードが安全であるかどうかを人の手ではなく形式検証するようにする研究は、ブロックチェーン業界で近年のトレンドです。イーサリアムでもこの研究は行われていますが、Tezosにおいてはこれをプロトコルの初期段階で実施しています。
Tezosの形式検証のアプローチは定理証明によるインタプリタを形式化していることと、静的型付された独自スマートコントラクト言語によって実現されます。つまり記述形式は限られた言語で、アプリケーション開発の自由をトレードオフにしている部分がありながらも、正しさを検証できるように設計されています。
ブロックチェーンにおいても大きい資産クラスを記録するのならば、同様にクリティカルなシステムとして扱われるべきだろうと言えます。既に述べたように黎明期でありながら、数十億円の資産がスマートコントラクトのバグによって複数回凍結されており、そういったユースケースでは安全なコードが使用されるべきというTezosのアプローチは合理性があります。
【こんな記事も読まれています】
・新しいスマートコントラクトブロックチェーンTezosとは?仕組みや特徴など
・仮想通貨で金利を得る？Tezos(テゾス)をウォレットからステーキングして報酬を得る方法
