一句话：提出半自动验证智能合约公平性的框架与工具 FairCon，可证伪或证明真实性、效率、最优性、无合谋等性质。
智能合约是在区块链平台上自动定义并执行交易的程序，其中许多可视为博弈：多方参与者投入输入，合约结束后按预定义规则自动产生结果并分配资产。参与者若不能清楚理解博弈规则，就可能受到虚假宣传误导并蒙受经济损失。本文提出一个对智能合约公平性进行（半）自动化验证的框架，验证结果既可用具体反例驳斥虚假声明，也可证明合约实现满足期望的公平性质。作者实现了 FairCon 工具，可对以太坊智能合约检查真实性（truthfulness）、效率（efficiency）、最优性（optimality）与无合谋性（collusion-freeness）等公平性质。在真实世界基准合约上的实验表明，FairCon 能有效检测性质违反，并能为常见类型的合约证明公平性。
Smart contracts are computer programs allowing users to define and execute transactions automatically on top of the blockchain platform. Many of such smart contracts can be viewed as games. A game-like contract accepts inputs from multiple participants, and upon ending, automatically derives an outcome while distributing assets according to some predefined rules. Without clear understanding of the game rules, participants may suffer from fraudulent advertisements and financial losses. In this paper, we present a framework to perform (semi-)automated verification of smart contract fairness, whose results can be used to refute false claims with concrete examples or certify contract implementations with respect to desired fairness properties. We implement FairCon, which is able to check fairness properties including truthfulness, efficiency, optimality, and collusion-freeness for Ethereum smart contracts. We evaluate FairCon on a set of real-world benchmarks and the experiment result indicates that FairCon is effective in detecting property violations and able to prove fairness for common types of contracts.
DOI 原文 ·
@inproceedings{paperbot5806,
title = {Towards automated verification of smart contract fairness},
author = {Ye Liu and Yi Li and Shang-Wei Lin and Rong Zhao},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3409740}
}