首页/论文/2106.12973

arXiv 2106.129732021-06-24cs.PL

通过Coq使Tezos智能合约更加可靠

Making Tezos smart contracts more reliable with Coq

Bruno Bernardo, Raphaël Cauderlier, Guillaume Claret, Arvid Jakobsson, Basile Pesin, Julien Tesson

DOI：: 10.1007/978-3-030-61467-6_5

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

Tezos是一个智能合约区块链。Tezos的智能合约是用一种名为Michelson的底层堆栈语言编写的。本文概述了使用Coq证明助手对Michelson智能合约进行更强保证的努力：Mi-Cho-Coq框架，定义Michelson形式语义的Coq库，以及解释器，简单优化器和最弱前提演算来推理Michelson智能合约; Albert是一种抽象Michelson堆栈的中间语言，使用以Mi-Cho-Coq为目标的Coq编写的编译器。

英文摘要：

Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. This article gives an overview of efforts using the Coq proof assistant to have stronger guarantees on Michelson smart contracts: the Mi-Cho-Coq framework, a Coq library defining formal semantics of Michelson, as well as an interpreter, a simple optimiser and a weakest-precondition calculus to reason about Michelson smart contracts; Albert, an intermediate language that abstracts Michelson stacks with a compiler written in Coq that targets Mi-Cho-Coq.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Mi-Cho-Coq，Tezos智能合约认证框架

Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts

Tezos是2018年6月推出的区块链。它是用OCaml编写的，支持智能合约。它的智能合约语言被称为Michelson，它的设计考虑到了形式化验证。在本文中，我们介绍了Mi-Cho-Coq，这是一个用于验证Michelson智能合约功能正确性的Coq框架。作为一个案例研究，我们详细介绍了一个Multisig合同与Mi-Cho-Coq框架的认证。

2019-09-18cs.PL

Albert，Tezos区块链的中间智能合约语言

Albert, an intermediate smart-contract language for the Tezos blockchain

Tezos是一个智能合约区块链。Tezos的智能合约是用一种名为Michelson的底层堆栈语言编写的。在本文中，我们介绍了Albert，这是Tezos智能合约的中间语言，它将Michelson堆栈抽象为线性类型的记录。我们还描述了它的编译器，以迈克尔逊，写在Coq，目标Mi-Cho-Coq，迈克尔逊在Coq实现的正式规范。

2020-01-07cs.PL

Coq中的智能合约交互

Smart Contract Interactions in Coq

我们在Coq中提出了一个智能合约执行的模型/可执行规范。我们的形式化允许合约间通信，并通过允许深度优先执行区块链（如以太坊）和广度优先执行区块链（如Tezos）的建模来推广现有工作。我们用Coq的函数语言Gallina表示智能合约程序，比其他方法更容易推理具体合约的功能正确性。特别是，我们以这种风格制定了一份国会合同。这个合约--臭名昭著的DAO的简化版本--很有趣，因为它与其他合约的通信模式非常动态。我们给出了国会行为的高级部分规范，与可重入性相关，并证明国会满足所有可能的智能合约执行命令。

2019-11-12cs.LOcs.PL

HELMHOLTZ：一个基于细化类型的Tezos智能合约验证器

HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types

DaiLambda, Inc.（DaiLambda公司）；Kyoto University（京都大学）

智能合约是在区块链上执行的程序，许多加密货币都是在此基础上实现的，并被用于自动化交易。由于智能合约涉及大量资金，因此对一种可以静态和正式验证它们的方法的需求激增。本文介绍了我们为Michelson开发的基于类型的静态验证工具HELMHOLTZ，这是一种基于静态类型的堆栈语言，用于编写在区块链平台Tezos上执行的智能合约。HELMHOLTZ是在我们对迈克尔逊类型系统的细化类型扩展之上设计的。HELMHOLTZ以用户定义的规范（以精化类型的形式编写）注释迈克尔逊程序作为输入;然后根据精化类型系统的规范对程序进行类型化，使用SMT求解器Z3释放生成的验证条件。我们简要地介绍了我们的精化类型系统的核心演算迈克尔逊的迷你迈克尔逊，它结合了特征，如复合数据集（例如，列表和对）、高阶函数和调用另一个合约。\HELMHOLTZ{}成功地验证了几个实用的迈克尔逊程序，包括一个向帐户转账和检查数字签名的程序。

2021-09-10cs.CLcs.LOcs.PL

FEther：一个可扩展的Coq智能合约验证解释器

FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq

区块链技术使用加密链接将记录添加到列表中。因此，区块链智能合约的安全性是当代最热门的研究课题之一。为了改进该领域的定理证明技术，我们正在开发一个可扩展的混合验证工具链，表示为FSPVM-E，用于以太坊智能合约验证。这个混合系统扩展了Coq中的证明助手，Coq是一个正式的证明管理系统。结合符号执行与高阶定理证明，它解决了一致性，自动化和可重用性问题的标准定理证明方法。本文通过对FSPVM-E证明引擎的开发，完成了FSPVM-E的实现。FSPVM-E是在我们前期工作FEther的基础上，完全在Coq证明助手上开发的一个可扩展的定义解释器。它支持Solidity编程语言的几乎所有语义，并同时执行多种类型的符号。FEther还包含一组自动化策略，以高自动化水平执行和验证Coq中的智能合约。在Coq中验证了FEther的功能正确性。在标准教程中，FEther的执行效率远远超过Coq中开发的解释器。

2018-10-19cs.PL

基于Coq的混合形式化验证系统用于确保以太坊服务智能合约的可靠性和安全性

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts

本文报告了一个正式的符号过程虚拟机（FSPVM）的开发，表示为FSPVM-E，用于在智能合约的源代码级别验证基于以太坊的服务的可靠性和安全性，并使用Coq证明助手来编程系统并证明其正确性。当前版本的FSPVM-E采用Curry-Howard同构的应用扩展--执行-验证同构作为其基本理论框架，将符号执行和高阶逻辑定理证明结合起来。FSPVM-E的四个主要组件包括通用的、可扩展的和可重用的形式存储器框架、表示为Lolisa的可扩展的和通用的形式中间程序设计语言（其是使用广义代数数据库的Solidity程序设计语言的大子集）、表示为FEther的相应的形式验证的Lolisa解释器以及辅助工具和库。所有组件的自正确性都经过Coq认证。目前，FSPVM-E支持ERC 20令牌标准，可以自动和象征性地执行基于以太坊的智能合约，扫描其标准漏洞，并使用Coq中的Hoare风格逻辑验证其可靠性和安全性。据作者所知，目前的工作代表了第一个在Coq中实现的以太坊智能合约混合形式化验证系统，该系统应用于Solidity源代码级别。

2020-01-23cs.PL

更多相关论文收起更多论文

区块链上合同的类型化编程接口

A Typed Programmatic Interface to Contracts on the Blockchain

区块链上的智能合约应用程序只有通过编程接口与传统软件系统无缝集成，才能充分发挥其潜力。这个接口应该提供发起和调用合同以及观察区块链的状态。为此，我们提出了一个类型化的API，并建立了一些属性的组合系统。具体来说，我们提供了一个执行模型，使我们能够证明程序和区块链之间的类型安全交互。我们建立了模型的进一步属性，这些属性引起了对API的要求。该接口的原型在Tezos区块链的OCaml中实现。

2021-08-29cs.PL

WhylSon：在Why3中验证您的迈克尔逊智能合约

WhylSon: Proving your Michelson Smart Contracts in Why3

本文介绍了WhylSon，一个用Michelson编写的智能合约演绎验证工具，这是Tezos区块链的低级语言。WhylSon接受正式指定的Michelson契约，并自动将其转换为用WhyML（Why3框架的编程和规约语言）编写的等效程序。智能合约指令被映射到其公理语义的相应WhyML浅嵌入中，我们也在这项工作的上下文中开发了这一点。这种方法的一个主要优点是，它允许与Why3框架进行开箱即用的集成，即其VCGen和对几个自动定理证明器的后端支持。我们还讨论了使用WhylSon来自动证明各种注释智能合约的正确性。

2020-05-29cs.PL

SMLtoCoq：从带有合同的SML程序自动生成Coq规范和证明义务

SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts

函数式程序的形式化推理应该是直接和优雅的，然而，它通常不是理所当然的。在证明助手中进行推理需要在那些工具中“重新实现”代码，这远非小事一桩。SMLtoCoq提供SML程序和函数契约到Coq的自动翻译。程序被翻译成Coq规范，函数合同成定理，然后可以正式证明。使用Equations插件和其他成熟的Coq库，SMLtoCoq能够翻译SML程序，而不会产生包含部分函数，结构，函子，记录等的副作用。此外，我们提供了SML基础库的许多部分的Coq版本，因此对这些库的调用几乎保持原样。

2021-07-16cs.LOcs.PL

提取在Coq中测试和验证的智能合约

Extracting Smart Contracts Tested and Verified in Coq

我们实现了基于MetaCoq的认证擦除的Coq程序的函数式语言的提取。作为其中的一部分，我们实现了一个优化通道，删除了未使用的参数。我们证明了这个传递是正确的。函数式语言的传统按值调用操作语义。我们将其应用于两种功能性智能合约语言，Liquidity和Midlang，以及功能性语言Elm。我们的开发是在支持智能合约验证的ConCert框架的背景下完成的。我们提供了一个经过验证的董事会投票智能合约，具有最大的投票者隐私，这样每次投票都是保密的，除非所有其他方勾结。我们还使用QuickChick将基于属性的测试集成到ConCert中，我们的开发是第一个支持交互智能合约测试属性的开发。我们测试了几个复杂的合约，例如类DAO合约，托管合约，包括自定义令牌标准（Tezos FA2）的去中心化金融（DeFi）合约的实现等等。总的来说，这为我们提供了一种用Coq编写依赖程序的方法，半自动地测试它们，验证，然后提取到功能性智能合约语言，同时保留了一个只有MetaCoq和这些语言的漂亮打印机的小型可信计算基础。

2021-04-26cs.LOcs.PL

ConCert：Coq中的智能合约认证框架

ConCert: A Smart Contract Certification Framework in Coq

提出了一种利用元编程将函数式语言嵌入Coq证明助手的新方法。这使我们能够使用深度嵌入来开发语言的元理论，并为使用浅嵌入来推理具体程序提供了一种方便的方法。我们通过一个可靠性定理将深嵌入和浅嵌入联系起来。作为我们方法的一个例子，我们开发了一个核心智能合约语言嵌入到Coq中，并基于区块链中智能合约执行的先前形式化验证了众筹合约的几个重要属性。

2019-12-20cs.LOcs.PL

使用ConCert基于属性的测试框架发现智能合约漏洞

Finding smart contract vulnerabilities with ConCert's property-based testing framework

我们提供了三个关于智能合约漏洞的详细案例研究，并展示了基于属性的测试如何发现它们：1. Dexter 1代币交易所; 2. iToken; 3. Brave的BAT代币的ICO最后一个例子实际上是新的，在审计过程中被遗漏了。我们已经在ConCert中实现了这种测试，ConCert是Coq证明助手中智能合约执行的通用可执行模型/规范。ConCert合约可用于在Tezos的LIGO和Concordium的Rust语言中生成经过验证的智能合约。因此，我们展示了智能合约的形式化验证和基于属性的测试相结合的有效性。

2022-08-01cs.LOcs.PL

从Coq中提取函数式程序，在Coq中

Extracting functional programs from Coq, in Coq

我们实现了基于MetaCoq的认证擦除的Coq程序的函数式语言的提取。我们扩展了MetaCoq擦除输出语言的类型信息，并使用它作为一个中间表示，我们称之为$λ^T_\square$。我们用一个完整的管道来补充提取功能，其中包括以证明生成方式实现的几个标准转换（eta-expansion，inlining等），以及经过验证的优化通道，删除未使用的参数。我们证明了这个传递是正确的。函数式语言的传统按值调用操作语义。从优化的$λ^T_\square$表示中，我们获得了两种功能智能合约语言（Liquidity和CameLIGO）的代码，功能语言Elm和用于系统编程的多范式语言Rust的子集。Rust目前作为智能合约的语言越来越受欢迎，我们演示了如何使用我们的提取来提取Concordium网络的智能合约代码。开发是在支持智能合约验证的ConCert框架的背景下完成的。我们贡献了两个经过验证的真实世界智能合约（董事会投票和托管），我们使用这些合约来验证管道的适用性。此外，我们开发了一个经过验证的Web应用程序，并将其提取为功能齐全的Elm代码。总的来说，这给了我们一种方法来用Coq编写依赖类型的程序，验证，然后将它们提取到几种目标语言，同时保留一个小的可信计算基础，只有MetaCoq和这些语言的漂亮打印机。

2021-08-06cs.LOcs.PL

用于智能合约验证的形式化流程虚拟机

Formal Process Virtual Machine for Smart Contracts Verification

本文报告了一种新的正式符号过程虚拟机（FSPVM）的开发和验证，用于完全在Coq证明助手中验证以太坊智能合约的可靠性和安全性，表示为FSPVM-E。它采用Curry-Howard同构（CHI）的扩展--执行-验证同构（EVI）作为其基本理论框架。当前版本的FSPVM-E构建在通用的、可扩展的和可重用的形式存储器（GERM）框架、可扩展的和通用的形式中间程序设计语言Lolisa（其是使用广义代数数据库的Solidity程序设计语言的大子集）以及Lolisa的相应的形式验证解释器（表示为FEther）上。它支持ERC 20标准，可以自动同时象征性地执行以太坊的智能合约程序，并使用Coq中的霍尔逻辑验证其可靠性和安全性。此外，本文的工作有助于解决高阶逻辑定理证明的自动化、不一致性和可重用性问题。

2018-05-01cs.PL

Crystality 的操作语义：一种面向并行 EVM 的智能合约语言

Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs

本文为面向并行EVM的智能合约语言Crystality提出首个形式化结构操作语义，并在Coq中机械化验证，通过代币转账案例展示其确保合约正确性的能力。

2025-04-24cs.PL

Lolisa：Mathematical Tool Coq中solidity程序设计语言子集的形式语法和语义

Lolisa: Formal syntax and semantics for a subset of the solidity programming language in Mathematical Tool Coq

本文介绍了为Etheruem区块链平台开发的Solidity程序设计语言的一个大子集的形式语法和语义，基于我们最近开发的一个通用的，可扩展的，可重用的形式内存（GERM）框架和Curry-Howard同构的扩展，表示为执行-验证同构（EVI）。这个子集被表示为Lolisa，据我们所知，它是为Solidity开发的第一个机械化和验证的正式语法和语义。Lolisa的形式语法采用了比Solidity更强大的静态类型系统，以增强类型安全性。此外，Lolisa不仅包含Solidity的几乎所有语法组件，如映射、修饰符、合约和地址类型，而且还包含通用程序设计语言功能，如多个返回值、指针算术、结构和字段访问。因此，Lolisa固有的兼容性允许Solidity程序直接翻译成Lolisa，而无需重建或抽象，并且Lolisa固有的通用性允许它扩展到表达其他程序设计语言。为此，我们还提出了一个初步的计划，系统地扩展到其他语言。

2021-01-04cs.PL

SciviK：一个通用的智能合约框架

SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts

区块链上越来越多地采用智能合约带来了新的安全风险，可能导致重大的金钱损失，而现有的方法要么不为智能合约提供（或部分）安全保证，要么需要大量的证明工作。为了应对这一挑战，我们提出了SciviK，这是一个用于指定和验证工业级智能合约的通用框架。SciviK的多功能方法扩展了以前的工作，有三个关键贡献：（i）一个表达性注释系统，支持内置指令进行漏洞模式检查、基于神经的循环不变推理以及验证现实世界智能合约的丰富属性（ii）以太坊虚拟机的细粒度模型（EVM）提供低级执行语义，（iii）集成SMT求解器和Coq证明助手的IR级验证框架。我们使用SciviK来指定和验证12个基准合约和一个真实世界的去中心化金融（DeFi）智能合约的安全属性。在所有158个指定的安全属性（六种类型）中，151个属性可以在2秒内自动验证，5个属性可以在适度修改后自动验证，两个属性需要大约200行Coq代码手动验证。

2021-03-03cs.CRcs.PL

形式化的冒险：金融契约、模块和两级类型论

Adventures in Formalisation: Financial Contracts, Modules, and Two-Level Type Theory

我们提出了三个项目有关证明助手在程序设计语言理论和数学领域的应用。第一个项目是关于金融合同领域特定程序设计语言（CL语言）的认证编译技术。CL中的代码被翻译成一种简单的表达式语言，非常适合与实现蒙特卡罗模拟技术（定价引擎）的软件组件集成。编译过程伴随着在Coq中进行的正确性的正式证明。第二个项目提出的技术，允许从有限的地图和集合建立嵌套和相互归纳的结构进行正式推理。的技术，建立在理论上的名义集结合的能力，同构表示的有限映射，使之有可能给一个正式的治疗，在Coq，高阶模块系统，包括能够消除在编译时引入的模块系统的抽象障碍。开发是基于早期的静态解释模块的工作，并提供了一个高阶模块语言的基础Futhark，优化编译器的目标数据并行架构。第三个项目提出了一个两级类型论的实现，一个版本的马丁-洛夫类型论与两个平等的类型：第一个作为同伦类型论通常的平等，而第二个允许我们的原因严格平等。在这个系统中，我们可以形式化部分元理论性质的结果。我们详细地开发和探索了如何在证明助手中实现两级类型论，并在证明助手精益中提供了原型实现。我们展示了两个层次的类型论的应用，通过开发一些结果的理论，使用我们的精益实现的逆图。

2018-11-28cs.PL

智能合约翻译认证

Translation Certification for Smart Contracts

更高的正确性是一个老问题，但随着区块链上智能合约的出现，这个问题以一种新的方式出现。智能合约是一种独立的软件，可以在对抗性的环境中控制资产，这些资产通常具有很高的财务价值，一旦投入区块链，就不能再改变。智能合约通常使用高级合约语言开发，并在提交到区块链之前编译为低级虚拟机器码。对于智能合约用户来说，要信任区块链上给定的一段低级代码，他们必须说服自己：（a）他们拥有匹配的源代码;（b）编译器忠实地翻译了源代码的语义。编译器正确性的经典方法解决了第二点。我们认为翻译认证也解决了第一个问题。我们描述了一种新的翻译认证框架的证明架构，该框架在Coq中实现，用于功能智能合约语言。我们证明，我们可以建模的编译管道作为一个序列的翻译关系，方便模块化的证明方法，并在面对不断发展的编译器实现是强大的。

2022-02-22cs.PL

迈克尔逊智能合约的抽象解释

Abstract interpretation of Michelson smart-contracts

智能合约的静态分析在区块链平台上变得越来越普遍。分析器依赖于符号执行或模型检验等技术，但很少有分析器能同时提供强可靠性和保证分析的终止性。由于智能合约经常操纵经济资产，因此证明数字属性超出了运行时错误的情况也是可取的。智能合约执行模型与主流程序设计语言有很大不同，并且因区块链而异，使得最先进的分析难以适应。例如，智能合约调用可能会修改影响后续调用的持久性存储。这使得工具很难推断出正式确保不存在可利用漏洞所需的不变量。Tezos区块链中使用的Michelson智能合约语言是强类型的，基于堆栈的，并且具有严格的执行模型，几乎没有隐式运行时错误的机会。我们提出了一个正在进行的静态分析迈克尔逊的基础上抽象解释和MOPSA，一个模块化的静态分析器内实现。我们的工具支持迈克尔逊语义特征，包括对外部契约的内部调用。它可以证明不存在运行时错误，并在无限数量的调用上推断持久存储上的不变量。它也被扩展到证明高级别的数值和安全属性。CCS概念：$\bullet$安全和隐私$\rightarrow$逻辑和验证; $\bullet$软件及其工程$\rightarrow$自动化静态分析。

2022-10-11cs.CRcs.PLcs.SE