What are the Actual Flaws in Important Smart Contracts (and How Can We Find Them)?
智能合约安全性的一个重要问题是了解合约中发现或潜在弱点的可能性和关键性。在本文中，我们总结了对23个专业利益相关者进行的以太坊智能合约审计，避免了低质量合约中常见的报告问题。这些审计是在区块链安全领域的领先公司进行的，使用了开源和专有工具，以及由专业安全工程师进行的人工代码分析。我们对246个单独的缺陷进行了分类，从而可以比较不同漏洞类型的严重性和频率，比较智能合约和非智能合约缺陷，并评估自动漏洞检测方法的有效性。
2020-01-10 cs.CR cs.PL cs.SE
Smart Contract Repair
智能合约是自动化或自我执行的合约，可用于交换资产，而无需信任第三方。许多商业交易使用智能合约，因为它们在独立于外部方的安全点对点交易方面具有潜在的好处。经验表明，许多常用的智能合约容易受到严重的恶意攻击，这可能使攻击者能够窃取参与方的宝贵资产。因此，需要应用分析和自动修复技术，在部署之前检测和修复智能合约中的错误。在这项工作中，我们提出了第一个通用的自动智能合约修复方法，也是气体感知的。我们的修复方法是基于搜索的，并在有缺陷的合同的突变中搜索。我们的方法还考虑了气体使用的候选补丁，利用我们的新概念的气体优势关系。我们已经将我们的智能合约修复工具SCRepair开源，供更广泛的社区调查。
2020-05-20 cs.CR cs.PL cs.SE
Gradual Verification for Smart Contracts
针对外部合约实现缺失导致重入攻击难以验证的问题，本文提出结合静态与动态技术的渐进式验证方法，并通过 pyTEAL 上的 Algorand 原型验证其安全、灵活与资源优化效果。
2024-07-03 cs.CR cs.LO cs.PL
Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts
本文介绍了Tezla，这是Michelson智能合约的中间表示，可以简化静态智能合约分析器的设计。这种中间表示使用存储并保留原始智能合约的语义，ow和资源使用。这使得像气体消耗这样的属性能够被静态地验证。我们为Tezla提供了Michelson智能合约的自动化反编译器。为了支持我们关于Tezla充分性的主张，我们开发了一个静态分析器，它利用Michelson智能合约的Tezla表示来证明简单但不平凡的属性。
2020-05-24 cs.PL
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-18 cs.PL
Protocol-based Smart Contract Generation
智能合约的受欢迎程度正在上升，但可靠性和安全性方面的漏洞仍然存在。在智能合约可靠性的许多方面中，我们专注于根源于与合约端点的无序交互的故障。我们提出SmartScribble，一种协议语言来描述有效的用户和端点之间的交互模式。SmartScribble不仅确保了正确的交互行为，还简化了智能合约编码。从协议描述中，我们的编译器生成一个智能合约，然后程序员可以使用相关的业务逻辑完成该合约。生成的合约依赖于有限状态机来控制端点调用。作为概念验证，我们的目标是Plutus，这是Cardano区块链的合约程序设计语言。初步评估表明，开发人员必须编写的代码大小减少了75%，并且通过强制执行指定的交互模式来提高可靠性。
2021-08-05 cs.PL
Making Tezos smart contracts more reliable with Coq
Tezos是一个智能合约区块链。Tezos的智能合约是用一种名为Michelson的底层堆栈语言编写的。本文概述了使用Coq证明助手对Michelson智能合约进行更强保证的努力：Mi-Cho-Coq框架，定义Michelson形式语义的Coq库，以及解释器，简单优化器和最弱前提演算来推理Michelson智能合约; Albert是一种抽象Michelson堆栈的中间语言，使用以Mi-Cho-Coq为目标的Coq编写的编译器。
2021-06-24 cs.PL
Albert, an intermediate smart-contract language for the Tezos blockchain
Tezos是一个智能合约区块链。Tezos的智能合约是用一种名为Michelson的底层堆栈语言编写的。在本文中，我们介绍了Albert，这是Tezos智能合约的中间语言，它将Michelson堆栈抽象为线性类型的记录。我们还描述了它的编译器，以迈克尔逊，写在Coq，目标Mi-Cho-Coq，迈克尔逊在Coq实现的正式规范。
2020-01-07 cs.PL
Mandala: A Smart Contract Programming Language
区块链上的智能合约的行为完全符合其代码的规定。此代码中的漏洞可能导致意外行为，这很难修复，因为区块链不允许在部署后更改智能合约代码。这种脆弱性导致了几起事件。在这样的事件之后，以太坊和以太坊经典之间的硬分叉是结果。本论文提出开发一种新的智能合约程序设计语言，主要关注安全性，可扩展性，并通过设计尽可能多地防止已知类别的漏洞。程序设计语言的代码在部署期间进行验证，然后与在同一区块链上运行的其他智能合约隔离，以在运行时强制执行编译时保证。设计的程序设计语言确实评估了在非智能合约环境中很少使用的新概念和范式，以了解它们在智能合约环境中的潜在利益。
2019-11-26 cs.PL
Rich Specifications for Ethereum Smart Contract Verification
智能合约是在以太坊等区块链内部执行的程序，用于操纵数字资产。由于智能合约中的错误可能会导致重大的财务损失，因此人们对正式证明其正确性非常感兴趣。然而，智能合约的规范和验证面临着在其他应用领域中不会出现的挑战。智能合约经常与未经验证的、可能具有对抗性的外部代码交互，这大大削弱了正式分析可以（合理地）做出的假设。此外，智能合约的核心功能是操纵和转移资源;简明地描述此功能需要专门的规范支持。目前的推理技术并没有完全解决这些挑战，限制在其范围或表现力（特别是，在存在可重入调用），并提供有限的手段来表达合同执行的资源转移。在本文中，我们提出了一种针对智能合约领域的新型规范方法。我们的规范结构和相关的推理技术是第一个实现：（1）在存在未经验证的代码和任意重入的情况下进行合理和精确的推理，（2）关于协作智能合约的模块化推理，以及（3）基于资源和资源转移的特定于域的规范，允许以直观和简洁的方式表达合约的行为，并在默认情况下排除典型错误。我们已经在2 vyper中实现了我们的方法，2 vyper是一个基于SMT的自动验证工具，用于用Vyper语言编写的以太坊智能合约，并证明了它在简洁地捕获和验证真实世界合约的强正确性保证方面的有效性。
2021-09-09 cs.PL
Formal Specification and Verification of Smart Contracts for Azure Blockchain
确保智能合约的正确性对于确保基于区块链的系统的信任至关重要。本文研究了\emph{Azure Blockchain Workbench}中智能合约的安全性，这是微软提供的企业区块链即服务。作为本研究的一部分，我们针对具有访问控制策略的状态机模型对智能合约的\emph{semantic conformance}进行了形式化，并为Solidity开发了一个高度自动化的形式化验证器，该验证器可以生成证明和反例。我们已应用验证程序{ \sc VeriSol}来分析Azure Blockchain随附的{ \it all}合约，其中包括应用程序示例以及授权证明（PoA）的治理合约。我们在这些已发布的智能合约中发现了以前未知的错误。修复这些漏洞后，{ \sc VeriSol}能够成功对所有这些合同执行全面验证。
2019-04-29 cs.PL
Quantitative Analysis of Smart Contracts
智能合约是由相互不信任的代理网络执行的计算机程序，不需要外部可信机构。智能合约处理和转移价值可观的资产（以比特币等加密货币的形式）。因此，至关重要的是，它们的实现是无bug的。我们将与此类智能合约交互的效用（或预期收益）确定为此类合约的基本和规范量化属性。我们提出了一个智能合约定量分析的框架。这样一个正式的框架提出了新的和新颖的研究挑战，在程序设计语言，因为它需要建模的博弈论方面分析激励偏离诚实的行为和建模公用事业没有指定为标准的时间属性，如安全和终止。虽然博弈论的激励机制已经在安全社区进行了分析，但其分析仅限于非常特殊的无状态博弈情况。然而，要分析智能合约，需要进行状态分析，因为它必须考虑协议的不同程序状态。我们的主要贡献如下：我们提出了（i）~一种简化的智能合约程序设计语言;（ii）~一种将程序自动转换为基于状态的游戏的方法;（iii）~一种解决此类游戏的抽象-细化方法;以及（iv）~在现实世界启发的智能合约上的实验结果。
2018-06-17 cs.PL
Ergo -- a programming language for Smart Legal Contracts
我们提出了一个智能法律合同平台，以支持广泛的智能法律合同用例。我们认为这是朝着改进现有方法的一步，以表示法律协议的复杂性和执行这些协议的各个方面。
2021-12-23 cs.CY cs.PL
A true concurrent model of smart contracts executions
区块链技术的发展已经实现了所谓的智能合约的无信任执行，即规范资产交换的程序（例如，cryptocurrency）之间的用户。在去中心化的区块链中，智能合约的状态由相互不信任的节点组成的点对点网络协同维护，这些节点从用户那里收集一组交易（代表合约上所需的操作），并以某种顺序执行它们。一旦这个交易序列被附加到区块链上，其他节点就会对其进行验证，以相同的顺序重新执行交易。事务的串行执行没有利用现代处理器的多核架构，因此有助于限制吞吐量。在本文中，我们提出了一个智能合约执行的真正并发模型。在此基础上，我们展示了如何利用智能合约的静态分析来并行化交易的执行。
2020-04-27 cs.PL
OV: Validity-based Optimistic Smart Contracts
智能合约（SC）平台将交易块形成一个链，并通过用户定义的智能合约执行它们。在比特币和以太坊等传统平台中，区块内的交易由矿工执行\emph{sequentially}，然后由验证者验证\emph{sequentially}，以达成关于区块最终状态的共识。为了利用多核技术的进步，本文探讨了下一代智能合约平台，该平台支持此类合约的并发执行。在并发智能合约中，对对象状态的有效性进行推理是一个挑战。我们研究了一个编程模型，以支持\emph{optimistic}执行SCT。我们引入了一种新的程序设计语言，即所谓的OV和Solidity API，以简化乐观智能合约的编程。OV语言与静态检查一起将有助于推理乐观执行智能合约的一个关键属性-无信任系统中对象状态的有效性。
2020-04-09 cs.DC cs.PL
Blockly2Hooks: Smart Contracts for Everyone with the XRP Ledger and Google Blockly
针对智能合约因学习曲线陡峭、工具不足导致非专家难以使用的问题，本文设计并测试了Blockly2Hooks，借助XRP账本和Google Blockly可视化编程，降低非专家使用智能合约的门槛，让其轻松学习和创建智能合约。
2025-11-11 cs.CR cs.HC cs.PL
WhylSon: Proving your Michelson Smart Contracts in Why3
本文介绍了WhylSon，一个用Michelson编写的智能合约演绎验证工具，这是Tezos区块链的低级语言。WhylSon接受正式指定的Michelson契约，并自动将其转换为用WhyML（Why3框架的编程和规约语言）编写的等效程序。智能合约指令被映射到其公理语义的相应WhyML浅嵌入中，我们也在这项工作的上下文中开发了这一点。这种方法的一个主要优点是，它允许与Why3框架进行开箱即用的集成，即其VCGen和对几个自动定理证明器的后端支持。我们还讨论了使用WhylSon来自动证明各种注释智能合约的正确性。
2020-05-29 cs.PL
Specification Mining for Smart Contracts with Automatic Abstraction Tuning
智能合约是根据特定协议管理数字资产的程序，例如表示拍卖规则。理解智能合约的可能行为是困难的，这使得开发、审计和攻击的事后分析变得复杂。本文介绍了智能合约的第一个规范挖掘技术。我们的技术从区块链上记录的合约执行中提取智能合约的可能行为，并将其表示为有限自动机。一种新的依赖分析允许我们将独立的交互与合同分开。例如，我们的技术根据可配置的指标自动调整自动机构造的抽象，以最大限度地提高可读性或精度。我们为以太坊区块链实现了我们的技术，并在几个现实世界的合同上评估了它的可用性。
2018-07-20 cs.PL cs.SE
Executable Operational Semantics of Solidity
比特币最近引起了大家的关注和兴趣。以太坊（ETH）是第二代加密货币，它通过提供一种名为Solidity的图灵完备程序设计语言来开发智能合约，从而扩展了比特币的设计。智能合约允许在没有第三方的情况下在EVM（以太坊虚拟机）上可信地执行合约。开发正确的智能合约是具有挑战性的，因为它的分散计算性质。错误的智能合约可能会导致巨大的财务损失。此外，智能合约一旦部署，即使不是不可能，也很难打补丁。因此，最近对分析/验证智能合约的兴趣激增。虽然现有的工作主要集中在EVM操作码上，但我们认为理解和定义Solidity的语义同样重要，因为程序员在源代码级别对智能合约进行编程和推理。在这项工作中，我们开发了Solidity的结构操作语义，这使我们能够识别出许多有问题的智能合约中的多个设计问题。此外，我们的语义在K框架中是可执行的，这允许我们自动验证/伪造合同。
2018-04-04 cs.PL
Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs
本文为面向并行EVM的智能合约语言Crystality提出首个形式化结构操作语义，并在Coq中机械化验证，通过代币转账案例展示其确保合约正确性的能力。
2025-04-24 cs.PL
Translation Certification for Smart Contracts
更高的正确性是一个老问题，但随着区块链上智能合约的出现，这个问题以一种新的方式出现。智能合约是一种独立的软件，可以在对抗性的环境中控制资产，这些资产通常具有很高的财务价值，一旦投入区块链，就不能再改变。智能合约通常使用高级合约语言开发，并在提交到区块链之前编译为低级虚拟机器码。对于智能合约用户来说，要信任区块链上给定的一段低级代码，他们必须说服自己：（a）他们拥有匹配的源代码;（b）编译器忠实地翻译了源代码的语义。编译器正确性的经典方法解决了第二点。我们认为翻译认证也解决了第一个问题。我们描述了一种新的翻译认证框架的证明架构，该框架在Coq中实现，用于功能智能合约语言。我们证明，我们可以建模的编译管道作为一个序列的翻译关系，方便模块化的证明方法，并在面对不断发展的编译器实现是强大的。
2022-02-22 cs.PL
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-01 cs.LO cs.PL
Inheritance software metrics on smart contracts
区块链系统最近获得了巨大的吸引力，部分原因是分散的不可变的经济活动调解的潜力。以太坊是一个突出的例子，它提供了执行被称为智能合约的有状态计算脚本。这些智能合约类似于传统程序，但不变性是核心区别因素。考虑到它们的不变性和潜在的高货币价值，开发高质量的智能合约势在必行。软件度量传统上是确定编程质量的重要工具。考虑到智能合约（用Solidity for Ethereum编写）和面向对象（OO）编程之间的相似性，OO指标似乎是适用的。在本文中，我们实证评估了应用于智能合约的基于继承的指标。我们之所以关注这一点，是因为传统上，继承与更复杂的代码库相关联，而我们认为基于Solidity的智能合约并非如此。在这项工作中，我们评估了一个假设，即由于智能合约和OO程序的背景不同，使用相同的基于继承的指标进行评估可能是不合适的。
2020-07-16 cs.PL cs.SE
Smart Contract Interactions in Coq
我们在Coq中提出了一个智能合约执行的模型/可执行规范。我们的形式化允许合约间通信，并通过允许深度优先执行区块链（如以太坊）和广度优先执行区块链（如Tezos）的建模来推广现有工作。我们用Coq的函数语言Gallina表示智能合约程序，比其他方法更容易推理具体合约的功能正确性。特别是，我们以这种风格制定了一份国会合同。这个合约--臭名昭著的DAO的简化版本--很有趣，因为它与其他合约的通信模式非常动态。我们给出了国会行为的高级部分规范，与可重入性相关，并证明国会满足所有可能的智能合约执行命令。
2019-11-12 cs.LO cs.PL
Low-level Comments auto-generation for Solidity Smart Contracts
背景：区块链平台上的去中心化应用通过智能合约实现。然而，缺乏编程知识的参与者往往难以阅读智能合约源代码，这导致潜在的安全风险和参与障碍。目的：我们的目标是将智能合约源代码翻译成自然语言描述，以帮助人们更好地理解、操作和学习智能合约。方法：本文提出了一种基于抽象语法树和形式语法的Solidity智能合约自动翻译工具SolcTrans。我们调查了3,000个智能合约，并确定了相应区块链术语的词性。其中，我们进一步过滤出没有详细注释的合同片段，留下811个片段来评估SolcTrans的翻译质量。结果如下：实验结果表明，即使是一个小的语料库，SolcTrans可以实现类似的性能，国家的最先进的代码注释生成模型的其他程序设计语言。此外，SolcTrans在处理不同长度和gas消耗的代码片段时具有一致的性能。结论：SolcTrans能够正确解释Solidity代码并自动将其转换为可理解的英文文本。我们将发布我们的工具和数据集，以支持相关领域的复制和进一步研究。
2022-01-08 cs.PL cs.SE
Developing a Compiler for EROP -- A Language for the Specification of Smart Contracts, An Experience Report
智能合约是标准纸质合约的翻译，可以由合约管理系统强制执行。在高度抽象的层面上，合同只是一份描述签字各方在不同情况下如何行事的文件;然而，将典型的纸质合同翻译成电子合同既费时又困难。要求一种语言能够用简单的短语和定义抓住合同的核心，这是多年来研究的重点。EROP（事件、权利、义务、禁止）是一种契约规约语言，它将契约分解为事件、权利、义务和禁止的集合。
2023-03-02 cs.DC cs.PL cs.SE
