智能合约不够安全？微软建专项小组从编程语言入手根治

据外媒报道，微软对外公开其已经成立了一个专门负责提高智能合约安全性的工作小组“Kinakuta”，旨在让行业内共享智能合约信息和协议更加简单。

所谓智能合约，是指基于区块链自动执行命令的代码的合约形式。但由于The DAO等安全事件暴露了该技术还处于早期阶段的现状，不少对区块链抱有希望的人们更多的意识到，如果使用不当时是相当危险的。

不过，微软商业发展和战略主管Marley Gray表示，开放共享的信息和革新的工具或将帮助开发者在未来避免类似错误。Gray称，他已经和纽约初创公司ConsensYs的全球业务发展负责人Andrew Keys达成了合作，并准备邀请以太坊基金、R3CEV和初创公司BlockApps等35家公司进行合作。

Gray称：“我们想要探索能否有可能在最开始编写智能合约的时候就使用一种安全的语言来书写。”

据悉，微软将于本月不久后推出与哈佛大学研究员共同完成的白皮书，并正式发布成立智能合约小组的公告。这本白皮书提出了一种“形式验证”，或者说证明和反证明一个软件程序的正确性，这里指的就是智能合约。

此外，这个白皮书提出了用三种方法验证智能合约的两个工具：

第一种是Solidity*。将一部分Solidity代码翻译为F*——一种能够验证程序是否会正确执行设计的编程语言。然后还有EVM*，它会把智能合约的EVM字节码陈述反编译为Solidity源代码。

第二个工具十分必要，因为为112802个合约中只有396个可以形成Solidity版本的Etherscan（区块链浏览器）代码，因此未来的最佳选择是使用字节码。

尽管Solidity*目前缺少复杂的Solidity功能支持，比如loops，但团队还是成功地从396份智能合约当中破译出46份。通过Solidity*运行这46份合约之后，他们发现当中只有一小部分是“有效的”。

值得注意的是，虽然许多人对于智能合约安全工具的迅猛发展感到兴奋，白皮书总结道：“很明显，经过对已发布合约的大量分析之后，很有可能会发掘出普遍存在的漏洞；我们把这些分析留给未来的工作。”但也有一位行业领导认为，近期而言，开发者们将会继续犯错。