solidity-vs-move-verification

本研究构建了一个公开的数据集，用于支持对Solidity和Move两种智能合约语言的验证任务进行比较。该数据集包含了在Certora和Aptos Move Prover上执行验证任务的案例，旨在为两种语言的规范语言和验证器提供一个实验性和可扩展性的比较基础。数据集涵盖了不同复杂度的智能合约用例，以及从低级别函数特性到高级别合同业务逻辑的多样属性，为智能合约验证的研究提供了丰富的案例和属性集合。This study develops a public dataset to support comparative research on verification tasks for two smart contract languages, Solidity and Move. This dataset contains verification task cases executed on both Certora and Aptos Move Prover, aiming to provide an experimental and scalable benchmark for comparing the specification languages and verifiers of the two languages. The dataset covers smart contract use cases of varying complexities, as well as diverse properties ranging from low-level function features to high-level contract business logic, offering a rich collection of cases and properties for smart contract verification research.

搜集汇总

数据集介绍

构建方式

本数据集是通过在Certora和Aptos Move Prover中执行验证任务的方式构建的。研究者选取了三个具有代表性的智能合约用例，并在Solidity和Move中分别实现了这些合约。对于每个用例，研究者定义了一系列属性，并将这些属性的自然语言描述转换为Certora Verification Language (CVL)和Move Specification Language (MSL)中的形式化规格。然后，研究者使用Certora Prover和Aptos Move Prover对这些规格进行了验证，并记录了验证结果和过程中的技术假设。

特点

该数据集的特点在于它提供了一个用于比较Solidity和Move两种智能合约语言在形式化验证方面的表现的平台。数据集包含了66个属性，涵盖了从低级功能到高级业务逻辑的各个方面。这些属性在两种语言的实现中进行了验证，并且记录了验证过程中的所有细节，包括验证结果、技术假设和任何遇到的问题。数据集的开放性使得其他研究者可以在此基础上进行进一步的分析和扩展。

使用方法

使用该数据集的方法包括：1) 研究者可以根据自己的需求选择特定的属性或用例进行分析；2) 研究者可以使用数据集中的验证结果来比较Certora Prover和Aptos Move Prover的性能和功能；3) 研究者可以添加新的属性或用例到数据集中，以扩展其范围和深度。为了使用数据集，研究者需要具备对智能合约语言和形式化验证工具的基本了解，并且熟悉CVL和MSL规格语言。

背景与挑战

背景概述

在智能合约安全领域中，形式化验证扮演着至关重要的角色。它能够发现智能合约中的漏洞，保证其安全性，并检查业务逻辑是否正确实现。针对Solidity语言，尽管已经存在一些成熟的验证工具，但该语言的语义特性使得实际验证过程相当困难。相比之下，Move语言在设计之初就考虑了安全和验证的需求，并伴随着一个形式化验证工具——Move Prover。本研究通过比较分析探讨了Solidity和Move两种合约语言的设计如何影响验证过程，以及两种语言的验证工具的现状，并在三个典型的用例上进行了比较。研究基于在Certora和Aptos Move Prover中执行的验证任务的开源数据集进行。

当前挑战

本研究的主要挑战在于分析Solidity和Move两种合约语言的不同设计对验证过程的影响，并比较两种语言的验证工具在三个典型用例上的表现。此外，研究还面临着如何将自然语言描述的属性转换为形式化规范的问题，以及如何在形式化规范中添加必要的低级技术假设。另一个挑战是，尽管Certora Prover能够表达比Move Prover更广泛的属性，但Move Prover在某些方面仍然存在局限性，例如缺乏一个构造来强制执行合约变量的不可变性。此外，两种工具都无法处理某些重要类型的属性，如活性、流动性和启用性等，这些属性在现实世界的智能合约中非常重要。

常用场景

经典使用场景

在智能合约领域，安全性至关重要。Solidity和Move是两种主要的智能合约编程语言，但由于其设计上的差异，它们在形式化验证方面表现出不同的特性。solidity-vs-move-verification数据集通过比较分析这两种语言的验证过程，提供了对智能合约验证的深刻见解。该数据集最经典的使用场景是研究不同语言设计对验证的影响，以及当前验证工具的状态和它们在不同用例上的表现。

实际应用

在现实世界中，solidity-vs-move-verification数据集可以应用于智能合约的审计和安全性评估。通过比较Solidity和Move的验证过程，开发者可以更好地理解两种语言的特点和优缺点，从而选择更适合其需求的编程语言。此外，该数据集还可以用于验证工具的开发和改进，以提高智能合约的安全性。

衍生相关工作

solidity-vs-move-verification数据集衍生了许多相关的研究工作，包括对智能合约验证工具的比较研究、对智能合约安全性分析的研究，以及对不同编程语言设计对安全性影响的研究。这些研究工作进一步推动了智能合约安全性的发展，并为智能合约的广泛应用奠定了基础。