Declarative smart contracts

Declarative smart contracts
复制标题

DOI:
10.1145/3540250.3549121
复制
发表时间:
2022-07
期刊:
Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
影响因子:
--
通讯作者:
Haoxian Chen;Gerald Whitters;Mohammad Javad Amiri;Yuepeng Wang;B. T. Loo
Haoxian Chen;Gerald Whitters;Mohammad Javad Amiri;Yuepeng Wang;B. T. Loo
中科院分区:
其他
文献类型:
--
作者:
Haoxian Chen;Gerald Whitters;Mohammad Javad Amiri;Yuepeng Wang;B. T. Loo

文献摘要

相似文献

本文介绍了DeCon,这是一种用于实现智能合约和指定合约级别属性的声明性编程语言。在观察到智能合约操作和合约级属性可以自然地表示为关系约束的驱动下,DeCon将每个智能合约建模为一组存储交易记录的关系表。智能合约的这种关系表示可以方便地指定合约属性,便于对潜在的属性违规进行运行时监控,并通过数据来源为合约调试带来清晰度。具体来说,DeCon程序由一组关系表示上的声明性规则和违规查询规则组成,分别描述智能合约实现和合约级属性。我们已经开发了一个工具,可以编译DeCon程序到可执行的Solidity程序,与仪器运行时的属性监控。我们的案例研究表明,DeCon可以实现现实的智能合约,如ERC20和ERC721数字代币。我们的评估结果显示,与开源参考实现相比,DeCon的边际开销为14%,执行时的平均气体开销为14%,运行时验证的平均气体开销为16%。
This paper presents DeCon, a declarative programming language for implementing smart contracts and specifying contract-level properties. Driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints, DeCon models each smart contract as a set of relational tables that store transaction records. This relational representation of smart contracts enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to contract debugging via data provenance. Specifically, a DeCon program consists of a set of declarative rules and violation query rules over the relational representation, describing the smart contract implementation and contract-level properties, respectively. We have developed a tool that can compile DeCon programs into executable Solidity programs, with instrumentation for run-time property monitoring. Our case studies demonstrate that DeCon can implement realistic smart contracts such as ERC20 and ERC721 digital tokens. Our evaluation results reveal the marginal overhead of DeCon compared to the open-source reference implementation, incurring 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.