一句话：提出声明式语言 DeCon，用关系约束建模智能合约并规格化合约级属性，可编译为带运行时监控的 Solidity。
论文针对智能合约实现与合约级属性难以清晰表达和监控的问题，观察到合约操作与属性可自然表示为关系约束，提出声明式语言 DeCon。DeCon 将每个合约建模为存储交易记录的关系表，程序由声明式规则和违规查询规则构成，分别描述合约实现与合约级属性。该关系表示便于规格化属性、运行时监控违规并借助数据溯源调试合约。作者实现工具将 DeCon 编译为可执行 Solidity，并注入运行时监控。案例研究显示可表达 ERC20、ERC721 等真实合约；评估表明相比开源参考实现，执行 gas 中位数开销 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.
DOI 原文 ·
@inproceedings{paperbot7131,
title = {Declarative smart contracts},
author = {Haoxian Chen and Gerald Whitters and Mohammad Javad Amiri and Yuepeng Wang and Boon Thau Loo},
booktitle = {FSE},
year = {2022},
doi = {10.1145/3540250.3549121}
}