【摘要】 区块链智能合约是运行在区块链网络中的代码,它能够根据外部环境条件自动执行相应的规则,完成对应的交易和数字资产的转移.Auction合约是一个公开拍卖的智能合约,广泛应用到竞拍、游戏和博彩等行业,吸引了众多用户参与.近年来,该合约暴露出了拒绝服务攻击漏洞,导致很多参与者无法竞拍成功.为此,本文基于CPN模型对Auction合约进行形式化验证,检测漏洞并确定漏洞位置.首先使用CPN中的建模工具分别对Auction合约整体、无攻击操作和有攻击操作进行建模,然后使用CPN中的仿真工具对合约的执行过程进行仿真.结果表明,通过该方法,不仅可以发现和定位Auction合约的逻辑漏洞,而且也可以发现Auction合约语言的局限性.更多还原

【Abstract】 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.更多还原