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