在Coq建立一个智能合约核查框架
Danil Annnkov和Bas Spitters
Aarhus大学
PDF版下载：https://kdocs.cn/l/scd3M1Hcd?f=111
[文档] 在Coq中建立智能合约验证框架_translate.pdf
摘要
基于区块链的智能合约的概念自出现以来以几种方式演变。从设计用于验证交易的限制和非图灵完备比特币开始，智能合约的概念扩展到像在Ethereum虚拟机上运行的Solidity这样功能齐全的语言。最近关于智能合约验证的研究发现，在用Solidity[3,6]编写的许多智能合约中存在多个漏洞。智能合约实施中的几次问题导致了巨大的财务损失（例如，DAO合约和 Ethereum上的Parity多签钱包）。智能合约的设置是相当独特的：一旦部署，它们就不能更改，合约逻辑中的任何小错误都可能导致严重的财务后果。这不仅表明了正式验证智能合约的重要性，也表明了有原则的编程语言设计的重要性。下一代智能合约语言倾向于采用功能编程范式。许多区块链实现已经采用了某些功能语言的变体作为底层智能合约语言。这些语言从简约和低级别 (Simplicity [5], Michelson)，到功能齐全的OCaml-和Haskell类语言(Liquidity[2], Plutus)。这种趋势有一个很好的理由。静态类型的功能编程语言可以排除许多错误。此外，由于没有（或更精确的控制）功能语言中的副作用程序表现为数学函数，使推理更容易。然而，人们不能希望只执行无状态计算：状态是区块链固有的。解决这一问题的方法之一是限制改变国家的方式。虽然Solidity允许在任何执行点进行任意状态修改，但许多现代智能合约语言将智能合约执行表示为从当前状态到新状态的函数。现代智能合约语言的这种功能性质使它们非常适合于形式推理。
Ethereum虚拟机和Solidity智能合约语言仍然是编写智能合约最常用的平台之一。由于底层执行模型的允许性和语言验证在此设置中的复杂性是相当具有挑战性的。另一方面，许多新一代语言，如Oak, Liquidity and Scilla，提供了一个不同的执行模型和类型系统，允许通过类型检查来排除许多错误。当然，即使使用功能强大的智能合约语言类型系统，也无法捕获许多重要的属性。因此，为了提供更高的保证，例如功能正确性，人们必须使用更强的类型系统/逻辑来推理程序和使用演绎验证技术。 在用于这一目的的各种工具中，证明助手为这一问题提供了一个通用的解决方案。
证明助手，或交互式定理证明者是允许通过与用户交互来陈述和证明定理的工具。证明助手通常通过实现决策和半决策过程，或与自动定理证明器（SAT和SMT求解器）交互，提供一定程度的证明自动化。 一些证明助手允许编写用户定义的自动化脚本，或者使用插件系统编写扩展。 这一点尤为重要，因为编程语言验证中的许多问题是不可避免的，并且为用户提供了一种方便的交互证明方式，同时保留了进行自动推理的可能性，这使得证明助手非常灵活地使用智能合约验证工具。�
功能智能合约语言的现有形式主要集中在元理论上[7]除了Scilla，，它的特点是验证特定的智能合约在Coq语言上通过手工浅层嵌套。Simplicity[5]是一种低层次的基于组合器的功能语言，它的形式化允许从深度到浅层嵌套翻译为元论推理的目的。这些发展都没有将高级功能智能合约语言的深度和浅层嵌套结合在一个框架中，或者提供了一种将智能合约转换为Coq程序的自动方式，以便于验证具体的智能合约。我们正在朝着这个方向努力，允许深和浅的嵌套共存并在Coq中相互作用。
本文的贡献如下：（1）我们开发了一种允许在一个框架内开发智能合约语言的元理论和关于具体合约的方便推理方法；（2）我们使用MetaCoq插件[1]的元编程设施将深度和浅层嵌套结合起来（3）作为我们的方法的实例，我们定义了Oak语言的语法和语义（深度嵌套）以及相应的Oak程序转换为Coq函数（浅层嵌套）；（4）我们证明了作为Oak程序的深度嵌套（抽象语法树）给出的众筹合约的属性。我们在第二章节中讨论了我们的方法的细节，并在第三章节中提供了众筹合约的示例。�
关于证明助手中的功能编程语言的属性，有各种推理方法。首先，让我们将属性分成两组：元论属性（语言本身的属性）和用语言编写的程序的属性。由于我们专注于功能智能合约语言，而且许多证明助手都带有内置的功能语言，因此可以合理地假设我们可以重用证明助手的编程语言，用来表达智能合约和对其属性的推理
hs-to-coq库[8]的作者也采用了类似的方法通过源代码到源代码的转换，将Haskell程序转换为Coq。不幸的是,在在这种情况下，不可能对翻译的正确性进行推理。
�我们希望在同一个框架内有两个功能程序的表示：以抽象语法树（AST）的形式进行深度嵌套，以及作为Coq函数的浅层嵌套。虽然深度嵌套适用于元理论推理，但浅层嵌套便于证明具体程序的性能。我们使用MetaCoq插件�[1]的元编程设施来连接关于功能程序的两种推理方式。
图1中给出了框架结构的概述。比起从hs-to-coq[8]和coq-olocamwel源到源的翻译相比，我们希望所有的重要转换都发生在coq中。 这使得在Coq内部对翻译进行推理和形式化语言所需的元理论成为可能。 也就是说，我们首先使用Haskell、OCaml或其他实现的智能合约语言中的AST，然后通过print程序的desugared AST，在Coq（深度嵌套）中使用相应的感应类型的构造函数生成一个AST表示。 通过print，即一个递归过程，将AST转换为由Coq表示的构造函数组成的字符串。 其主要思想是，这个过程应该尽可能简单，不涉及任何重要操作，因为它将是可信代码基础的一部分。如果需要任何重要的转换，它们应该在Coq中实现。
Meta Coq允许我们将表示为归纳类型的AST转换为Coq项。 因此，从我们的功能语言中的程序语法开始，通过一系列转换，我们产生了一个Meta Coq AST，然后用Coq的Gallina语言（浅嵌套）将其解释为一个程序。转换包括从命名到无名表示的转换（如果需要的话）和转换到Meta Coq AST。 深度嵌套也是智能合约语言元理论发展的输入。
��作为我们的方法的一个例子，我们开发了一个嵌套的Oak智能合约语言到Coq，Oak的语义作为定义解释器。这为我们提供了语言的可执行语义。该解释器是以环境传递的方式实现的，同时使用变量的命名和无名表示。为了能够解释一般的定位点，我们评估定位点在扩展环境中的应用与递归调用对应的闭包。由于潜在的非终止，我们使用燃料习语来定义我们的解释器：通过对附加参数的结构递归（a自然数）
图2：众筹合约
作为我们方法的一个例子，我们考虑验证众筹合约的一些属性（图2）。这样的合约允许任意用户在期限内捐款。如果达到众筹目标，业主可以在截止日期过后从账户中提取总金额。此外，用户可以在截止日期后撤回他们的捐款，如果目标尚未达到。像这样的合约是智能合约的标准应用程序，并出现在许多教程中。我们以Scilla[7]为例，采用（略有变化）众筹合约作为演示验证技术的好例子。
我们广泛地使用Coq的一个新特性，称为“自定义条目”，为我们的深度嵌套提供了一个方便的符号-在图形2中特殊括号[\ ... \] 和[| ... |]内写入的的程序文本根据自定义符号规则进行解析。例如，在不使用符号的情况下，action_syn的定义如下：
gdlnd action0[（“transfer”，[（n Anon，ty ind“nat”）；（n Anon，ty ind“nat”）]；（“air”，[]）false。
否则，这个AST将通过一个简单的过程直接从智能合约AST print（正如我们在章节�2）中概述的那样）。我们首先定义所需的数据结构，如状态、操作、结果和MSG意义合约状态、结果类型（相当于Coq的选项类型）和本合约接受的消息。我们为相应的归纳类型、构造函数等名称预先生成字符串常量。使用Meta Coq模板Monad，这允许使用我们的符号机制进行更可读的表示。目前，我们使用NAT类型的Coq来表示帐户地址和货币。 最终，这些类型将被这些原始类型的相应形式所取代。
����trans_global_dec：global_decT mutual_inductive_entry函数采用了数据类型声明的语法，生成了一个mutual_inductive_entry元素——一个用于归纳类型的Meta Coq表示。 对于我们的每一个深度嵌套的数据类型定义，我们在Coq中使用MetaCoq的Make Inductive命令生成相应的归纳类型定义，该命令“解引”给定mutual_inductive_entry类型的实例。 类似的符号机制被用来编写程序使用深度嵌套。众筹的定义代表了众筹合约的语法.. 我们使用expr_to_term：global_envtexprt函数将众筹合约的AST转换为MetaCoqAST。 在这里，global_env是一个包含函数定义中使用的归纳类型声明的全局环境，expr是Oak表达式的类型，术语是MetaCoq术语的类型。 在翻译Oak AST之前，我们应用indexify函数将命名变量转换为DeBruijn索引。 这些转换的结果不引用Make Definition命令。 相应的函数有以下类型的条目：CTXT State_coqT msg_coqT Result_coq，其中CTX是一个调用上下文，包含当前块时间、传输金额、发件人地址和合约调用期间可供检查的其他信息。带有“coq”后缀的类型名称对应于图2中未引用的数据类型。
录入功能对应的是从合约的当前状态过渡到新状态。这允许使用前置和后置条件来证明功能正确性属性。与�[7]类似，我们用浅嵌套法来证明合约的性质. 具体来说，我们证明了以下属性：合约没有泄漏资金；如果在期限内未达到目标，捐款可以退还给支持者；捐赠在合约状态下记录正确。此外，在我们的Coq开发中，我们展示了如何通过证明Oak函数与Coq标准库中的相应函数等价来验证Oak的库代码。 特别是，我们为有限映射上的某些函数提供了这样一个过程的示例。
在本文中，我们重点研究了基于功能编程范式的现代智能合约语言。在许多情况下，这些语言的类型系统可以排除智能合约中的各种小错误。捕获更严重的错误需要使用诸如演绎验证（用于验证具体合约）和元理论的形式化（以确保类型系统的可靠性）等技术。与这类语言的形式相关的作品在章节 1
中提到，包括 Plutus, Michelson, Liquidity, Scilla 和Simplicity等语言。
��我们提出了一项正在进行的关于智能合约核查框架的工作。我们的方法的一个重要特征是能够开发智能合约语言的元理论，并方便地对智能合约进行推理。可以证明智能合约语言的元理论与嵌套的合理性定理。这种选择通常不适用于源到源的翻译。我们将我们的方法应用于Oak智能合约语言的嵌套，并提供了一个从合约的AST开始验证众筹合约的示例。然而，这种方法是相当通用的，适用于其他功能智能合约语言。
��作为未来的工作，我们希望提供与Oak语言基础设施的集成，允许方便地将Oak程序翻译到Coq。 由于我们的框架不专注于一种特定的智能合约语言，我们还考虑通过开发用于翻译其他语言的“后端”来衡量我们的发展。 （例如：Liquidity, Simplicity）。目前，我们的框架允许证明从当前状态到新状态的一个“步骤”对应的合约的功能正确性。为了能够对合约链进行推理，需要在Coq中形成一个执行模型。 我们计划为Oak编程语言的形式化和模型执行，将我们的开发与正在进行的工作联系起来。[4]
扩展Oak语言元理论的形式也是我们的框架目标之一。Oak的元理论的一个重要部分是成本语义，允许对“gas”进行推理。 我们想给出一个深度嵌套的成本语义，并探讨如何在浅层嵌套上扩展它。
参考文献
[1] Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. Towards
Certified Meta-Programming with Typed Template-Coq. In ITP18, volume 10895 of LNCS, pages
20–39, 2018.
[2] C¸ agdas Bozman, Mohamed Iguernlala, Michael Laporte, Fabrice Le Fessant, and Alain Mebsout.
Liquidity: OCaml pour la Blockchain. In JFLA18, 2018.
[3] Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. Making smart con�tracts smarter. In CCS16, pages 254–269, 2016.
[4] Jakob Botsch Nielsen and Bas Spitters. Smart Contract Interactions in Coq. Submitted to FMBC19.
[5] Russell O’Connor. Simplicity: A New Language for Blockchains. PLAS17, pages 107–120. ACM,
2017.
[6] Ilya Sergey and Aquinas Hobor. A concurrent perspective on smart contracts. In Financial Cryp�tography and Data Security, pages 478–493, 2017.
[7] Ilya Sergey, Amrit Kumar, and Aquinas Hobor. Scilla: a Smart Contract Intermediate-Level LAn�guage. CoRR, abs/1801.00687, 2018.
[8] Antal Spector-Zabusky, Joachim Breitner, Christine Rizkall
