如何验证区块链开发程序和验证程序的正确性

无bug编程是一项艰巨的任务，也是关键系统面临的基本挑战。为此，形式化方法提供了开发程序和验证程序正确性的技术。

正式核查是一项艰苦的工作。它要求很高，需要大量的脑力，需要大量的投资，但它已经成为软件行业许多领域的强制性标准。

从区块链的早期开始，这种科学似乎就违背了开发人员采用这种技术的必要性，但同时也降低了这种必要性。最流行的智能合约语言的成功难道不归功于它类似javascript的语言吗？

但是，采用这种方式是一把双刃剑：与以前的任何其他网络相比，经济上都会直接受到威胁。

既然新的共识方法和区块链协议的安全性得到了越来越多的科学文献的支持，现在是时候重新引入正式的方法，让智能合与开发人员受益了。经过几十年的研究，这门科学是建立分散式应用信心的必要纽带。

本文旨在介绍正式的验证，回顾区块链时代的现有工具，并强调以太坊特有的挑战。

正式验证的简短介绍

智能合约是一种自我执行的工具，它的增长是随着区块链的兴起而出现的。随着这项技术的采用，这些金融工具的实际存款额不断增加，同时它们的复杂性也严重升级。这种情况会周期性地导致代价高昂的bug和漏洞，从而为更严格的程序分析方法带来光明。

在这方面，在永久部署分散式的应用程序之前，测试和审计通常为开发人员和用户提供一定的保证。但是，由于没有代码检查可以100%保证消除所有bug，所以正式的验证可以通过数学方法带来更高的可信度。这就是为什么这一领域受到以太坊基金会的积极支持，并可能迅速得到更广泛的应用。

在进一步讨论之前，应该简要介绍一些数学概念。

正确性： 如果一个程序执行分配给它的任务没有错误，并且在所有可能的情况下都是正确的，那么这个程序就是正确的。

规范： 程序的规范是对分配给它的任务和允许用例的明确描述。指定一个程序需要抽象它的属性，因此是一项困难的任务。根据规范验证程序实现的正确性也很困难。

动态分析包括执行代码或模拟代码，以发现任何bug。创建测试计划包括列出要测试的用例，并为每个用例建立一个测试。由于这些测试不能全面，动态分析一般不能构成正确性的证明。

另一方面，静态分析包括遍历代码而不执行代码，以证明某些属性。存在不同的方法，例如基于模型检查或Hoare逻辑。形式验证依赖于静态分析。

Hoare逻辑有助于证明，从验证某些属性的初始状态（前置条件）开始，通过执行一系列指令，我们可以获得验证其他属性的状态（后置条件）。如果总是这样，这就叫做完全正确。

如果有一个带有Hoare三元组（前置条件-指令-后置条件）的自然演绎，那么程序相对于其前置条件和后置条件是正确的。

像Coq这样的证明助手帮助交互式地构建这样的演绎树。

总结一下，要理解正式验证智能合约的挑战，必须牢记两个基本概念：

1. 我们不能证明合约是明智的。我们证明了它们的一些性质。我们根据规范证明了它们的正确性。

2. 要被认为是有效的，必须在一个单一的、可信的逻辑框架内生成一个证明，从规范语言级别到虚拟机执行级别。

在构建区块链时考虑到验证

2016 年初，一组研究人员分析了部署在以太坊主网上的字节码，以查找常见的安全缺陷。他们惊人的评估被大量引用：在19366份研究合约中，8833份至少存在一次安全漏洞。在本文提倡改进以太坊的操作语义以帮助形式化验证的同时，出现了一个问题：一些区块链框架是否比其他框架更不容易进行形式化验证？

很难否认，每个区块链都是为了满足特定的期望子集而设计的，比如快速采用或安全性。

直接的结果是，正式的验证在一些框架上是当前的现实，而在另一些框架上可能是长期的目标。

在这方面，2018年发表的一份有趣的研究报告概述了合同语言和验证方法，作为对当前解决方案的全面调查。它有助于确定以下区分因素，并概述当前主要框架上正式方法的可用性。

合约语言

在软件行业，特别是在区块链领域，区分三种类型的语言是很有帮助的：

· 高级语言，如以太坊上的solability或Vyper， Tezos上的Liquidity，都旨在易于学习，并帮助大型开发人员社区编写智能契约。

· 底层基于堆栈的语言，如比特币脚本，代表了实际机器之前的最后一个抽象步骤

· 中间表示，如Tezos上的Michelson或Ziliqa上的Scilla，是对合约验证和代码优化最合适的支持。

图1：不同级别的智能合约语言和编译过程。（A）与更直接的（B）相比，便于验证和代码优化。

只有一种低级语言，比特币脚本在于第一个区块链上编写智能合约。当图灵完备的区块链框架出现时，就需要更富表现力的高级合约语言。

它们中的一些本质上允许直接编译字节码，如（B） path（图1）所示。例如，在以太坊上，solid作为一种智能合约语言被广泛采用，开发人员的代码可以直接编译为EVM字节码。

还设计了其他高级语言，以便可以首先将合约代码编译为中级表示，然后再编译为低级语言，如（a） path（图1）所示。

由于促进了中间代码的正式验证，不同的区块链框架在验证智能合约方面的能力出现了重大差异。

验证方法

根据前面对语言的分类，我们可以区分出三种主要的验证方法：

（I）：规范可以直接在字节码级别进行评估。由于合约源不一定可用，因此提供了一种方法来评估已经部署的合约上的一些属性。

（II）：中间表示形式可专门设计为验证工具（例如证明助手）的目标。这可以根据规范为代码优化和动态验证提供非常合适的环境。中间代码表示形式可以来自高级合约的编译，也可以来自低级代码的反编译。

（III）：一些工具也直接针对高级语言进行推理。这种方法在验证时为开发人员提供了宝贵的直接反馈。

图2：基于与规范化比较对象的不同验证方法。

正式的语义

当新的编程语言出现时，它们的语义可能被正式地描述出来。程序的确切行为由正式语义定义，而对于具有非正式语义的语言，则需要更灵活性的编译器。

在大多数情况下，定义在任何级别上使用的所有语言的正式语义都是至关重要的，因为它为开发单个可信逻辑框架提供了条件，在这个框架中，从一种形式主义到另一种形式的转换都要经过正式建模和验证。

所有翻译的正确性决定了一个人对整个框架的信心程度。如果对程序的中间表示形式执行形式化验证，则反向翻译将允许以更高级别的原始语言显示有意义的消息。此外，如果转换成机器字节码不安全，那么没有人可以正式信任它的执行，无论在其他级别的验证工作如何。

例如，与Tezos和Cardano相反，EVM的正式语义只被描述在帖子前。并且，由于 Solidity 编译器变化迅速，在缺少允许逐构造自动生成验证工具的正式语义的情况下，后者也需要遵循变化的速度。这些原因使得在以太坊上对智能合约的正式验证比其他区块链更难。

到目前为止，以太坊的实际合约验证

如上所述，静态分析可以用多种方法进行。在智能合约中，大多数都是基于模型或基于验证的。在以太坊上介绍有前途的项目，并将注意力吸引到他们的LIM上，这可能会带来惊人的启示。

在以上综述的基础上，介绍以太坊上有前途的项目，并提请注意它们的局限性，这可能具有惊人的启示意义。

智能合约的模型检查表明，由于状态组合，智能合约在实践中不可行。基于VeriSolid•的模型提供了一个方便的界面来排列，还避免了已知安全流而构建的块，从而强加一些属性，并自动生成正确的Solidity 智能合约。但是，到目前为止，仅支持一组属性，不能将 Solidity 代码编译为字节码。

基于Hoare 逻辑的几个项目寻求带来的益处，以正式验证其源代码中智能合约。一些人试图对 Solidity 代码进行说明 ，而另一些人则选择直接使用ML 函数式编程语言进行开发，从而获得正确的构建程序。这种类型的努力可能会引起很多关注，因为它们会导致强大的开发人员工具和出色的经验。

然而，应该指出的是，在Why3中实现所有可靠类型和逻辑（公共/私有函数、gas注意事项……）需要大量的工作，而且目前还没有从Why3到EVM的可生产的完整编译器。

研究团队还尝试对字节码进行全编译，以验证中间表示的前期/后期样式中的协定属性。但更复杂的合约需要全面实施 EVM 字节码，例如，可以这样评估一些GAS消耗属性。当还支持从高级语言翻译为相同的中间表示形式时，可以验证功能正确性，并使在两个中间表示形式（一个来自高级代码的编译，另一个来自字节码的反编译）等效。如果没有，由于缺乏可用的用户反馈，这种方法不太可能帮助开发人员在实践中验证他们的智能合约。

目前在以太坊上可用的最完整的环境可能是K-framework。如果定义了语言的正式规范，它就可以处理各种工具的自动生成，比如解释器和编译器。尽管如此，这个框架要求很高（需要大量规范的手工翻译，这很容易出错），而且仍然存在一些缺陷（例如，主网上的EVM实现可能与机器语义不匹配）。尽管如此，已经进行了大量的工作来使这个现有的框架适应区块链。

结论

随着区块链价值的增加和分散化应用程序复杂性的增加，推广一种更严格的程序分析方法似乎是向客户和合与所有者提供更高安全级别的唯一可接受的方法。

形式验证是一门成熟的科学，可以为实现这一目标作出重大贡献。但是，尽管一些区块链的设计考虑到了这一目标，但在以太坊上验证智能合与，尤其是那些以可靠方式编写的合与，还远远不够明显。然而，在其他框架上，今天可以进行正式的验证。现在要靠分散式应用程序的创建者来迎接这一挑战，并努力为更安全的智能合约铺平道路。