ニュース

米マイクロソフト、Azure Blockchain用のスマートコントラクト検証ツールVeriSolを発表

イーサリアム等の開発言語Solidity対応。動作検証・バグの抽出を自動化

(Image: VDB Photos / Shutterstock.com)

米Microsoft(以下、マイクロソフト)は6月3日、同社が提供するブロックチェーン基盤サービスAzure Blockchain用のスマートコントラクト検証ツール「VeriSol」を発表した。同ツールはオープンソースで開発され、Ethereum等のスマートコントラクトで利用される開発言語Solidityで記述されたプラグラムの動作検証が可能とのこと。

スマートコントラクトは、ブロックチェーン上で動作するプログラムだ。従来のプログラムとの相違点として、ブロックチェーンの特性上、一度本番環境に移してしまうと修正ができないという点に注意しなければならない。巨額の損失が発生したThe DAO事件などはスマートコントラクトの脆弱性に起因しており、その動作検証は極めて重要となる。

マイクロソフトの基礎研究機関マイクロソフトリサーチ(MSR)が中心となり開発された「VeriSol」は、本番環境へ移る前にスマートコントラクトが設計通り動作するか、コード上にバグがないかを数学的に検証するツール。Solidityで記述されたスマートコントラクトの形式的検証(Formal Verification)に対応する。

開発者の能力に極端に依存することなく、自動的にモデル検査を実施できるという。Solidityのコードを中間検証言語Boogieに変換することで、MSRがこれまでに開発してきたZ3やCorralをはじめとした、オープンソースの複数の検証コンポーネントを用いた動作検証を実現している。

VeriSolの動作模式図

「VeriSol」は2018年夏から開発が開始された。2019年4月にAzure Blockchainのスマートコントラクト開発のための継続的開発項目として正式に組み込まれ、その仕様等を説明したホワイトペーパーが公開されている。

開発段階の「VeriSol」を用いて、Azure Blockchain Workbench上にあるすべてのスマートコントラクトに対して検証を実施したところ、いくつかの未知のバグを発見することができたという。開発チームは今後、検証機能の扱いやすさや自動化部分の効率化などを中心に開発を進めていくとしている。