Microsoft は、DAO と同様のインシデントを防止するためにスマート コントラクト セキュリティ ワーキング グループを立ち上げました (ホワイト ペーパー全文をダウンロード)

海外メディアの報道によると、マイクロソフトはスマートコントラクトのセキュリティを向上させるためのワーキンググループを組織していることを明らかにした。

「Kinakuta」と呼ばれるこのワーキンググループは、ブロックチェーンに基づく自動実行コードであるスマートコントラクトに関する情報を業界がより簡単に共有できるようにすることを目的としています。

スマートコントラクトのアイデアは複雑なトランザクションを自動的に完了することができますが、最初の大規模プロジェクトであるThe DAOが崩壊した後、デジタル通貨コミュニティ内でスマートコントラクトに関する懸念が高まり始めました。

それ以来、スマート コントラクトは不適切に使用すると非常に危険な新しいものであることが徐々に認識されるようになりました。

しかし、マイクロソフトのビジネス開発および戦略責任者であるマーリー・グレイ氏は、オープンな情報と新しいツールによって、開発者が同様のミスを回避できると考えている。

グレイ氏は、コンセンシスのグローバル事業開発責任者アンドリュー・キーズ氏と提携し、マイクロソフトが招待したい開発者および企業35社のリストを作成したと述べた。これらには、Ethereum Foundation、R3CEV、BlockApps が含まれます。

今月初めに正式発表されると報じられている。さらに、マイクロソフトはハーバード大学の研究者と共同で新しいホワイトペーパーを執筆し (ホワイトペーパーの全文を参照するには、コイン ライブラリ (http://8btc.com/doc-view-844.html))、イーサリアムのスマート コントラクトが期待どおりに機能するかどうかを証明しました。開発者はこれらのリソースを使用して、自分が作成したコードの問題を発見できます。

形式検証

この論文では、ソフトウェア プログラム（この場合はスマート コントラクト）の正しさを証明または反証できる「形式検証」の方法を提案しています。

ホワイト ペーパーでは、3 つの方法でスマート コントラクトを検証するのに役立つ 2 つのツールも提案されています。

1 つ目はSolidity*で、これは Solidity コードの一部を、プログラムが正しく実行されるかどうかを検証するプログラミング言語であるF*に変換します。次に、スマート コントラクトの EVM バイトコード ステートメントを Solidity ソース コードに逆コンパイルするEVM *があります。

2 番目のツールが必要なのは、Solidity で記述された 112,802 の契約のうち、Etherscan で実行できるのは 396 のみであるため、バイトコードを使用するのが最善の選択肢だからです。

Solidity* は現在、ループなどの複雑な Solidity 機能をサポートしていませんが、チームは 396 の Solidity 契約のうち 46 を変換することができました。これら 46 件の契約を Solidity* で実行したところ、そのうちのほんの一部だけが「有効」であることがわかりました。

「これはほとんどのスマートコントラクトが脆弱であることを示す明確な兆候だ」と論文は結論づけている。

しかし、多くの人がスマート コントラクト セキュリティ ツールの急速な発展に興奮している一方で、業界の中には短期的には開発者がミスを犯し続けるだろうと考える人もいることには注目すべきです。

イーサリアムの創始者ヴィタリック・ブテリン氏は、新たな研究によってThe DAOのようなことが再び起こるのを防げるとは思わないと書いている。

「間違いはこれからも起こるだろう」とブテリン氏はイーサリアムの最近のブログ投稿で述べた。「そして我々はそこから学ぶだろう。」