共计 5066 个字符，预计需要花费 13 分钟才能阅读完成。
【摘要】区块链联盟链智能合约形式化验证揭秘，解释了咱们为什么要对区块链上的智能合约进行形式化验证，以及形式化验证的分类和业界针对每种分类所推出的形式化验证工具，最初作者形容了一下目前模式华验证的种种办法所面临的问题及对于这个畛域技术倒退的瞻望。
什么是形式化验证？
维基百科对形式化验证的解释是这样的：在计算机硬件（特地是集成电路）和软件系统的设计过程中，形式化验证的含意是依据某个或某些形式化标准或属性，应用数学的办法证实其正确性或非正确性。传统上在硬件设计畛域比拟罕用。次要起因就是硬件设计周期长，老本高，一旦生产进去就很难改变了。例如一个 CPU 设计如果曾经出芯片了，那么出了问题就是小事。模式验证能够分为三大类：形象解释（Abstract Interpretation）、模式模型查看（Formal Model Checking，也被称作个性查看）和定理证实（Theory Prover）。
区块链智能合约为什么须要形式化验证？
在区块链零碎中能够编程且主动运行的程序被称为智能合约。智能合约最早在以太坊区块链平台上利用，如 Solidity 就是一种智能合约编程语言，以使传统应用程序开发人员可能编写智能合约。初期会 Solidity 语言的寰球只有几百人，起初随着以太坊与区块链的炽热，参加 Solidity 智能合约的人才开始逐步减少，然而跟整个 IT 市场的从业人群比起来，会编写智能合约的人还是太少，大量的 IT 从业者要想开发智能合约只能去学习 Solidity。为了让更多的 IT 从业者能够参加智能合约的编写与业务规定的实现，智能合约平台在原有 Solidity 的根底上扩大了对更多支流语言，甚至高级语言的反对，这样能够让多一般 It 从业人员也有了能够进行智能合约编写的可能性，大量相熟 Java、Go、Php 等技术编程的开发人员都能够参加智能合约的开发。
然而，因为区块链交易是不可变的，智能合约代码中的谬误会产生毁灭性的结果，毁坏了对底层区块链技术的信赖。例如，臭名远扬的 TheDAO 破绽导致价值近 6000 万美元的以太损失，奇偶校验钱包破绽导致价值 1.69 亿美元的以太永远被锁定。解决这些事件的惟一补救方法是硬分叉区块链，并将其中一个分叉复原到事件产生前的状态。然而，这种补救方法自身是毁灭性的，因为它捣毁了区块链的外围价值，如不可变性和扩散信赖。然而智能合约的编写目标是为了行业利用，一旦利用到理论中必须思考智能合约的安全性，智能合约要达到机器可信，就必须首先排除掉因人为因素而造成的智能合约毁坏情景。智能合约形式化验证提供了一种能够证实的平安测验机制，通过形式化语言把合约中的概念、判断、推理转化成智能合约模型，能够打消自然语言的歧义性、不通用性，进而采纳形式化工具对智能合约建模、剖析和验证，进行一致性测试，最初主动生成验证过的合约代码，造成智能合约生产的可信全生命周期。能够把市场上曾经呈现的平安危险进行排查与审计，通过审计后的智能合约代码天然安全性就失去加强，同时智能合约形式化验证也是目前对智能合约进行平安保障最牢靠的措施。行业利用区块链与智能合约，就须要进行智能合约 的形式化验证，打消安全隐患。
智能合约形式化验证办法分类
业界通常对智能合约进行形式化验证都有一些通用的办法，大体上分为上面几种通用的办法，每种办法都有一些工具和框架进行撑持。
- 定理证实
定理证实是一种利用演绎推理在符号逻辑中提供证实的形式化办法．在这种办法中，证实的每个步骤都 会引入一个公理或一个前提，并提供一个陈说，应用谓词逻辑将其进行推导，最终失去想要验证的后果．在证实零碎满足要害冀望的过程中，个别应用定理证实器来做辅助验证工作，因为这须要将手工证实的过程变成一系列可能在计算机上运行的符号演算，且能够对正确性进行查看。
其劣势是这个形式是应用数学的办法，通过公理或前提进行推导，保障验证的严谨性。其有余是在做数学验证前须要将不同类型的源代码转换为相干框架的验证代码，而目前没有很好地方法保障在源代码与验证代码之间的转换一致性，实现老本高，自动化程度低，正确性也是很难保障的。在区块链智能合约畛域个别对于有高隐衷性，安全性，功能性，语义一致性等强烈的需要会通过这种法法来保障。
那业界在定理证实还是实现了很多工具和框架撑持这一能力，根本有上面的一些工具：
Solidity and EVM，该框架应用函数式语言 F 剖析验证了 Solidity 智能合约运行时的正确性，F 是一种函数式编程语言，用于形式化验证程序的正确性。
Corral 是 Boogie 语言的剖析工具．默认状况下，Corral 会进行有界搜寻，直到递归深度和固定数量达到肯定限度为止，Boogie 是一种两头验证语言，旨在构建其余语言的验证程序的中间层。
Coq 是一个交互式定理证实助手，它提供了一种形式化的语言来编写数学定义，可执行 算法和定理
Isabelle/HOL 是一个基于高阶逻辑的通用交互式定理证实器.
Raziel 是一个编程框架，用于验证智能合约的多方计算的平安问题，为智能合约的隐衷 性提供保障.
- 符号执行
符号执行（英語：symbolic execution）是一种计算机科学畛域的程序剖析技术，通过采纳形象的符号代替准确值作为程序输出变量，得出每个门路形象的输入后果。这一技术在硬件、底层程序测试中有肯定的利用，可能无效的发现程序中的破绽。这种形式的长处是以符号值作为输出，借助相应工具，可失去具体测试用例，具备很高的代码覆盖率。那这种形式实质上属于测试，不能100%证实智能合约是没有问题的，因为基于测试是很难以 100% 笼罩所有的场景，个别在做合约的安全性，功能性验证会举荐应用这种形式。
基于符号执行的业界的一些比拟有名的架构如下：
SASC，这个工具被用来发现潜在的逻辑危险，它是一种动态剖析的工具，且能够生成调用关系的拓扑图。
MAIAN，这个工具被用来查问破绽，被设计成利用符号分析和具体验证器来跟踪智能合约中的属性。
Securify，这个工具被用来进行安全漏洞剖析，它是一个专门针对以太坊智能合约的工具。
Mythril，这个工具被用来进行代码平安剖析，是一个针对以太坊的智能合约的符号执行的工具。
Verx 是一个能够主动验证以太坊智能合约功能性的验证器，以太坊相干的问题能够通过下面三个工具组合应用来进步覆盖面。
Oyente，这个工具被用来检测合约代码潜在的安全漏洞，是一个基于符号执行技术的测试工具。
- 模型检测
模型检测 (model checking)，是一种重要的主动验证和剖析技术，由 Clarke 和 Emerson 以及 Quelle 和 Sifakis 提出，次要通过显式状态搜寻或隐式不动点计算来验证有穷状态并发零碎的模态 / 命题性质。其根本思维是测验一个构造是否满足一个公式要比证实公式在所有构造下均被满足容易得多，进而面向并发零碎创建了在有穷状态模型上测验公式可满足性的验证新模式，这种办法也被用于验证智能合约的正确性。
它的长处是能够应用市面上现有的模型检测工具，并且反对自动化验证，缩小人为参加。然而其无奈保障所应用的模型检测工具的齐备性与正确性，合约简单度过高会导致状态空间爆炸，进而导致无奈实现验证能力。个别状况下须要保障合约的安全性，功能性会应用这种形式。
业界也有不少这种类型的工具和架构如下：
NuSMV，这个工具被用于用于工业设计的验证，具备极高的可靠性，且被设计成模型查看的凋谢架构。它是 SMV 工具的从新实现和扩大，而 SMV 是第一个基于 BDD 的模型查看器。
BIP，这个框架蕴含一整套反对建模、模型转换、仿真、验证和代码生成的工具集，还反对层次化构造, 被设计成为一个通用的零碎级形式化建模框架。
Prism，这个工具只针对体现出随机或概率行为的零碎，被设计成一个概率模型查看器，对概率行为进行形式化建模和剖析。
SMC，这个工具被设计成模型检测器，用于查看在不同公平性假如下并发程序的安全性和活性。
- 形式化建模
能够通过精确的数学语句和模型组件去定义不同组件的关系，打消零碎中存在的二义性，这种设计零碎的技术就是形式化建模。基于这种形式的零碎的仿真后果是能够复现的，不会存在偶发性事件。这种办法的长处就是应用准确的数学语句或模型组件来设计零碎，从而保障其仿真后果可被复现。然而此办法大多应用市面上已有的建模框架，其框架的齐备性与正确性无奈保障。基于智能合约的隐衷性，安全性和功能性能够应用这种办法来测验。Hydra，就是基于形式化建模的一个框架，该框架激励开发者和用户诚恳地披露智能合约中的谬误和破绽，它的设计是基于破绽赏金的模式和 NNVP 编程。
- 无限状态机
无限状态机是一种用来进行对象行为建模的工具，其作用次要是形容对象在它的生命周期内所经验的状态序列，以及如何响应来自外界的各种事件。智能合约的执行也能够看作从一个状态到下一个状态的变迁。
这个办法的长处是思维导向简略，将智能合约形象转换为状态机的模式，易于操作，且具备图形界面。然而状态定义的好坏，对智能合约的验证难易水平有很强相关性，合约简单度过高也会导致状态空间爆炸。对智能合约的安全性，语义一致性校验个别会应用这种形式。
业界个别的工具介绍如下：
Contract Larva, 这个工具能够验证智能合约运行时的平安情况，它目前只反对以太坊的 Solidity。
VeriSol，这个工具反对对智能合约语义的一致性进行形式化检测，具体原理是应用拜访控制策略查看状态机工作流。
FSolidM，这个工具能够主动生成以太坊智能合约代码，并且带有图形画界面，界面上反对将智能合约设计为无限状态机的模式并进行验证。
SPIN，这个工具能够检测一个无限状态零碎是否满足 PLTL 公式以及其余一些性质，包含是否有循环或可达性，它是一种显式模型检测工具。
- 着色 Petri 网
Petri 网是 20世纪 60年代由 Carl Adam Petri 发 明的，适宜于形容异步的、并发的零碎模型。所谓的着色 Petri 网就是在原有 Petri 网的根底上退出了色彩集和模型申明等元素，借此能够表白更简单的类型信息。这种形式的长处是基于已有的 Petri 网模型，进行形式化验证，具备良好的语义形容且具备图形界面。然而当智能合约逻辑较为简单时，可能会导致可达图生成难度减少，状态空间爆炸等一系列问题。对于智能合约的安全性，功能性验证能够抉择此种形式。
以后技术利用的问题与瞻望
智能合约的形式化验证尽管曾经有了一些成绩和停顿，然而这个畛域还只是刚刚开始，离倒退齐备还有很大的间隔，在商用过程中可能还存有下列问题：
易用性问题，形式化验证通常须要具备专业知识的人员参加调试，通常参加编写智能合约的人无奈把握这种技术来测验合约的正确性，须要破费大量金钱找专业人士花很长时间来实现检测。自动化的对智能合约进行形式化验证也存在相干局限性，个别状况下自动化水平越高的办法和框架，验证智能合约的性质越局限。那将自动化形式化验证办法扩充其普世性，并且反对非专业人士应用是急需解决的一个问题，从而能力立于形式化智能合约办法的广泛应用。
执行验证的计算机的工夫和内存的问题，形式化验证通过摸索尽可能多的执行状态来发现错误和平安问题的可能性。在这种状况下，计算机运行时内存的下限和执行工夫成为简单程序和协定的根本限度。商用场景中对于用户无奈施行检测出后果，须要长时间的期待和剖析也会影响相干体验。
正确性问题，当咱们应用形式化验证工具时，咱们将代码、平安指标和操作环境通过工具在不同模型之间转换，将高级语言转换为形式化验证工具反对的语言。工具的执行后果决定了形式化的准确性。然而，咱们没有一个好的工具查看语言转换或者模型转换的准确性，不足对源代码和目标语言的语义一致性须要进行严格的证实。对于任意的形式化零碎，咱们须要通过查看人类的形式化代码来查看正确性，因而这就限度了形式化验证的个别适用性。
信赖性问题，以后形式化验证智能合约的办法一直减少，如何评判这种形式的准确度，其验证的必要性，验证合约的效率，都要靠开发人员凭借其教训，这种形式是不是和不必形式化验证的测试没有区别。而且当解决问题的老本超过问题自身时，咱们也会质疑解决该问题是否有意义。
咱们置信，随着智能合约利用的法律化、区块链技术的倒退，形式化验证办法在智能合约的全生命周期过程中，将会起到越来越重要的作用，失去更广泛的利用。华为区块链服务基于下面的问题以及现有形式登程也打造了本人的形式化验证工具，给出了其证实内容的正确性和必要性，并且进步其验证效率，也是为业界应用自动化形式化验证形式给出一条摸索和思考的门路。