【摘要】近年来，智能合约的形式化验证工作主要集中在编程语言层面的漏洞研究，而交易顺序依赖作为区块链层面的漏洞更不易被检测。基于着色Petri网对智能合约中潜在的交易顺序依赖漏洞进行形式化验证。以Decode悬赏合约为对象，分析合约中潜在的漏洞，自顶向下地对合约本身及其执行环境建立着色Petri网模型，并引入攻击者模型来考虑合约遭受攻击的情况。通过运行模型以验证合约存在交易顺序依赖漏洞，最后基于Remix平台在以太坊网络中证实结论的正确性。
【关键词】区块链;;智能合约;;着色Petri网;;形式化验证;;交易顺序依赖漏洞
【DOI】10.16182/j.issn1004731x.joss.21-0208
评论