Microsoft launches smart contract security working group to try to prevent similar incidents to The DAO (full white paper download)

According to foreign media reports, Microsoft revealed that it is organizing a working group to improve the security of smart contracts.

The working group, called Kinakuta, aims to make it easier for the industry to share information about smart contracts, which are self-executing codes based on blockchain.

Although the idea of ​​smart contracts can automatically complete complex transactions, after the collapse of the first large-scale project, The DAO, concerns about smart contracts began to grow within the digital currency community.

Since then, people have gradually realized that smart contracts are a new thing that can be very dangerous if used improperly.

However, Marley Gray, Microsoft's head of business development and strategy, believes that open information, along with new tools, can help developers avoid similar mistakes.

Gray said he has partnered with Andrew Keys, head of global business development at Consensys, and has drafted a list of 35 developers and companies Microsoft wants to invite, including the Ethereum Foundation, R3CEV, and BlockApps.

It is reported that the official announcement will be released early this month. In addition, Microsoft has co-authored a new white paper with researchers from Harvard University (to view the full white paper, please visit the Coin Library: http://8btc.com/doc-view-844.html) to prove whether Ethereum smart contracts will work as expected. Developers can use these resources to discover problems with the code they write.

Formal Verification

The paper proposes a method of “formal verification” that can prove or disprove the correctness of a software program, in this case, a smart contract.

The white paper also proposes two tools to help verify smart contracts in three ways.

The first is Solidity* , which converts a portion of Solidity code into F* , a programming language that verifies whether a program will execute correctly. The other is EVM * , which decompiles the EVM bytecode statements of the smart contract into Solidity source code.

The second tool is necessary because, out of 112,802 contracts written in Solidity, only 396 can be run on Etherscan, so using bytecode is the best option.

Although Solidity* currently lacks support for complex Solidity features (such as loops), the team was able to translate 46 of the 396 Solidity contracts. After running these 46 contracts through Solidity*, they found that only a few of them were "valid".

“This is a clear sign that most smart contracts are vulnerable,” the paper concluded.

However, it’s worth noting that while many are excited about the rapid development of smart contract security tools, some in the industry believe that in the short term, developers will continue to make mistakes.

Ethereum creator Vitalik Buterin wrote that he does not think the new research will prevent something like The DAO from happening again.

“There will be more mistakes,” Buterin wrote in a recent ethereum blog post, “and we will learn from them.”