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

ブログランキングに参加中!!ポチッと押して応援よろしくお願い致します!!

にほんブログ村 投資ブログ 仮想通貨投資へ

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

(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上にあるすべてのスマートコントラクトに対して検証を実施したところ、いくつかの未知のバグを発見することができたという。開発チームは今後、検証機能の扱いやすさや自動化部分の効率化などを中心に開発を進めていくとしている。

引用元はこちら

当サイトは非営利にて運営を行わせて頂いております。 運営に関する募金はビットコインにて随時行わせて頂いております。 もし今後も当サイトを応援して頂ける方は是非ビットコインにて募金して頂けますと幸いです。

■ビットコイン(Bitcoin)
1L1mCDuAPZJJtt7boJvDzBNCqv66X3eqgQ

■イーサリアム(Ether)
0xB6c362e6c49F54F271E17CC1D064D5Ae6605066B