形式化验证：让智能合约更安全

区块链是一种分布式账本技术，其通过提供业务交易和数字资产的一致性、不可变性来提高参与方的可信度，还能通过交易中提供更大的透明度来减少参与方之间的摩擦，这些特性使得更多行业的应用场景得以重塑。区块链技术的快速发展，促使企业架构和技术创新的领导人开始重新思考分布式信任世界里的价值交换概念，同时也因之而滋生了众多新技术。从下图中能够看出，目前还有许多技术尚处于科技诞生的促动期，如智能合约。

目前数字经济正在向可编程经济时代演进，区块链技术支持着智能资产和智能合约以编程方式促进、核实或执行合同条款，促使着可编程经济的发展。智能合约对可编程经济起着重要的推动作用，但在其应用却面临着种种问题。一直在跟踪研究区块链及其相关技术安全性问题的梆梆安全研究院，结合智能合约的技术发展历程、应用特点和安全风险等，探索出了一套直指其核心本质的安全解决方案。

区块链技术成熟度曲线(来自Gartner,2018)

一、智能合约与区块链完美结合，应用广泛

第二代区块链技术与第一代的显著区别是智能合约的使用，梆梆安全研究院发现智能合约(Smart contract)这个术语在区块链出现之前已出现，至少可以追溯到1995年，由多产的跨领域法律学者、受到广泛赞誉的密码学家尼克·萨博(Nick Szabo)所提出，他在发表于自己网站的几篇文章中提到了智能合约理念，定义如下：

智能合约理念几乎与互联网(world wide web)同时出现，从本质上讲，这些自动合约的工作原理类似于其它计算机程序的if-then语句，一种旨在以信息化方式传播、验证或执行合同的计算机协议。允许在没有第三方的情况下进行可信交易，这些交易可追踪且不可逆转。当一个预先编好的条件被触发时，智能合约执行相应的合同条款。

在计算机上进行智能合约实际应用时，需要控制实物资产保证有效地执行合约，同时做到执行合约条款时，能获取到的第三方审核的合约方的信息，即需要解决信息传递与信任问题。

在无法建立信任关系的互联网上，区块链技术依靠密码学和巧妙的分布式算法，无需借助任何第三方中心机构的介入，用数学的方法使参与者达成共识，保证交易记录的存在性、合约的有效性以及身份的不可抵赖性，解决了互联网上信任和价值传递，为智能合约的广泛应用提供了绝佳的温床。第二代区块链开源项目——以太坊ethereum使用了智能合约，Linux基金会主导推动区块链跨行业应用的开源项目——hyperledge也支持智能合约。智能合约使很多不同类型的程序和操作得以自动化，最明显的体现之处在于支付环节及付款时的步骤操作。

2016年底由智能合约联盟支持下编写的数字商务商会的白皮书介绍了数字身份、抵押、供应链、癌症研究等 12 项智能合约商业使用案例，目前智能合约已在金融、医疗等多个领域实际应用，坊间认为2017年是智能合约元年。

二、智能合约代码漏洞越来越多，频遭攻击

随着人们越来越多地了解区块链技术，以太坊的热度逐渐增加。然而，最新的研究显示基于以太坊架构，被称作是“最安全、最可靠、最方便”的智能合约技术却漏洞百出。来自新加坡国立大学、新加坡耶鲁大学学院和伦敦大学学院的一组研究人员发布了一份报告，声称已经发现了超过34，200个不安全的智能合约。他们还声称其中大约3000个不安全的智能合约可能会造成600万美元的ETH被盗，具体发生的智能合约攻击事件有：

2016年6月18日，TheDAO遭黑客发起Renntrancy攻击，导致300多万以太币资产被分离出DAO资产给自己。

2017年7月21日，智能合约编码公司警告1.5版本及之后的钱包软件存在漏洞，Etherscan.io的数据确认有价值3000万美元的15万以太币被盗;

2017年11月8日，钱包再现重大Bug，多重签名漏洞被黑客利用，导致上亿美元资金被冻结。

2018年4月22日，BEC市场瞬间蒸发64亿人民币，黑客利用以太坊ERC-20智能合约中BatchOverFlow漏洞，攻击了美链BEC的智能合约。

2018年4月25日，各大交易所暂停SmartMesh(SMT)的充值和提现交易， SMT也曝出存在安全漏洞;

2018年5月23日，EDU(EduCoin)被爆出现合约漏洞，多达数十亿代币被盗。