イーサリアムはスマートコントラクトのセキュリティを向上させるために形式検証を使用しています

クレイジーレビュー：今月上海で開催されたイーサリアム開発者会議（Devcon2）では、形式検証がコミュニティのホットな話題となり、大きな注目を集め、白熱した議論が交わされました。 Solidity 言語の補足として、ブロックチェーン スマート コントラクトのセキュリティを強化し、The DAO と同様の事件の発生を防ぐ可能性があります。しかし、まだ克服すべき技術的な困難がいくつか残っており、すべての問題に対する万能薬ではありませんが、その可能性は開発者コミュニティによって高く評価されています。

翻訳: Annie_Xu

最近、ブロックチェーン分野で「形式検証」という新しい流行語が登場しました。

このフレーズは、数学的アルゴリズムを使用してソフトウェア プログラムを検証することを指し、メディアの報道に頻繁に登場します。しかし、先週上海で開催されたブロックチェーンサミットでは、スマートコントラクトとブロックチェーンの両方に現在セキュリティ上の問題があることが示唆されており、形式検証の重要性はますます高まるはずです。

イーサリアム開発者会議 Devcon2 での複数のセッションでは、開発者コミュニティがイーサリアム コーダーを支援するこの新しいプログラムを明らかに歓迎していることが示されました。このコンセプトにより、イーサリアム プロトコルとプルーフオブステーク ブロックチェーン プロジェクトに対する信頼が高まりました。

DAO は、分散型アプリケーション開発プラットフォームにおけるこれまでで最大のスマート コントラクト プロジェクトでしたが、その突然の崩壊は、このコンセプトが注目を集めている理由を確かに説明しています。

形式検証は複雑に思えるかもしれませんが、Ethereum のアプリケーションとして簡単に理解できます。現在、プログラマーは基本的に Solidity 言語でスマート コントラクトを記述し、それが Ethereum Virtual Machine (EVM) 用のバイトコードにコンパイルされ、ネットワークのノードに配布されてコード プログラムを実行します。

形式検証は、さまざまなネットワーク要素が指示を受信し、ユーザーに代わって意図したとおりに実行することを確認する客観的な方法と見なすことができます。

Aesthetic Integration の創設者 Grant Passmore 氏は、この技術を宣伝する機会を見出し、Devcon2 でブロックチェーンとスマート コントラクトの形式検証プラットフォームである Imandra Contracts をリリースしました。

グラント・パスモア

同氏はカンファレンスで、コミュニティの目標とコードに課せられた重い責任を考慮すると、イーサリアムは形式検証の「楽園」として機能する可能性があると示唆した。

「イーサリアムコミュニティはユニークです。DAOの後、私たちは強力なコンピューターエンジニアリングの必要性を発見しました。スマートコントラクトをWebアプリケーションのように見せることは不可能です。」

もう一人の講演者であるコーネル大学のフィリップ・ダイアン氏は、より広く方法論について議論し、形式検証がイーサリアムの主要な問題を解決するのに役立つと考えていると述べた。

「これは重要な基盤となるでしょう。イーサリアムを通じて標準を設定し、この経験を共有することを楽しみにしています。」

補助輪

金融企業は最近スマートコントラクト言語を重視しており、Solidityと形式検証の統合が最近最もホットな話題となっています。

Solidity は Ethereum プラットフォーム用に開発されましたが、言語がテストされておらず、記述が難しいため、多くの批判を受けています。これらの問題は、言語コンパイラのコード ベースの不足と DAO システムの崩壊によって後に拡大しました。

そのため、Solidity の作成者である Christian Reitweissner 氏は、Ethereum のコーダーがより効果的に脆弱性を見つけられるようにするために形式検証を使用する必要があると認めました。

同氏は、将来的にはスマートコントラクトの開発者は形式検証を利用して、自分たちの作業に抜け穴があるかどうかを判断できるようになるだろうと述べた。このツールを使用して、2 つの平均を追加した結果がコンパイラによって割り当てられた結果よりも優れているかどうかを判断することもできます。

「このようなことが起こる可能性はありますが、形式検証によって自動的に検出できます。早期に検出して、スマート コントラクトを調整することができます。」

Reitweissner 氏は、Solidity チームはすでに形式検証を統合する方法を検討していると述べた。この目標の達成に Why3 ツールキットがどのように役立つかを調査するために、昨年 10 月にプロトタイプが開発されましたが、この製品はまだ Solidity 全体では公開されていません。

実験場

サミットでは、イーサリアムを使用して金融業界に形式検証を適用する方法を探る方法についての議論にも焦点が当てられました。

パスモア氏は、同社は2014年から金融機関と協力し、システム統合の方法を模索してきたと述べた。顧客はすでにダークプールなど、トレーダーからその公平性が批判されているいくつかのアプリケーションを使い始めている。

パスモア氏は、イーサリアムコミュニティがスマートコントラクトの採用を推進できると述べた。

「当社が初めて銀行の顧客と仕事を始めたとき、彼らの多くはこの分野に大きな関心を示しましたが、スマートコントラクトの正確性については懸念がありました。」

形式検証の成長は、現在 Ethereum Foundation で働いている形式検証エンジニアの Yoichi Hirai 氏も魅了しました。彼はサイバーセキュリティのリーダーであるFireEyeの研究員だった頃からこの技術に興味を持っていた。

平井氏は会議で、ソースコードがない場合やタスクが複雑すぎる場合には形式検証を使用できないと述べた。

「イーサリアム、イーサリアム仮想マシン、イエローペーパーには紹介が32ページしかないことがわかり、それを翻訳してスマートコントラクトの概念実証を書くことができると思いました。」

一方、イーサリアムは、彼が言うところの「より小さなフォームファクター」と「解決可能な問題」を提供することができ、開発者がSolidityをバイトコードに効率的にコンパイルする方法を決定できる。

「形式検証の研究者はもっと増えると思います。」

万能薬ではない

しかし、この概念に対する大きな関心にもかかわらず、形式的な検証がどのような形をとるかについては慎重にならなければなりません。 EVM のアップグレードに取り組んでいる開発者の Alex Beregszaszi 氏は、現在、開発者がスマート コントラクト コードの機能性を確保するためのソリューションを模索していると述べました。

パスモア氏はまた、正式な検証ツールでは依然として人間の入力が必要であるため、新しいシステムがDAOの問題を発見したかどうかを判断することは現時点では不可能であると指摘した。

「DAO イベントをエンコードして脆弱性をチェックすることはできますが、まず注意すべき点が何であるかを知っておく必要があります。」

Reitweissner 氏と Passmore 氏はどちらもこの制限を認めており、開発者に対して形式検証を万能薬と見なさないよう警告しています。

しかし、Reitweissner 氏は、アプリケーションが推進されるにつれて、この方法論は発展し続け、開発者は徐々に問題をより適切に特定し、必要な一般的な問題を記録するための対応するコード ライブラリを開発する方法を学ぶようになると考えています。

パスモア氏は、この方法でイーサリアムコミュニティがこの概念をうまく推進し、最終的にはブロックチェーンの研究開発を促進することができると考えています。

「まだ多くの人が馴染みがないかもしれませんが、私たちには必要なのです。私たちはまだ学習中ですが、受け入れなければなりませんし、とてもワクワクしています。」