据外媒报道，微软透露其正在组织一个工作组，致力于改善智能合约的安全性。

该工作组名为“Kinakuta”，其目标是让行业更容易地分享智能合约信息，而所谓智能合约，是指基于区块链，自动执行的代码。

智能合约的想法虽可自动完成复杂的交易，但当第一个大规模项目The DAO崩溃之后，数字货币社区内有关于智能合约的担忧开始渐渐增多。

自那时以来，人们已逐渐意识到，智能合约这种新事物，如果其使用不当，会是非常危险的。

然而，微软业务发展和战略主管Marley Gray 相信，开放式信息以及新的工具，可帮助开发人员避免类似错误的发生。

Gray表示他已与Consensys公司全球业务发展负责人Andrew Keys达成了合作，并已草拟了35个微软想要邀请的开发者及公司。其中包括以太坊基金会、R3CEV以及BlockApps。

据悉，正式的公告将在本月初发布，此外，微软已联合哈佛大学的研究人员共同撰写了一份新的白皮书（查看完整白皮书可访问币文库：http://8btc.com/doc-view-844.html），以证明以太坊智能合约是否会如预期般奏效，开发者可利用这些资源来发现自己所写代码的问题。

 （关注资讯微信公众号，回复关键词“102534”下载报告全文）

形式验证

该论文提出了一种“形式验证”的方法，可证明或反证明一个软件程序的正确性，在这个情况下，就是指一个智能合约。

该白皮书还提出了两个工具，以三种方式来帮助验证智能合约。

第一种是Solidity*，它会将一部分Solidity代码转换为F* ，这是一种验证程序是否会正确执行的编程语言。再有就是EVM *，它会将智能合约的EVM字节码陈述反编译为Solidity源代码。

第二种工具是有必要的，因为就目前，通过Solidity 编写的112,802份合约当中，可在Etherscan上运行的仅有396份，因此，使用字节码是最好的选择。

尽管 Solidity*目前缺少对复杂型Solidity功能（例如loops）的支持，该团队能够翻译出 396个Solidity合约当中的 46个。通过Solidity*来运行这46个合约之后，他们发现，这些合约当中仅有少部分是“有效”的。

“这是一个明显的迹象，大部分智能合约都存在着漏洞，”该论文总结说。

然而，值得注意的是，虽然很多人对智能合约安全工具的迅速发展感到兴奋，行业当中也有人认为，短期内，开发者们仍将继续犯错。

以太坊的创造者Vitalik Buterin写道，他并不认为这些新研究将阻止The DAO类似事件的发生。

“将会出现更多的错误，” Buterin在最近的一篇以太坊博文中写道，“我们将进一步吸取经验教训。”