基于CPN模型Auction智能合约的形式化验证  

Formal Validation of Auction Smart Contract Based on CPN Model

作　　者：董春燕 谭良[1,2] DONG Chun-yan;TAN Liang(College of Computer Science,Sichuan Normal University,Chengdu 610101,China;Institute of Computing Technology,Chinese Academy of Sciences,Beijing 100190,China)

机构地区：[1]四川师范大学计算机学院,成都610101 [2]中国科学院计算技术研究所,北京100190

出　　处：《小型微型计算机系统》2020年第11期2292-2297,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61373162)资助;四川省科技厅重点研发项目(2019YFG0183)资助.

摘　　要：区块链智能合约是运行在区块链网络中的代码,它能够根据外部环境条件自动执行相应的规则,完成对应的交易和数字资产的转移.Auction合约是一个公开拍卖的智能合约,广泛应用到竞拍、游戏和博彩等行业,吸引了众多用户参与.近年来,该合约暴露出了拒绝服务攻击漏洞,导致很多参与者无法竞拍成功.为此,本文基于CPN模型对Auction合约进行形式化验证,检测漏洞并确定漏洞位置.首先使用CPN中的建模工具分别对Auction合约整体、无攻击操作和有攻击操作进行建模,然后使用CPN中的仿真工具对合约的执行过程进行仿真.结果表明,通过该方法,不仅可以发现和定位Auction合约的逻辑漏洞,而且也可以发现Auction合约语言的局限性.Blockchain smart contract is code that runs on a blockchain network,it can automatically execute the corresponding rules according to the external environment conditions to complete the corresponding transactions and the transfer of digital assets.The Auction smart contract is a smart contract for public auctions,which is widely used in auctions,games and gambling industries,attracting many users to participate.In recent years,the contract has exposed a denial-of-service attack vulnerability,resulting in many participants being unable to bid successfully.Therefore,based on the CPN model,this paper carries out formal verification of the auction contract,detects the vulnerability and determines the vulnerability location.Firstly,use the modeling tools in CPN to model the entire auction contract,no-attack operations and attack operations,and then use the simulation tools in CPN to simulate the execution process of the contract.The results show that the method can not only find and locate the logic vulnerabilities of Auction contract,but also find the limitation of auction contract language.

关 键 词：Auction智能合约 漏洞 形式化验证 CPN 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]