智能合约的形式化验证工作主要集中在编程语言层面的漏洞研究，而交易顺序依赖作为区块链层面的漏洞更不易被检测。基于着色Petri网对智能合约中潜在的交易顺序依赖漏洞进行形式化验证。以Decode悬赏合约为对象，分析合约中潜在的漏洞，自顶向下地对合约本身及其执行环境建立着色Petri网模型，并引入攻击者模型来考虑合约遭受攻击的情况。通过运行模型以验证合约存在交易顺序依赖漏洞，最后基于Remix平台在以太坊网络中证实结论的正确性。
科研之友
微信
新浪微博
Facebook
分享链接
