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

本文研究区块链智能合约的缺陷检测问题,即检测合约中是否存在部分合约方无论选择什么动作,均无法避免损失的状态.将智能合约问题转换成合约状态迁移图上的博弈策略选择问题,提出了基于纳什均衡理论的合约缺陷自动检测方法,以及为了提高检测效率,提出了针对合约状态变迁图和博弈策略形式的一系列化简方法.最后,实现了一个智能合约建模、分析和部署工具.针对一组真实合同的实验表明,该工具能自动发现部分合同缺陷,化简方法提升缺陷检测效率的效果明显.

Detecting Smart Contract Loopholes Based on Nash Equilibrium

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 cannot improve their utilities even if they change their own strategies.In this way,we are able to automatically find out the loopholes by computing the Nash equilibriums of smart contract game.However,the strategy forms obtained from the state-transition-graph may be too large due to state explosion.There could be millions of and even larger number of states in a strategy form,which causes very expensive time costs of computing Nash equilibriums.We then propose two rules,i.e.Strategy equivalence and Nash equivalence rules,for simplifying the state-transition-graph and strategy forms,which can greatly cut down the time costs.In order to further cut down the time costs of computing Nash equilibrium,we also propose a method to find out the redundant strategy combinations and prove that we can obtain the same Nash equilibriums when these strategy combinations are removed.Based on these methods,we design and implement a tool for modelling,analyzing and deploying smart contracts.We analyze a set of real contracts crawled from two professional lawyer web sites.These contracts cover the main contract categories listed in Contract Law of People’s Republic of China.We discuss some contract loopholes detected by this tool,and evaluate the ability of our proposed methods to improve the performance.As illustrated by the experimental results,our methods can greatly reduce the strategy forms and the time costs.