基于纳什均衡的智能合约缺陷检测  

Detecting Smart Contract Loopholes Based on Nash Equilibrium

作　　者：陈晋川[1,2] 夏华辉 王璞巍 马纳波[1] 王琪 李浩然 杜小勇 CHEN Jin-Chuan;XIA Hua-Hui;WANG Pu-Wei;MA Na-Bo;WANG Qi;LI Hao-Ran;DU Xiao-Yong(School of Information,Renmin University of China,Beijing 100872;Key Lab of Data Engineering and Knowledge Engineering,Ministry of Education,Renmin University of China,Beijing 100872)

机构地区：[1]中国人民大学信息学院,北京100872 [2]数据工程与知识工程教育部重点实验室(中国人民大学),北京100872

出　　处：《计算机学报》2021年第1期147-161,共15页Chinese Journal of Computers

基　　金：国家自然科学基金(U1911203);贵州财经大学与商务部国际贸易经济合作研究院联合基金(2017SWBZD08)资助

摘　　要：本文研究区块链智能合约的缺陷检测问题,即检测合约中是否存在部分合约方无论选择什么动作,均无法避免损失的状态.将智能合约问题转换成合约状态迁移图上的博弈策略选择问题,提出了基于纳什均衡理论的合约缺陷自动检测方法,以及为了提高检测效率,提出了针对合约状态变迁图和博弈策略形式的一系列化简方法.最后,实现了一个智能合约建模、分析和部署工具.针对一组真实合同的实验表明,该工具能自动发现部分合同缺陷,化简方法提升缺陷检测效率的效果明显.In recent years,blockchain has attracted many interests form both academic and research communities,and been applied in cryptocurrency,financial techniques,logistics,copyright protection etc.Blockchain is basically a distributed storage system,consisting of a set of servers or nodes.In blockchain systems,smart contracts are widely adopted as the code laws to be obeyed by all participants.Before storing the data item into blockchain,each node needs to verify the validity of this operation by executing its corresponding smart contracts,i.e.computer programs.Noted that,in this paper we focus on classic smart contracts,i.e.computer codes for verifying,executing,or disseminating contracts in an informational manner.Smart contract has become one of the core techniques of blockchain,and it is very important to study how to detect loopholes existing in smart contracts.Here,the term loophole does not mean bugs in the contract codes,but some bad outputs of executing the contracts.These outputs are unfavorable to some contract partners.If all partners are rational and have complete information about the contracts,these outputs cannot be avoided no matter what choices the partners choose during executing the contracts.Therefore these contracts will not become repeated games since some partners cannot benefit from joining the contracts.These kind of contracts will be one-shot games and are harmful to business zoology.We propose a method to detect the loopholes of formalized smart contracts based on the Nash equilibrium theory.Instead of hiring lawyers to check the contract terms one by one,we can now automatically find out the loopholes of contracts.We propose a data structure,called state-transition-graph,to describe the outputs for each partner of choosing different strategies of executing a contract.Based on the state-transition-graph,we further define the problem of smart contract game,and define the loopholes as a special kind of Nash equilibriums,where some partners would obtain zero or negative utilities and they canno

关 键 词：智能合约 纳什均衡 缺陷检测 区块链 博弈论 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]