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

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

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

区块链技术成熟度曲线（来自Gartner,2018）

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

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

一个智能合约是一套以数字形式定义的承诺（promises），包括合约参与方可以在上面执行这些承诺的协议。

智能合约理念几乎与互联网(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)被爆出现合约漏洞，多达数十亿代币被盗。

智能合约本质上是一段运行在区块链网络中的代码，而代码在设计和开发过程中，不可避免出现漏洞。部署在公链上的智能合约，由于暴露在开放网络上，容易被黑客获得，成为黑客的金矿和攻击目标，造成无法弥补的损失。

三、形式化验证方法保障智能合约安全

梆梆安全研究院在研究区块链安全时发现，加强智能合约审计是提高区块链安全的重要保证，其中形式化验证是解决智能合约审计的一个有效方法。

所谓形式化验证方法，即指在计算机科学领域，特别是软件工程和硬件工程中，一种特殊的基于数学的技术，用于规范、开发和验证软件和硬件系统，以提高系统的安全性、可靠性和鲁棒性。形式化方法可以形容为建立在相当广泛的理论计算机科学基础上的应用，特别是逻辑演算、形式语言、自动机理论、离散事件动态系统和程序的语义，还包括类型系统和代数数据类型等理论。一般这类研究主要应用于昂贵的航空、航天、军事器材的操作系统、危险的医疗设备程序之中。

形式化验证方法就是基于已建立的形式化规格，对所规格系统的相关特性进行分析和验证，以评判系统是否满足期望的特性。形式化验证并不能完全确保系统的性能正确无误，但是可以最大限度地理解和分析系统，并尽可能地发现其中不一致性、模糊性、不完备性等错误。形式化验证可用来消除高风险代码漏洞。

形式化验证主要包括定理证明和模型验证两种技术：

现有的定理证明器包括：用户导引自动推演工具、证明检验器和复合证明器。用户导引自动推演工具有ACL2、Eves、LP、Nqthm、Reve和RRL，这些工具由引理或者定义序列导引，每一个定理采用已建立的推演、引理驱动重写和简化启发式来自动证明；证明检验器有Coq、HOL、LEGO、LCF和Nuprl；复合证明器Analytica中将定理证明和符号代数系统Mathematica复合，PVS和Step将决策过程模型检验和交互式证明复合在一体。
模型检验是一种基于有限模型并检验该模型的期望特性的一种技术。粗略地讲，检验就是状态空间的蛮力搜索，模型的有限性确保了搜索可以终止。模型检验有两种主要方法。其一是时态模型检验，该方法中规格以时态逻辑形式表述，系统模拟为有限状态迁移系统。有效的搜索过程用来检验给定的有限状态迁移系统是否是规格的一个模型。另一种方法中，规格以自动机方式给出，系统也模拟为一个自动机。系统的自动机模型和规格比较，以确定其行为是否与规格的自动机模型一致。基于模型检验的工具有描述语言为Promela 的SPIN和UPPAL等。

智能合约采用全生命周期的形式化验证，在设计和开发过程都可用形式化验证，代码的形式化验证在统一的环境可以采用源码和编译后的字节码进行双管齐下的验证，源代码进行转换验证，编译后的字节码进行反编译验证低级别性能，两个验证方法利用等价证明保证功能、运行上的一致。如以太坊可用在F*环境下进行验证，反编译字节验证gas总量上限。

梆梆安全研究院于2016年就开始布局区块链安全，最初着手于区块链的私钥安全研究，之后开始逐渐深入研究基于区块链的数字货币交易系统、业务系统的安全性问题。在研究过程中梆梆安全研究院发现，作为区块链第二代技术的核心创新点——智能合约，其安全性问题非常重要，需要用形式化验证的方法保障其安全，由此来有效抵御利用智能合约安全漏洞所发起的恶意攻击，并降低因此而产生的巨大经济损失。