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* で実行したところ、そのうちのほんの一部だけが「有効」であることがわかりました。