Microsoft Launches Smart Contracts Security Working Group

Microsoft has revealed it is organizing a working group dedicated to improving smart contracts security.

Named 'Kinakuta', the group aims to make it easier for the industry to share information and tips about smart contracts, the term that somewhat loosely has come to refer to self-executing blockchain-based code.

Yet even while incumbents increasingly express interest in the idea blockchains could come to automate complex transactions, concerns about this use case have grown after a vulnerability led to the collapse of the technology's first large-scale implementation, The DAO.

Since then, there has been a growing realization that smart contracts are new and can sometimes be dangerous if used improperly.

However, Microsoft's director of business development and strategy Marley Gray believes open information and new tools might help developers avoid future mistakes.

Gray told CoinDesk:

"We feel there’s a huge opportunity here to involve the community. Kinakuta is the community building around Microsoft best practices and elsewhere, to collect best practices and tools and involve developers in creating these best practices."

Together with Andrew Keys, head of global business development at Consensys, Gray said he has drafted a list of 35 developers and companies that Microsoft wants in the group. These include organizations like the Ethereum Foundation, which oversees development of the ethereum blockchain; R3CEV, a banking consortium focused on blockchain; and startup BlockApps.

The formal announcement follows news earlier this month that Microsoft had authored a new white paper with researchers from Harvard that outlines a way to prove whether ethereum smart contracts will work as expected.

Developers can potentially use these resources to spot issues with their code.

"We wanted to explore the ability to potentially write smart contracts in a language where from the onset your smart contracts would be secure," Gray said.

Formal verification

The paper proposes a method of "formal verification," or the process of proving or disproving the correctness of a software program, or in this case, a smart contract.

This paper is one of the latest in a wave of tools trying to make smart contracts safer, such as entirely new programing languages tailored to smart contracts. The white paper proposes two tools to help verify smart contracts in three ways.

The first is Solidity*, which translates a piece of Solidity code to F*, a programming language that verifies whether programs will act as they should. Then there's EVM*, which decompiles the EVM bytecode representation of a smart contract to the Solidity source code.

This second tool is necessary because only 396 out of 112,802 contracts made the Solidity version of the code available on Etherscan at the time of the white paper, so using the bytecode is the next best option.

Despite Solidity*’s current lack of support for complex Solidity features like loops, the team was able to translate 46 out of the 396 contracts written in Solidity. After running these 46 contracts through Solidity*, they found that only a few of these contracts were "valid".

"This is a clear sign that a large scale analysis of published contract is likely to uncover widespread vulnerabilities; we leave such analysis to future work," the paper concluded.

However, it's worth noting that while many are excited about the speedy development of tools with a focus on smart contract safety, one industry leader thinks that developers will continue to make mistakes in the near term.

Ethereum creator Vitalik Buterin wrote that he doesn't think that these new areas of research will necessarily stop future situations like The DAO.

"There will be further bugs," Buterin said in an ethereum blog post exploring future smart contract security, “and we will learn further lessons.”

Colorful gears via Shutterstock