这些智能合约漏洞，可能会影响你的帐户安全！

摘要：区块链联盟链智能合约形式化验证揭秘，解释了咱们为何要对区块链上的智能合约进行形式化验证，以及形式化验证的分类和业界针对每种分类所推出的形式化验证工具，最后做者描述了一下目前形式化验证的种种方法所面临的问题及对于这个领域技术发展的展望。

本文分享自华为云社区《这些智能合约漏洞，可能会影响你的帐户安全！》，做者：麦冬爸 。

什么是形式化验证？

维基百科对形式化验证的解释是这样的：在计算机硬件（特别是集成电路）和软件系统的设计过程当中，形式化验证的含义是根据某个或某些形式化规范或属性，使用数学的方法证实其正确性或非正确性。传统上在硬件设计领域比较经常使用。主要缘由就是硬件设计周期长，成本高，一旦生产出来就很难改动了。例如一个 CPU 设计若是已经出芯片了，那么出了问题就是大事。形式验证能够分为三大类：抽象解释（AbstractInterpretation）、形式模型检查（FormalModel Checking，也被称做特性检查）和定理证实（TheoryProver）。

区块链智能合约为何须要形式化验证？

在区块链系统中能够编程且自动运行的程序被称为智能合约。智能合约最先在以太坊区块链平台上应用，如 Solidity 就是一种智能合约编程语言，以使传统应用程序开发人员可以编写智能合约。初期会 Solidity 语言的全球只有几百人，后来随着以太坊与区块链的火热，参与 Solidity 智能合约的人才开始逐渐增长，可是跟整个 IT 市场的从业人群比起来，会编写智能合约的人仍是太少，大量的 IT 从业者要想开发智能合约只能去学习 Solidity。为了让更多的 IT 从业者能够参与智能合约的编写与业务规则的实现，智能合约平台在原有 Solidity 的基础上扩展了对更多主流语言，甚至高级语言的支持，这样可让多普通 It 从业人员也有了能够进行智能合约编写的可能性，大量熟悉 Java、Go、Php 等技术编程的开发人员均可以参与智能合约的开发。

然而，因为区块链交易是不可变的，智能合约代码中的错误会产生毁灭性的后果，破坏了对底层区块链技术的信任。例如，臭名昭著的 TheDAO 漏洞致使价值近 6000 万美圆的以太损失，奇偶校验钱包漏洞致使价值 1.69 亿美圆的以太永远被锁定。解决这些事件的惟一补救办法是硬分叉区块链，并将其中一个分叉恢复到事件发生前的状态。然而，这种补救办法自己是毁灭性的，由于它摧毁了区块链的核心价值，如不可变性和分散信任。可是智能合约的编写目的是为了行业应用，一旦应用到实际中必须考虑智能合约的安全性，智能合约要达到机器可信，就必须首先排除掉因人为因素而形成的智能合约破坏情形。智能合约形式化验证提供了一种能够证实的安全检验机制，经过形式化语言把合约中的概念、判断、推理转化成智能合约模型，能够消除天然语言的歧义性、不通用性，进而采用形式化工具对智能合约建模、分析和验证，进行一致性测试，最后自动生成验证过的合约代码，造成智能合约生产的可信全生命周期。能够把市场上已经出现的安全风险进行排查与审计，通过审计后的智能合约代码天然安全性就获得加强，同时智能合约形式化验证也是目前对智能合约进行安全保证最可靠的措施。行业应用区块链与智能合约，就须要进行智能合约 的形式化验证，消除安全隐患。

智能合约形式化验证方法分类

业界一般对智能合约进行形式化验证都有一些通用的方法，大致上分为下面几种通用的方法，每种方法都有一些工具和框架进行支撑。

1. 定理证实

定理证实是一种利用演绎推理在符号逻辑中提供证实的形式化方法．在这种方法中，证实的每一个步骤都 会引入一个公理或一个前提，并提供一个陈述，使用谓词逻辑将其进行推导，最终获得想要验证的结果．在证实系统知足关键指望的过程当中，通常使用定理证实器来作辅助验证工做，由于这须要将手工证实的过程变成一系列可以在计算机上运行的符号演算，且能够对正确性进行检查。

其优点是这个方式是使用数学的方法，经过公理或前提进行推导，保证验证的严谨性。其不足是在作数学验证前须要将不一样类型的源代码转换为相关框架的验证代码，而目前没有很好地办法保证在源代码与验证代码之间的转换一致性，实现成本高，自动化水平低，正确性也是很难保证的。在区块链智能合约领域通常对于有高隐私性，安全性，功能性，语义一致性等强烈的需求会经过这种法法来保证。

那业界在定理证实仍是实现了不少工具和框架支撑这一能力，基本有下面的一些工具：

Solidity* and EVM*，该框架使用函数式语言 F*分析验证了 Solidity 智能合约运行时的正确性，F*是一种函数式编程语言，用于形式化验证程序的正确性。

Corral 是 Boogie 语言的分析工具．默认状况下，Corral 会进行有界搜索，直到递归深度和固定数量到达必定限度为止，Boogie 是一种中间验证语言，旨在构建其余语言的验证程序的中间层。

Coq 是一个交互式定理证实助手，它提供了一种形式化的语言来编写数学定义，可执行 算法和定理

Isabelle/HOL 是一个基于高阶逻辑的通用交互式定理证实器。

Raziel 是一个编程框架，用于验证智能合约的多方计算的安全问题，为智能合约的隐私 性提供保障。

2. 符号执行

符号执行（英語：symbolicexecution）是一种计算机科学领域的程序分析技术，经过采用抽象的符号代替精确值做为程序输入变量，得出每一个路径抽象的输出结果。 这一技术在硬件、底层程序测试中有必定的应用，可以有效的发现程序中的漏洞。这种方式的优势是以符号值做为输入，借助相应工具，可获得具体测试用例，具备很高的代码覆盖率。那这种方式本质上属于测试，不能１００％证实智能合约是没有问题的，由于基于测试是很难以 100%覆盖全部的场景，通常在作合约的安全性，功能性验证会推荐使用这种方式。

基于符号执行的业界的一些比较有名的架构以下：

• SASC，这个工具被用来发现潜在的逻辑风险，它是一种静态分析的工具，且能够生成调用关系的拓扑图。

• MAIAN，这个工具被用来查询漏洞，被设计成利用符号分析和具体验证器来跟踪智能合约中的属性。

• Securify，这个工具被用来进行安全漏洞分析，它是一个专门针对以太坊智能合约的工具。

• Mythril，这个工具被用来进行代码安全分析，是一个针对以太坊的智能合约的符号执行的工具。

• Verx 是一个能够自动验证以太坊智能合约功能性的验证器，以太坊相关的问题能够经过上面三个工具组合使用来提升覆盖面。

• Oyente，这个工具被用来检测合约代码潜在的安全漏洞，是一个基于符号执行技术的测试工具。

3. 模型检测

模型检测(modelchecking)，是一种重要的自动验证和分析技术，由 Clarke 和 Emerson 以及 Quelle 和 Sifakis 提出，主要经过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的模态/命题性质。其基本思想是检验一个结构是否知足一个公式要比证实公式在全部结构下均被知足容易得多，进而面向并发系统创立了在有穷状态模型上检验公式可知足性的验证新形式，这种方法也被用于验证智能合约的正确性。

它的优势是可使用市面上现有的模型检测工具，而且支持自动化验证，减小人为参与。可是其没法保证所使用的模型检测工具的完备性与正确性，合约复杂度太高会致使状态空间爆炸，进而致使没法完成验证能力。通常状况下须要保证合约的安全性，功能性会使用这种方式。

业界也有很多这种类型的工具和架构以下：

• NuSMV，这个工具被用于用于工业设计的验证，具备极高的可靠性，且被设计成模型检查的开放架构。它是 SMV 工具的从新实现和扩展，而 SMV 是第一个基于 BDD 的模型检查器。

• BIP， 这个框架包含一整套支持建模、模型转换、仿真、验证和代码生成的工具集，还支持层次化结构, 被设计成为一个通用的系统级形式化建模框架。

• Prism，这个工具只针对表现出随机或几率行为的系统，被设计成一个几率模型检查器，对几率行为进行形式化建模和分析。

• SMC，这个工具被设计成模型检测器，用于检查在不一样公平性假设下并发程序的安全性和活性。

4. 形式化建模

能够经过准确的数学语句和模型组件去定义不一样组件的关系，消除系统中存在的二义性，这种设计系统的技术就是形式化建模。基于这种方式的系统的仿真结果是能够复现的，不会存在偶发性事件。这种方法的优势就是使用精确的数学语句或模型组件来设计系统，从而保证其仿真结果可被复现。可是此方法大多使用市面上已有的建模框架，其框架的完备性与正确性没法保证。基于智能合约的隐私性，安全性和功能性可使用这种方法来检验。Hydra，就是基于形式化建模的一个框架，该框架鼓励开发者和用户诚实地披露智能合约中的错误和漏洞，它的设计是基于漏洞赏金的模式和 NNVP 编程。

5. 有限状态机

有限状态机是一种用来进行对象行为建模的工具，其做用主要是描述对象在它的生命周期内所经历的状态序列，以及如何响应来自外界的各类事件。智能合约的执行也能够看做从一个状态到下一个状态的变迁。

这个方法的优势是思惟导向简单，将智能合约抽象转换为状态机的形式，易于操做，且具备图形界面。可是状态定义的好坏，对智能合约的验证难易程度有很强相关性，合约复杂度太高也会致使状态空间爆炸。对智能合约的安全性，语义一致性校验通常会使用这种方式。

业界通常的工具介绍以下：

• Contract Larva, 这个工具能够验证智能合约运行时的安全情况，它目前只支持以太坊的 Solidity。

• VeriSol，这个工具支持对智能合约语义的一致性进行形式化检测，具体原理是使用访问控制策略检查状态机工做流。

• FSolidM，这个工具能够自动生成以太坊智能合约代码，而且带有图形画界面，界面上支持将智能合约设计为有限状态机的形式并进行验证。

• SPIN，这个工具能够检测一个有限状态系统是否知足 PLTL 公式以及其余一些性质，包括是否有循环或可达性，它是一种显式模型检测工具。

6. 着色 Petri 网

Petri 网是 ２０世纪 ６０年代由 Carl Adam Petri 发 明的，适合于描述异步的、并发的系统模型。所谓的着色 Petri 网就是在原有 Petri 网的基础上加入了颜色集和模型声明等元素，借此能够表达更复杂的类型信息。这种方式的优势是基于已有的 Petri 网模型，进行形式化验证，具备良好的语义描述且具备图形界面。可是当智能合约逻辑较为复杂时，可能会致使可达图生成难度增长，状态空间爆炸等一系列问题。对于智能合约的安全性，功能性验证能够选择此种方式。

当前技术应用的问题与展望

智能合约的形式化验证虽然已经有了一些成果和进展，可是这个领域还只是刚刚开始，离发展完备还有很大的距离，在商用过程当中可能还存有下列问题：

• 易用性问题，形式化验证一般须要具有专业知识的人员参与调试，一般参与编写智能合约的人没法掌握这种技术来检验合约的正确性，须要花费大量金钱找专业人士花很长时间来完成检测。自动化的对智能合约进行形式化验证也存在相关局限性，通常状况下自动化程度越高的方法和框架，验证智能合约的性质越局限。那将自动化形式化验证方法扩大其普世性，而且支持非专业人士使用是急需解决的一个问题，从而才能立于形式化智能合约方法的普遍应用。

• 执行验证的计算机的时间和内存的问题，形式化验证经过探索尽量多的执行状态来发现错误和安全问题的可能性。在这种状况下，计算机运行时内存的上限和执行时间成为复杂程序和协议的基本限制。商用场景中对于用户没法实施检测出结果，须要长时间的等待和分析也会影响相关体验。

• 正确性问题，当咱们使用形式化验证工具时，咱们将代码、安全目标和操做环境经过工具在不一样模型之间转换，将高级语言转换为形式化验证工具支持的语言。工具的执行结果决定了形式化的准确性。可是，咱们没有一个好的工具检查语言转换或者模型转换的准确性，缺少对源代码和目标语言的语义一致性须要进行严格的证实。对于任意的形式化系统，咱们须要经过查看人类的形式化代码来检查正确性，所以这就限制了形式化验证的通常适用性。

• 信任性问题，当前形式化验证智能合约的方法不断增长，如何评判这种方式的准确度，其验证的必要性，验证合约的效率，都要靠开发人员凭借其经验，这种方式是否是和不用形式化验证的测试没有区别。并且当解决问题的成本超过问题自己时，咱们也会质疑解决该问题是否有意义。

咱们相信，随着智能合约应用的法律化、区块链技术的发展，形式化验证方法在智能合约的全生命周期过程当中，将会起到愈来愈重要的做用，获得更广泛的应用。华为区块链服务基于上面的问题以及现有方式出发也打造了本身的形式化验证工具，给出了其证实内容的正确性和必要性，而且提升其验证效率，也是为业界使用自动化形式化验证方式给出一条探索和思考的路径。

1. Luu, L.; Chu, D.H.; Olickel, H.; Saxena, P.; Hobor, A. Makingsmart contracts smarter. In Proceedings of the ACM SIGSAC Conf. Comput. Commun.Securit, New York, NY, USA, 24–28 October 2016; pp. 254–269.

2. Atzei, N.; Bartoletti, M.; Cimoli, T. A Survey of Attacks onEthereum Smart Contracts (SoK). In Proceedings of the Int. Conf. Princ. Secur.Trust, Uppsala, Sweden, 22–29 April 2017; pp. 164–186. 3. The DAO Attacked:Code Issue Leads to $60 Million Ether Theft. Available online:www.coindesk. com/dao-attacked-code-issue-leads-60-million-ether-theft/(accessed on 17 June 2017).

3. Liu, J.; Liu, Z.T. A Survey on Security Verification of BlockchainSmart Contracts. IEEE Access 2019, 7, 77894–77904. [CrossRef]

4. 王璞巍，杨航天，孟佶，等．面向合同的智能合约的形式化定义及参考实现［Ｊ］．软件学报，２０１９，３０（９）：２６０８－２６１９．

5. 胡凯，白晓敏，等．智能合约的形式化验证方法［Ｊ］．信息安全研究，２０１６，２（１２）：１０８０－１０８９．

点击关注，第一时间了解华为云新鲜技术~