基于CPN的智能合约交易顺序依赖漏洞的验证

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

Verification of Transaction Ordering Dependence Vulnerability of Smart Contract Based on CPN

The formal verification of smart contracts researches mainly focus on programming language-level vulnerabilities, and the transaction ordering dependence is more difficult to be detected as a blockchain-level vulnerability.The latent transaction ordering dependence vulnerability in smart contracts is formally verified based on colored Petri nets.The latent vulnerability in the Decode reward contractis analyzed, anda colored Petri net model of the contract itself and its execution environment is established from top to bottom.The attacker model is introduced to consider the situation that the contract is attacked. By running the model to verify the existence of transaction ordering dependence vulnerability in the contract,thecorrectness of the conclusion is finally verified in the Ethereum network based on Remix platform.