Solidity 0.5: when typed does not mean type safe
最近发布的Solidity 0.5引入了一种新类型，以防止以太坊转移到不应该接收资金的智能合约。不幸的是，编译器无法强制执行此类型想要传达的保证，因此Solidity 0.5的类型可靠性并不比Solidity 0.4好。在本文中，我们讨论了一个典型的例子，表明基于潜在不安全的回调表达式的脆弱Solidity模式仍然未经检查。我们还指出了一个解决方案，该解决方案强烈依赖于形式化方法来支持类型安全的智能合约编程规则，同时与遗留Solidity代码追溯兼容。
2019-07-05 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
A true concurrent model of smart contracts executions
区块链技术的发展已经实现了所谓的智能合约的无信任执行，即规范资产交换的程序（例如，cryptocurrency）之间的用户。在去中心化的区块链中，智能合约的状态由相互不信任的节点组成的点对点网络协同维护，这些节点从用户那里收集一组交易（代表合约上所需的操作），并以某种顺序执行它们。一旦这个交易序列被附加到区块链上，其他节点就会对其进行验证，以相同的顺序重新执行交易。事务的串行执行没有利用现代处理器的多核架构，因此有助于限制吞吐量。在本文中，我们提出了一个智能合约执行的真正并发模型。在此基础上，我们展示了如何利用智能合约的静态分析来并行化交易的执行。
2020-04-27 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
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
An Empirical Study of Protocols in Smart Contracts
智能合约是在区块链上执行的程序。它们已被用于投票，分散金融和供应链管理中的应用。然而，智能合约的漏洞被黑客滥用，导致财务损失。理解智能合约中的状态机协议对于捕捉常见错误、改进文档和优化智能合约非常重要。我们分析了部署在以太坊区块链上的Solidity智能合约，并研究了协议和基于协议的错误的流行程度，以及gas优化的机会。
2021-10-18 cs.CR cs.PL
Ergo -- a programming language for Smart Legal Contracts
我们提出了一个智能法律合同平台，以支持广泛的智能法律合同用例。我们认为这是朝着改进现有方法的一步，以表示法律协议的复杂性和执行这些协议的各个方面。
2021-12-23 cs.CY 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
Specification Mining for Smart Contracts with Automatic Abstraction Tuning
智能合约是根据特定协议管理数字资产的程序，例如表示拍卖规则。理解智能合约的可能行为是困难的，这使得开发、审计和攻击的事后分析变得复杂。本文介绍了智能合约的第一个规范挖掘技术。我们的技术从区块链上记录的合约执行中提取智能合约的可能行为，并将其表示为有限自动机。一种新的依赖分析允许我们将独立的交互与合同分开。例如，我们的技术根据可配置的指标自动调整自动机构造的抽象，以最大限度地提高可读性或精度。我们为以太坊区块链实现了我们的技术，并在几个现实世界的合同上评估了它的可用性。
2018-07-20 cs.PL cs.SE
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
VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts
我们介绍了VeriSmart，一个高度精确的验证器，用于确保以太坊智能合约的算术安全性。编写没有意外行为的安全智能合约至关重要，因为智能合约是不可变的，即使是一个缺陷也可能造成巨大的财务损失。特别是，确保算术运算是安全的，是当今以太坊智能合约最重要和最常见的安全问题之一。作为回应，在过去的几年里，已经提出了几种安全分析器，但最先进的技术仍然不能令人满意;没有现有的工具同时实现高精度和召回，本质上局限于产生烦人的假警报或错过关键错误。相比之下，VeriSmart的目标是一个不妥协的分析器，执行详尽的验证，而不影响精度或可扩展性，从而大大减少了手动检查未发现或不正确报告的问题的负担。为了实现这一目标，我们提出了一种新的特定于域的算法来验证智能合约，该算法能够自动发现和利用精确分析智能合约所必需的交易不变量。对真实世界智能合约的评估表明，VeriSmart可以检测到所有算术错误，而错误警报的数量可以忽略不计，远远超过现有的分析器。
2019-08-30 cs.CR cs.PL
Smart Contract Vulnerability Detection Technique: A Survey
智能合约是区块链最成功的应用之一，正在席卷全球，在区块链生态系统中发挥着至关重要的作用。然而，频繁的智能合约安全事件不仅造成了巨大的经济损失，也破坏了基于区块链的信用体系。因此，智能合约的安全性和可靠性得到了全球研究人员的广泛关注。在本次调查中，我们首先从三个层面总结了智能合约漏洞的常见类型和典型案例，即：Solidity代码层、EVM执行层和Block依赖层。此外，我们回顾了智能合约漏洞检测的研究进展，并将现有的同行分为五类，即，形式化验证、符号执行、模糊检测、中间表示和深度学习。从经验上讲，我们以以太坊上部署的300个真实智能合约作为测试样本，并在准确性，F1分数和平均检测时间方面比较了代表性方法。最后讨论了智能合约漏洞检测领域面临的挑战，并结合深度学习技术展望了未来的研究方向。
2022-09-13 cs.CR 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
Flint for Safer Smart Contracts
以太坊区块链平台支持去中心化应用程序或智能合约的执行。它们通常持有数字货币并将其转移给平台上的其他方;然而，由于无意中引入了漏洞，它们受到了许多攻击。自2015年7月发行以来，价值超过10亿美元的货币被盗。由于智能合约在部署后无法更新，因此程序设计语言必须支持健壮合约的开发。我们提出了Flint，一种新的静态类型的程序设计语言，专门用于编写健壮的智能合约。Flint的特性强制编写安全和可预测的代码。为了鼓励良好的实践，我们引入了保护块。保护块限制谁可以运行代码以及何时（使用typestate）可以执行代码。为了防止与货币意外丢失相关的漏洞，Flint Asset特征提供了安全的原子操作，确保合约状态始终一致。对状态的写入受到限制，简化了对智能合约的推理。
2019-04-13 cs.CR cs.PL
SAILFISH: Vetting Smart Contract State-Inconsistency Bugs in Seconds
本文介绍了SAILFISH，这是一个可扩展的系统，用于自动发现智能合约中的状态不一致错误。为了使分析易于处理，我们引入了一种混合方法，包括（i）一个轻量级的探索阶段，大大减少了要分析的指令的数量，以及（ii）一个精确的细化阶段，该阶段基于符号评估，由我们新颖的值汇总分析指导，它生成额外的约束，以过度近似整个程序执行的副作用，从而确保符号评估的精度。我们开发了一个SAILFISH的原型，并评估了它检测两个状态不一致缺陷的能力，即，以太坊智能合约中的可重入性和交易顺序依赖性（TOD）。此外，我们还提出了其他类型智能合约缺陷的检测规则，SAILFISH可以扩展到检测。我们的实验证明了我们的混合方法的效率，以及价值摘要分析的好处。特别是，我们发现S SAILFISH在性能和精度方面优于五种最先进的智能合约分析器（SECURITY，MYTHRIL，OYENTE，SEREUM和VANDAL）。总的来说，SAILFISH在ETHERSCAN的89，853个智能合约中发现了47个以前未知的易受攻击的智能合约。
2021-12-13 cs.CR cs.PL
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
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-03 cs.CR cs.PL
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
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
Blockly2Hooks: Smart Contracts for Everyone with the XRP Ledger and Google Blockly
University of Luxembourg（卢森堡大学）
针对智能合约因学习曲线陡峭、工具不足导致非专家难以使用的问题，本文设计并测试了Blockly2Hooks，借助XRP账本和Google Blockly可视化编程，降低非专家使用智能合约的门槛，让其轻松学习和创建智能合约。
2025-11-11 cs.CR cs.HC cs.PL
